Dans une infrastructure logicielle, les systèmes critiques ont souvent besoin de garder des clés cryptographiques sur des HSM ou des serveurs consacrés à la gestion de clés. Ils ont pour but de séparer les opérations cryptographiques, très critiques, du reste du réseau, qui est plus vulnérable. L'accès aux clés est fourni au travers des APIs de sécurité, comme par exemple le standard PKCS#11 de RSA, CCA d'IBM, ou encore l'API du TPM, qui ne permettent qu'un accès indirect aux clés. Cette thèse est composée de deux parties. La première introduit des méthodes formelles qui ont pour but l'identification des configurations dans lesquelles les APIs de sécurité peuvent améliorer le niveau de sûreté des protocoles existants, par exemple en cas de compromission d'un participant. Un paradigme prometteur considère les APIs de sécurité comme des participants d'un protocole afin d'étendre l'emploi des méthodes traditionnelles d'analyse de protocole à ces interfaces. À l'opposé des protocoles réseau, les APIs de sécurité utilisent souvent une base de données interne. Ces outils traditionnels d'analyse ne sont adaptés que pour le cas où le nombre des clés est borné a priori. Nous exposons également des arguments pour l'utilisation de la réécriture de multi-ensembles (MSR), lors de la vérification. De plus, nous proposons un langage dérivant du pi-calcul appliqué possédant des opérateurs qui permettent la manipulation d'un état explicite. Ce langage se traduit en règles MSR en préservant des propriétés de sécurité qui s'expriment dans une logique de premier ordre. La traduction a été implémentée sous forme d'un prototype produisant des règles spécifiquement adapté au prouveur tamarin. Plusieurs études de cas, dont un fragment de PKCS#11, le jeton d'authentification Yubikey, et un protocole de signature de contrat optimiste ont été effectuées. Le deuxième partie de la présente thèse a pour but l'identification des propriétés de sécurité qui a) peuvent être établies indépendamment du protocole b) permettent de trouver des failles au niveau de la cryptographie b) facilitent l'analyse des protocoles utilisant cette API de sécurité. Nous adoptons ici l'approche plus générale de Kremer et al. dans un cadre qui permet la composition universelle, à travers une fonctionnalité de gestion de clés. La nouveauté de ce genre de définition est qu'elle dépend des opérations mises à disposition par l'API. Ceci est seulement possible grâce à la composition universelle. Une API de sécurité n'est sûre que si elle réalise correctement la gestion des clés (selon la fonctionnalité présentée dans ce travail) et les opérations utilisant les clés (selon les fonctionalités qui les définissent). Pour finir, nous présentons aussi une implémentation de gestion de clés définie par rapport à des opérations arbitraires utilisant des clés non concernées par la gestion des clés. Cette réalisation représente ainsi un modèle générique pour le design des APIs de sécurité. / Security critical applications often store keys on dedicated HSM or key-management servers to separate highly sensitive cryptographic operations from more vulnerable parts of the network. Access to such devices is given to protocol parties by the means of Security APIs, e.g., the RSA PKCS#11 standard, IBM's CCA and the TPM API, all of which protect keys by providing an API that allows to address keys only indirectly. This thesis has two parts. The first part deals with formal methods that allow for the identification of secure configurations in which Security APIs improve the security of existing protocols, e.g., in scenarios where parties can be corrupted. A promising paradigm is to regard the Security API as a participant in a protocol and then use traditional protocol analysis techniques. But, in contrast to network protocols, Security APIs often rely on the state of an internal database. When it comes to an analysis of an unbounded number of keys, this is the reason why current tools for protocol analysis do not work well. We make a case for the use of MSR as the back-end for verification and propose a new process calculus, which is a variant of the applied pi calculus with constructs for manipulation of a global state. We show that this language can be translated to MSR rules while preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a back-end. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and a contract signing protocol. The second part of this thesis aims at identifying security properties that a) can be established independent of the protocol, b) allow to catch flaws on the cryptographic level, and c) facilitate the analysis of protocols using the Security API. We adapt the more general approach to API security of Kremer et.al. to a framework that allows for composition in form of a universally composable key-management functionality. The novelty, compared to other definitions, is that this functionality is parametric in the operations the Security API allows, which is only possible due to universal composability. A Security API is secure if it implements correctly both key-management (according to our functionality) and all operations that depend on keys (with respect to the functionalities defining those operations). We present an implementation which is defined with respect to arbitrary functionalities (for the operations that are not concerned with key-management), and hence represents a general design pattern for Security APIs.

Les protocoles cryptographiques sont cruciaux pour sécuriser les transactions électroniques. La confiance en ces protocoles peut être augmentée par l'analyse formelle de leurs propriétés de sécurité. Bien que beaucoup de travaux aient été dédiés pour les protocoles classiques comme le protocole de Needham-Schroeder, très peu de travaux s'adressent à la classe des protocoles de groupe dont les caractéristiques principales sont : les propriétés de sécurité spécifiques qu'ils doivent satisfaire, et le nombre arbitraire des participants qu'ils impliquent. Cette thèse comprend deux contributions principales. La première traite la première caractéristique des protocoles de groupe. Pour cela, nous avons défini un modèle appelé modèle de services que nous avons utilisé pour proposer une stratégie de recherche d'attaques se basant sur la résolution de contraintes. L'approche proposée a permis de retrouver d'anciennes attaques et d'en découvrir de nouvelles sur quelques protocoles de groupe. Certaines attaques ont aussi pu être généralisées pour couvrir le cas de n participants. La deuxième contribution principale de cette thèse consiste à définir un modèle synchrone qui généralise les modèles standards de protocoles en permettant les listes non bornées à l'intérieur des messages. Ceci est assuré par l'introduction d'un nouvel opérateur appelé mpair qui représente une liste construite sur un même patron. Dans ce modèle étendu, nous avons proposé une procédure de décision pour une classe particulière des protocoles de groupe appelée classe de protocoles bien-tagués avec clefs autonomes, en présence d'un intrus actif et avec des clefs composées. / Cryptographic protocols are crucial for securing electronic transactions. The con?dence in these protocols can be increased by the formal analysis of their security properties. Although many works have been dedicated to standard protocols like Needham-Schroeder, very few address the class of group protocols whose main characteristics are : the speci?c security properties that they must satisfy, and the arbitrary number of participants they imply. This thesis provides two main contributions. The ?rst one deals with the ?rst characteristic of group protocols. For that, we de?ned a model called the services model which we used to propose a strategy for ?aws detection based on constraints solving. The suggested approach allows us to ?nd known attacks and new ones on some group protocols. Some attacks have been also generalized to cover the case of n participants. The second main contribution of this thesis consists in de?ning a synchronous model, that generalizes standard protocol models by permitting unbounded lists inside messages. This is ensured by the introduction of a new operator called mpair which represents a list built on the same pattern. In this extended model, we have proposed a decision procedure for a particular class of group protocols called the class of well-tagged protocols with autonomous keys, in presence of an active intruder and with composed keys.

Mobile Ad hoc networks are a step closer to the vision of pervasive computing where all devices dynamically discover each other, organize communication networks between themselves and share resources/information to provide seamless service to the end-user. But providing any reliable service over such a network requires a secure and well-functioning network. Lack of infrastructure, energy-constrained nature of devices and high dynamism in the network makes the task of securing such networks quite challenging. In this thesis we propose cryptographic protocols, which are a stepping stone to a secure ad hoc network. In particular, we contribute to the areas of key establishment and secure routing in ad hoc networks. Key establishment is concerned with making available cryptographic keys to the devices, necessary for participating in the security services of the network. On the other hand routing needs to be secured in such networks as almost all nodes need to participate in the routing process (for eciency reasons) and presence of one malicious node could easily have drastic consequences on the routing performance of the whole network. Thus security checks are required to prevent such malicious nodes from hampering the routing process and to recover from it in case they do succeed. Our rst result is a new group key agreement protocol which is especially suitable for ad hoc networks but also outperforms most known protocols for traditional networks as well. The protocol adapts well to the dynamics of the network and is robust enough to deal with message losses and link failures. It requires little self-organization by the nodes in the network. We present some modied versions of the same and vii tel-00469429, version 1 - 1 Apr 2010 security proofs showing that the security of these protocols is tightly related to the security of the Decisional Die-Hellman problem. We also discuss issues related to implementation of this protocol in real scenarios. Our second result is the introduction of the notion of an Aggregate Designated Verier Signature (ADVS) scheme. An ADVS scheme allows ecient aggregation of multiple signatures on dierent messages designated to the same verier. We show how this primitive can be eciently utilized to secure reactive routing protocols in ad hoc networks. We provide a security model to analyze such schemes and propose an ADVS scheme which aggregates signatures more eciently than existing schemes.

Cette these concerne la verification formelle et la composition de protocoles de securite, motivees en particulier par l'analyse des protocoles de vote electronique. Les chapitres 3 a 5 ont comme sujet la verification de protocoles de securite et le Chapitre 6 vise la composition.Nous montrons dans le Chapitre 3 comment reduire certains problemes d'une algebre quotient des termes a l'algebre libre des termes en utilisant des ensembles fortement complets de variants. Nous montrons que, si l'algebre quotient est donnee par un systeme de reecriture de termes convergent et optimalement reducteur (optimally reducing), alors des ensembles fortement complets de variants existent et sont finis et calculables.Dans le Chapitre 4, nous montrons que l'equivalence statique pour (des classes) de theories equationnelles, dont les theories sous-terme convergentes, la theorie de l'engagement a trappe (trapdoor commitment) et la theorie de signature en aveugle (blind signatures), est decidable en temps polynomial. Nous avons implemente de maniere efficace cette procedure.Dans le Chapitre 5, nous etendons la procedure de decision precedente a l'equivalence de traces. Nous utilisons des ensembles fortement complets de variants du Chapitre 3 pour reduire le probleme a l'algebre libre. Nous modelisons chaque trace du protocole comme une theorie de Horn et nous utilisons un raffinement de la resolution pour resoudre cette theorie. Meme si nous n'avons pas reussi a prouver que la procedure de resolution termine toujours, nous l'avons implementee et utilisee pour donner la premiere preuve automatique de l'anonymat dans le protocole de vote electronique FOO.Dans le Chapitre 6, nous etudions la composition de protocoles. Nous montrons que la composition de deux protocoles qui utilisent des primitives cryptographiques disjointes est sure s'ils ne revelent et ne reutilisent pas les secrets partages. Nous montrons qu'une forme d'etiquettage de protocoles est suffisante pour assurer la disjonction pour un ensemble fixe de primitives cryptographiques. / This thesis is about the formal verification and composition of security protocols, motivated by applications to electronic voting protocols. Chapters 3 to 5 concern the verification of security protocols while Chapter 6 concerns composition.We show in Chapter 3 how to reduce certain problems from a quotient term algebra to the free term algebra via the use of strongly complete sets of variants. We show that, when the quotient algebra is given by a convergent optimally reducing rewrite system, finite strongly complete sets of variants exist and are effectively computable.In Chapter 4, we show that static equivalence for (classes of) equational theories including subterm convergent equational theories, trapdoor commitment and blind signatures is decidable in polynomial time. We also provide an efficient implementation.In Chapter 5 we extend the previous decision procedure to handle trace equivalence. We use finite strongly complete sets of variants introduced in Chapter 3 to get rid of the equational theory and we model each protocol trace as a Horn theory which we solve using a refinement of resolution. Although we have not been able to prove that this procedure always terminates, we have implemented it and used it to provide the first automated proof of vote privacy of the FOO electronic voting protocol.In Chapter 6, we study composition of protocols. We show that two protocols that use arbitrary disjoint cryptographic primitives compose securely if they do not reveal or reuse any shared secret. We also show that a form of tagging is sufficient to provide disjointness in the case of a fixed set of cryptographic primitives.

On ne s’en inquiète peut-être pas assez, mais toute communication confidentielle sur Internet, dont on prend désormais la sécurité pour acquise, pourrait du jour au lendemain devenir très facile à espionner. Nous savons en effet qu’un ordinateur quantique, s’il en existe un de suffisante envergure, pourra –ou peut déjà, qui sait ?– rendre obsolète les protocoles cryptographiques qui nous permettent de gérer nos comptes utilisateurs, faire des transactions bancaires et simplement d’avoir des conversations privées. Heureusement, une communauté de chercheurs se penche déjà sur des protocoles alternatifs ; cependant chacune des propositions est isolée dans son propre sous-domaine de recherche et il est difficile de faire la lumière sur laquelle est la plus prometteuse. À travers trois horizons, explorant respectivement pourquoi la cryptographie actuelle est considérée sécuritaire, comment l’arrivée d’un seul ordinateur quantique sur la planète changera toute la cryptographie, et que faire pour communiquer confidentiellement dans un monde où l’informatique quantique est omniprésente, nous développons un cadre uniforme pour analyser lesquels de ces nouveaux protocoles cryptographiques sont assis sur les bases théoriques présageant la plus grande sécurité.

Les protocoles cryptographiques constituent le coeur de la sécurité dans les communications de tous genres. Ils assurent l’authentification des agents, la confidentialité des données, leur intégrité, l’atomicité des biens et de l’argent, la non-répudiation, etc. Ils sont utilisés dans tous les domaines : le commerce électronique, le domaine militaire, le vote électronique, etc. L’utilisation de la cryptographie est essentielle pour assurer la sécurité d’un protocole, mais elle n’est pas suffisante. En effet, on rapporte un nombre important de protocoles qui ont été longtemps considérés sécuritaires, mais qui se sont avérés défaillants avec le l’usage. Dire qu’un protocole est correct ou non est un problème nondécidable en général. Cependant, plusieurs méthodes (basées sur les logiques, sur le Model-Checking ou sur le typage, etc.) ont vu le jour pour répondre à cette question sous des hypothèses restrictives et ont abouti à des résultats variables. Dans cette thèse, nous suggérons une méthode semi-décidable d’analyse des protocoles cryptographiques pour la propriété de confidentialité. Elle se base sur une intuition : "Un protocole croissant est correct". Nous validons cette intuition et nous proposons le théorème fondamental de correction des protocoles croissants sous des conditions minimales. Ensuite nous proposons une famille de fonctions témoins ayant les propriétés requises pour certifier qu’un protocole est correct. Nous validons enfin notre méthode sur des protocoles communs. / Cryptographic protocols are the fundament of security in all communications. They allow agents’ authentication, data confidentiality, data integrity, atomicity of goods, atomicity of money, nonrepudiation, etc. They are used in all areas: e-commerce, military fields, electronic voting, etc. The use of cryptography is essential to ensure the protocol security, but it is not sufficient. Indeed, we report a significant number of cryptographic protocols that had long been considered safe, but have been proven faulty with usage. Saying that a protocol is correct or not is an undecidable problem in general. However, several methods (logic-based methods, Model-Checking-based methods, typing-based methods, etc.) have emerged to address this question under restrictive assumptions and led to varying results. In this thesis, we suggest a semi-decidable method for analyzing cryptographic protocols for secrecy. It is based on an intuition: "An increasing protocol is correct". We formally validate this intuition, and we state the fundamental theorem of correctness of increasing protocols under few conditions. Then, we propose a safe way to build a family of reliable functions that we call the witness-functions, to certify protocol’s correctness. Finally, we validate our method on common protocols.

Plusieurs outils ont été développé pour vérifier automatiquement les propriétés de sécurité sur des protocoles cryptographiques. Jusqu'à maintenant, la plupart de ces outils permettent de vérifier des propriétés de trace (ou propriétés d'accessibilité) tel que le secret simple ou l'authentification. Néanmoins, plusieurs propriétés de sécurité ne peuvent pas être exprimés en tant que propriété de trace, mais peuvent l'être en tant que propriété d'équivalence. L'anonymat, la non-tracabilité ou le secret fort sont des exemples classique de propriété d'équivalence. Typiquement, deux protocoles P et Q sont équivalent si les actions d'un adversaire (intrus) ne lui permettent pas de distinguer P de Q. Dans la littérature, plusieurs notions d'équivalence ont été étudiés, par exemple l'équivalence de trace ou l'équivalence observationnelle. Néanmoins, ces équivalences se relèvent être très difficiles à démontrer , d'où l'importance de développer des outils de vérification automatique efficaces de ces équivalences. Au sein de cette thèse, nous avons dans un premier temps travaillé sur une approche reposant sur des techniques de résolution de contraintes et nous avons créé un nouvel algorithme pour décider l'équivalence de trace entre deux protocoles pouvant contenir des conditionnelles avec branches "else", et pouvant également être non-déterministe. Cet algorithme a été appliqué sur des exemples concrets comme le "Private authentification protocol" ainsi que le "E-passport protocol". Cette thèse propose également des résultats de composition pour l'équivalence de trace. En particulier, nous nous sommes intéressé à la composition parallèle de protocoles partageant certains secrets. Ainsi dans cette thèse, nous avons démontré que, sous certaines conditions, la composition parallèle de protocoles préserve les propriétés d'équivalence. Ce résultat fut appliqué au "E-passport protocol". Enfin, cette thèse présente une extension à l'outil de vérification automatique ProVerif afin de démontrer automatiquement plus de propriétés d'équivalence. Cette extension a été implémenté au sein de ProVerif ce qui a permis de démontrer la propriété d'anonymat pour le "Private authentification protocol" . / Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or reachability properties) such as authentication and secrecy. However, many security properties cannot be expressed as trace properties, but can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties. Intuitively, two protocols P, Q are equivalent if an adversary can not distinguish P from Q by interacting with these processes. In the literature, several notions of equivalence were studied, e.g. trace equivalence or a stronger one, observational equivalence. However, it is often very difficult to prove by hand any of these equivalences, hence the need for efficient and automatic tools. We first worked on an approach that rely on constraint solving techniques and that is well suited for bounded number of sessions. We provided a new algorithm for deciding the trace equivalence between processes that may contain negative tests and non-determinism. We applied our results on concrete examples such as anonymity of the Private Authentication protocol and the E-passport protocol. We also investigated composition results. More precisely, we focused on parallel composition under shared secrets. We showed that under certain conditions on the protocols, the privacy type properties are preserved under parallel composition and under shared secrets. We applied our result on the e-passport protocol. At last this work presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. This extension have been implemented in ProVerif and allows us to automatically prove anonymity in the private authentication protocol.

Les protocoles cryptographiques jouent un rôle majeur dans les applications ou l'intégrité des données, la confidentialité, l'authenticité et autres propriétés sont essentielles. Ils sont utilisés par exemple dans le commerce électronique, la téléphonie mobile, le vote électronique. Dans la première partie de la thèse nous montrons que le problème d'atteignabilité pour des protocoles cryptographiques temporisés bornés est décidable est NP-complet. Notre procédure se base sur une logique de Hoare complète pour des protocoles cryptographiques bornés et un langage de propriétés très expressif. Dans la deuxième partie, en utilisant des techniques d'interprétation abstraite, nous appliquons cette méthode pour vérifier des propriétés de secret pour les protocoles cryptographiques dans un modèle général. Nous traitons un nombre non borné de sessions, de participants et de nonces ainsi que des messages de taille arbitraire. Nous proposons un algorithme qui calcule un invariant inductif en utilisant des patterns comme représentation symbolique. Cette méthode a été implanté dans l'outil Hermes et validée sur plusieurs études de cas.

Cette thèse est consacrée au problème de la vérification automatique des protocoles cryptographiques d'un point de vue logique et calculatoire.<br />Dans une première partie, nous abordons la sécurité des protocoles dans le cadre logique (formel). Nous montrons comment spécifier différentes propriétés de sécurité des protocoles (secret, authentification, <br />résistance aux attaques par dictionnaire) au moyen d'un langage de processus et comment les analyser de manière automatique pour un nombre borné de sessions.<br />La seconde partie traite de la justification cryptographique des modèles logiques. Nous nous intéressons ici à la notion d'équivalence statique, appliquée en particulier au chiffrement et aux données vulnérables aux attaques par dictionnaire (par ex. des mots de passe). Dans ce cadre, nous montrons que sous certaines conditions simples, toute preuve logique d'équivalence statique implique d'indistinguibilité cryptographique des données modélisées.

La vérification des protocoles cryptographiques assure qu'il n'existe pas d'attaque possible lors d'une exécution du protocole face à un certain intrus ou permet de trouver une attaque. Nous affaiblissons "l'hypothèse de chiffrement parfait" : le seul moyen d'obtenir le contenu d'un message chiffré est de connaître la clef de déchiffrement. Si un protocole est prouvé sûr sous cette hypothèse, cela est insuffisant pour assurer qu'une information confidentielle échangée sur le réseau grâce à un protocole cryptographique entre deux participants reste secrète. Un des moyens pour affaiblir cette hypothèse de chiffrement parfait est de prendre en compte certaines propriétés algébriques dans le modèle de vérification afin d'analyser de manière plus réaliste les protocoles. Nous développons une approche formelle pour la vérification de la propriété de secret d'information pour les protocoles cryptographiques en présence de théories équationnelles et de l'homomorphisme.