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
}