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. Game-based techniques provide a popular approach in which proofs are structured as sequences of games, and in which proof steps establish the validity of transitions between successive 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 proof steps. While code-based techniques contribute 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 code-based proofs. CertiCrypt is built upon the general-purpose proof assistant Coq, and draws on many areas, including prob...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Benjamin Grégoire, Gilles Barthe, Santiago Zanella Béguelin
• Keywords: Code-based Proofs, Cryptographic Proofs, POPL 2009, Programming Languages, Typical Proofs