Formal certification of code-based cryptographic proofs Export

@inproceedings{citeulike:4264147, abstract = {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 probability, complexity, algebra, and semantics of programming languages. Certicrypt 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 game-based techniques such as reasoning about failure events. The usefulness of Certicrypt is demonstrated through various examples, including a proof of semantic security of OAEP (with a bound that improves upon existing published results), and a proof of existential unforgeability of FDH signatures. Our work provides a first yet significant step towards Halevi's ambitious programme of providing tool support for cryptographic proofs.}, address = {New York, NY, USA}, author = {Barthe, Gilles and Gr\'{e}goire, Benjamin and B\'{e}guelin, Santiago Z.}, booktitle = {POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, citeulike-article-id = {4264147}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1480881.1480894}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1480881.1480894}, doi = {10.1145/1480881.1480894}, isbn = {978-1-60558-379-2}, keywords = {formal, games, proof}, location = {Savannah, GA, USA}, pages = {90--101}, posted-at = {2009-04-02 21:53:58}, priority = {2}, publisher = {ACM}, title = {Formal certification of code-based cryptographic proofs}, url = {http://dx.doi.org/10.1145/1480881.1480894}, year = {2009} }

TY - CONF ID - citeulike:4264147 L3 - citeulike-article-id:4264147 N2 - 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 probability, complexity, algebra, and semantics of programming languages. Certicrypt 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 game-based techniques such as reasoning about failure events. The usefulness of Certicrypt is demonstrated through various examples, including a proof of semantic security of OAEP (with a bound that improves upon existing published results), and a proof of existential unforgeability of FDH signatures. Our work provides a first yet significant step towards Halevi's ambitious programme of providing tool support for cryptographic proofs. CY - Savannah, GA, USA SN - 978-1-60558-379-2 AD - New York, NY, USA EP - 101 TI - Formal certification of code-based cryptographic proofs PB - ACM T2 - POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages SP - 90 KW - formal KW - games KW - proof AU - Barthe, Gilles AU - Gr\'{e}goire, Benjamin AU - B\'{e}guelin, Santiago PY - 2009/// UR - http://dx.doi.org/10.1145/1480881.1480894 ER -