Documentation

Cryptlib.Primitives.MKEM.Adapter

MKEM from a NIKE, an AEAD and a hash #

The only NIKE law used is NIKE.commutes.

ENCAPSULATE(keys, payload):
    eph            := GEN_KEYPAIR()
    secret_i       := HASH(DH(eph, keys[i]))            -- error if DH output is all zero
    msgKey         := RANDOM(32)
    envelope       := nonce ‖ AEAD_seal(msgKey, payload)
    dek_i          := nonce_i ‖ AEAD_seal(secret_i, msgKey)
    return eph, (eph_pub, [dek_i], envelope)

DECAPSULATE(sk, ct):
    secret         := HASH(DH(sk, ct.eph_pub))
    for dek in ct.deks: first one that opens under secret gives msgKey
    return open(msgKey, ct.envelope)

The pure functions take explicit randomness (Rand); the MKEM instance draws it from an Adapter.St seed stream, which must be unpredictable.

structure Cryptlib.Primitives.MKEM.Adapter.Base :

The three primitives, and the fact that lets a hash output be an AEAD key.

nike : NIKE.NIKE.NIKE
aead : Cipher.AEAD.AEAD
hash : Hash.Hash.Hash
digest_eq_key : self.hash.digestSize = self.aead.keySize

Instances For

structure Cryptlib.Primitives.MKEM.Adapter.Rand (S : Base) :

The sender's randomness, explicit so the pure construction is a function.

seed : Vector UInt8 32
msgKey : Vector UInt8 S.aead.keySize
envNonce : Vector UInt8 S.aead.nonceSize
dekNonces : List (Vector UInt8 S.aead.nonceSize)

Instances For

List lemmas #

theorem Cryptlib.Primitives.MKEM.Adapter.mapM_getElem {α β : Type} (f : α → Option β) (l : List α) (r : List β) :

List.mapM f l = some r → ∃ (h : r.length = l.length), ∀ (i : Nat) (hi : i < l.length), f l[i] = some r[i]

theorem Cryptlib.Primitives.MKEM.Adapter.findSome?_of_index {α β : Type} (f : α → Option β) (l : List α) (i : Nat) (hi : i < l.length) (x : β) :

(∀ (j : Nat) (hj : j < i), f l[j] = none) → f l[i] = some x → List.findSome? f l = some x

def Cryptlib.Primitives.MKEM.Adapter.Base.keyOfBytes (S : Base) (b : ByteArray) :

Option S.aead.Key

A raw byte string as an AEAD key, if it is the right length.

Equations

S.keyOfBytes b = if b.size = S.aead.keySize then some (S.aead.keyFromBytes (Cryptlib.Util.Bytes.toVecN S.aead.keySize b)) else none

Instances For

def Cryptlib.Primitives.MKEM.Adapter.Base.deriveKey (S : Base) (sk : S.nike.PrivateKey) (pk : { pk : S.nike.PublicKey // S.nike.Safe pk }) :

Option S.aead.Key

The hash of the Diffie-Hellman output; none if the output is all zero.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Cryptlib.Primitives.MKEM.Adapter.Base.deriveKey_comm (S : Base) (sk₁ sk₂ : S.nike.PrivateKey) :

S.deriveKey sk₁ ⟨S.nike.derivePublicKey sk₂, ⋯⟩ = S.deriveKey sk₂ ⟨S.nike.derivePublicKey sk₁, ⋯⟩

Both parties derive the same key.

Sealing under a key: nonce, then AEAD ciphertext #

def Cryptlib.Primitives.MKEM.Adapter.Base.sealUnder (S : Base) (key : S.aead.Key) (nonce : Vector UInt8 S.aead.nonceSize) (pt : ByteArray) :

Equations

S.sealUnder key nonce pt = Cryptlib.Util.Bytes.ofVector nonce ++ S.aead.encrypt key nonce ByteArray.empty pt

Instances For

def Cryptlib.Primitives.MKEM.Adapter.Base.unsealUnder (S : Base) (key : S.aead.Key) (ct : ByteArray) :

Option ByteArray

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Cryptlib.Primitives.MKEM.Adapter.Base.get!_eq_getElem (x : ByteArray) (i : Nat) (h : i < x.size) :

x.get! i = x[i]

theorem Cryptlib.Primitives.MKEM.Adapter.Base.toVecN_append {n : Nat} (v : Vector UInt8 n) (c : ByteArray) :

Util.Bytes.toVecN n (Util.Bytes.ofVector v ++ c) = v

theorem Cryptlib.Primitives.MKEM.Adapter.Base.unsealUnder_sealUnder (S : Base) (key : S.aead.Key) (nonce : Vector UInt8 S.aead.nonceSize) (pt : ByteArray) :

S.unsealUnder key (S.sealUnder key nonce pt) = some pt

What was sealed opens.

theorem Cryptlib.Primitives.MKEM.Adapter.Base.size_sealUnder (S : Base) (key : S.aead.Key) (nonce : Vector UInt8 S.aead.nonceSize) (pt : ByteArray) :

(S.sealUnder key nonce pt).size = S.aead.nonceSize + (pt.size + S.aead.tagSize)

The construction, with explicit randomness #

def Cryptlib.Primitives.MKEM.Adapter.Base.encapsulateP (S : Base) (rand : Rand S) (keys : List { pk : S.nike.PublicKey // S.nike.Safe pk }) (payload : ByteArray) :

Option (S.nike.PrivateKey × MKEM.Ciphertext S.nike.PublicKey)

Encrypt payload to every recipient. none if any Diffie-Hellman output is degenerate.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cryptlib.Primitives.MKEM.Adapter.Base.decapsulateP (S : Base) (sk : S.nike.PrivateKey) (ct : MKEM.Ciphertext S.nike.PublicKey) :

Option ByteArray

Open the first DEK that opens under the shared key, then the envelope.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Cryptlib.Primitives.MKEM.Adapter.Base.encapsulateP_ephPub (S : Base) (rand : Rand S) (keys : List { pk : S.nike.PublicKey // S.nike.Safe pk }) (payload : ByteArray) (eph : S.nike.PrivateKey) (ct : MKEM.Ciphertext S.nike.PublicKey) (h : S.encapsulateP rand keys payload = some (eph, ct)) :

ct.ephPub = S.nike.derivePublicKey eph

theorem Cryptlib.Primitives.MKEM.Adapter.Base.encapsulateP_spec (S : Base) (rand : Rand S) (keys : List { pk : S.nike.PublicKey // S.nike.Safe pk }) (payload : ByteArray) (eph : S.nike.PrivateKey) (ct : MKEM.Ciphertext S.nike.PublicKey) (h : S.encapsulateP rand keys payload = some (eph, ct)) :

eph = S.nike.privateKeyFromSeed rand.seed ∧ ∃ (secrets : List S.aead.Key), List.mapM (S.deriveKey eph) keys = some secrets ∧ ct = { ephPub := S.nike.derivePublicKey eph, deks := List.map (fun (p : S.aead.Key × Vector UInt8 S.aead.nonceSize) => S.sealUnder p.fst p.snd (Util.Bytes.ofVector rand.msgKey)) (secrets.zip rand.dekNonces), envelope := S.sealUnder (S.aead.keyFromBytes rand.msgKey) rand.envNonce payload }

Unpack a successful encapsulation.

theorem Cryptlib.Primitives.MKEM.Adapter.Base.encapsulateP_shape (S : Base) (rand : Rand S) (keys : List { pk : S.nike.PublicKey // S.nike.Safe pk }) (payload : ByteArray) (eph : S.nike.PrivateKey) (ct : MKEM.Ciphertext S.nike.PublicKey) (hlen : rand.dekNonces.length = keys.length) (h : S.encapsulateP rand keys payload = some (eph, ct)) :

ct.deks.length = keys.length ∧ (∀ (d : ByteArray), d ∈ ct.deks → d.size = S.aead.nonceSize + S.aead.keySize + S.aead.tagSize) ∧ ct.envelope.size = payload.size + (S.aead.nonceSize + S.aead.tagSize)

One nonce + key + tag-byte DEK per recipient, and an envelope nonce + tag longer than the payload.

theorem Cryptlib.Primitives.MKEM.Adapter.Base.decapsulateP_forRecipient (S : Base) (rand : Rand S) (keys : List { pk : S.nike.PublicKey // S.nike.Safe pk }) (payload : ByteArray) (eph : S.nike.PrivateKey) (ct : MKEM.Ciphertext S.nike.PublicKey) (hlen : rand.dekNonces.length = keys.length) (henc : S.encapsulateP rand keys payload = some (eph, ct)) (i : Nat) (hi : i < keys.length) (sk : S.nike.PrivateKey) (hsk : keys[i] = ⟨S.nike.derivePublicKey sk, ⋯⟩) :

S.decapsulateP sk (ct.forRecipient i) = some payload

Recipient i recovers the payload from the ciphertext carrying only its DEK.

theorem Cryptlib.Primitives.MKEM.Adapter.Base.decapsulateP_encapsulateP_full (S : Base) (rand : Rand S) (keys : List { pk : S.nike.PublicKey // S.nike.Safe pk }) (payload : ByteArray) (eph : S.nike.PrivateKey) (ct : MKEM.Ciphertext S.nike.PublicKey) (hlen : rand.dekNonces.length = keys.length) (henc : S.encapsulateP rand keys payload = some (eph, ct)) (i : Nat) (hi : i < keys.length) (sk : S.nike.PrivateKey) (hsk : keys[i] = ⟨S.nike.derivePublicKey sk, ⋯⟩) (hcross : ∀ (k : S.aead.Key), S.deriveKey eph keys[i] = some k → ∀ (j : Nat), j < i → ∀ (hj' : j < ct.deks.length), S.unsealUnder k ct.deks[j] = none) :

S.decapsulateP sk ct = some payload

Recipient i recovers the payload from the full ciphertext, provided no earlier DEK opens under its key (hcross).

Replies #

def Cryptlib.Primitives.MKEM.Adapter.Base.envelopeReplyP (S : Base) (sk : S.nike.PrivateKey) (pub : { pk : S.nike.PublicKey // S.nike.Safe pk }) (nonce : Vector UInt8 S.aead.nonceSize) (pt : ByteArray) :

Option ByteArray

Equations

S.envelopeReplyP sk pub nonce pt = do let k ← S.deriveKey sk pub pure (S.sealUnder k nonce pt)

Instances For

def Cryptlib.Primitives.MKEM.Adapter.Base.decryptEnvelopeP (S : Base) (sk : S.nike.PrivateKey) (pub : { pk : S.nike.PublicKey // S.nike.Safe pk }) (envelope : ByteArray) :

Option ByteArray

Equations

S.decryptEnvelopeP sk pub envelope = do let k ← S.deriveKey sk pub S.unsealUnder k envelope

Instances For

theorem Cryptlib.Primitives.MKEM.Adapter.Base.decryptEnvelopeP_envelopeReplyP (S : Base) (eph sk : S.nike.PrivateKey) (nonce : Vector UInt8 S.aead.nonceSize) (pt env : ByteArray) (h : S.envelopeReplyP sk ⟨S.nike.derivePublicKey eph, ⋯⟩ nonce pt = some env) :

S.decryptEnvelopeP eph ⟨S.nike.derivePublicKey sk, ⋯⟩ env = some pt

The `MKEM` instance #

def Cryptlib.Primitives.MKEM.Adapter.counterBytes (i : Nat) :

i as 8 little-endian bytes.

Equations

Cryptlib.Primitives.MKEM.Adapter.counterBytes i = { data := Array.map (fun (k : Nat) => (i >>> (8 * k)).toUInt8) (Array.range 8) }

Instances For

def Cryptlib.Primitives.MKEM.Adapter.randOf (S : Base) (i : Nat) (str : Nat → KEM.Adapter.Bytes32) (n : Nat) :

Randomness for encapsulating to n recipients, from stream position i: ephemeral seed, message key, envelope nonce, then one nonce per recipient.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Cryptlib.Primitives.MKEM.Adapter.randOf_dekNonces_length (S : Base) (i : Nat) (str : Nat → KEM.Adapter.Bytes32) (n : Nat) :

(randOf S i str n).dekNonces.length = n

def Cryptlib.Primitives.MKEM.Adapter.encapM (S : Base) (keys : List { pk : S.nike.PublicKey // S.nike.Safe pk }) (payload : ByteArray) :

EStateM MKEM.MKEMError KEM.Adapter.St (S.nike.PrivateKey × MKEM.Ciphertext S.nike.PublicKey)

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Cryptlib.Primitives.MKEM.Adapter.encapM_ok (S : Base) (keys : List { pk : S.nike.PublicKey // S.nike.Safe pk }) (payload : ByteArray) (s : KEM.Adapter.St) (r : S.nike.PrivateKey × MKEM.Ciphertext S.nike.PublicKey) (s' : KEM.Adapter.St) (h : encapM S keys payload s = EStateM.Result.ok r s') :

∃ (rand : Rand S), rand.dekNonces.length = keys.length ∧ S.encapsulateP rand keys payload = some r

def Cryptlib.Primitives.MKEM.Adapter.decapE (S : Base) (sk : S.nike.PrivateKey) (ct : MKEM.Ciphertext S.nike.PublicKey) :

Except MKEM.MKEMError ByteArray

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cryptlib.Primitives.MKEM.Adapter.replyM (S : Base) (sk : S.nike.PrivateKey) (pub : { pk : S.nike.PublicKey // S.nike.Safe pk }) (pt : ByteArray) :

EStateM MKEM.MKEMError KEM.Adapter.St ByteArray

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cryptlib.Primitives.MKEM.Adapter.decryptE (S : Base) (sk : S.nike.PrivateKey) (pub : { pk : S.nike.PublicKey // S.nike.Safe pk }) (env : ByteArray) :

Except MKEM.MKEMError ByteArray

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cryptlib.Primitives.MKEM.Adapter.generateM (S : Base) :

EStateM MKEM.MKEMError KEM.Adapter.St (S.nike.PublicKey × S.nike.PrivateKey)

Equations

Cryptlib.Primitives.MKEM.Adapter.generateM S (i, str) = EStateM.Result.ok (S.nike.derivePublicKey (S.nike.privateKeyFromSeed (str i)), S.nike.privateKeyFromSeed (str i)) (i + 1, str)

Instances For

def Cryptlib.Primitives.MKEM.Adapter.ofBase (S : Base) :

MKEM over the given NIKE, AEAD and hash.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cryptlib.Primitives.MKEM.Adapter.mkemOfNike (nike : NIKE.NIKE.NIKE) (aead : Cipher.AEAD.AEAD) (hash : Hash.Hash.Hash) (h : hash.digestSize = aead.keySize) :

MKEM over a NIKE, an AEAD, and a hash whose digest is an AEAD key.

Equations

Cryptlib.Primitives.MKEM.Adapter.mkemOfNike nike aead hash h = Cryptlib.Primitives.MKEM.Adapter.ofBase { nike := nike, aead := aead, hash := hash, digest_eq_key := h }

Instances For