Formal Certification of Code-Based Cryptographic Proofs

As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of developing techniques that help tame the complexity of their proofs. The game-based approach is a popular method in which proofs are structured as sequences of games and in which proof steps establish the validity of transitions between successive games. Game-based proofs can be rigorously formalized by taking a code-centric view of games as probabilistic programs and relying on programming language theory to justify proof steps.

While this code-based view contributes to formalize the security statements precisely and to carry out proofs systematically, typical proofs are so long and involved that formal verification is necessary to achieve a high degree of confidence. We present CertiCrypt, a framework that enables the machine-checked construction and verification of game-based proofs. CertiCrypt is built upon the general-purpose proof assistant Coq, and draws on many areas, including probability and complexity theory, algebra, and semantics of programming languages. The framework provides certified tools to reason about the equivalence of probabilistic programs, including a relational Hoare logic, a theory of observational equivalence, verified program transformations, and ad-hoc techniques such as reasoning about failure events. We demonstrate the usefulness of CertiCrypt through various examples, including proofs of the security of OAEP against adaptive chosen-ciphertext attacks (with a bound that improves upon previously published results) and of the existential unforgeability of FDH signatures. Our work constitutes a first yet significant step towards Halevi’s ambitious program of providing tool support for cryptographic proofs.