Security preserving KEM combiner

splitPRF is the PRF-then-XOR core function of Giacon, Heuer & Poettering ("KEM Combiners", https://eprint.iacr.org/2018/024.pdf, Lemma 8), for any number of KEMs. With BLAKE2b-256 as the PRF:

  key_i  := BLAKE2b-256(unkeyed)(ss_i)
  hash_i := BLAKE2b-256(
               key = key_i,
               msg = "splitprf-v1" || u32be(n) ||
                     u32be(len(cct_1)) || cct_1 ||
                     ...                ||
                     u32be(len(cct_n)) || cct_n
           )
  return hash_1 XOR hash_2 XOR ... XOR hash_n

Each shared secret keys the PRF, and every component hash binds the full, unambiguously encoded ciphertext vector. By Theorem 1 of the paper the combined KEM is IND-CCA2 if at least one component is.

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.Combiner.Bytes32 : Type

Equations

• Cryptlib.Primitives.KEM.Combiner.Bytes32 = Vector UInt8 32

def Cryptlib.Primitives.KEM.Combiner.toBytes {n : Nat} (v : Vector UInt8 n) : ByteArray

Equations

• Cryptlib.Primitives.KEM.Combiner.toBytes v = { data := v.toArray }

def Cryptlib.Primitives.KEM.Combiner.zero32 : Bytes32

Equations

• Cryptlib.Primitives.KEM.Combiner.zero32 = Vector.replicate 32 0

def Cryptlib.Primitives.KEM.Combiner.xorBytes (a b : Bytes32) : Bytes32

Equations

• Cryptlib.Primitives.KEM.Combiner.xorBytes a b = Vector.ofFn fun (i : Fin 32) => a[i] ^^^ b[i]

theorem Cryptlib.Primitives.KEM.Combiner.zero_xorBytes (a : Bytes32) : xorBytes zero32 a = a

theorem Cryptlib.Primitives.KEM.Combiner.xorBytes_zero (a : Bytes32) : xorBytes a zero32 = a

theorem Cryptlib.Primitives.KEM.Combiner.xorBytes_comm (a b : Bytes32) : xorBytes a b = xorBytes b a

theorem Cryptlib.Primitives.KEM.Combiner.xorBytes_self (a : Bytes32) : xorBytes a a = zero32

theorem Cryptlib.Primitives.KEM.Combiner.xorBytes_assoc (a b c : Bytes32) : xorBytes (xorBytes a b) c = xorBytes a (xorBytes b c)

Split PRF

def Cryptlib.Primitives.KEM.Combiner.splitPRFLabel : String

Domain-separation tag.

Equations

• Cryptlib.Primitives.KEM.Combiner.splitPRFLabel = "splitprf-v1"

def Cryptlib.Primitives.KEM.Combiner.splitPRFLabelBytes : ByteArray

Equations

• Cryptlib.Primitives.KEM.Combiner.splitPRFLabelBytes = Cryptlib.Primitives.KEM.Combiner.splitPRFLabel.toUTF8

def Cryptlib.Primitives.KEM.Combiner.splitPRFOutputSize : Nat

Length in bytes of the value splitPRF returns.

Equations

• Cryptlib.Primitives.KEM.Combiner.splitPRFOutputSize = 32

def Cryptlib.Primitives.KEM.Combiner.u32be (v : UInt32) : ByteArray

Big-endian u32.

Equations

• Cryptlib.Primitives.KEM.Combiner.u32be v = { data := #[(v >>> 24).toUInt8, (v >>> 16).toUInt8, (v >>> 8).toUInt8, v.toUInt8] }

structure Cryptlib.Primitives.KEM.Combiner.PRF : Type

An unkeyed hash for key derivation and a keyed hash as the per-component PRF.

• hash : ByteArray → Bytes32
• keyed : Bytes32 → ByteArray → Bytes32

def Cryptlib.Primitives.KEM.Combiner.PRF.deriveKey (F : PRF) (ss : ByteArray) : Bytes32

Hash a shared secret of any length to a 32-byte PRF key.

Equations

• F.deriveKey ss = F.hash ss

def Cryptlib.Primitives.KEM.Combiner.transcript (cct : List ByteArray) : ByteArray

Label, component count, then each ciphertext with a 32-bit length prefix.

Equations

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

def Cryptlib.Primitives.KEM.Combiner.splitPRFCore (F : PRF) (parts : List (ByteArray × ByteArray)) : Bytes32

XOR of the per-component keyed hashes; zero32 on the empty list.

Equations

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

def Cryptlib.Primitives.KEM.Combiner.splitPRF (F : PRF) (p : ByteArray × ByteArray) (ps : List (ByteArray × ByteArray) := []) : Bytes32

Split PRF over one or more (shared secret, ciphertext) components.

Equations

• Cryptlib.Primitives.KEM.Combiner.splitPRF F p ps = Cryptlib.Primitives.KEM.Combiner.splitPRFCore F (p :: ps)

inductive Cryptlib.Primitives.KEM.Combiner.SplitPRFError : Type

• noInputs : SplitPRFError
• mismatchedSlices : SplitPRFError
• emptyComponent : SplitPRFError

def Cryptlib.Primitives.KEM.Combiner.instReprSplitPRFError.repr : SplitPRFError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cryptlib.Primitives.KEM.Combiner.instReprSplitPRFError : Repr SplitPRFError

Equations

• Cryptlib.Primitives.KEM.Combiner.instReprSplitPRFError = { reprPrec := Cryptlib.Primitives.KEM.Combiner.instReprSplitPRFError.repr }

@[instance_reducible]

instance Cryptlib.Primitives.KEM.Combiner.instDecidableEqSplitPRFError : DecidableEq SplitPRFError

Equations

• Cryptlib.Primitives.KEM.Combiner.instDecidableEqSplitPRFError x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cryptlib.Primitives.KEM.Combiner.splitPRF? (F : PRF) (ss cct : List ByteArray) : Except SplitPRFError Bytes32

splitPRF over separate secret and ciphertext lists, rejecting malformed input.

Equations

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

theorem Cryptlib.Primitives.KEM.Combiner.splitPRF_pair (F : PRF) (s₁ c₁ s₂ c₂ : ByteArray) : splitPRF F (s₁, c₁) [(s₂, c₂)] = xorBytes (F.keyed (F.deriveKey s₁) (transcript [c₁, c₂])) (F.keyed (F.deriveKey s₂) (transcript [c₁, c₂]))

splitPRF on two components.

The combined KEM

combineKEM F k₀ ks combines a head KEM with a possibly empty list of more. Combined keys, ciphertexts and states for ks are nested products ending in PUnit.

def Cryptlib.Primitives.KEM.Combiner.CombinedState : List KEM.KEM → Type

Equations

• Cryptlib.Primitives.KEM.Combiner.CombinedState [] = PUnit
• Cryptlib.Primitives.KEM.Combiner.CombinedState (k :: ks) = (k.State × Cryptlib.Primitives.KEM.Combiner.CombinedState ks)

def Cryptlib.Primitives.KEM.Combiner.CombinedPublicKey : List KEM.KEM → Type

Equations

• Cryptlib.Primitives.KEM.Combiner.CombinedPublicKey [] = PUnit
• Cryptlib.Primitives.KEM.Combiner.CombinedPublicKey (k :: ks) = (k.PublicKey × Cryptlib.Primitives.KEM.Combiner.CombinedPublicKey ks)

def Cryptlib.Primitives.KEM.Combiner.CombinedPrivateKey : List KEM.KEM → Type

Equations

• Cryptlib.Primitives.KEM.Combiner.CombinedPrivateKey [] = PUnit
• Cryptlib.Primitives.KEM.Combiner.CombinedPrivateKey (k :: ks) = (k.PrivateKey × Cryptlib.Primitives.KEM.Combiner.CombinedPrivateKey ks)

def Cryptlib.Primitives.KEM.Combiner.CombinedCiphertext : List KEM.KEM → Type

Equations

• Cryptlib.Primitives.KEM.Combiner.CombinedCiphertext [] = PUnit
• Cryptlib.Primitives.KEM.Combiner.CombinedCiphertext (k :: ks) = (k.Ciphertext × Cryptlib.Primitives.KEM.Combiner.CombinedCiphertext ks)

def Cryptlib.Primitives.KEM.Combiner.defaultState (ks : List KEM.KEM) : CombinedState ks

Equations

• Cryptlib.Primitives.KEM.Combiner.defaultState [] = PUnit.unit
• Cryptlib.Primitives.KEM.Combiner.defaultState (k :: ks) = (default, Cryptlib.Primitives.KEM.Combiner.defaultState ks)

def Cryptlib.Primitives.KEM.Combiner.defaultPublicKey (ks : List KEM.KEM) : CombinedPublicKey ks

Equations

• Cryptlib.Primitives.KEM.Combiner.defaultPublicKey [] = PUnit.unit
• Cryptlib.Primitives.KEM.Combiner.defaultPublicKey (k :: ks) = (default, Cryptlib.Primitives.KEM.Combiner.defaultPublicKey ks)

def Cryptlib.Primitives.KEM.Combiner.defaultPrivateKey (ks : List KEM.KEM) : CombinedPrivateKey ks

Equations

• Cryptlib.Primitives.KEM.Combiner.defaultPrivateKey [] = PUnit.unit
• Cryptlib.Primitives.KEM.Combiner.defaultPrivateKey (k :: ks) = (default, Cryptlib.Primitives.KEM.Combiner.defaultPrivateKey ks)

def Cryptlib.Primitives.KEM.Combiner.defaultCiphertext (ks : List KEM.KEM) : CombinedCiphertext ks

Equations

• Cryptlib.Primitives.KEM.Combiner.defaultCiphertext [] = PUnit.unit
• Cryptlib.Primitives.KEM.Combiner.defaultCiphertext (k :: ks) = (default, Cryptlib.Primitives.KEM.Combiner.defaultCiphertext ks)

def Cryptlib.Primitives.KEM.Combiner.sumPublicKeySize : List KEM.KEM → Nat

Equations

• Cryptlib.Primitives.KEM.Combiner.sumPublicKeySize [] = 0
• Cryptlib.Primitives.KEM.Combiner.sumPublicKeySize (k :: ks) = k.publicKeySize + Cryptlib.Primitives.KEM.Combiner.sumPublicKeySize ks

def Cryptlib.Primitives.KEM.Combiner.sumPrivateKeySize : List KEM.KEM → Nat

Equations

• Cryptlib.Primitives.KEM.Combiner.sumPrivateKeySize [] = 0
• Cryptlib.Primitives.KEM.Combiner.sumPrivateKeySize (k :: ks) = k.privateKeySize + Cryptlib.Primitives.KEM.Combiner.sumPrivateKeySize ks

def Cryptlib.Primitives.KEM.Combiner.sumCiphertextSize : List KEM.KEM → Nat

Equations

• Cryptlib.Primitives.KEM.Combiner.sumCiphertextSize [] = 0
• Cryptlib.Primitives.KEM.Combiner.sumCiphertextSize (k :: ks) = k.ciphertextSize + Cryptlib.Primitives.KEM.Combiner.sumCiphertextSize ks

def Cryptlib.Primitives.KEM.Combiner.stateFromSeedN (ks : List KEM.KEM) : Vector UInt8 32 → CombinedState ks

Equations

• Cryptlib.Primitives.KEM.Combiner.stateFromSeedN [] x✝ = PUnit.unit
• Cryptlib.Primitives.KEM.Combiner.stateFromSeedN (k :: ks) x✝ = (k.stateFromSeed x✝, Cryptlib.Primitives.KEM.Combiner.stateFromSeedN ks x✝)

def Cryptlib.Primitives.KEM.Combiner.derivePublicKeyN (ks : List KEM.KEM) : CombinedPrivateKey ks → CombinedPublicKey ks

Equations

• Cryptlib.Primitives.KEM.Combiner.derivePublicKeyN [] x_2 = PUnit.unit
• Cryptlib.Primitives.KEM.Combiner.derivePublicKeyN (k :: ks) (sk, sks) = (k.derivePublicKey sk, Cryptlib.Primitives.KEM.Combiner.derivePublicKeyN ks sks)

def Cryptlib.Primitives.KEM.Combiner.ReliableN (ks : List KEM.KEM) : CombinedState ks → Prop

Equations

• Cryptlib.Primitives.KEM.Combiner.ReliableN [] x_2 = True
• Cryptlib.Primitives.KEM.Combiner.ReliableN (k :: ks) (s, ss) = (k.Reliable s ∧ Cryptlib.Primitives.KEM.Combiner.ReliableN ks ss)

Wire encoding

Components are concatenated as ByteArrays and converted to Vector only in combineKEM.

def Cryptlib.Primitives.KEM.Combiner.encodePublicKeyN (ks : List KEM.KEM) : CombinedPublicKey ks → ByteArray

Equations

• Cryptlib.Primitives.KEM.Combiner.encodePublicKeyN [] x_2 = ByteArray.empty
• Cryptlib.Primitives.KEM.Combiner.encodePublicKeyN (k :: ks) (pk, pks) = Cryptlib.Util.Bytes.ofVector (k.encodePublicKey pk) ++ Cryptlib.Primitives.KEM.Combiner.encodePublicKeyN ks pks

def Cryptlib.Primitives.KEM.Combiner.decodePublicKeyN (ks : List KEM.KEM) : ByteArray → Option (CombinedPublicKey ks)

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.KEM.Combiner.decodePublicKeyN [] x✝ = some PUnit.unit

def Cryptlib.Primitives.KEM.Combiner.encodePrivateKeyN (ks : List KEM.KEM) : CombinedPrivateKey ks → ByteArray

Equations

• Cryptlib.Primitives.KEM.Combiner.encodePrivateKeyN [] x_2 = ByteArray.empty
• Cryptlib.Primitives.KEM.Combiner.encodePrivateKeyN (k :: ks) (sk, sks) = Cryptlib.Util.Bytes.ofVector (k.encodePrivateKey sk) ++ Cryptlib.Primitives.KEM.Combiner.encodePrivateKeyN ks sks

def Cryptlib.Primitives.KEM.Combiner.decodePrivateKeyN (ks : List KEM.KEM) : ByteArray → Option (CombinedPrivateKey ks)

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.KEM.Combiner.decodePrivateKeyN [] x✝ = some PUnit.unit

def Cryptlib.Primitives.KEM.Combiner.encodeCiphertextN (ks : List KEM.KEM) : CombinedCiphertext ks → ByteArray

Equations

• Cryptlib.Primitives.KEM.Combiner.encodeCiphertextN [] x_2 = ByteArray.empty
• Cryptlib.Primitives.KEM.Combiner.encodeCiphertextN (k :: ks) (c, cs) = Cryptlib.Util.Bytes.ofVector (k.encodeCiphertext c) ++ Cryptlib.Primitives.KEM.Combiner.encodeCiphertextN ks cs

def Cryptlib.Primitives.KEM.Combiner.decodeCiphertextN (ks : List KEM.KEM) : ByteArray → Option (CombinedCiphertext ks)

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.KEM.Combiner.decodeCiphertextN [] x✝ = some PUnit.unit

theorem Cryptlib.Primitives.KEM.Combiner.encodePublicKeyN_size (ks : List KEM.KEM) (pk : CombinedPublicKey ks) : (encodePublicKeyN ks pk).size = sumPublicKeySize ks

theorem Cryptlib.Primitives.KEM.Combiner.encodePrivateKeyN_size (ks : List KEM.KEM) (sk : CombinedPrivateKey ks) : (encodePrivateKeyN ks sk).size = sumPrivateKeySize ks

theorem Cryptlib.Primitives.KEM.Combiner.encodeCiphertextN_size (ks : List KEM.KEM) (c : CombinedCiphertext ks) : (encodeCiphertextN ks c).size = sumCiphertextSize ks

theorem Cryptlib.Primitives.KEM.Combiner.decode_encode_pub_N (ks : List KEM.KEM) (pk : CombinedPublicKey ks) : decodePublicKeyN ks (encodePublicKeyN ks pk) = some pk

theorem Cryptlib.Primitives.KEM.Combiner.decode_encode_priv_N (ks : List KEM.KEM) (sk : CombinedPrivateKey ks) : decodePrivateKeyN ks (encodePrivateKeyN ks sk) = some sk

theorem Cryptlib.Primitives.KEM.Combiner.decode_encode_ct_N (ks : List KEM.KEM) (c : CombinedCiphertext ks) : decodeCiphertextN ks (encodeCiphertextN ks c) = some c

Encapsulation and decapsulation over the tail list

def Cryptlib.Primitives.KEM.Combiner.liftHead {k : KEM.KEM} {ks : List KEM.KEM} {α : Type} (x : EStateM KEM.KEMError k.State α) : EStateM KEM.KEMError (k.State × CombinedState ks) α

Equations

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

def Cryptlib.Primitives.KEM.Combiner.liftTail {k : KEM.KEM} {ks : List KEM.KEM} {α : Type} (x : EStateM KEM.KEMError (CombinedState ks) α) : EStateM KEM.KEMError (k.State × CombinedState ks) α

Equations

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

def Cryptlib.Primitives.KEM.Combiner.encapAllM (ks : List KEM.KEM) : CombinedPublicKey ks → EStateM KEM.KEMError (CombinedState ks) (CombinedCiphertext ks × List (ByteArray × ByteArray))

Each tail component's encoded (shared secret, ciphertext).

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.KEM.Combiner.encapAllM [] x_2 = pure (PUnit.unit, [])

def Cryptlib.Primitives.KEM.Combiner.decapAllM (ks : List KEM.KEM) : CombinedPrivateKey ks → CombinedCiphertext ks → EStateM KEM.KEMError (CombinedState ks) (List (ByteArray × ByteArray))

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.KEM.Combiner.decapAllM [] x_3 x_4 = pure []

def Cryptlib.Primitives.KEM.Combiner.encapM (F : PRF) (k₀ : KEM.KEM) (ks : List KEM.KEM) (pk : k₀.PublicKey × CombinedPublicKey ks) : EStateM KEM.KEMError (k₀.State × CombinedState ks) ((k₀.Ciphertext × CombinedCiphertext ks) × Bytes32)

Equations

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

def Cryptlib.Primitives.KEM.Combiner.decapM (F : PRF) (k₀ : KEM.KEM) (ks : List KEM.KEM) (sk : k₀.PrivateKey × CombinedPrivateKey ks) (ct : k₀.Ciphertext × CombinedCiphertext ks) : EStateM KEM.KEMError (k₀.State × CombinedState ks) Bytes32

Equations

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

Correctness

def Cryptlib.Primitives.KEM.Combiner.AllHonestFor (ks : List KEM.KEM) : CombinedPublicKey ks → CombinedPrivateKey ks → Prop

Every tail component round-trips for its (pk, sk) pair.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.KEM.Combiner.AllHonestFor [] x_3 x_4 = True

theorem Cryptlib.Primitives.KEM.Combiner.allHonestFor_derivePublicKey (ks : List KEM.KEM) (sks : CombinedPrivateKey ks) : AllHonestFor ks (derivePublicKeyN ks sks) sks

theorem Cryptlib.Primitives.KEM.Combiner.encapAllM_decapAllM (ks : List KEM.KEM) (pks : CombinedPublicKey ks) (sks : CombinedPrivateKey ks) : AllHonestFor ks pks sks → ∀ (s : CombinedState ks), ReliableN ks s → ∀ (ct : CombinedCiphertext ks) (comps : List (ByteArray × ByteArray)) (s' : CombinedState ks), encapAllM ks pks s = EStateM.Result.ok (ct, comps) s' → ∀ (t : CombinedState ks), ∃ (t' : CombinedState ks), decapAllM ks sks ct t = EStateM.Result.ok comps t'

decapAllM recovers the (shared secret, ciphertext) list encapAllM produced.

theorem Cryptlib.Primitives.KEM.Combiner.combinedRoundTrip (F : PRF) (k₀ : KEM.KEM) (ks : List KEM.KEM) (pk₀ : k₀.PublicKey) (pks : CombinedPublicKey ks) (sk₀ : k₀.PrivateKey) (sks : CombinedPrivateKey ks) (h₀ : ∀ (s : k₀.State), k₀.Reliable s → ∀ (c : k₀.Ciphertext) (p : k₀.Plaintext) (s' : k₀.State), k₀.encap pk₀ s = EStateM.Result.ok (c, p) s' → ∀ (t : k₀.State), ∃ (t' : k₀.State), k₀.decap sk₀ c t = EStateM.Result.ok p t') (hs : AllHonestFor ks pks sks) (s : k₀.State × CombinedState ks) : k₀.Reliable s.fst ∧ ReliableN ks s.snd → ∀ (ct : k₀.Ciphertext × CombinedCiphertext ks) (key : Bytes32) (s' : k₀.State × CombinedState ks), encapM F k₀ ks (pk₀, pks) s = EStateM.Result.ok (ct, key) s' → ∀ (t : k₀.State × CombinedState ks), ∃ (t' : k₀.State × CombinedState ks), decapM F k₀ ks (sk₀, sks) ct t = EStateM.Result.ok key t'

If the head and every tail KEM round-trip for the given (pk, sk) pairs, so does the combination.

def Cryptlib.Primitives.KEM.Combiner.generateN (ks : List KEM.KEM) : EStateM KEM.KEMError (CombinedState ks) ((pk : CombinedPublicKey ks) ×' { sk : CombinedPrivateKey ks // AllHonestFor ks pk sk })

Key pairs for the tail list, with their AllHonestFor witness.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.KEM.Combiner.generateN [] = pure ⟨PUnit.unit, ⟨PUnit.unit, trivial⟩⟩

theorem Cryptlib.Primitives.KEM.Combiner.decodePrivateKeyN_total (ks : List KEM.KEM) (b : ByteArray) : ∃ (sk : CombinedPrivateKey ks), decodePrivateKeyN ks b = some sk

def Cryptlib.Primitives.KEM.Combiner.combineKEM (F : PRF) (k₀ : KEM.KEM) (ks : List KEM.KEM) : KEM.KEM

One KEM plus a possibly empty list of more, combined with the split PRF.

Equations

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