International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Gilles Barthe

Affiliation: IMDEA Software Institute

Publications

Year
Venue
Title
2018
EUROCRYPT
2017
EUROCRYPT
2017
CRYPTO
2017
EUROCRYPT
2016
EUROCRYPT
2016
FSE
2015
EPRINT
2015
EPRINT
2015
EPRINT
2015
EPRINT
2015
PKC
2015
EUROCRYPT
2015
EUROCRYPT
2015
ASIACRYPT
2014
CRYPTO
2014
EPRINT
2014
EPRINT
2014
EPRINT
2014
EPRINT
2014
EPRINT
2014
CHES
2011
CRYPTO
2007
EPRINT
Formal Certification of Code-Based Cryptographic Proofs
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.

Program Committees

Crypto 2018
Eurocrypt 2015