for expressing the actions of principals, assumptions on intruders, and properties of cryptographic primitives. The dynamic behaviour of the protocol is described by an initial state of knowledge, and a collection of rules that dictate how knowledge may flow amongst principals. A state is given by a relation mapping principals to the values they know; the allowable knowledge flows can thus be succinctly described as a standard transition relation on knowledge states, written as a constraint.

This simple setup allows us to model a range of intruder capabilities and to detect replay, parallel session, type flaw, and binding attacks. We have applied it to both symmetric and public-key cryptography under the Dolev-Yao [@DY83] approach. The modeling framework itself is more general, however, and can be extended to include the properties of cryptographic primitives [@ComonShmatikov03IntruderDeductionsConstraintSolvingInsecurity; @ChevalierETAL03NPDecisionProcedureProtocolInsecurityXOR; @Shmatikov04ProtocolsProductsModularExponentiation; @MillenShmatikov04SymbolicProtocolAnalysisAbelianGroup] and an unbounded number of sessions with bounded messages [@ChevalierETAL03ExtendingDolevYaoIntruderAnalyzing].

This approach grew out of an effort to check a new cryptographic scheme [@Gassend03PhysicalRandomFunctions; @GassendETAL02ControlledPhysicalRandomFunctions]. Knowledge flow analysis described here was the final result of a series of incremental attempts at formalizing and checking the protocol using the Alloy language and tool. This process helped crystallize our intuitions, and drew out a number 