TY - GEN
T1 - State space reduction in the maude-NRL protocol analyzer
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
N1 - Funding Information:
We would like to thank Antonio Gonzalez for his help in providing several protocol specifications in Maude-NPA. S. Escobar and S. Santiago have been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02 , and by Generalitat Valenciana PROMETEO2011/052 . J. Meseguer and S. Escobar have been partially supported by NSF grants CNS 09-04749 , and CCF 09-05584 .
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=57049108197&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=57049108197&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-88313-5_35
DO - 10.1007/978-3-540-88313-5_35
M3 - Conference contribution
AN - SCOPUS:57049108197
SN - 3540883126
SN - 9783540883128
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 548
EP - 562
BT - Computer Security - ESORICS 2008 - 13th European Symposium on Research in Computer Security, Proceedings
PB - Springer
T2 - 13th European Symposium on Research in Computer Security, ESORICS 2008
Y2 - 6 October 2008 through 8 October 2008
ER -