International Association for Cryptologic Research

International Association
for Cryptologic Research


Paper: Formal Certification of Code-Based Cryptographic Proofs

G. Barthe
Benjamin Grégoire
R. Janvier
S. Zanella Béguelin
Search ePrint
Search Google
Abstract: As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of systematically structuring proofs as sequences of games. Code-based techniques form an instance of this approach that takes a code-centric view of games, and that relies on programming language theory to justify steps in the proof-transitions between games. While these techniques contribute to increase confidence in the security of cryptographic systems, code-based proofs involve such a large palette of concepts from different fields that machine-verified proofs seem necessary to achieve the highest degree of confidence. Indeed, Halevi has convincingly argued that a tool assisting in the construction and verification of proofs is necessary to solve the crisis with cryptographic proofs. This article reports a first step towards the completion of Halevi's programme through the implementation of a fully formalized framework, CertiCrypt, for code-based proofs built on top of the Coq proof assistant. The framework has been used to yield machine-checked proofs of the PRP/PRF switching lemma and semantic security of ElGamal and OAEP encryption schemes.
  title={Formal Certification of Code-Based Cryptographic Proofs},
  booktitle={IACR Eprint archive},
  keywords={foundations / game-based cryptographic proofs, compiler transformations and optimizations, relational Hoare logic, the Coq proof assistant},
  note={Submitted for publication 13787 received 13 Aug 2007, withdrawn 1 Oct 2007},
  author={G. Barthe and Benjamin Grégoire and R. Janvier and S. Zanella Béguelin},