Formal certification of game-based cryptographic proofs

Santiago Zanella Beguelin 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.
Document type :
Computer Science and Game Theory [cs.GT]. École Nationale Supérieure des Mines de Paris, 2010. English. <NNT : 2010ENMP0050>
Contributor : Doriane Ibarra <>
Submitted on : Friday, April 8, 2011 - 11:48:18 AM
Last modification on : Monday, October 5, 2015 - 4:58:52 PM


  • HAL Id : pastel-00584350, version 1



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>




Consultation de
la notice


Téléchargement du document