Formal certification of code-based cryptographic proofs

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.

REFERENCES

• 1: M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15(2):103--127, 2002.
• 2: 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.
• 3: Torben Amtoft , Sruthi Bandhakavi , Anindya Banerjee, A logic for information flow in object-oriented programs, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.91-102, January 11-13, 2006, Charleston, South Carolina, USA
• 4: P. Audebaud and C. Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 2008.
• 5: Michael Backes , Peeter Laud, Computationally sound secrecy proofs by mechanized flow analysis, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180405.1180450]
• 6: 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.
• 7: 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.
• 8: 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.
• 9: Nick Benton, Simple relational correctness proofs for static analyses and program transformations, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 14-16, 2004, Venice, Italy
• 10: 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.
• 11: Bruno Blanchet, A Computationally Sound Mechanized Prover for Security Protocols, Proceedings of the 2006 IEEE Symposium on Security and Privacy, p.140-154, May 21-24, 2006 [doi>10.1109/SP.2006.1]
• 12: 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.
• 13: Ran Canetti , Oded Goldreich , Shai Halevi, The random oracle methodology, revisited, Journal of the ACM (JACM), v.51 n.4, p.557-594, July 2004 [doi>10.1145/1008731.1008734]
• 14: 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.
• 15: Jean-Sébastien Coron, On the Exact Security of Full Domain Hash, Proceedings of the 20th Annual International Cryptology Conference on Advances in Cryptology, p.229-235, August 20-24, 2000
• 16: Judicaël Courant , Marion Daubignard , Cristian Ene , Pascal Lafourcade , Yassine Lakhnech, Towards automated proofs for asymmetric encryption schemes in the random oracle model, Proceedings of the 15th ACM conference on Computer and communications security, October 27-31, 2008, Alexandria, Virginia, USA [doi>10.1145/1455770.1455817]
• 17: Eiichiro Fujisaki , Tatsuaki Okamoto , David Pointcheval , Jacques Stern, RSA-OAEP Is Secure under the RSA Assumption, Journal of Cryptology, v.17 n.2, p.81-104, March 2004 [doi>10.1007/s00145-002-0204-y]
• 18: 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.
• 19: Joe Hurd , Annabelle McIver , Carroll Morgan, Probabilistic guarded commands mechanized in HOL, Theoretical Computer Science, v.346 n.1, p.96-112, 23 November 2005 [doi>10.1016/j.tcs.2005.08.005]
• 20: B. Jonsson, K. G. Larsen, and W. Yi. Probabilistic extensions of process algebras. In Handbook of Process Algebra, pages 685--711. Elsevier, 2001.
• 21: D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22:328--350, 1981.
• 22: Peeter Laud, Semantics and Program Analysis of Computationally Secure Information Flow, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.77-91, April 02-06, 2001
• 23: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 24: C. Meadows. Formal methods for cryptographic protocol analysis: Emerging issues and trends. IEEE Journal on Selected Areas in Communications, 21(1):44--54, 2003.
• 25: D. Nowak. A framework for game-based security proofs. In Information and Communications Security, volume 4861, pages 319--333. Springer-Verlag, 2007.
• 26: Norman Ramsey , Avi Pfeffer, Stochastic lambda calculus and monads of probability distributions, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-165, January 16-18, 2002, Portland, Oregon
• 27: Arnab Roy , Anupam Datta , Ante Derek , John C. Mitchell, Inductive Proofs of Computational Secrecy, Proceedings of the 12th European symposium on Research In Computer Security, September 24-26, 2007, Dresden, Germany [doi>10.1007/978-3-540-74835-9_15]
• 28: Andrei Sabelfeld , David Sands, A Per Model of Secure Information Flow in Sequential Programs, Higher-Order and Symbolic Computation, v.14 n.1, p.59-91, March 2001 [doi>10.1023/A:1011553200337]
• 29: Victor Shoup, OAEP Reconsidered, Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology, p.239-259, August 19-23, 2001
• 30: V. Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332, 2004.
• 31: Christoph Sprenger , David Basin, Cryptographically-Sound Protocol-Model Abstractions, Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, p.115-129, June 23-25, 2008 [doi>10.1109/CSF.2008.19]
• 32: J. Stern. Why provable security matters? In Advances in Cryptology -- EUROCRYPT'03, volume 2656 of Lecture Notes in Computer Science. Springer-Verlag, 2003.
• 33: The Coq development team. The Coq Proof Assistant Reference Manual v8.1, 2006. Available at http://coq.inria.fr

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization; Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Security, Theory, Verification

Keywords:
coq proof assistant, cryptographic proofs, observational equivalence, program transformations, relational hoare logic