v : Value) { \[ns-rules\]

 v [**in**]{} Ciphertext && {

   (x : [**some**]{} Oscar.draws &&

   [**let**]{} text = v.plaintext, n = text & Nonce |

   \#text = 2 && [**one**]{} n && n.seed [**in**]{} AtomicValue &&

   n.id = text & Identity) ||

  (x : [**one**]{} Ciphertext && ([**some**]{} n : seed.x |

   \#x.plaintext = 2 && v.key [**in**]{} x.plaintext &&

   n.id = x.key &&

   v.plaintext = (x.plaintext - v.key) + n)) ||

  (x : [**one**]{} Ciphertext &&

   ([**some**]{} n : id.(x.key) & Nonce |

   \#x.plaintext = 2 && n [**in**]{} x.plaintext &&

   v.plaintext = x.plaintext - n)) }}

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

 [**all**]{} v : Value | [**let**]{} x = Oscar.learns.v |

  [**some**]{} x &lt;=&gt; PrimitiveRules(x, v) ||

   ProtocolRules(x, v) }

Principals’ identifiers are modelled as atomic values contained in the set $Identity$ (Model Excerpt \[protocol-rules\], line \[identity\]). Each principal $owns$ an $Identity$ (\[unique-ids\]), which also doubles as its owners’ public/private key pairs (\[id-keys\]).

The `ProtocolRules` predicate (line \[ns-rules\]) embeds the knowledge flow rules given by equations \[ns1\]-\[ns3\] into first-order logic. The predicate `ApplyRules` states that the $learns$ relation may map the set of values $x$ to the value $v$ if and only if the protocol or primitive rules define a 