} c = E_{PK(p')}(I(p),v). \nonumber\end{aligned}$$ The variable $V$ denotes the set of all values, or the fixed pool of knowledge. Note that our formalization constrains the seed of Bob’s nonce to be Alice’s initialization message. This is needed to establish that Bob’s nonce was generated in the context of the protocol session started by Alice with $E_{PK(B)}(A, N_A)$. The resulting correspondence between the nonces prevents our analysis from sounding false alarms when Oscar legitimately obtains two nonces from Alice and Bob by running a valid protocol session with each.

Oscar learns the final message, $E_{PK(B)}(N_B)$, as a consequence of knowing $E_{PK(A)}(N_A, N_B)$. Formally, $$\begin{aligned}
 \forall_{p\in \{a,b\}, p'\in \{a,b\}\cup O, v\in V} \nonumber \\ 
 \left [\{E_{PK(p)}(N(\epsilon,I(p)),v))\}  \rightarrow E_{PK(p')}(v) \right].\label{ns3}\end{aligned}$$

Example
=======

The Needham-Schroeder protocol is vulnerable to a parallel session attack discovered by Gavin Lowe [@Lowe96]. This section presents a knowledge flow analysis of the protocol that reproduces Lowe’s results, and gives a flavor of the expressiveness and simplicity of our method. We have encoded the knowledge flows in the Alloy modelling language [@Jackson02AlloyTOSEM] and used the Alloy Analyzer [@Jackson00AutomatingFOL] to find the attack. However, the modelling pattern presented here is applicable to any first-order logic with relations and transitive closure.

