Paper 2007/314

Formal Certification of Code-Based Cryptographic Proofs

G. Barthe, B. Grëgoire, R. Janvier, and S. Zanella Bëguelin

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.

Note: We decide to withdraw this report following an anonymous reviewer's suggestion. The reviewer opined that the report is misleading because it contained claims about proofs that were not entirely complete in the actual development. We acknowledge that the snapshot of the development on which the reviewer based his opinion did not reflect accurately some claims made in the report. Although the current state of the development matches more accurately what is claimed, in order to avoid further controversies we withdraw the report until the development reflects what our claims down to every single detail.