Towards automated proofs for asymmetric encryption schemes in the random oracle model

ABSTRACT

Chosen-ciphertext security is by now a standard security property for asymmetric encryption. Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures that analyze such cryptosystems and provide security proofs. This paper presents an automated procedure for analyzing generic asymmetric encryption schemes in the random oracle model. It has been applied to several examples of encryption schemes among which the construction of Bellare-Rogaway 1993, of Pointcheval at PKC'2000 and REACT.

REFERENCES

• 1: G. Barthe, J. Cederquist, and S. Tarento. A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In D. Basin and M. Rusinowitch, editors, Proceedings of IJCAR'04, volume 3097 of LNCS, pages 385--399, 2004.
• 2: Gilles Barthe, Bejamin Gregoire, Romain Janvier, and Santiago Zanella Beguelin. A framework for language-based cryptographic proofs. In 2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory, Oct 2007.
• 3: Gilles Barthe and Sabrina Tarento. A machine-checked formalization of the random oracle model. In Jean-Christophe Filliatre, Christine Paulin-Mohring, and Benjamin Werner, editors, Proceedings of TYPES'04, volume 3839 of Lecture Notes in Computer Science, pages 33--49. Springer, 2004.
• 4: Mihir Bellare , Anand Desai , David Pointcheval , Phillip Rogaway, Relations Among Notions of Security for Public-Key Encryption Schemes, Proceedings of the 18th Annual International Cryptology Conference on Advances in Cryptology, p.26-45, August 23-27, 1998
• 5: Mihir Bellare , Phillip Rogaway, Random oracles are practical: a paradigm for designing efficient protocols, Proceedings of the 1st ACM conference on Computer and communications security, p.62-73, November 03-05, 1993, Fairfax, Virginia, United States [doi>10.1145/168588.168596]
• 6: Mihir Bellare and Phillip Rogaway. Optimal asymmetric encryption. In Alfredo De Santis, editor, EUROCRYPT, volume 950 of Lecture Notes in Computer Science, pages 92--111. Springer, 1994.
• 7: Mihir Bellare and Phillip Rogaway. Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004/331, 2004. http://eprint.iacr.org/.
• 8: 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]
• 9: Bruno Blanchet and David Pointcheval. Automated security proofs with sequences of games. In Cynthia Dwork, editor, CRYPTO, volume 4117 of Lecture Notes in Computer Science, pages 537--554. Springer, 2006.
• 10: Ricardo Corin and Jerry den Hartog. A probabilistic hoare-style logic for game-based cryptographic proofs. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, ICALP (2), volume 4052 of Lecture Notes in Computer Science, pages 252--263. Springer, 2006.
• 11: Ivan Damgård, Towards Practical Public Key Systems Secure Against Chosen Ciphertext Attacks, Proceedings of the 11th Annual International Cryptology Conference on Advances in Cryptology, p.445-456, August 11-15, 1991
• 12: Anupam Datta , Ante Derek , John C. Mitchell , Bogdan Warinschi, Computationally Sound Compositional Logic for Key Exchange Protocols, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.321-334, July 05-07, 2006 [doi>10.1109/CSFW.2006.9]
• 13: U. Feige , A. Fiat , A. Shamir, Zero-knowledge proofs of identity, Journal of Cryptology, v.1 n.2, p.77-94, Aug. 1988 [doi>10.1007/BF02351717]
• 14: Eiichiro Fujisaki , Tatsuaki Okamoto, How to Enhance the Security of Public-Key Encryption at Minimum Cost, Proceedings of the Second International Workshop on Practice and Theory in Public Key Cryptography, p.53-68, March 01-03, 1999
• 15: Shai Halevi. A plausible approach to computer-aided cryptographic proofs. http://theory.lcs.mit.edu/ shaih/pubs.html, 2005.
• 16: David Nowak. A framework for game-based security proofs. In ICICS, pages 319--333, 2007.
• 17: Tatsuaki Okamoto , David Pointcheval, REACT: Rapid Enhanced-Security Asymmetric Cryptosystem Transform, Proceedings of the 2001 Conference on Topics in Cryptology: The Cryptographer's Track at RSA, p.159-175, April 08-12, 2001
• 18: David Pointcheval, Chosen-Ciphertext Security for Any One-Way Cryptosystem, Proceedings of the Third International Workshop on Practice and Theory in Public Key Cryptography: Public Key Cryptography, p.129-146, January 18-20, 2000
• 19: Victor Shoup. Oaep reconsidered. J. Cryptology, 15(4):223--249, 2002.
• 20: Victor Shoup. Sequences of games: a tool for taming complexity in security proofs, 2004. http://eprint.iacr.org/2004/332.
• 21: David Soldera , Jennifer Seberry , Chengxin Qu, The Analysis of Zheng-Seberry Scheme, Proceedings of the 7th Australian Conference on Information Security and Privacy, p.159-168, July 03-05, 2002
• 22: Sabrina Tarento. Machine-checked security proofs of cryptographic signature schemes. In Sabrina De Capitani di Vimercati, Paul F. Syverson, and Dieter Gollmann, editors, Computer Security -- ESORICS 2005, volume 3679 of Lecture Notes in Computer Science, pages 140--158. Springer, 2005.
• 23: Yuliang Zheng and Jennifer Seberry. Immunizing public key cryptosystems against chosen ciphertext attacks. IEEE Journal on Selected Areas in Communications, 11(5):715--724, 1993.

INDEX TERMS

Primary Classification:
  E. Data
  E.3 DATA ENCRYPTION
      Subjects: Public key cryptosystems

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions

General Terms:
Security, Verification

Keywords:
asymmetric encryption, automated proofs, hoare logics, provable security, random oracle model