of important assumptions. The final analysis, although only performed over a finite domain, actually establishes the correctness of the protocol for unbounded instantiations because of a special property of this protocol. The Alloy models developed for this case study were generalized into a simple framework that was subsequently applied to some standard protocols, such as Needham-Schroeder [@NS78] and Otway-Rees [@Otway-Rees87].

The contributions of this paper are:

[.]{}

the knowledge flow formalism, which characterizes the dynamic behaviour of a cryptographic protocol in terms of the increasing knowledge of the principals, avoiding the need to impose an explicit ordering on messages;

a realization in the Alloy modelling language as a generic framework with a library of primitives that can be easily instantiated for a variety of protocols;

soundness and completeness results that guarantee that (1) any counterexample generated by the analyzer to a security theorem is legitimate, and not an artifact of the modelling framework, formalism or analysis; and (2) that if a counterexample exists involving any number of message exchanges and any number of steps, it will be found, so long as the number of parallel sessions is within a prescribed bound;

case study applications of the approach to two well-known 