Alloy Analyzer generates a counterexample to the `Security` assertion (Figure \[lowe-attack\]) that is a knowledge flow representation of the parallel session attack discovered by Lowe [@Lowe96]. Alice uses $cipher0$ to initiate the protocol with Oscar, who extracts $nA$ and forwards it to Bob in $cipher1$. Thinking that he is authenticating with Alice, Bob responds with $cipher2$ which Oscar simply forwards to Alice. She completes the session with Oscar by sending him $nB$, which she believes is his nonce, in $cipher3$. Oscar now knows both $nA$ and $nB$, contrary to our claim.

![image](lowe-attack.eps)

Knowledge Flow Analysis
=======================

Knowledge flow analysis is based on a simple mathematical foundation. This section formalizes the ideas outlined in the discussion of knowledge flow basics. We describe how *communication rules* direct knowledge flows (\[kf-basic-defs\]), show that our treatment of primitives ensures a fixed pool of values (\[initial-knowledge\]), formulate the analysis problem in terms of Oscar’s knowledge flows (\[adversary\]), and present a small-model theorem which makes our analysis complete for a bounded number of parallel protocol sessions (\[kf-completeness\]).

Communicating Knowledge {#kf-basic-defs}
-----------------------

We denote the sets of all [*principals*]{} and [*values*]{} by $P$ and $V$. A subset of $P\times V$ is a [*state of knowledge*]{} drawn from 