includes the mapping $$\langle E_{PK(B)}(A, N_A),  E_{PK(A)}(N_A, N_B)\rangle.$$

The predicate `InitialKnowledge` states that Oscar may not draw any composite values. Rather, he must learn them from the protocol rules or the primitives. The predicate `FinalKnowledge` specifies that Oscar’s maximal knowledge contains a value $v$ if and only if Oscar draws $v$ or he learns it from a knowledge flow originating in his initial knowledge.

Modelling Cryptographic Primitives
----------------------------------

The Needham-Schroeder protocol requires the use of cryptographic primitives to encrypt/decrypt messages and generate nonces. Our encoding of the knowledge flows and values associated with these primitives is shown in Model Excerpt \[primitives\]. Note that we do not explicitly model primitives as principals. Instead, we define the pools of values drawn by the primitives as signatures and encode their input/output behavior as predicates. For example, the initial knowledge of $Encryptor$ is given by the set $Ciphertext$, and $Encryptor$’s operation is encoded in the predicates `Encryptor` and `Decryptor`.

[ ]{}

module kf/primitives/encryption

open kf/basicdeclarations

[**sig**]{} Ciphertext [**extends**]{} CompositeValue {

 plaintext: [**some**]{} Value, \[plaintext\]

 key: Value } \[key\]

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

 Ciphertext.key [**in**]{} Principal.owns & AtomicValue }

[**pred**]{} Encryptor(x: [**set**]{} Value, v : Value) {

 v [**in**]{} Ciphertext && x = v.key + 