Formal certification of game-based cryptographic proofs

Santiago Zanella Beguelin 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Les séquences de jeux sont une méthodologie établie pour structurer les preuves cryptographiques. De telles preuves peuvent être formalisées rigoureusement en regardant les jeux comme des programmes probabilistes et en utilisant des méthodes de vérification de programmes. Cette thèse décrit CertiCrypt, un outil permettant la construction et vérification automatique de preuves basées sur les jeux. CertiCrypt est implémenté dans l'assistant à la preuve Coq, et repose sur de nombreux domaines, en particulier les probabilités, la complexité, l'algèbre, et la sémantique des langages de programmation. CertiCrypt fournit des outils certifiés pour raisonner sur l'équivalence de programmes probabilistes, en particulier une logique de Hoare relationnelle, une théorie équationnelle pour l'équivalence observationnelle, une bibliothèque de transformations de programme, et des techniques propres aux preuves cryptographiques, permettant de raisonner sur les évènements. Nous validons l'outil en formalisant les preuves de sécurité de plusieurs exemples emblématiques, notamment le schéma de chiffrement OAEP et le schéma de signature FDH.
Type de document :
Thèse
Computer Science and Game Theory [cs.GT]. École Nationale Supérieure des Mines de Paris, 2010. English. <NNT : 2010ENMP0050>


https://pastel.archives-ouvertes.fr/pastel-00584350
Contributeur : Doriane Ibarra <>
Soumis le : vendredi 8 avril 2011 - 11:48:18
Dernière modification le : lundi 5 octobre 2015 - 16:58:52
Document(s) archivé(s) le : samedi 9 juillet 2011 - 02:40:08

Fichier

Identifiants

  • HAL Id : pastel-00584350, version 1

Collections

Citation

Santiago Zanella Beguelin. Formal certification of game-based cryptographic proofs. Computer Science and Game Theory [cs.GT]. École Nationale Supérieure des Mines de Paris, 2010. English. <NNT : 2010ENMP0050>. <pastel-00584350>

Exporter

Partager

Métriques

Consultations de
la notice

4676

Téléchargements du document

302