Towards computationally sound symbolic analysis of key exchange protocols

ABSTRACT

We present a cryptographically sound formal method for proving correctness of key exchange protocols. Our main tool is a fragment of a symbolic protocol logic. We demonstrate that proofs of key agreement and key secrecy in this logic imply simulatability in Shoup's secure multi-party framework for key exchange. As part of the logic, we present cryptographically sound abstractions of CMA-secure digital signatures and a restricted form of Diffie-Hellman exponentiation, which is a technical result of independent interest. We illustrate our method by constructing a proof of security for a simple authenticated Diffie-Hellman protocol.

REFERENCES

• 1: M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology, 15(2):103--127, 2002.
• 2: Michael Backes , Birgit Pfitzmann, Relating Symbolic and Cryptographic Secrecy, Proceedings of the 2005 IEEE Symposium on Security and Privacy, p.171-182, May 08-11, 2005 [doi>10.1109/SP.2005.17]
• 3: Michael Backes , Birgit Pfitzmann , Michael Waidner, A composable cryptographic library with nested operations, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948140]
• 4: M. Backes, B. Pfitzmann, and M. Waidner. A general composition theorem for secure reactive systems. In Proc. 1st Theory of Cryptography Conference (TCC), volume 3378 of LNCS, pages 336--354. Springer-Verlag, 2004.
• 5: D. Beaver. Secure multiparty protocols and zero-knowledge proof systems tolerating a faulty minority. J. Cryptology, 4(2):75--122, 1991.
• 6: Mihir Bellare , Ran Canetti , Hugo Krawczyk, A modular approach to the design and analysis of authentication and key exchange protocols (extended abstract), Proceedings of the thirtieth annual ACM symposium on Theory of computing, p.419-428, May 24-26, 1998, Dallas, Texas, United States [doi>10.1145/276698.276854]
• 7: Mihir Bellare , Phillip Rogaway, Entity Authentication and Key Distribution, Proceedings of the 13th Annual International Cryptology Conference on Advances in Cryptology, p.232-249, August 22-26, 1993
• 8: Ray Bird , Inder S. Gopal , Amir Herzberg , Philippe A. Janson , Shay Kutten , Refik Molva , Moti Yung, Systematic Design of Two-Party Authentication Protocols, Proceedings of the 11th Annual International Cryptology Conference on Advances in Cryptology, p.44-61, August 11-15, 1991
• 9: Simon Blake-Wilson , Don Johnson , Alfred Menezes, Key Agreement Protocols and Their Security Analysis, Proceedings of the 6th IMA International Conference on Cryptography and Coding, p.30-45, December 17-19, 1997
• 10: R. Canetti. Studies in secure multiparty computation and applications. PhD thesis, The Weizmann Institute of Science, 1995.
• 11: R. Canetti. Security and composition of multiparty cryptographic protocols. J. Cryptology, 13(1):143--202, 2000.
• 12: R. Canetti, Universally Composable Security: A New Paradigm for Cryptographic Protocols, Proceedings of the 42nd IEEE symposium on Foundations of Computer Science, p.136, October 14-17, 2001
• 13: Ran Canetti, Universally Composable Signature, Certification, and Authentication, Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), p.219, June 28-30, 2004 [doi>10.1109/CSFW.2004.24]
• 14: R. Canetti and J. Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). http://eprint.iacr.org/2004/334, 2005.
• 15: Ran Canetti , Hugo Krawczyk, Analysis of Key-Exchange Protocols and Their Use for Building Secure Channels, Proceedings of the International Conference on the Theory and Application of Cryptographic Techniques: Advances in Cryptology, p.453-474, May 06-10, 2001
• 16: Ran Canetti , Hugo Krawczyk, Universally Composable Notions of Key Exchange and Secure Channels, Proceedings of the International Conference on the Theory and Applications of Cryptographic Techniques: Advances in Cryptology, p.337-351, May 02, 2002
• 17: R. Canetti and T. Rabin. Universal composition with joint state. In Proc. Advances in Cryptology -- CRYPTO 2003, volume 2729 of LNCS, pages 265--281. Springer-Verlag, 2003.
• 18: V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In Proc. 14th European Symposium on Programming (ESOP), volume 3444 of LNCS, pages 157--171. Springer-Verlag, 2005.
• 19: A. Datta, A. Derek, J.C. Mitchell, and D. Pavlovic. A derivation system for security protocols and its logical formalization. In Proc. 16th IEEE Computer Security Foundations Workshop (CSFW), pages 109--125. IEEE, 2003.
• 20: A. Datta, A. Derek, J.C. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In Proc. 32nd International Colloquium on Automata, Languages and Programming (ICALP) - to appear, 2005.
• 21: T. Dierks and C. Allen. The TLS protocol Version 1.0. Internet RFC: http://www.ietf.org/rfc/rfc2246.txt, January 1999.
• 22: Whitfield Diffie , Paul C. Van Oorschot , Michael J. Wiener, Authentication and authenticated key exchanges, Designs, Codes and Cryptography, v.2 n.2, p.107-125, June 1992 [doi>10.1007/BF00124891]
• 23: Nancy Durgin , John Mitchell , Dusko Pavlovic, A compositional logic for proving security properties of protocols, Journal of Computer Security, v.11 n.4, p.677-721, 01/01/2004
• 24: Oded Goldreich, Foundations of Cryptography: Volume 2, Basic Applications, Cambridge University Press, New York, NY, 2004
• 25: Shafi Goldwasser , Silvio Micali , Ronald L. Rivest, A digital signature scheme secure against adaptive chosen-message attacks, SIAM Journal on Computing, v.17 n.2, p.281-308, April 1988 [doi>10.1137/0217017]
• 26: P. Gupta and V. Shmatikov. Towards computationally sound symbolic analysis of key exchange protocols. http://eprint.iacr.org/2005/171, 2005.
• 27: R. Impagliazzo and D. Zuckerman. How to recycle random bits. In Proc. 30th Annual Symposium on Foundations of Computer Science (FOCS), pages 248--253. IEEE, 1989.
• 28: C. Kaufman (ed.). Internet key exchange (IKEv2) protocol. Internet draft: http://www.ietf.org/internet-drafts/draft-ietf-ipsec-ikev2-17.txt, September 2004.
• 29: J. Kohl and C. Neuman. The Kerberos network authentication service (V5). Internet RFC: http://www.ietf.org/rfc/rfc1510.txt, September 1993.
• 30: P. Laud. Symmetric encryption in automatic analyses for confidentiality against active adversaries. In Proc. IEEE Symposium on Security and Privacy, pages 71--85. IEEE, 2004.
• 31: D. Micciancio and B. Warinschi. Completeness theorems for the Abadi-Rogaway language of encrypted expressions. J. Computer Security, 12(1):99--130, 2004.
• 32: D. Micciancio and B. Warinschi. Soundness of formal encryption in the presence of active adversaries. In Proc. 1st Theory of Cryptography Conference (TCC), volume 3378 of LNCS, pages 133--151. Springer-Verlag, 2004.
• 33: Birgit Pfitzmann , Michael Waidner, A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.184, May 14-16, 2001
• 34: V. Shoup. On formal models for secure key exchange (version 4). http://shoup.net/papers/skey.pdf, November 1999.
• 35: F. Javier Thayer Fábrega, Strand spaces: proving security protocols correct, Journal of Computer Security, v.7 n.2-3, p.191-230, Jan. 1999

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Authentication

General Terms:
Security

Keywords:
computational soundness, cryptographic protocols, protocol logic, symbolic analysis