Abstract
Recent techniques for analyzing security protocols have tended to concentrate upon the small protocols that are typically found in the academic literature. However, there is a huge gulf between these and most large commercial protocols: the latter typically have many more fields, and much higher levels of nested encryption. As a result, existing techniques are difficult to apply directly to these large protocols.
In this paper we develop the notion of fault-preserving simplifying transformations: transformations that have the property of preserving insecurities; the effect of such transformations is that if we can verify the transformed protocol, then we will have verified the original protocol. We identify a number of such fault-preserving simplifying transformations, and use them in the analysis of a commercial protocol.