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 :
Theses
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
Contributor : Doriane Ibarra <>
Submitted on : Friday, April 8, 2011 - 11:48:18 AM
Last modification on : Thursday, February 7, 2013 - 10:37:54 AM

Identifiers

  • 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>

Export

Share

Metrics

Consultation de
la notice

4601

Téléchargement du document

132