International Association for Cryptologic Research

Ph.D. Database

The aim of the IACR Ph.D. database is twofold. On the first hand, we want to offer an overview of Ph.D. already completed in the domain of cryptology. Where possible, this should also include a subject classification, an abstract, and access to the full text. On the second hand, it deals with Ph.D. subjects currently under investigation. This way, we provide a timely map of contemporary research in cryptology. All entries or changes need to be approved by an editor. You can contact them via phds (at) iacr.org.

Details

Santiago Zanella Beguelin (#218)
Name Santiago Zanella Beguelin
Personal Homepage http://software.imdea.org/~szanella/
Topic of his/her doctorate. Formal Certification of Game-Based Cryptographic Proofs
Category foundations
Keywords foundations, cryptanalysis, complexity theory, public-key cryptography, digital signatures, zero knowledge
Ph.D. Supervisor(s) Gilles Barthe
Year of completion 2010
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.
E-Mail Address Santiago.Zanella (at) imdea.org
Last Change 2011-04-12 05:25:30
To provide an update on this entry, please click .

Contact: phds (at) iacr.org

[ IACR home page ] [ IACR PhDs page ] © IACR