CryptoDB
Formal Certification of Code-Based Cryptographic Proofs
Authors: | |
---|---|
Download: | |
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. |
BibTeX
@misc{eprint-2007-13594, 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}, url={http://eprint.iacr.org/2007/314}, note={Submitted for publication Santiago.Zanella@sophia.inria.fr 13787 received 13 Aug 2007, withdrawn 1 Oct 2007}, author={G. Barthe and Benjamin Grégoire and R. Janvier and S. Zanella Béguelin}, year=2007 }