Formal Security Proofs of Cryptographic Standards : A necessity achieved using EasyCrypt - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Thèse Année : 2020

Formal Security Proofs of Cryptographic Standards : A necessity achieved using EasyCrypt

Preuves formelles de la sécurité de standards : Un objectif nécessaire, possible grâce à EasyCrypt

Résumé

In cryptography, Shannon showed that perfect secrecy does not exist. Thus, modern cryptography considers security property in which attackers may break the cryptographic algorithm only with a small (negligible) probability. In this context, cryptographic algorithms, security properties, and security assumptions are expressed as probabilistic programs. Security proofs consist of bounding the probability of an event in such programs. Such profs have been peer-reviewed for some decades, but since they are difficult to prove and to verify, fallacies keep emerging. We propose to use formal proofs to provide enough trustworthiness for crypto-systems such as cryptographic standards. My thesis provides the formal security proofs of three standards that are formally verified using the proof assistant EasyCrypt. The cryptographic standards I have worked on are CMAC (that provides message authentication and integrity), SHA-3 (a cryptographic hash function), and ChaCha20-Poly1305 (an authenticated encryption scheme with associated data). The goal of the thesis is not only to provide formal proof of those standards, but also to develop generic techniques and libraries that can be reused. However, the formal security proofs only ensure the security of the algorithms and not its implementation. To circumvent this gap, with my collaborators, we have developed fast and secure implementations of the last two schemes that are also side-channel resistant. Furthermore, we formally link the implementation with the security proof, leading to the first formal security proof of an implemented standard.
En cryptographie, Shannon a montré que le secret parfait n’existe pas. Ainsi, la cryptographie moderne considère des propriétés de sécurité dans lesquelles un attaquant peut briser l’algorithme cryptographique mais seulement avec une faible probabilité. Dans ce contexte, les algorithmes cryptographiques, les propriétés de sécurité et hypothèses de sécurité sont exprimés sous forme de programmes probabilistes. Les preuves de sécurité consistent à borner la probabilité d’un événement dans de tels programmes. Ces preuves sont difficiles à prouver et vérifier, et malgré le système de relecture académique des erreurs continuent d’être publiées. Nous proposons l’utilisation des preuves formelles pour assurer une fiabilité suffisante dans le cas des standards cryptographiques. Ma thèse fournit les preuves formelles de sécurité de trois standards vérifiées dans l’assistant de preuve EasyCrypt. Ces schémas sont CMAC (qui fournit l’authentification et l’intégrité des messages), SHA-3 (une fonction de hachage cryptographique), et ChaCha20-Poly1305 (un schéma de chiffrement authentifié avec données associées). L’objectif de la thèse n’est pas seulement de formaliser la preuve de sécurité de ces standards, mais aussi de développer des techniques génériques et des bibliothèques qui peuvent être réutilisées. Toutefois, les preuves formelles de sécurité n’assurent que la sécurité des algorithmes et non de leurs implémentations. Pour contourner cette lacune, avec mes collaborateurs, nous lions formellement nos implémentations sûres et efficaces avec la preuve de sécurité, ceci conduit à la première preuve de sécurité cryptographique d’implémentations.
Fichier principal
Vignette du fichier
2020COAZ4049.pdf (2.86 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

tel-03150443 , version 1 (23-02-2021)
tel-03150443 , version 2 (23-03-2021)

Licence

Paternité

Identifiants

  • HAL Id : tel-03150443 , version 2

Citer

Cécile Baritel-Ruet. Formal Security Proofs of Cryptographic Standards : A necessity achieved using EasyCrypt. Cryptography and Security [cs.CR]. Université Côte d'Azur, 2020. English. ⟨NNT : 2020COAZ4049⟩. ⟨tel-03150443v2⟩
367 Consultations
2382 Téléchargements

Partager

Gmail Facebook X LinkedIn More