Many-Time → One-Time CPA$ Reduction via SLIDE

This file implements Case Study 1 from "Mechanizing Nested Hybrid Arguments" (Larsen & Schurmann, CSF 2025): reducing many-time CPA$ security to one-time CPA$ security using the SLIDE construction.

Main Results

• dHybrid - Decomposed hybrid game (equivalent to hybrid_game from Scheme)
• dHybrid_zero - Boundary: game 0 = MT_CPA_real
• dHybrid_length - Boundary: game n = MT_CPA_ideal
• dHybrid_step_bound - Per-step advantage ≤ OT-CPA$ advantage
• Adv_MT_CPA_OT - Main: Adv(MT_CPA, A) ≤ q * max Adv(OT_CPA)

SLIDE Construction (Fig. 9)

The SLIDE oracle for hybrid index i:

• Query j < i: return random ciphertext (ideal)
• Query j = i: forward to single-instance oracle (real or ideal)
• Query j > i: encrypt the real message (real)

Adjacent hybrids differ only at position i: one encrypts, the other samples random. This difference is exactly one OT-CPA$ query.

References

• [Larsen & Schurmann, Mechanizing Nested Hybrid Arguments, CSF 2025, §4.1]

Decomposed Hybrid Game

We define `dHybrid` as an alias for `hybrid_game` from Scheme.lean.
The `hybrid_game` uses recursive `hybridLoop` with a position counter,
which avoids the need for `LawfulMonad` instances. 

noncomputable def CatCrypt.Examples.PKE.OneToMany.dHybrid (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (i : ℕ) : Core.SPComp (List P.C)

Decomposed hybrid game: first i positions get random ciphertexts, remaining positions get real encryptions.

Equivalent to hybrid_game from Scheme.lean.

Equations

• CatCrypt.Examples.PKE.OneToMany.dHybrid P pk msgs i = CatCrypt.Examples.PKE.hybrid_game P pk msgs i

Boundary Conditions

theorem CatCrypt.Examples.PKE.OneToMany.dHybrid_zero (P : PKEScheme) (pk : P.PK) (msgs : List P.M) : dHybrid P pk msgs 0 = MT_CPA_real P pk msgs

Boundary: dHybrid at 0 = all encrypted (real game).

theorem CatCrypt.Examples.PKE.OneToMany.dHybrid_length (P : PKEScheme) (pk : P.PK) (msgs : List P.M) : dHybrid P pk msgs msgs.length = MT_CPA_ideal P msgs

Boundary: dHybrid at length = all random (ideal game).

Recursive Helpers

These avoid `List.mapM` (which requires `LawfulMonad` for lemmas)
by defining the prefix/suffix computations recursively. 

noncomputable def CatCrypt.Examples.PKE.OneToMany.sampleN (P : PKEScheme) : ℕ → Core.SPComp (List P.C)

Sample n random ciphertexts.

Equations

• CatCrypt.Examples.PKE.OneToMany.sampleN P 0 = CatCrypt.Core.SPComp.pure []
• CatCrypt.Examples.PKE.OneToMany.sampleN P n.succ = do let c ← P.sampleCip let cs ← CatCrypt.Examples.PKE.OneToMany.sampleN P n CatCrypt.Core.SPComp.pure (c :: cs)

noncomputable def CatCrypt.Examples.PKE.OneToMany.encList (P : PKEScheme) (pk : P.PK) : List P.M → Core.SPComp (List P.C)

Encrypt a list of messages under a public key.

Equations

• CatCrypt.Examples.PKE.OneToMany.encList P pk [] = CatCrypt.Core.SPComp.pure []
• CatCrypt.Examples.PKE.OneToMany.encList P pk (m :: ms) = do let c ← P.enc pk m let cs ← CatCrypt.Examples.PKE.OneToMany.encList P pk ms CatCrypt.Core.SPComp.pure (c :: cs)

Structural helpers for hybridLoop

theorem CatCrypt.Examples.PKE.OneToMany.hybridLoop_shift (P : PKEScheme) (pk : P.PK) (i j : ℕ) (msgs : List P.M) : hybridLoop P pk (i + 1) (j + 1) msgs = hybridLoop P pk i j msgs

Shifting both threshold and position by 1 is a no-op.

theorem CatCrypt.Examples.PKE.OneToMany.hybridLoop_suffix_eq_encList (P : PKEScheme) (pk : P.PK) (i j : ℕ) (msgs : List P.M) (hj : i ≤ j) : hybridLoop P pk i j msgs = encList P pk msgs

When threshold ≤ position, hybridLoop encrypts everything = encList.

IsPure helpers

theorem CatCrypt.Examples.PKE.OneToMany.sampleN_isPure (P : PKEScheme) (hP : P.IsPure) (n : ℕ) : (sampleN P n).IsPure

theorem CatCrypt.Examples.PKE.OneToMany.encList_isPure (P : PKEScheme) (hP : P.IsPure) (pk : P.PK) (ms : List P.M) : (encList P pk ms).IsPure

Decomposition Lemmas

These show that `hybridLoop` decomposes as: sample prefix + core + encrypt suffix.
Proved by induction on `i` (the switch position), using `hybridLoop_shift` to
reduce the successor case to the base case on the tail of the message list. 

theorem CatCrypt.Examples.PKE.OneToMany.hybridLoop_decomp_enc (P : PKEScheme) (pk : P.PK) (i : ℕ) (msgs : List P.M) (hi : i < msgs.length) : hybridLoop P pk i 0 msgs = (sampleN P i).bind fun (pre : List P.C) => (P.enc pk msgs[i]).bind fun (c : P.C) => (encList P pk (List.drop (i + 1) msgs)).bind fun (suf : List P.C) => Core.SPComp.pure (pre ++ [c] ++ suf)

theorem CatCrypt.Examples.PKE.OneToMany.hybridLoop_decomp_samp (P : PKEScheme) (pk : P.PK) (i : ℕ) (msgs : List P.M) (_hi : i < msgs.length) : hybridLoop P pk (i + 1) 0 msgs = (sampleN P i).bind fun (pre : List P.C) => P.sampleCip.bind fun (c : P.C) => (encList P pk (List.drop (i + 1) msgs)).bind fun (suf : List P.C) => Core.SPComp.pure (pre ++ [c] ++ suf)

The SLIDE Adversary

The "context" adversary: given a single ciphertext at position i,
fills in the prefix with random ciphertexts and suffix with real
encryptions, then runs the original adversary on the assembled list. 

noncomputable def CatCrypt.Examples.PKE.OneToMany.slideAdv (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (i : ℕ) (A : List P.C → Core.SPComp Bool) (c : P.C) : Core.SPComp Bool

SLIDE adversary: embeds a single ciphertext into the full list context.

Samples min i msgs.length random prefix ciphertexts, encrypts suffix messages from position i + 1 onward.

Equations

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

Per-Step Advantage Bound

theorem CatCrypt.Examples.PKE.OneToMany.dHybrid_step_eq (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (i : ℕ) (hi : i < msgs.length) (A : List P.C → Core.SPComp Bool) (hP : P.IsPure) : Crypto.AdvantageA (dHybrid P pk msgs i) (dHybrid P pk msgs (i + 1)) A = OT_CPA_Advantage P pk msgs[i] (slideAdv P pk msgs i A)

Per-step advantage equality: adjacent hybrid advantage = OT-CPA$ advantage.

Theorem 4 (CSF 2025). Equality is established by decomposing both hybrids and commuting the prefix past the core operation using P.IsPure.

theorem CatCrypt.Examples.PKE.OneToMany.dHybrid_step_bound (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (i : ℕ) (hi : i < msgs.length) (A : List P.C → Core.SPComp Bool) (hP : P.IsPure) : Crypto.AdvantageA (dHybrid P pk msgs i) (dHybrid P pk msgs (i + 1)) A ≤ OT_CPA_Advantage P pk msgs[i] (slideAdv P pk msgs i A)

Per-step advantage reduction: adjacent hybrid advantage ≤ OT-CPA$ advantage.

Requires P.IsPure to commute the prefix sampling past enc/sampleCip.

theorem CatCrypt.Examples.PKE.OneToMany.dHybrid_step_bound' (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (i : ℕ) (hi : i < msgs.length) (A : List P.C → Core.SPComp Bool) (hP : P.IsPure) : Crypto.AdvantageA (dHybrid P pk msgs i) (dHybrid P pk msgs (i + 1)) A ≤ OT_CPA_Advantage P pk msgs[i] (slideAdv P pk msgs i A)

dHybrid_step_bound follows from dHybrid_step_eq.

Main Reduction Theorems

theorem CatCrypt.Examples.PKE.OneToMany.Adv_MT_CPA_OT (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (ε : ENNReal) (A : List P.C → Core.SPComp Bool) (hP : P.IsPure) (hOT : ∀ (i : ℕ) (hi : i < msgs.length), OT_CPA_Advantage P pk msgs[i] (slideAdv P pk msgs i A) ≤ ε) : MT_CPA_Advantage P pk msgs A ≤ ↑msgs.length * ε

Many-time to one-time CPA$ reduction (CSF 2025, Theorem 1).

Adv(MT_CPA, A) ≤ q * max_i OT_CPA_Advantage(m_i, slideAdv_i)

Requires P.IsPure for the per-step decomposition.

theorem CatCrypt.Examples.PKE.OneToMany.Adv_MT_CPA_direct (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (ε : ENNReal) (A : List P.C → Core.SPComp Bool) (hstep : ∀ i < msgs.length, Crypto.AdvantageA (dHybrid P pk msgs i) (dHybrid P pk msgs (i + 1)) A ≤ ε) : MT_CPA_Advantage P pk msgs A ≤ ↑msgs.length * ε

Alternative: MT-CPA bound with explicit per-step hypothesis.

This version takes the per-step bound directly as a hypothesis, without requiring it to be bounded by OT-CPA. Useful when the step bound comes from a different source.

theorem CatCrypt.Examples.PKE.OneToMany.MT_CPA_perfect (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (hperf : ∀ i < msgs.length, Relational.rHoare Relational.eqPre (dHybrid P pk msgs i) (dHybrid P pk msgs (i + 1)) Relational.eqPost) (A : List P.C → Core.SPComp Bool) : MT_CPA_Advantage P pk msgs A = 0

Perfect security for many-time CPA$: when all hybrid steps are perfectly indistinguishable, the advantage is 0.