  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. In order for the techniques to prove useful, they need not only
to speed up the search, but should not violate completeness, so that failure to
find attacks still guarantees security. In this paper we describe some state
space reduction techniques that we have implemented in Maude-NPA. We also
provide completeness proofs, and experimental evaluations of their effect on
the performance of Maude-NPA.
