Formal certification of game-based cryptographic proofs

Santiago Zanella-Béguelin 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : The game-based approach is a popular methodology for structuring cryptographic proofs as sequences of games. Game-based proofs can be rigorously formalized by taking a code-centric view of games as probabilistic programs and relying on programming language techniques to justify proof steps. In this dissertation we present CertiCrypt, a framework that enables the machine-checked construction and verification of game-based cryptographic proofs. CertiCrypt is built upon the general-purpose proof assistant Coq, from which it inherits the ability to provide independently verifiable evidence that proofs are correct, and draws on many areas, including probability and complexity theory, algebra, and semantics of programming languages. The framework provides certified tools to reason about the equivalence of probabilistic programs, including a relational Hoare logic, a theory of observational equivalence, verified program transformations, and ad-hoc programming language techniques of particular interest in cryptographic proofs, such as reasoning about failure events. We validate our framework through the formalization of several significant case studies, including proofs of security of the Optimal Asymmetric Encryption Padding scheme against adaptive chosen-ciphertext attacks, and of existential unforgeability of Full-Domain Hash signatures.
Liste complète des métadonnées

Cited literature [99 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00584350
Contributor : Bibliothèque Mines Paristech <>
Submitted on : Friday, April 8, 2011 - 11:48:18 AM
Last modification on : Thursday, January 11, 2018 - 4:19:44 PM
Document(s) archivé(s) le : Saturday, July 9, 2011 - 2:40:08 AM

Identifiers

  • HAL Id : pastel-00584350, version 1

Collections

Citation

Santiago Zanella-Béguelin. 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⟩

Share

Metrics

Record views

4867

Files downloads

869