The first successful application of general-purpose model-checking tools to analysis of the security of cryptographic protocols was achieved by the second author [1]. This paper is important in that it seems to be the first exposition of this technique in an archival journal. It is reasonably self-contained, but the reader will have to look elsewhere for an introduction to the cryptographic protocol failure problem. Model-checking is most easily applied to secrecy goals and often assumes that keys are primitive, but this paper shows how it can handle authentication goals and the combination of two keys with a bitwise exclusive-or. The results of the FDR analysis are compared favorably with known prior analyses of the protocol.

The tool used is FDR, which accepts a machine-readable version of C.A. R. Hoare’s communicating sequential processes (CSP) process algebra, for system specifications. While CSP takes some effort to read, the authors have taken care to explain their use of it. Different versions of the protocol specification are used to uncover different attacks. The analysis also requires a model of the hostile network environment, containing an intruder who can intercept and fake messages. Security failures are encoded as special messages generated by the intruder. The tool runs automatically, exploring a finite part of the state space, covering about 4,000 states in about two minutes for this  example.  This approach is therefore a practical technique that helps to locate flaws in a protocol design, though failure to find an attack does not by itself prove that a protocol is secure.