Encoding Basic Entities and Relations
-------------------------------------

The basic components of a knowledge flow model are the sets $Principal$ and $Value$, and the relations $draws$, $learns$, and $knows$ (Model Excerpt \[basicdeclarations\]).

[ ]{}

module kf/basicdeclarations

[**abstract sig**]{} Value {} \[Value\]

[**sig**]{} CompositeValue [**extends**]{} Value {} \[CompositeValue\]

[**sig**]{} AtomicValue [**extends**]{} Value {} \[AtomicValue\]

[**abstract sig**]{} Principal { \[Principal\]

  draws: [**set**]{} Value, \[draws\]

  owns: [**set**]{} draws \[owns\]

}{ [**no**]{} owns & (Principal - this).@owns } \[owns-constraint\]

[**sig**]{} HonestUser [**extends**]{} Principal { \[HonestUser\]

}{ draws = Value } \[draws-constraint\]

[**one sig**]{} Oscar [**extends**]{} Principal { \[Oscar\]

  knows: [**set**]{} Value, \[knows\]

  learns: knows-&gt;knows \[learns\]

}{ [**no**]{} `^`learns & iden } \[learns-constraint\]

[**pred**]{} InitialKnowledge() { \[InitialKnowledge\]

 no CompositeValue & Oscar.draws }

[**pred**]{} FinalKnowledge() { \[FinalKnowledge\]

 [**all**]{} v: Value |

  v [**in**]{} (Oscar.draws).\*(Oscar.learns) [**iff**]{}

  v [**in**]{} Oscar.knows }

The set $Principal$ includes all principals in a protocol – the legitimate protocol participants, represented by the subset $HonestUser$, and the intruders, represented by $Oscar$. The set $Value$ models the fixed pool of knowledge on which a protocol operates. We distinguish between $AtomicValue$s, which are uninterpreted, and $CompositeValue$s, which may consist of other values and are learned by communicating with cryptographic primitives. In the example from Figure \[ns-diagram\], Alice 