knowledge flow from $x$ to $v$.

Checking Security
-----------------

The predicate `SecurityAssumptions` in Model Excerpt \[security-theorem\] models our assumptions about the properties of cryptographic primitives and principals. We assume perfect public key cryptography (line \[perfect-pk-crypto\]) and the use of identifiers as public/private key pairs (line \[ids-as-keys\]).

The security property that the protocol should satisfy is given by the predicate `SecurityTheorem`. It states that Oscar’s maximal knowledge never contains two nonces, $nA$ and $nB$, such that $nB$ is generated by Bob in response to a protocol initialization message sent by Alice (a cipher containing Alice’s identity and one of her nonces). The assertion `Security` stitches the model together to stipulate that the security property should hold if Oscar obtains his maximal knowledge by applying the knowledge flow rules to the values he draws.

[ ]{}

[**pred**]{} SecurityAssumptions() {

 PerfectCryptography() && PublicKeyCryptography()\[perfect-pk-crypto\]

 IdentitiesAreKeys() } \[ids-as-keys\]

[**pred**]{} SecurityTheorem() {

 [**no**]{} [**disj**]{} Alice, Bob : HonestUser,

 nA, nB : Oscar.knows & Nonce |

  nA.id [**in**]{} Alice.owns && nB.id [**in**]{} Bob.owns &&

  ([**some**]{} c : Ciphertext | nB.seed = c &&

   c.key = nB.id &&

   c.plaintext = nA.id + nA) }

[**assert**]{} Security {

 InitialKnowledge() && FinalKnowledge() &&

 SecurityAssumptions() && ApplyRules() =&gt;

 SecurityTheorem() }

The 