Gilles Barthe
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.
- M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15(2):103--127, 2002.Google Scholar
Digital Library
- R. Affeldt, M. Tanaka, and N. Marti. Formal proof of provable security by game-playing in a proof assistant. In Proceedings of security by game-playing in a proof assistant. In Proceedings of Lecture Notes in Computer Science, pages 151--168. Springer, 2007. Google ScholarDigital Library
- T. Amtoft, S. Bandhakavi, and A. Banerjee. A logic for information flow in object-oriented programs. In Proceedings of the 33rd ACM Symposium on Principles of Programming Languages, pages 91--102. ACM Press, 2006. Google ScholarDigital Library
- P. Audebaud and C. Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 2008. Google ScholarDigital Library
- M. Backes and P. Laud. Computationally sound secrecy proofs by mechanized flow analysis. In Proceedings of the 13th ACM Conference on Computer and Communications Security, pages 370--379. ACM Press, 2006. Google ScholarDigital Library
- G. Barthe, J. Cederquist, and S. Tarento. A machine-checked formalization of the generic model and the random oracle model. In 2nd International Joint Conference on Automated Reasoning, pages 385--399. Springer-Verlag, 2004.Google ScholarCross Ref
- M. Bellare and P. Rogaway. Optimal asymmetric encryption -- How to encrypt with RSA. In Advances in Cryptology - EUROCRYPT'94, volume 950 of Lecture Notes in Computer Science, pages 92--111. Springer-Verlag, 1995.Google ScholarCross Ref
- M. Bellare and P. Rogaway. The security of triple encryption and a framework for code-based game-playing proofs. In Advances in Cryptology -- EUROCRYPT'06, volume 4004 of Lecture Notes in Computer Science, pages 409--426, 2006. Google ScholarDigital Library
- N. Benton. Simple relational correctness proofs for static analyses and program transformations. In Proceedings of the 31th ACM Symposium on Principles of Programming Languages, pages 14--25. ACM Press, 2004. Google ScholarDigital Library
- Y. Bertot, B. Gregoire, and X. Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In International Workshop on Types for Proofs and Programs, volume 3839 of LNCS, pages 66--81. Springer-Verlag, 2006. Google ScholarDigital Library
- B. Blanchet. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, pages 140--154, 2006. Google ScholarDigital Library
- B. Blanchet and D. Pointcheval. Automated security proofs with protocols. In IEEE Symposium on Security and Privacy, pages 140--154, 2006. volume 4117 of Lecture Notes in Computer Science, pages 537--554. Springer-Verlag, 2006. Google ScholarDigital Library
- R. Canetti, O. Goldreich, and S. Halevi. The random oracle methodology, revisited. J. ACM, 51(4):557--594, 2004. Google ScholarDigital Library
- R. Corin and J. den Hartog. A probabilistic Hoare-style logic for game-based cryptographic proofs. In Proceedings of the 33rd International Colloquium on Automata, Languages and Programming, volume 4052 of LNCS, pages 252--263, 2006. Google ScholarDigital Library
- J.-S. Coron. On the exact security of Full Domain Hash. In Advances in Cryptology, volume 1880 of Lecture Notes in Computer Science, pages 229--235. Springer-Verlag, 2000. Google ScholarDigital Library
- J. Courant, M. Daubignard, C. Ene, P. Lafourcade, and Y. Lakhnech. Towards automated proofs for asymmetric encryption in the random oracle model. In Computer and Communications Security. ACM Press, 2008. Google ScholarDigital Library
- E. Fujisaki, T. Okamoto, D. Pointcheval, and J. Stern. RSA-OAEP is secure under the RSA assumption. Journal of Cryptology, 17(2):81--104, 2004. Google ScholarDigital Library
- S. Goldwasser and S. Micali. Probabilistic encryption. J. Comput. Syst. Sci., 28(2):270--299, 1984. S. Halevi. A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181, 2005.Google ScholarCross Ref
- J. Hurd, A. McIver, and C. Morgan. Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci., 346(1):96--112, 2005. Google ScholarDigital Library
- B. Jonsson, K. G. Larsen, and W. Yi. Probabilistic extensions of process algebras. In Handbook of Process Algebra, pages 685--711. Elsevier, 2001.Google ScholarCross Ref
- D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22:328--350, 1981.Google ScholarCross Ref
- P. Laud. Semantics and program analysis of computationally secure information flow. In European Symposium on Programming, volume 2028 of Lecture Notes in Computer Science, pages 77--91. Springer-Verlag, 2001. Google ScholarDigital Library
- X. Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In Proceedings of the 33rd ACM Symposium Principles of Programming Languages, pages 42--54. ACM Press, 2006. Google ScholarDigital Library
- C. Meadows. Formal methods for cryptographic protocol analysis: Emerging issues and trends. IEEE Journal on Selected Areas in Communications, 21(1):44--54, 2003. Google ScholarDigital Library
- D. Nowak. A framework for game-based security proofs. In Information and Communications Security, volume 4861, pages 319--333. Springer-Verlag, 2007. Google ScholarDigital Library
- N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages, pages 154--165. ACM Press, 2002. Google ScholarDigital Library
- A. Roy, A. Datta, A. Derek, and J. C. Mitchell. Inductive proofs of computational secrecy. In European Symposium On Research In Computer Security, volume 4734 of Lecture Notes in Computer Science, pages 219--234. Springer-Verlag, 2007. Google ScholarDigital Library
- A. Sabelfeld and D. Sands. A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation, 14(1):59--91, 2001. Google ScholarDigital Library
- V. Shoup. OAEP reconsidered. In Advances in Cryptology -- CRYPTO'01, volume 2139 of Lecture Notes in Computer Science, pages 239--259. Springer-Verlag, 2001. Google ScholarDigital Library
- V. Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332, 2004.Google Scholar
- C. Sprenger and D. Basin. Cryptographically-sound protocol-model abstractions. In Proceedings of CSF'08, pages 115--129. IEEE Computer Society, 2008. Google ScholarDigital Library
- J. Stern. Why provable security matters? In Advances in Cryptology -- EUROCRYPT'03, volume 2656 of Lecture Notes in Computer Science. Springer-Verlag, 2003. Google ScholarDigital Library
- The Coq development team. The Coq Proof Assistant Reference Manual v8.1, 2006. Available at http://coq.inria.frGoogle Scholar
Index Terms
- Formal certification of code-based cryptographic proofs
Recommendations
Formal certification of code-based cryptographic proofs
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesAs 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 ...
Formally Certifying the Security of Digital Signature Schemes
SP '09: Proceedings of the 2009 30th IEEE Symposium on Security and PrivacyWe present two machine-checked proofs of the existentialunforgeability under adaptive chosen-message attacks of the FullDomain Hash signature scheme. These proofs formalize the originalargument of Bellare and Rogaway, and an optimal reduction by ...
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making ...
Comments