Safe simplifying transformations for security protocols or not just the Needham Schroeder pubic key protocol
Mei Lin Hui, Gavin Lowe · 2003
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 safe 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 safe simplifying transformations, and use them in the analysis of a commercial protocol.