set $k_\sigma\subseteq k_0$ of cardinality $|Knowledge(k_\sigma)|\leq wm$. By Lemma \[arrow\], we can conclusively [*decide*]{} whether there is an attack which uses $w$ parallel protocol sessions by computing $$\left\{v\in g^*_{R,k_\sigma}(X_\sigma) : 
\begin{array}{l} \mbox{for }  
[\{o\}\times X_\sigma] \subseteq k_\sigma \subseteq k_0\\
\mbox{with } |Knowledge(k_\sigma)|\leq wm  
\end{array} 
\right\}. \label{comp}$$

Evaluation
==========

We have applied the theory developed in the previous section to check the security of the original [@NS78] and modified [@Lowe96] Needham-Schroeder Public Key Protocol, the Otway-Rees Mutual Authentication Protocol [@Otway-Rees87], and the bootstrapping and renewal protocols based on Controlled Physical Random Functions (CPUFs) [@Gassend03PhysicalRandomFunctions; @GassendETAL02ControlledPhysicalRandomFunctions].

The knowledge flows of the protocols were embedded into Alloy using the pattern presented in section \[example\]. The pattern is embodied in a general Alloy framework for knowledge flow analysis which includes definitions of basic concepts (Model Excerpt \[basicdeclarations\]), a library of primitives, and a model outline for specifying protocol rules and security theorems. For example, Model Excerpt \[primitives\] shows portions of Alloy modules that encode generic encryption/decryption and nonce generator primitives, and Model Excerpts \[protocol-rules\] and \[security-theorem\] comprise an instantiation of the modelling outline for the Needham-Schroeder protocol.

We have found that the Alloy framework and its associated tool support make the process of knowledge 