KEM-DEM Composition (Hybrid Encryption)

The KEM-DEM construction is the standard recipe for hybrid public-key encryption: a key encapsulation mechanism (KEM) ships a fresh symmetric key under the public key, and a data encapsulation mechanism (DEM) encrypts the payload under that key. This file builds the composition as a core PKEScheme and proves its security by a three-hop hybrid argument.

This is the proof-ladders "asymmetric" benchmark (Rosulek, The Joy of Cryptography, hybrid encryption): a secure KEM composed with a secure DEM yields a secure public-key scheme.

Overview

To encrypt m under pk:

1. (k, ek) ← KEM.encap pk — encapsulate a fresh symmetric key k
2. c := DEM.enc k m — encrypt the payload under k
3. output (ek, c)

To decrypt (ek, c) under sk: recover k := KEM.decap sk ek, then m := DEM.dec k c.

Security

These are IND-CPA games: the real game encrypts the actual message and the ideal game encrypts a null message, and the adversary sees only (pk, ek, c) — there is no decryption oracle, so the statement is confidentiality (CPA), not CCA.

The distinguishing advantage against the composed PKE-CPA game is bounded by

Adv_PKE ≤ Adv_KEM + Adv_DEM + Adv_KEM,

via three game hops (pke_security): swap the encapsulated key for a random key (KEM), swap the payload for a null message (DEM), swap the random key back (KEM). When both components are perfectly secure the composition is perfectly secure (pke_perfect_security): every advantage collapses to 0.

As a concrete headline, BoolXorDEM (the one-time-pad DEM over Bool) is perfectly DEM-secure via the XOR bijection coupling, so composing it with any perfectly-secure KEM gives a perfectly-secure hybrid PKE (xorHybrid_perfect_security).

Main definitions

• KEMScheme, DEMScheme, PKEScheme — the component and target interfaces.
• HybridPKE — the KEM-DEM composition as a PKEScheme.
• BoolXorDEM — the XOR (one-time-pad) DEM over Bool.

Main results

• hybridPKE_correct — correctness of the composition from component correctness.
• pke_security — the three-term hybrid bound Adv_PKE ≤ Adv_KEM + Adv_DEM + Adv_KEM.
• pke_perfect_security — perfect KEM + perfect DEM ⇒ perfect PKE.
• boolXorDEM_perfect — the XOR DEM is perfectly DEM-secure (XOR-bijection coupling).
• xorHybrid_perfect_security — perfect hybrid PKE from a perfect KEM and the XOR DEM.

References

• [Rosulek, The Joy of Cryptography — hybrid (KEM-DEM) encryption]
• [Cramer & Shoup, Design and Analysis of Practical Public-Key Encryption Schemes]
• [Brzuska et al., State-Separating Proofs, ASIACRYPT 2018: https://eprint.iacr.org/2018/306]

KEM Scheme

A Key Encapsulation Mechanism generates a fresh symmetric key and encapsulates it under the public key; the key is recovered from the encapsulation using the secret key.

structure CatCrypt.Examples.KEMDEM.KEMScheme (PKey SKey Key EKey : Type) : Type

A Key Encapsulation Mechanism (KEM) scheme.

Type parameters: PKey public key, SKey secret key, Key symmetric key, EKey encapsulation (KEM ciphertext).

• kgen : Core.SPComp (PKey × SKey)

  Key generation: produces a public/secret key pair.

• encap : PKey → Core.SPComp (Key × EKey)

  Encapsulation: from a public key, a symmetric key and its encapsulation.

• decap : SKey → EKey → Key

  Decapsulation: deterministically recovers the symmetric key.

def CatCrypt.Examples.KEMDEM.KEMScheme.Correct {PKey SKey Key EKey : Type} (KEM : KEMScheme PKey SKey Key EKey) : Prop

KEM correctness: decapsulation inverts encapsulation for generated key pairs.

Equations

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

DEM Scheme

A Data Encapsulation Mechanism is a deterministic symmetric cipher.

structure CatCrypt.Examples.KEMDEM.DEMScheme (Key Plain Cipher : Type) : Type

A Data Encapsulation Mechanism (DEM): deterministic encryption/decryption.

• enc : Key → Plain → Cipher

  Deterministic encryption.

• dec : Key → Cipher → Plain

  Deterministic decryption.

def CatCrypt.Examples.KEMDEM.DEMScheme.Correct {Key Plain Cipher : Type} (DEM : DEMScheme Key Plain Cipher) : Prop

DEM correctness: decryption inverts encryption.

Equations

• DEM.Correct = ∀ (k : Key) (m : Plain), DEM.dec k (DEM.enc k m) = m

PKE Scheme

The target interface implemented by the KEM-DEM composition.

structure CatCrypt.Examples.KEMDEM.PKEScheme (PKey SKey Plain EKey Cipher : Type) : Type

A Public Key Encryption (PKE) scheme.

The ciphertext is a pair (EKey × Cipher) of the KEM encapsulation and the DEM ciphertext.

• kgen : Core.SPComp (PKey × SKey)

  Key generation: produces a public/secret key pair.

• enc : PKey → Plain → Core.SPComp (EKey × Cipher)

  Encryption: public key and plaintext to a ciphertext pair.

• dec : SKey → EKey × Cipher → Plain

  Decryption: deterministic, secret key and ciphertext pair to plaintext.

KEM-DEM Hybrid Construction

noncomputable def CatCrypt.Examples.KEMDEM.HybridPKE {PKey SKey Key EKey Plain Cipher : Type} (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) : PKEScheme PKey SKey Plain EKey Cipher

The KEM-DEM hybrid encryption scheme built from a KEM and a DEM.

Equations

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

Correctness

theorem CatCrypt.Examples.KEMDEM.hybridPKE_correct {PKey SKey Key EKey Plain Cipher : Type} (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (hKEM : KEM.Correct) (hDEM : DEM.Correct) (pk : PKey) (sk : SKey) (h h' : Core.Heap) (m : Plain) (ek : EKey) (c : Cipher) (h'' : Core.Heap) : ((pk, sk), h') ∈ (KEM.kgen h).support → ((ek, c), h'') ∈ ((HybridPKE KEM DEM).enc pk m h').support → (HybridPKE KEM DEM).dec sk (ek, c) = m

Correctness of the hybrid scheme from KEM and DEM correctness.

KEM-CPA Security Game

Real: the challenge key is the encapsulated key. Ideal: the challenge key is fresh and independent of the encapsulation.

noncomputable def CatCrypt.Examples.KEMDEM.KEM_CPA_real {PKey SKey Key EKey : Type} (KEM : KEMScheme PKey SKey Key EKey) : Core.SPComp (PKey × EKey × Key)

KEM-CPA real game: return (pk, ek, k) for the actual encapsulated key k.

Equations

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

noncomputable def CatCrypt.Examples.KEMDEM.KEM_CPA_ideal {PKey SKey Key EKey : Type} [Fintype Key] [Nonempty Key] (KEM : KEMScheme PKey SKey Key EKey) : Core.SPComp (PKey × EKey × Key)

KEM-CPA ideal game: return (pk, ek, k') for a fresh random key k'.

Equations

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

noncomputable def CatCrypt.Examples.KEMDEM.KEM_CPA_Advantage {PKey SKey Key EKey : Type} [Fintype Key] [Nonempty Key] (KEM : KEMScheme PKey SKey Key EKey) (A : PKey × EKey × Key → Core.SPComp Bool) : ENNReal

KEM-CPA advantage.

Equations

• CatCrypt.Examples.KEMDEM.KEM_CPA_Advantage KEM A = CatCrypt.Crypto.AdvantageA (CatCrypt.Examples.KEMDEM.KEM_CPA_real KEM) (CatCrypt.Examples.KEMDEM.KEM_CPA_ideal KEM) A

def CatCrypt.Examples.KEMDEM.PerfectKEM_CPA {PKey SKey Key EKey : Type} [Fintype Key] [Nonempty Key] (KEM : KEMScheme PKey SKey Key EKey) : Prop

Perfect KEM-CPA security: the real and ideal games are perfectly coupled.

Equations

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

DEM-CPA Security Game

Real: encrypt the actual message. Ideal: encrypt a fixed null message.

noncomputable def CatCrypt.Examples.KEMDEM.DEM_CPA_real {Key Plain Cipher : Type} [Fintype Key] [Nonempty Key] (DEM : DEMScheme Key Plain Cipher) (m : Plain) : Core.SPComp Cipher

DEM-CPA real game: sample a key, encrypt the actual message.

Equations

• CatCrypt.Examples.KEMDEM.DEM_CPA_real DEM m = do let k ← CatCrypt.Core.SPComp.sample Key pure (DEM.enc k m)

noncomputable def CatCrypt.Examples.KEMDEM.DEM_CPA_ideal {Key Plain Cipher : Type} [Fintype Key] [Nonempty Key] (DEM : DEMScheme Key Plain Cipher) (nullPlain _m : Plain) : Core.SPComp Cipher

DEM-CPA ideal game: sample a key, encrypt the null message.

Equations

• CatCrypt.Examples.KEMDEM.DEM_CPA_ideal DEM nullPlain _m = do let k ← CatCrypt.Core.SPComp.sample Key pure (DEM.enc k nullPlain)

noncomputable def CatCrypt.Examples.KEMDEM.DEM_CPA_Advantage {Key Plain Cipher : Type} [Fintype Key] [Nonempty Key] (DEM : DEMScheme Key Plain Cipher) (nullPlain m : Plain) (A : Cipher → Core.SPComp Bool) : ENNReal

DEM-CPA advantage.

Equations

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

def CatCrypt.Examples.KEMDEM.PerfectDEM_CPA {Key Plain Cipher : Type} [Fintype Key] [Nonempty Key] (DEM : DEMScheme Key Plain Cipher) (nullPlain : Plain) : Prop

Perfect DEM-CPA security: real and ideal games are perfectly coupled.

Equations

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

PKE-CPA Security Game (for the hybrid scheme)

noncomputable def CatCrypt.Examples.KEMDEM.PKE_CPA_real {PKey SKey EKey Plain Cipher : Type} (PKE : PKEScheme PKey SKey Plain EKey Cipher) (m : Plain) : Core.SPComp (PKey × EKey × Cipher)

PKE-CPA real game: return (pk, ek, c) encrypting the actual message.

Equations

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

noncomputable def CatCrypt.Examples.KEMDEM.PKE_CPA_ideal {PKey SKey EKey Plain Cipher : Type} (PKE : PKEScheme PKey SKey Plain EKey Cipher) (nullPlain _m : Plain) : Core.SPComp (PKey × EKey × Cipher)

PKE-CPA ideal game: return (pk, ek, c) encrypting the null message.

Equations

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

noncomputable def CatCrypt.Examples.KEMDEM.PKE_CPA_Advantage {PKey SKey EKey Plain Cipher : Type} (PKE : PKEScheme PKey SKey Plain EKey Cipher) (nullPlain m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) : ENNReal

PKE-CPA advantage.

Equations

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

def CatCrypt.Examples.KEMDEM.PerfectPKE_CPA {PKey SKey EKey Plain Cipher : Type} (PKE : PKEScheme PKey SKey Plain EKey Cipher) (nullPlain : Plain) : Prop

Perfect PKE-CPA security.

Equations

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

Hybrid Games for the Security Reduction

Game 0 (PKE real) → Game 1 (random key) → Game 2 (random key + null) → Game 3 (PKE ideal).

noncomputable def CatCrypt.Examples.KEMDEM.HybridGame1 {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (m : Plain) : Core.SPComp (PKey × EKey × Cipher)

Hybrid Game 1: encrypt the actual message under a random key.

Equations

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

noncomputable def CatCrypt.Examples.KEMDEM.HybridGame2 {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (nullPlain _m : Plain) : Core.SPComp (PKey × EKey × Cipher)

Hybrid Game 2: encrypt the null message under a random key.

Equations

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

Security Reductions

noncomputable def CatCrypt.Examples.KEMDEM.ReductionKEM1 {PKey Key EKey Plain Cipher : Type} (DEM : DEMScheme Key Plain Cipher) (m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) (challenge : PKey × EKey × Key) : Core.SPComp Bool

Reduction to KEM-CPA (first hop): receive (pk, ek, k), DEM-encrypt m, run A.

Equations

• CatCrypt.Examples.KEMDEM.ReductionKEM1 DEM m A (pk, ek, k) = A (pk, ek, DEM.enc k m)

noncomputable def CatCrypt.Examples.KEMDEM.ReductionDEM {PKey SKey Key EKey Cipher : Type} (KEM : KEMScheme PKey SKey Key EKey) (A : PKey × EKey × Cipher → Core.SPComp Bool) (c : Cipher) : Core.SPComp Bool

Reduction to DEM-CPA (second hop): run KEM, receive c, run A.

Equations

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

noncomputable def CatCrypt.Examples.KEMDEM.ReductionKEM2 {PKey Key EKey Plain Cipher : Type} (DEM : DEMScheme Key Plain Cipher) (nullPlain : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) (challenge : PKey × EKey × Key) : Core.SPComp Bool

Reduction to KEM-CPA (third hop): as ReductionKEM1 but on nullPlain.

Equations

• CatCrypt.Examples.KEMDEM.ReductionKEM2 DEM nullPlain A (pk, ek, k) = A (pk, ek, DEM.enc k nullPlain)

Game Equivalences

Each consecutive pair of games equals a component game composed with a reduction.

theorem CatCrypt.Examples.KEMDEM.pke_real_eq_kem_real_bind {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] [Fintype EKey] [Nonempty EKey] [Fintype Cipher] [Nonempty Cipher] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) : (PKE_CPA_real (HybridPKE KEM DEM) m).bind A = (KEM_CPA_real KEM).bind (ReductionKEM1 DEM m A)

PKE-CPA real, post-composed with A, equals KEM-CPA real ∘ ReductionKEM1.

theorem CatCrypt.Examples.KEMDEM.hybrid1_eq_kem_ideal_bind {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] [Fintype EKey] [Nonempty EKey] [Fintype Cipher] [Nonempty Cipher] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) : (HybridGame1 KEM DEM m).bind A = (KEM_CPA_ideal KEM).bind (ReductionKEM1 DEM m A)

HybridGame1 ∘ A equals KEM-CPA ideal ∘ ReductionKEM1.

theorem CatCrypt.Examples.KEMDEM.hybrid1_eq_dem_real_bind {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] [Fintype EKey] [Nonempty EKey] [Fintype Cipher] [Nonempty Cipher] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) : (HybridGame1 KEM DEM m).bind A = (DEM_CPA_real DEM m).bind (ReductionDEM KEM A)

HybridGame1 ∘ A equals DEM-CPA real ∘ ReductionDEM.

Uses SDistr.bind_comm to commute the (independent) uniform key sampling past the KEM operations.

theorem CatCrypt.Examples.KEMDEM.hybrid2_eq_dem_ideal_bind {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] [Fintype EKey] [Nonempty EKey] [Fintype Cipher] [Nonempty Cipher] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (nullPlain m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) : (HybridGame2 KEM DEM nullPlain m).bind A = (DEM_CPA_ideal DEM nullPlain m).bind (ReductionDEM KEM A)

HybridGame2 ∘ A equals DEM-CPA ideal ∘ ReductionDEM.

theorem CatCrypt.Examples.KEMDEM.hybrid2_eq_kem_ideal_bind2 {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] [Fintype EKey] [Nonempty EKey] [Fintype Cipher] [Nonempty Cipher] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (nullPlain m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) : (HybridGame2 KEM DEM nullPlain m).bind A = (KEM_CPA_ideal KEM).bind (ReductionKEM2 DEM nullPlain A)

HybridGame2 ∘ A equals KEM-CPA ideal ∘ ReductionKEM2.

theorem CatCrypt.Examples.KEMDEM.pke_ideal_eq_kem_real_bind2 {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] [Fintype EKey] [Nonempty EKey] [Fintype Cipher] [Nonempty Cipher] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (nullPlain m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) : (PKE_CPA_ideal (HybridPKE KEM DEM) nullPlain m).bind A = (KEM_CPA_real KEM).bind (ReductionKEM2 DEM nullPlain A)

PKE-CPA ideal ∘ A equals KEM-CPA real ∘ ReductionKEM2.

Main Security Theorem

theorem CatCrypt.Examples.KEMDEM.pke_security {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] [Fintype EKey] [Nonempty EKey] [Fintype Cipher] [Nonempty Cipher] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (nullPlain m : Plain) (A : PKey × EKey × Cipher → Core.SPComp Bool) : PKE_CPA_Advantage (HybridPKE KEM DEM) nullPlain m A ≤ KEM_CPA_Advantage KEM (ReductionKEM1 DEM m A) + DEM_CPA_Advantage DEM nullPlain m (ReductionDEM KEM A) + KEM_CPA_Advantage KEM (ReductionKEM2 DEM nullPlain A)

KEM-DEM security: the hybrid PKE-CPA advantage is bounded by two KEM-CPA advantages and one DEM-CPA advantage,

Adv_PKE(A) ≤ Adv_KEM(A₁) + Adv_DEM(A₂) + Adv_KEM(A₃),

where A₁ = ReductionKEM1, A₂ = ReductionDEM, A₃ = ReductionKEM2. Proved by the triangle inequality over the three hybrid games and the game equivalences.

Corollary: Perfect Security

If both components are perfectly secure, so is the composition.

theorem CatCrypt.Examples.KEMDEM.pke_perfect_security {PKey SKey Key EKey Plain Cipher : Type} [Fintype Key] [Nonempty Key] [Fintype EKey] [Nonempty EKey] [Fintype Cipher] [Nonempty Cipher] (KEM : KEMScheme PKey SKey Key EKey) (DEM : DEMScheme Key Plain Cipher) (nullPlain : Plain) (hKEM : PerfectKEM_CPA KEM) (hDEM : PerfectDEM_CPA DEM nullPlain) : PerfectPKE_CPA (HybridPKE KEM DEM) nullPlain

Perfect KEM-DEM security: if the KEM and DEM are perfectly secure, then the hybrid PKE is perfectly secure. Proved by transitivity through the hybrid games PKE_real ≈ Hybrid1 ≈ Hybrid2 ≈ PKE_ideal.

XOR-DEM Instantiation: Perfect Security

The one-time-pad DEM over Bool (enc k m = k ⊕ m) is perfectly DEM-secure: encrypting the real message and encrypting the null message false are both uniform over the sampled key, so they couple through the XOR bijection (Prob/XorBij). Composed with any perfectly-secure KEM, the hybrid PKE has advantage exactly 0.

def CatCrypt.Examples.KEMDEM.BoolXorDEM : DEMScheme Bool Bool Bool

The XOR (one-time-pad) DEM over Bool: enc k m = k ⊕ m, dec k c = k ⊕ c.

Equations

• CatCrypt.Examples.KEMDEM.BoolXorDEM = { enc := fun (k m : Bool) => k ^^ m, dec := fun (k c : Bool) => k ^^ c }

theorem CatCrypt.Examples.KEMDEM.boolXorDEM_correct : BoolXorDEM.Correct

The XOR DEM is correct: dec k (enc k m) = m.

theorem CatCrypt.Examples.KEMDEM.boolXorDEM_perfect : PerfectDEM_CPA BoolXorDEM false

The XOR DEM is perfectly DEM-secure (null message false).

For every message m, encrypting m and encrypting false under a uniform key are equidistributed: mapping the real key k to k ⊕ m is a bijection (boolXorBij) under which the real ciphertext k ⊕ m equals the ideal ciphertext (k ⊕ m) ⊕ false.

theorem CatCrypt.Examples.KEMDEM.xorHybrid_perfect_security {PKey SKey EKey : Type} [Fintype EKey] [Nonempty EKey] (KEM : KEMScheme PKey SKey Bool EKey) (hKEM : PerfectKEM_CPA KEM) : PerfectPKE_CPA (HybridPKE KEM BoolXorDEM) false

Perfect hybrid PKE from the XOR DEM: composing any perfectly-secure KEM with the one-time-pad DEM over Bool yields a perfectly-secure hybrid PKE — every distinguisher has advantage exactly 0.

theorem CatCrypt.Examples.KEMDEM.xorHybrid_advantage_zero {PKey SKey EKey : Type} [Fintype EKey] [Nonempty EKey] (KEM : KEMScheme PKey SKey Bool EKey) (hKEM : PerfectKEM_CPA KEM) (m : Bool) (A : PKey × EKey × Bool → Core.SPComp Bool) : PKE_CPA_Advantage (HybridPKE KEM BoolXorDEM) false m A = 0

The XOR-hybrid PKE is perfectly indistinguishable, so every adversary's distinguishing advantage is exactly 0.