Formalisation en Coq de modèles cryptographiques idéalisés et application au cryptosystème ElGamal
Institution:
NiceDisciplines:
Directors:
Abstract EN:
The work begun in this thesis concerns the formal check of cryptographic algorithms under the proof assistant Coq. The cryptographic algorithms base on cryptographic primitives aiming at assuring the confidentiality of the data, the indistinguabilité, the infalsifiabilité, etc… However, most approaches to the formal analyses of cryptographic protocols make the perfect cryptographic assumption, i. E. The hypothese that there is no way to obtain knowledge about the plaintext pertaining to a ciphertext without knowing the key. Ideally, one would prefer to rely on a weaker hypothesis on the computational cost of gaining information about the plaintext pertaining ti a ciphertext without knowing the key. Such a view is permitted by the generic model and the random oracle model which provide non-standard computational models in which one may reason about the computational cost of breaking a cryptographic scheme. Using the proof assistant Coq, we provide a machine-checked account of the Generic Model and the Random >Oracle Model. We exploit this framework to prove the safety of cryptosystems that depend on a cyclic group (like ElGamal cryptosystem), against non-interactive (by using the generic model) and interactive (by using the random oracle model) generic attacks ; and we prove the security of blind signatures against interactive attacks (by using the generic model and the random oracle model). To prove the last step, we use a generic parallel attack to create a forgery signature.
Abstract FR:
Le travail entrepris dans cette thèse porte sur la vérification formelle d’algorithmes cryptographiques sous l’assistant à la preuve Coq. Les algorithmes cryptographiques reposent sur des primitives cryptographiques visant à assurer la confidentialité des transactions, l’indistinguabilité, l’infalsifiabilité etc… Cependant, la plupart des approches d’analyse formelle d’algorithmes cryptographiques font l’hypothèse de cryptographie parfaite, c’est-à-dire qu’il est impossible de déchiffrer un message sans en connaître la clé de déchiffrement. Dans le meilleur des cas, nous préfèrerions nous baser sur une hypothèse plus faible sur le coût computationnel pour obtenir des informations sur le message clair concernant un message chiffré sans connaître la clé. Une telle vue est autorisée par le modèle générique et le modèle d’oracle aléatoire qui fournissent des modèles computationnels non standard dans lesquels nous pouvons raisonner sur le coût computationnel de casser un schéma cryptographique. En utilisant l’assistant à la preuve Coq, nous fournissons une preuve formelle du modèle générique et du modèle d’oracle aléatoire. Nous exploitons ce travail pour prouver la sécurité de cryptosystèmes dépendant d’un groupe cyclique (comme le cryptosystème ElGamal), contre des attaques non-interactives (en utilisant le modèle générique) et interactives (en utilisant le modèle d’oracle aléatoire). Nous prouvons également la sécurité contre une attaque interactive visant à contrefaire une signature (en utilisant le modèle d’oracle aléatoire) ; afin de prouver cette sécurité, nous utilisons une attaque parallèle pour créer une signature contrefaire.