Fault-preserving simplifying transformations for security protocols

Subtitle: Not Just the Needham Schroeder Public Key Protocol

Article type: Research Article

Authors: Hui, Mei Lin^a | Lowe, Gavin^{b; *}

Affiliations: [a] Communications and Electronic Security Group, GCHQ, P.O. Box 144, Cheltenham GL52 5UE, UK. E-mail: mlhui8@hotmail.com | [b] Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK. E-mail: gavin.lowe@comlab.ox.ac.uk

Correspondence: [*] Corresponding author.

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.

DOI: 10.3233/JCS-2001-91-202

Journal: Journal of Computer Security, vol. 9, no. 1-2, pp. 3-46, 2001