A rewriting-based inference system for the NRL protocol analyzer: grammar generation

ABSTRACT

The NRL Protocol Analyzer (NPA) is a tool for the formal specification and analysis of cryptographic protocols that has been used with great effect on a number of complex real-life protocols. It probably outranks any of the existing tools in the sheer range of the types of attacks it is able to model and discover. However, the techniques in NPA lack an independent formal specification and model, and instead are closely intertwined with other NPA features. The main contribution of this paper is to rectify this problem by giving for the first time a precise formal specification of one of the main features of the NPA inference system: its grammar-based techniques for invariant generation, as well as a backwards reachability analysis method that captures some of the key features of the NPA. This formal specification is given within the well-known rewriting framework so that the inference system is specified as a set of rewrite rules modulo an equational theory describing the behavior of the cryptographic algorithms involved.

REFERENCES

• 1: D. Basin, S. Mödersheim, and L. Viganò. OFMC: A symbolic model checker for security protocols. International Journal of Information Security, 4(3):181--208, June 2005. Published online December 2004.
• 2: Y. Chevalier, R. Kusters, M. Rusinowitch, and M. Turuani. Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In 23rd Conference on Foundations Software Technology and Theoretical Computer Science, volume 2914 of Lecture Notes in Computer Science, pages 124--135, 2003.
• 3: Yannick Chevalier , Ralf Küsters , Michaël Rusinowitch , Mathieu Turuani, An NP Decision Procedure for Protocol Insecurity with XOR, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.261, June 22-25, 2003
• 4: M. Clavel , F. Durán , S. Eker , P. Lincoln , N. Martí-Oliet , J. Meseguer , J. F. Quesada, Maude: specification and programming in rewriting logic, Theoretical Computer Science, v.285 n.2, p.187-243, 28 August 2002 [doi>10.1016/S0304-3975(01)00359-0]
• 5: H. Comon-Lundh , V. Shmatikov, Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.271, June 22-25, 2003
• 6: D. Dolev and A. Yao. On the security of public key protocols. IEEE Transaction on Information Theory, 29(2):198--208, 1983.
• 7: 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
• 8: James Heather , Steve Schneider, A decision procedure for the existence of a rank function, Journal of Computer Security, v.13 n.2, p.317-344, March 2005
• 9: C. Meadows. Applying formal methods to the analysis of a keymanagement protocol. Journal of Computer Security, 1(1), January 1992.
• 10: C. Meadows, Language generation and verification in the NRL protocol analyzer, Proceedings of the Ninth IEEE Computer Security Foundations Workshop, p.48, March 10-12, 1996
• 11: C. Meadows. The NRL Protocol Analyzer: An overview. The Journal of Logic Programming, 26(2):113--131, 1996.
• 12: Catherine Meadows, Invariant Generation Techniques in Cryptographic Protocol Analysis, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.159, July 03-05, 2000
• 13: Catherine Meadows , Paul Syverson , Iliano Cervesato, Formal specification and analysis of the group domain of interpretation protocol using NPATRL and the NRL protocol analyzer, Journal of Computer Security, v.12 n.6, p.893-931, December 2004
• 14: José Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, v.96 n.1, p.73-155, 6 April 1992
• 15: José Meseguer, Membership algebra as a logical framework for equational specification, Selected papers from the 12th International Workshop on Recent Trends in Algebraic Development Techniques, p.18-61, July 01, 1997
• 16: J. Meseguer and P. Thati. Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. In N. Martí-Oliet, editor, Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, 2004.
• 17: Jonathan Millen , Vitaly Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA [doi>10.1145/501983.502007]
• 18: 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]
• 19: S. Stubblebine and C. Meadows. Formal characterization and automated analysis of known-pair and chosen-text attacks. IEEE Journal on Selected Areas in Communications, 18(4):571--581, April 2000.
• 20: TeReSe, editor. Term Rewriting Systems. Cambridge University Press, Cambridge, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
      F.4.3 Formal Languages

General Terms:
Languages, Security, Theory, Verification

Keywords:
formal methods, protocol verification, rewriting logic