MultiRecipientHybrid from a KEM, an AEAD and a hash

ENCAPSULATE(keys, payload):
    for pk in keys: ct_i, ss_i := KEM_ENCAP(pk)        -- independent per recipient
    secret_i       := HASH(ss_i)
    msgKey         := RANDOM(32)
    envelope       := nonce ‖ AEAD_seal(msgKey, payload)
    dek_i          := nonce_i ‖ AEAD_seal(secret_i, msgKey)
    return [secret_i], ([ct_i], [dek_i], envelope)

DECAPSULATE(sk, ct):                                    -- ct already filtered to one recipient
    ss             := KEM_DECAP(sk, ct.kemCiphertexts[0])
    secret         := HASH(ss)
    msgKey         := AEAD_open(secret, ct.deks[0])
    return secret, AEAD_open(msgKey, ct.envelope)

The pure functions take explicit randomness (Rand); the instance draws it from a KEM.Adapter.St seed stream, which must be unpredictable. Reliable requires KEM.Reliable for every KEM seed the stream can yield.

structure Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base : Type 1

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

• kem : KEM.KEM.KEM
• aead : Cipher.AEAD.AEAD
• hash : Hash.Hash.Hash
• digest_eq_key : self.hash.digestSize = self.aead.keySize

structure Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Rand (S : Base) : Type

The sender's randomness, with one KEM seed per recipient.

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

def Cryptlib.Primitives.MultiRecipientHybrid.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

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.deriveKeyBytes (S : Base) (ss : S.kem.Plaintext) : ByteArray

The derived key: the hashed KEM shared secret.

Equations

• S.deriveKeyBytes ss = Cryptlib.Util.Bytes.ofVector (S.hash.hash (Cryptlib.Util.Bytes.ofVector (S.kem.encodePlaintext ss)))

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.deriveKeyAead (S : Base) (ss : S.kem.Plaintext) : S.aead.Key

The derived key as an AEAD.Key.

Equations

• S.deriveKeyAead ss = S.aead.keyFromBytes (Vector.cast ⋯ (S.hash.hash (Cryptlib.Util.Bytes.ofVector (S.kem.encodePlaintext ss))))

Sealing under a key: nonce, then AEAD ciphertext

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.get!_eq_getElem (x : ByteArray) (i : Nat) (h : i < x.size) : x.get! i = x[i]

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

Equations

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

def Cryptlib.Primitives.MultiRecipientHybrid.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.

theorem Cryptlib.Primitives.MultiRecipientHybrid.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.MultiRecipientHybrid.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

theorem Cryptlib.Primitives.MultiRecipientHybrid.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)

One KEM encapsulation, wrapped as Option

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.encapPair (S : Base) (pk : S.kem.PublicKey) (seed : Vector UInt8 32) : Option (S.kem.Ciphertext × S.kem.Plaintext)

kem.encap from a seed-derived state, none on error.

Equations

• S.encapPair pk seed = match S.kem.encap pk (S.kem.stateFromSeed seed) with | EStateM.Result.ok r a => some r | EStateM.Result.error a a_1 => none

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.RandReliable (S : Base) (rand : Rand S) : Prop

Every KEM seed a Rand draws lands on a Reliable state.

Equations

• S.RandReliable rand = ∀ (seed : Vector UInt8 32), seed ∈ rand.kemSeeds → S.kem.Reliable (S.kem.stateFromSeed seed)

The construction, with explicit randomness

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.encapsulateP (S : Base) (rand : Rand S) (keys : List S.kem.PublicKey) (payload : ByteArray) : Option (List ByteArray × MultiRecipientHybrid.Ciphertext S.kem.Ciphertext)

Encrypt payload to every recipient. none if any recipient's KEM.encap fails.

Equations

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

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.decapsulateP (S : Base) (sk : S.kem.PrivateKey) (ct : MultiRecipientHybrid.Ciphertext S.kem.Ciphertext) : Option (ByteArray × ByteArray)

Open a single-recipient ciphertext: decapsulate, open the DEK, then the envelope.

Equations

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

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.encapsulateP_spec (S : Base) (rand : Rand S) (keys : List S.kem.PublicKey) (payload : ByteArray) (derivedKeys : List ByteArray) (ct : MultiRecipientHybrid.Ciphertext S.kem.Ciphertext) (h : S.encapsulateP rand keys payload = some (derivedKeys, ct)) : ∃ (pairs : List (S.kem.Ciphertext × S.kem.Plaintext)), List.mapM (fun (p : S.kem.PublicKey × Vector UInt8 32) => S.encapPair p.fst p.snd) (keys.zip rand.kemSeeds) = some pairs ∧ derivedKeys = List.map (fun (p : S.kem.Ciphertext × S.kem.Plaintext) => S.deriveKeyBytes p.snd) pairs ∧ ct = { kemCiphertexts := List.map Prod.fst pairs, deks := List.map (fun (p : S.aead.Key × Vector UInt8 S.aead.nonceSize) => S.sealUnder p.fst p.snd (Util.Bytes.ofVector rand.msgKey)) ((List.map (fun (p : S.kem.Ciphertext × S.kem.Plaintext) => S.deriveKeyAead p.snd) pairs).zip rand.dekNonces), envelope := S.sealUnder (S.aead.keyFromBytes rand.msgKey) rand.envNonce payload }

Unpack a successful encapsulation.

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.encapsulateP_shape (S : Base) (rand : Rand S) (keys : List S.kem.PublicKey) (payload : ByteArray) (hlen : rand.kemSeeds.length = keys.length) (hlen' : rand.dekNonces.length = keys.length) (derivedKeys : List ByteArray) (ct : MultiRecipientHybrid.Ciphertext S.kem.Ciphertext) (h : S.encapsulateP rand keys payload = some (derivedKeys, ct)) : ct.kemCiphertexts.length = keys.length ∧ ct.deks.length = keys.length ∧ derivedKeys.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 KEM ciphertext, one nonce + key + tag-byte DEK and one derived key per recipient, and an envelope nonce + tag longer than the payload.

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.decapsulateP_forRecipient (S : Base) (rand : Rand S) (hrel : S.RandReliable rand) (keys : List S.kem.PublicKey) (payload : ByteArray) (hlen : rand.kemSeeds.length = keys.length) (hlen' : rand.dekNonces.length = keys.length) (derivedKeys : List ByteArray) (ct : MultiRecipientHybrid.Ciphertext S.kem.Ciphertext) (henc : S.encapsulateP rand keys payload = some (derivedKeys, ct)) (i : Nat) (hi : i < keys.length) (sk : S.kem.PrivateKey) (hsk : keys[i] = S.kem.derivePublicKey sk) (k : ByteArray) (hk : derivedKeys[i]? = some k) : S.decapsulateP sk (ct.forRecipient i) = some (k, payload)

If its KEM seed is Reliable, recipient i recovers the payload and its derived key from the ciphertext carrying only its KEM ciphertext and DEK.

Replies

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.envelopeReplyP (S : Base) (key : ByteArray) (nonce : Vector UInt8 S.aead.nonceSize) (pt : ByteArray) : Option ByteArray

Equations

• S.envelopeReplyP key nonce pt = do let k ← S.keyOfBytes key pure (S.sealUnder k nonce pt)

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.decryptEnvelopeP (S : Base) (key envelope : ByteArray) : Option ByteArray

Equations

• S.decryptEnvelopeP key envelope = do let k ← S.keyOfBytes key S.unsealUnder k envelope

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Base.decryptEnvelopeP_envelopeReplyP (S : Base) (key : ByteArray) (nonce : Vector UInt8 S.aead.nonceSize) (pt env : ByteArray) (h : S.envelopeReplyP key nonce pt = some env) : S.decryptEnvelopeP key env = some pt

The MultiRecipientHybrid instance

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

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

Equations

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

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.randOf_dekNonces_length (S : Base) (i : Nat) (str : Nat → KEM.Adapter.Bytes32) (n : Nat) : (randOf S i str n).dekNonces.length = n

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.randOf_kemSeeds_length (S : Base) (i : Nat) (str : Nat → KEM.Adapter.Bytes32) (n : Nat) : (randOf S i str n).kemSeeds.length = n

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Reliable (S : Base) (s : KEM.Adapter.St) : Prop

Every seed in the stream gives a Reliable KEM state.

Equations

• Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Reliable S s = ∀ (j : Nat), S.kem.Reliable (S.kem.stateFromSeed (s.snd j))

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.Reliable_randReliable (S : Base) (s : KEM.Adapter.St) (h : Reliable S s) (n : Nat) : S.RandReliable (randOf S s.fst s.snd n)

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.encapM (S : Base) (keys : List S.kem.PublicKey) (payload : ByteArray) : EStateM MultiRecipientHybrid.MultiRecipientHybridError KEM.Adapter.St (List ByteArray × MultiRecipientHybrid.Ciphertext S.kem.Ciphertext)

Equations

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

theorem Cryptlib.Primitives.MultiRecipientHybrid.Adapter.encapM_ok (S : Base) (keys : List S.kem.PublicKey) (payload : ByteArray) (s : KEM.Adapter.St) (r : List ByteArray × MultiRecipientHybrid.Ciphertext S.kem.Ciphertext) (s' : KEM.Adapter.St) (h : encapM S keys payload s = EStateM.Result.ok r s') : ∃ (rand : Rand S), rand.kemSeeds.length = keys.length ∧ rand.dekNonces.length = keys.length ∧ (Reliable S s → S.RandReliable rand) ∧ S.encapsulateP rand keys payload = some r

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.decapE (S : Base) (sk : S.kem.PrivateKey) (ct : MultiRecipientHybrid.Ciphertext S.kem.Ciphertext) : Except MultiRecipientHybrid.MultiRecipientHybridError (ByteArray × ByteArray)

Equations

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

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.replyM (S : Base) (key pt : ByteArray) : EStateM MultiRecipientHybrid.MultiRecipientHybridError KEM.Adapter.St ByteArray

Equations

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

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.decryptE (S : Base) (key env : ByteArray) : Except MultiRecipientHybrid.MultiRecipientHybridError ByteArray

Equations

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

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.generateM (S : Base) : EStateM MultiRecipientHybrid.MultiRecipientHybridError KEM.Adapter.St (S.kem.PublicKey × S.kem.PrivateKey)

Equations

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

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

MultiRecipientHybrid over the given KEM, AEAD and hash.

Equations

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

def Cryptlib.Primitives.MultiRecipientHybrid.Adapter.hybridOfKEM (kem : KEM.KEM.KEM) (aead : Cipher.AEAD.AEAD) (hash : Hash.Hash.Hash) (h : hash.digestSize = aead.keySize) : MultiRecipientHybrid.MultiRecipientHybrid

MultiRecipientHybrid over a KEM, an AEAD, and a hash whose digest is an AEAD key.

Equations

• Cryptlib.Primitives.MultiRecipientHybrid.Adapter.hybridOfKEM kem aead hash h = Cryptlib.Primitives.MultiRecipientHybrid.Adapter.ofBase { kem := kem, aead := aead, hash := hash, digest_eq_key := h }