Paper Info
Title
A rewriting-based inference system for the NRL Protocol analyzer and its meta-logical properties
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. 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.
Year
DOI
Venue
2006
10.1016/j.tcs.2006.08.035
Theor. Comput. Sci.
Keywords
DocType
Volume
search algorithm,NPA inference system,NRL Protocol analyzer,invariant generation,cryptographic protocol,equational theory,precise formal specification,backwards reachability analysis method,meta-logical property,rewriting-based inference system,inference system,formal specification,grammar generation algorithm
Journal
367
Issue
ISSN
Citations 
1
Theoretical Computer Science
53
PageRank 
References 
Authors
1.70
29
3
Name
Order
Citations
PageRank
Santiago Escobar145227.87
Catherine Meadows292889.05
José Meseguer39533805.39