Preuves formelles de la sécurité de standards : Un objectif nécessaire, possible grâce à EasyCrypt ; Formal Security Proofs of Cryptographic : A necessity achieved using EasyCrypt
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
E-Book
Title:
Preuves formelles de la sécurité de standards : Un objectif nécessaire, possible grâce à EasyCrypt ; Formal Security Proofs of Cryptographic : A necessity achieved using EasyCrypt
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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. ; 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 ...