`PublicKeyCryptography` switches on public key encryption. Any atomic value owned by a principal can serve as his public/private key pair. The public portion of any principal’s key is accessible to Oscar through the $draws$ relation. The decryption constraint on line \[sk-constraint\] ensures that Oscar can decrypt a message only if he $owns$ the value representing the public/private key pair.

Nonces are encoded as composites with two fields, $seed$ and $id$. The field $id$ stores the identity of the principal to whom the nonce was issued. The predicate `NonceGenerator` says that, from Oscar’s point of view, the generator will issue a nonce labeled with Oscar’s identifier when presented with the input seed $x$.

Modelling Protocol Rules
------------------------

The models presented so far are a part of a generic Alloy framework developed for analyzing knowledge flows. This section describes the values and rules specific to the Needham-Schroeder protocol.

[ ]{}

module kf/needham\_schroeder

open kf/basicdeclarations

open kf/primitives/encryption

open kf/primitives/nonces

[**sig**]{} Identity [**extends**]{} AtomicValue {}\[identity\]

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

 [**all**]{} p : Principal | [**some**]{} p.owns & Identity && \[unique-ids\]

 Ciphertext.key [**in**]{} Identity } \[id-keys\]

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

 Encryptor(x,v) || Decryptor(x,v) ||

 NonceGenerator(x,v) }

[**pred**]{} ProtocolRules(x : [**set**]{} Value, 