v.plaintext }

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

 [**some**]{} c : plaintext.v | x = (c.key + c) &&

  (PublicKeyCryptography() =&gt; \[sk-constraint\]

  c.key [**in**]{} Oscar.owns) }

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

 ([**all**]{} [**disj**]{} c1,c2: Ciphertext | c1.plaintext !=

  c2.plaintext || c1.key != c2.key)

 ([**all**]{} c : Ciphertext | c != c.key &&

  c != c.plaintext) }

module kf/primitives/nonces

open kf/basicdeclarations

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

 seed : Value,

 id : Value }

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

 v [**in**]{} Nonce && v.id [**in**]{} Oscar.owns && x = v.seed }

A $Ciphertext$ represents an encryption of a non-empty $plaintext$ (line \[plaintext\]) with a given $key$ (line \[key\]). The predicate `Encryptor` formalizes the encryption knowledge flow from Oscar’s perspective. It states that, in order to learn the cipher $v$ from the Encryptor, Oscar must provide the input $x$ consisting of the plaintext and the key associated with $v$. Similarly, the predicate `Decryptor` stipulates that Oscar can learn the plaintext $v$ after he presents the input $x$ consisting of an encryption of $v$ and the corresponding decryption key.

Note that this model of ciphers accommodates both public and symmetric key encryption. Symmetric key encryption is the default; invoking the predicate 