and Bob are members of $HonestUser$; $Value$ consists of the union of values enclosed in the boxes ‘Alice’ and ‘Bob’; the identifiers $A$ and $B$ are $AtomicValue$s, and the ciphers are $CompositeValue$s.

The relation $draws$ (line \[draws\]) maps each principal to the set of values known by that principal at the beginning of the protocol. For example, both Alice and Bob draw Alice’s identity $A$ at the start of the protocol session shown in Figure \[ns-diagram\]. The declaration of $owns$ (line \[owns\]) together with the constraint on line \[owns-constraint\] relate a principal to the set of drawn values which uniquely identify him. Bob, for instance, $owns$ his identity, $B$, even though both he and Alice draw it.

The field $knows$ (line \[knows\]) defines the set of all values that Oscar can learn by using the knowledge flows available to him; this includes the knowledge obtainable from both the protocol rules and the cryptographic primitives. The acyclic relation $learns$ (lines \[learns\]-\[learns-constraint\]) encodes the partial ordering on Oscar’s maximal knowledge, enforced by the flows from which the knowledge was acquired. For example, the protocol rule \[ns2\] specifies that Oscar learns $E_{PK(A)}(N_A, N_B)$ from $E_{PK(B)}(A, N_A)$. Hence, [Oscar.knows]{} contains both ciphers and [Oscar.learns]{} 