Skip to Main content Skip to Navigation
New interface

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.
Complete list of metadata

Cited literature [99 references]  Display  Hide  Download
Contributor : Bibliothèque MINES ParisTech Connect in order to contact the contributor
Submitted on : Friday, April 8, 2011 - 11:48:18 AM
Last modification on : Saturday, June 25, 2022 - 11:05:51 PM
Long-term archiving on: : Saturday, July 9, 2011 - 2:40:08 AM


  • HAL Id : pastel-00584350, version 1



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⟩



Record views


Files downloads