Multiset rewriting and the complexity of bounded security protocols

ABSTRACT

We formalize the Dolev-Yao model of security protocols, using a notation based on multiset rewriting with existentials. The goals are to provide a simple formal notation for describing security protocols, to formalize the assumptions of the Dolev-Yao model using this notation, and to analyze the complexity of the secrecy problem under various restrictions. We prove that, even for the case where we restrict the size of messages and the depth of message encryption, the secrecy problem is undecidable for the case of an unrestricted number of protocol roles and an unbounded number of new nonces. We also identify several decidable classes, including a DEXP-complete class when the number of nonces is restricted, and an NP-complete class when both the number of nonces and the number of roles is restricted. We point out a remaining open complexity problem, and discuss the implications these results have on the general topic of protocol analysis.

REFERENCES

• 1: Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols, Information and Computation, v.148 n.1, p.1-70, Jan. 10, 1999 [doi>10.1006/inco.1998.2740]
• 2: Roberto M. Amadio , Denis Lugiez, On the Reachability Problem in Cryptographic Protocols, Proceedings of the 11th International Conference on Concurrency Theory, p.380-394, August 22-25, 2000
• 3: Roberto M. Amadio , Denis Lugiez , Vincent Vanackère, On the symbolic reduction of processes with cryptographic functions, Theoretical Computer Science, v.290 n.1, p.695-740, 1 January 2003 [doi>10.1016/S0304-3975(02)00090-7]
• 4: {4} A. Asperti, A logic for concurrency, Technical report, Department of Computer Science, University of Pisa, 1987.
• 5: Jean-Pierre Banâtre , Daniel Le Métayer, Programming by multiset transformation, Communications of the ACM, v.36 n.1, p.98-111, Jan. 1993 [doi>10.1145/151233.151242]
• 6: Gerard Berry , Gerard Boudol, The chemical abstract machine, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-94, December 1989, San Francisco, California, United States [doi>10.1145/96709.96717]
• 7: Michael Burrows , Martin Abadi , Roger Needham, A logic of authentication, ACM Transactions on Computer Systems (TOCS), v.8 n.1, p.18-36, Feb. 1990 [doi>10.1145/77648.77649]
• 8: Frederick Butler , Iliano Cervesato , Aaron D. Jaggard , Andre Scedrov, A Formal Analysis of Some Properties of Kerberos 5 Using MSR, Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), p.175, June 24-26, 2002
• 9: {9} I. Cervesato, Petri nets and linear logic: a case study for logic programming, in: Proceedings of the 1995 joint conference on Declarative Programming-GULP-PRODE '95, M. Alpuente and M.I. Sessa, eds, Marina di Vietri, Italy, Palladio Press, 1995, pp. 313-318.
• 10: S. Lindell, The Dolev-Yaho Intruder is the Most Powerful Attacker, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.27, June 16-19, 2001
• 11: {11} I. Cervesato, A specification language for crypto-protocols based on multiset rewriting, dependent types and subsorting, in: Proceedings of the Workshop on specification, Analysis and Validation for Emerging Technologies-SAVE '01, G. Delzanno, S. Etalle and M. Gabbrielli, eds, Paphos, Cyprus, 2001, pp. 1-22
• 12: Iliano Cervesato, Typed MSR: Syntax and Examples, Proceedings of the International Workshop on Information Assurance in Computer Networks: Methods, Models, and Architectures for Network Security, p.159-177, May 21-23, 2001
• 13: {13} I. Cervesato, N. Durgin, M. Kanovich and A. Scedrov, Interpreting strands in linear logic, in: Proc. of FMCS '00, 2000.
• 14: I. Cervesato , N. A. Durgin , P. D. Lincoln , J. C. Mitchell , A. Scedrov, A Meta-Notation for Protocol Analysis, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.55, June 28-30, 1999
• 15: {15} I. Cervesato, N. Durgin, J. Mitchell, E Lincoln and A. Scedrov, A comparison between strand spaces and multiset rewriting for security protocol analysis, in: Software Security-Theories and Systems. Mext-NSF-JSPS International Symposium, ISSS 2002, Revised Papers, M. Okada, B. Pierce, A. Scedrov, H. Tokuda and A. Yonezawa, eds, Volume 426, Tokyo, Japan, Springer Lecture Notes in Computer Science, 2003.
• 16: Iliano Cervesato , Frank Pfenning, A Linear Logical Framework, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.264, July 27-30, 1996
• 17: Ashok K. Chandra , Harry R. Lewis , Johann A. Makowsky, Embedded implicational dependencies and their inference problem, Proceedings of the thirteenth annual ACM symposium on Theory of computing, p.342-354, May 11-13, 1981, Milwaukee, Wisconsin, United States [doi>10.1145/800076.802488]
• 18: {18} J. Clark and J. Jacob, A survey of authentication protocol literature, Web Draft Version 1.0 available from http://www.cs.york.ac.uk/-jac, 1997.
• 19: Edmund M. Clarke , Somesh Jha , Wilfredo R. Marrero, Using state space exploration and a natural deduction style message derivation engine to verify security protocols, Proceedings of the IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods, p.87-106, June 08-12, 1998
• 20: Ernie Cohen, TAPS: A First-Order Verifier for Cryptographic Protocols, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.144, July 03-05, 2000
• 21: {21} K. Compton and S. Dexter, Proving authentication protocols in a fragment of linear logic, Manuscript, 1998.
• 22: Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov, Complexity and Expressive Power of Logic Programming, Proceedings of the 12th Annual IEEE Conference on Computational Complexity, p.82, June 24-27, 1997
• 23: {23} G. Denker, J. Meseguer and C. Talcott, Protocol specification and analysis in Maude, in: Proc. of Workshop on Formal Methods and Security Protocols, 1998.
• 24: {24} G. Denker and J. Millen, CAPSL intermediate language, in: Proc. of Workshop on Formal Methods and Security Protocols (FMSP '99), N. Heintze and E. Clarke, eds, Trento, Italy, 1999, www.csl.sri.com/~denker/pub99.html.
• 25: {25} D. Dolev and A. Yao, On the security of public-key protocols, IEEE Transactions on Information Theory2(29) (1983).
• 26: {26} N. Durgin, P. Lincoln, J. Mitchell and A. Scedrov, Undecidability of bounded security protocols, in: Proceedings of the Workshop on Formal Methods and Security Protocols-FMSP, N. Heintze and E. Clarke, eds, Trento, Italy, 1999.
• 27: {27} N. Durgin and J. Mitchell, Analysis of security protocols, in: Calculational System Design, Series F: Computer and Systems Sciences, Vol. 173, IOS Press, 1999.
• 28: {28} H. Enderton, A Mathematical Introduction to Logic, Academic Press, 1972.
• 29: {29} S. Even and O. Goldreich, On the security of multi-party ping-pong protocols, Technical Report 285, Technion-Israel Institute of Technology, 1983.
• 30: {30} F.J.T. Fábrega, J.C. Herzog and J.D. Guttman, Strand spaces: Why is a security protocol correct? in: Proceedings of the 1998 IEEE symposium on Security and Privacy, Oakland, CA, IEEE Computer Society Press, 1998, pp. 160-171.
• 31: {31} A. Freier, P. Karlton and P. Kocher, The SSL protocol version 3.0. draft-ietf-tls-ssl-version3-00.txt, November 18 1996.
• 32: {32} V. Gehlot and C. Gunter, Normal process representatives, in: Proceedings of the Fifth symposium on Logic in Computer Science, Philadelphia, Pennsylvania, 1990, pp. 200-207.
• 33: {33} V. Gehlot and C. Gunther, Normal process representatives, in: Proceedings of the fifth Annual IEEE symposium on Logic in computer Science-LICS '90, Philadelphia, PA, IEEE Computer Society Press, 1990, pp. 200-207.
• 34: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 35: {35} J. Goguen, Order sorted algebra, Technical Report 14, Semantics and Theory of Computation Series, UCLA Computer Science Department, 1978.
• 36: Nevin Heintze , J. D. Tygar, A Model for Secure Protocols and Their Compositions, IEEE Transactions on Software Engineering, v.22 n.1, p.16-30, January 1996 [doi>10.1109/32.481514]
• 37: {37} A. Huima, Efficient infinite-state analysis of security protocols, 1999.
• 38: Neil Immerman, Relational queries computable in polynomial time, Information and Control, v.68 n.1-3, p.86-104, Jan/Feb/March 1986 [doi>10.1016/S0019-9958(86)80029-8]
• 39: {39} M. Kanovich, Linear logic as a logic of computation, Annals of pure and Applied Logic67(1-3) (1994), 183-212.
• 40: {40} M. Kanovich, M. Okada and A. Scedrov, Specifying real-time finite-state systems in linear logic, in: COTIC '98: Second Workshop on Concurrent Constraint Programming for Time-Critical Applications and Multi-Agent systems, Nice, France, 1998. Electronic Notes in Theoretical Computer Science, Volume 16, Issue I. http://www.elsevier.nl/locate/entcs.
• 41: {41} R. Kemmerer, C. Meadows and J. Millen, Three systems for cryptographic protocol analysis, J. cryptology7(2) (1994), 79-130.
• 42: {42} J. Klop, Term rewriting: a tutorial, EATCS Bulletin32 (1987), 143-182.
• 43: {43} J. Kohl and B. Neuman, The Kerberos network authentication service (version 5), Internet Request For Comment RFC-1510, September 1993.
• 44: {44} J. Kohl, B. Neuman and T. Ts'o, in: The Evolution of the Kerberos Authentication Service, IEEE Computer Society Press, 1994, pp. 78-94.
• 45: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 46: Narciso Martí-Oliet , José Meseguer, From Petri Nets to Linear Logic, Category Theory and Computer Science, p.313-340, September 05-08, 1989
• 47: {47} N. Marti-Oliet and J. Meseguer, From Petri nets to linear logic, Mathematical Structures in computer Science2(2) (1991), 69-101.
• 48: Yuri Matiyasevich , Geraud Senizergues, Decision Problems for Semi-Thue Systems with a Few Rules, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.523, July 27-30, 1996
• 49: David A. McAllester, Automatic recognition of tractability in inference relations, Journal of the ACM (JACM), v.40 n.2, p.284-303, April 1993 [doi>10.1145/151261.151265]
• 50: Catherine Meadows, Analyzing the Needham-Schroeder Public-Key Protocol: A Comparison of Two Approaches, Proceedings of the 4th European Symposium on Research in Computer Security: Computer Security, p.351-364, September 25-27, 1996
• 51: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
• 52: John C. Mitchell, Finite-State Analysis of Security Protocols, Proceedings of the 10th International Conference on Computer Aided Verification, p.71-76, June 28-July 02, 1998
• 53: J. C. Mitchell , M. Mitchell , U. Stern, Automated analysis of cryptographic protocols using Mur/spl phi/, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.141, May 04-07, 1997
• 54: Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
• 55: L. C. Paulson, Mechanized proofs for a recursive authentication protocol, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.84, June 10-12, 1997
• 56: Lawrence C Paulson, Proving Properties of Security Protocols by Induction, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.70, June 10-12, 1997
• 57: {57} E.L. Post, A variant of a recursively unsolvable problem, Bulletion of the American Mathematical Society52 (1946), 264-268.
• 58: R. Chadha , M. Kanovich , A. Scedrov, Inductive methods and contract-signing protocols, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA [doi>10.1145/501983.502008]
• 59: A. W. Roscoe, Modelling and verifying key-exchange protocols using CSP and FDR, Proceedings of the The Eighth IEEE Computer Security Foundations Workshop (CSFW '95), p.98, March 13-15, 1995
• 60: Michaël Rusinowitch , Mathieu Turuani, Protocol Insecurity with Finite Number of Sessions is NP-Complete, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.174, June 11-13, 2001
• 61: Steve Schneider, Security Properties and CSP, Proceedings of the 1996 IEEE Symposium on Security and Privacy, p.174, May 06-08, 1996
• 62: V. Shmatikov , U. Stern, Efficient Finite-State Analysis for Large Security Protocols, Proceedings of the 11th IEEE Computer Security Foundations Workshop, p.106, June 09-11, 1998
• 63: Michael Sipser, Introduction to the Theory of Computation, International Thomson Publishing, 1996
• 64: Dawn Xiaodong Song, Athena: a New Efficient Automatic Checker for Security Protocol Analysis, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.192, June 28-30, 1999
• 65: Moshe Y. Vardi, The complexity of relational query languages (Extended Abstract), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.137-146, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802186]
• 66: Thomas Y. C. Woo , Simon S. Lam, A Semantic Model for Authentication Protocols, Proceedings of the 1993 IEEE Symposium on Security and Privacy, p.178, May 24-26, 1993

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Cryptographic controls

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Information flow controls

  E. Data
  E.3 DATA ENCRYPTION
      Subjects: Standards (e.g., DES, PGP, RSA)

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Bounded-action devices (e.g., Turing machines, random access machines); Automata (e.g., finite, push-down, resource-bounded)

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

General Terms:
Algorithms, Security, Theory