Fault-preserving simplifying transformations for security protocols
Mei Lin Hui, Gavin Lowe · Journal of Computer Security · 2001
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 le vels 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.