Paper Info
Title
State space reduction in the Maude-NRL Protocol Analyzer.
Abstract
The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic properties that includes many crypto-systems of interest such as, for example, one-time pads and Diffie-Hellman. Maude-NPA, like the original NPA, looks for attacks by searching backwards from an insecure attack state, and assumes an unbounded number of sessions. Because of the unbounded number of sessions and the support for different equational theories, it is necessary to develop ways of reducing the search space and avoiding infinite search paths. As a result, we have developed a number of state space reduction techniques. In order for the techniques to prove useful, they need not only to speed up the search, but should not violate soundness so that failure to find attacks still guarantees security. In this paper we describe the state space reduction techniques we use. We also provide soundness proofs, and experimental evaluations of their effect on the performance of Maude-NPA.
Year
DOI
Venue
2008
10.1007/978-3-540-88313-5_35
Inf. Comput.
Keywords
DocType
Volume
state space reduction technique,state space reduction,different equational property,insecure attack state,equational reasoning,unbounded number,maude-nrl protocol analyzer,original npa,search space,different equational theory,infinite search path
Conference
238
ISSN
Citations 
PageRank 
0890-5401
11
0.53
References 
Authors
26
4
Name
Order
Citations
PageRank
Santiago Escobar145227.87
Catherine Meadows292889.05
José Meseguer39533805.39
S. Santiago4544.45