Notre société utilise de nombreux systèmes de communications. Parce que ces systèmes sont omniprésents et sont utilisés pour échanger des informations sensibles, ils doivent être protégés. Cela est fait à l'aide de protocoles cryptographiques. Il est crucial que ces protocoles assurent bien les propriétés de sécurité qu'ils affirment avoir, car les échecs peuvent avoir des conséquences importantes. Malheureusement, concevoir des protocoles cryptographiques est notoirement difficile, comme le montre la régularité avec laquelle de nouvelles attaques sont découvertes. Nous pensons que la vérification formelle est le meilleur moyen d'avoir de bonnes garanties dans la sécurité d'un protocole: il s'agit de prouver mathématiquement qu'un protocole satisfait une certaine propriété de sécurité.Notre objectif est de développer les techniques permettant de vérifier formellement des propriétés d'équivalence sur des protocoles cryptographiques, en utilisant une méthode qui fournit de fortes garanties de sécurités, tout en étant adaptée à des procédures de preuve automatique. Dans cette thèse, nous défendons l'idée que le modèle Bana-Comon pour les propriétés d'équivalences satisfait ces objectifs. Nous soutenons cette affirmation à l'aide de trois contributions.Tout d'abord, nous étayons le modèle Bana-Comon en concevant des axiomes pour les fonctions usuelles des protocoles de sécurités, et pour plusieurs hypothèses cryptographiques. Dans un second temps, nous illustrons l'utilité de ces axiomes et du modèle en réalisant des études de cas de protocoles concrets: nous étudions deux protocoles RFID, KCL et LAK, ainsi que le protocole d'authentification 5G-AKA, qui est utilisé dans les réseaux de téléphonie mobile. Pour chacun de ces protocoles, nous montrons des attaques existentes ou nouvelles, proposons des versions corrigées de ces protocoles, et prouvons que celles-ci sont sécurisées. Finalement, nous étudions le problème de l'automatisation de la recherche de preuves dans le modèle Bana-Comon. Pour cela, nous prouvons la décidabilité d'un ensemble de règles d'inférences qui est une axiomatisation correcte, bien que incomplète, de l'indistingabilité calculatoire, lorsque l'on utilise un schéma de chiffrement IND-CCA2. Du point de vue d'un cryptographe, cela peut être interprété comme la décidabilité d'un ensemble de transformations de jeux. / Our society extensively relies on communications systems. Because such systems are used to exchange sensitive information and are pervasive, they need to be secured. Cryptographic protocols are what allow us to have secure communications. It is crucial that such protocols do not fail in providing the security properties they claim, as failures have dire consequences. Unfortunately, designing cryptographic protocols is notoriously hard, and major protocols are regularly and successfully attacked. We argue that formal verification is the best way to get a strong confidence in a protocol security. Basically, the goal is to mathematically prove that a protocol satisfies some security property.Our objective is to develop techniques to formally verify equivalence properties of cryptographic protocols, using a method that provides strong security guarantees while being amenable to automated deduction techniques. In this thesis, we argue that the Bana-Comon model for equivalence properties meets these goals. We support our claim through three different contributions.First, we design axioms for the usual functions used in security protocols, and for several cryptographic hypothesis. Second, we illustrate the usefulness of these axioms and of the model by completing case studies of concrete protocols: we study two RFID protocols, KCL et LAK, as well as the 5G-AKA authentication protocol used in mobile communication systems. For each of these protocols, we show existing or new attacks against current versions, propose fixes, and prove that the fixed versions are secure. Finally, we study the problem of proof automation in the Bana-Comon model, by showing the decidability of a set of inference rules which is a sound, though incomplete, axiomatization of computational indistinguishability when using an IND-CCA2 encryption scheme. From a cryptographer's point of view, this can be seen as the decidability of a fixed set of cryptographic game transformations.

L'avènement de l'informatique quantique permet de réétudier les primitives cryptographiques avec une sécurité inconditionnelle, c'est à dire sécurisé même contre des adversaires tout puissants. En 1984, Bennett et Brassard ont construit un protocole quantique de distribution de clé. Dans ce protocole, deux joueurs Alice et Bob coopèrent pour partager une clé secrète inconnue d'une tierce personne Eve. Ce protocole a une sécurité inconditionnelle et n'a pasd'équivalent classique.Dans ma thèse, j'ai étudié les primitives cryptographiques à deux joueurs où ces joueurs ne se font pas confiance. J'étudie principalement le pile ou face quantique et la mise-en-gage quantique de bit. En informatique classique, ces primitivessont réalisables uniquement avec des hypothèses calculatoires, c'est-à-dire en supposant la difficulté d'un problème donné. Des protocoles quantiques ont été construits pour ces primitives où un adversaire peut tricher avec une probabilité constante strictement inférieure à 1, ce qui reste impossible classiquement. Néanmoins, Lo et Chau ont montré l'impossibilité de créer ces primitives parfaitement même en utilisant l'informatique quantique. Il reste donc à déterminer quelles sont les limites physiques de ces primitives.Dans une première partie, je construis un protocole quantique de pile ou face où chaque joueur peut tricher avec probabilité au plus 1/racine(2) + eps pour tout eps > 0. Ce résultat complète un résultat de Kitaev qui dit que dans un jeu de pile ou face quantique, un joueur peut toujours tricher avec probabilité au moins 1/racine(2). J'ai également construit un protocole de mise-en-gage de bit quantique optimal où un joueur peut tricher avec probabilité au plus 0,739 + eps pour tout eps > 0 puis ai montré que ce protocole est en fait optimal. Finalement, j'ai dérivé des bornes inférieures et supérieures pour une autre primitive: la transmission inconsciente, qui est une primitive universelle.Dans une deuxième partie, j'intègre certains aspects pratiques dans ces protocoles. Parfois les appareils de mesure ne donnent aucun résultat, ce sont les pertes dans la mesure. Je construis un protocole de lancer de pièce quantique tolérant aux pertes avec une probabilité de tricher de 0,859. Ensuite, j'étudie le modèle dispositif-indépendant où on ne suppose plus rien sur les appareils de mesure et de création d'état quantique.Finalement, dans une troisième partie, j'étudie ces primitives cryptographiques avec un sécurité computationnelle. En particulier, je fais le lien entre la mise en gage de bit quantique et les protocoles zero-knowledge quantiques.

L'avènement de l'informatique quantique permet de réétudier les primitives cryptographiques avec une sécurité inconditionnelle, c'est à dire sécurisé même contre des adversaires tout puissants. En 1984, Bennett et Brassard ont construit un protocole quantique de distribution de clé. Dans ce protocole, deux joueurs Alice et Bob coopèrent pour partager une clé secrète inconnue d'une tierce personne Eve. Ce protocole a une sécurité inconditionnelle et n'a pasd'équivalent classique.Dans ma thèse, j'ai étudié les primitives cryptographiques à deux joueurs où ces joueurs ne se font pas confiance. J'étudie principalement le pile ou face quantique et la mise-en-gage quantique de bit. En informatique classique, ces primitivessont réalisables uniquement avec des hypothèses calculatoires, c'est-à-dire en supposant la difficulté d'un problème donné. Des protocoles quantiques ont été construits pour ces primitives où un adversaire peut tricher avec une probabilité constante strictement inférieure à 1, ce qui reste impossible classiquement. Néanmoins, Lo et Chau ont montré l'impossibilité de créer ces primitives parfaitement même en utilisant l'informatique quantique. Il reste donc à déterminer quelles sont les limites physiques de ces primitives.Dans une première partie, je construis un protocole quantique de pile ou face où chaque joueur peut tricher avec probabilité au plus 1/racine(2) + eps pour tout eps > 0. Ce résultat complète un résultat de Kitaev qui dit que dans un jeu de pile ou face quantique, un joueur peut toujours tricher avec probabilité au moins 1/racine(2). J'ai également construit un protocole de mise-en-gage de bit quantique optimal où un joueur peut tricher avec probabilité au plus 0,739 + eps pour tout eps > 0 puis ai montré que ce protocole est en fait optimal. Finalement, j'ai dérivé des bornes inférieures et supérieures pour une autre primitive: la transmission inconsciente, qui est une primitive universelle.Dans une deuxième partie, j'intègre certains aspects pratiques dans ces protocoles. Parfois les appareils de mesure ne donnent aucun résultat, ce sont les pertes dans la mesure. Je construis un protocole de lancer de pièce quantique tolérant aux pertes avec une probabilité de tricher de 0,859. Ensuite, j'étudie le modèle dispositif-indépendant où on ne suppose plus rien sur les appareils de mesure et de création d'état quantique.Finalement, dans une troisième partie, j'étudie ces primitives cryptographiques avec un sécurité computationnelle. En particulier, je fais le lien entre la mise en gage de bit quantique et les protocoles zero-knowledge quantiques. / Quantum computing allows us to revisit the study of quantum cryptographic primitives with information theoretic security. In 1984, Bennett and Brassard presented a protocol of quantum key distribution. In this protocol, Alice and Bob cooperate in order to share a common secret key k, which has to be unknown for a third party that has access to the communication channel. They showed how to perform this task quantumly with an information theoretic security; which is impossible classically.In my thesis, I study cryptographic primitives with two players that do not trust each other. I study mainly coin flipping and bit commitment. Classically, both these primitives are impossible classically with information theoretic security. Quantum protocols for these primitives where constructed where cheating players could cheat with probability stricly smaller than 1. However, Lo, Chau and Mayers showed that these primitives are impossible to achieve perfectly even quantumly if one requires information theoretic security. I study to what extent imperfect protocols can be done in this setting.In the first part, I construct a quantum coin flipping protocol with cheating probabitlity of 1/root(2) + eps for any eps > 0. This completes a result by Kitaev who showed that in any quantum coin flipping protocol, one of the players can cheat with probability at least 1/root(2). I also constructed a quantum bit commitment protocol with cheating probability 0.739 + eps for any eps > 0 and showed that this protocol is essentially optimal. I also derived some upper and lower bounds for quantum oblivious transfer, which is a universal cryptographic primitive.In the second part, I study some practical aspects related to these primitives. I take into account losses than can occur when measuring a quantum state. I construct a Quantum Coin Flipping and Quantum Bit Commitment protocols which are loss-tolerant and have cheating probabilities of 0.859. I also construct these primitives in the device independent model, where the players do not trust their quantum device. Finally, in the third part, I study these cryptographic primitives with information theoretic security. More precisely, I study the relationship between computational quantum bit commitment and quantum zero-knowledge protocols.