Formal certification of code-based cryptographic proofs

12 years 15 days ago
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...
Benjamin Grégoire, Gilles Barthe, Santiago
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where POPL
Authors Benjamin Grégoire, Gilles Barthe, Santiago Zanella Béguelin
Comments (0)