State Space Reduction in the Maude-NRL Protocol Analyzer

11 years 11 months ago
State Space Reduction in the Maude-NRL Protocol Analyzer
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, onetime 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 spe...
Santiago Escobar, Catherine Meadows, José M
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Authors Santiago Escobar, Catherine Meadows, José Meseguer
Comments (0)