A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties

Santiago Escobar, Catherine Meadows, José Meseguer

Research output: Contribution to journalArticlepeer-review


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. One of the most interesting of its features is that it can be used to reason about security in face of attempted attacks on low-level algebraic properties of the functions used in a protocol. Indeed, it has been used successfully to either reproduce or discover a number of such attacks. In this paper we give for the first time a precise formal specification of the main features of the NPA inference system: its grammar-based techniques for invariant generation and its backwards reachability analysis method. 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. We then use this formalization to prove some important meta-logical properties about the NPA inference system, including the soundness and completeness of the search algorithm and soundness of the grammar generation algorithm. The formalization and soundness and completeness theorems not only provide also a better understanding of the NPA as it currently operates, but provide a modular basis which can be used as a starting point for increasing the types of equational theories it can handle.

Original languageEnglish (US)
Pages (from-to)162-202
Number of pages41
JournalTheoretical Computer Science
Issue number1-2
StatePublished - Nov 24 2006

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties'. Together they form a unique fingerprint.

Cite this