Multi-Instance → Single-Instance Reduction (Case Study 2)

This file implements Case Study 2 from "Mechanizing Nested Hybrid Arguments" (Larsen & Schurmann, CSF 2025): reducing multi-instance CPA$ security to single-instance (many-time) CPA$ security using a second layer of SLIDE.

Main Results

• MI_hybrid - Hybrid game indexed by instance switch position
• MI_slideAdv - SLIDE adversary for the instance dimension
• MI_step_eq - Per-step: Adv(MI_hybrid i, MI_hybrid (i+1)) = MT_CPA_Advantage
• Adv_MI_MT_CPA - Main: Adv(MI, A) ≤ n * ε where n = number of instances
• Adv_MI_MT_CPA_nested - Composed: Adv(MI, A) ≤ n * q * ε_OT

References

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

noncomputable def CatCrypt.Examples.PKE.MultiInstance.defPK (P : PKEScheme) : P.PK

Default public key (for out-of-bounds access via List.getD).

Equations

• CatCrypt.Examples.PKE.MultiInstance.defPK P = Classical.arbitrary P.PK

Multi-Instance Hybrid Game

noncomputable def CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop (P : PKEScheme) (pks : List P.PK) (i : ℕ) : ℕ → List (List P.M) → Core.SPComp (List (List P.C))

Multi-instance hybrid loop with position counter j and threshold i. When j < i: use MT_CPA_ideal (random ciphertexts). When j ≥ i: use MT_CPA_real (encrypted ciphertexts).

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop P pks i x✝ [] = CatCrypt.Core.SPComp.pure []

noncomputable def CatCrypt.Examples.PKE.MultiInstance.MI_hybrid (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) (i : ℕ) : Core.SPComp (List (List P.C))

Multi-instance hybrid game: first i instances ideal, rest real.

Equations

• CatCrypt.Examples.PKE.MultiInstance.MI_hybrid P pks msgs i = CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop P pks i 0 msgs

noncomputable def CatCrypt.Examples.PKE.MultiInstance.MI_Advantage (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) (A : List (List P.C) → Core.SPComp Bool) : ENNReal

Multi-instance advantage.

Equations

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

Prefix/Suffix Helpers

noncomputable def CatCrypt.Examples.PKE.MultiInstance.MI_sampleN (P : PKEScheme) : ℕ → List (List P.M) → Core.SPComp (List (List P.C))

Sample n instances as ideal (random) ciphertexts.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Examples.PKE.MultiInstance.MI_sampleN P 0 x✝ = CatCrypt.Core.SPComp.pure []
• CatCrypt.Examples.PKE.MultiInstance.MI_sampleN P n.succ [] = CatCrypt.Core.SPComp.pure []

noncomputable def CatCrypt.Examples.PKE.MultiInstance.MI_encList (P : PKEScheme) (pks : List P.PK) : ℕ → List (List P.M) → Core.SPComp (List (List P.C))

Encrypt instances under their keys (all real), starting at position j.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Examples.PKE.MultiInstance.MI_encList P pks x✝ [] = CatCrypt.Core.SPComp.pure []

Boundary Conditions

theorem CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop_zero_eq (P : PKEScheme) (pks : List P.PK) (j : ℕ) (msgs : List (List P.M)) : MI_hybridLoop P pks 0 j msgs = MI_encList P pks j msgs

theorem CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop_full_eq (P : PKEScheme) (pks : List P.PK) (j : ℕ) (msgs : List (List P.M)) {thresh : ℕ} (hi : j + msgs.length ≤ thresh) : MI_hybridLoop P pks thresh j msgs = MI_sampleN P msgs.length msgs

theorem CatCrypt.Examples.PKE.MultiInstance.MI_hybrid_length (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) : MI_hybrid P pks msgs msgs.length = MI_sampleN P msgs.length msgs

theorem CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop_suffix_eq (P : PKEScheme) (pks : List P.PK) (i j : ℕ) (msgs : List (List P.M)) (hj : i ≤ j) : MI_hybridLoop P pks i j msgs = MI_encList P pks j msgs

When threshold ≤ position, MI_hybridLoop encrypts everything.

IsPure Lemmas

theorem CatCrypt.Examples.PKE.MultiInstance.MI_sampleN_isPure (P : PKEScheme) (hP : P.IsPure) (n : ℕ) (msgs : List (List P.M)) : (MI_sampleN P n msgs).IsPure

theorem CatCrypt.Examples.PKE.MultiInstance.MI_encList_isPure (P : PKEScheme) (hP : P.IsPure) (pks : List P.PK) (j : ℕ) (msgs : List (List P.M)) : (MI_encList P pks j msgs).IsPure

Decomposition Lemmas

We decompose `MI_hybridLoop pks (j + k) j msgs` as:
prefix (k ideal instances) + core (at position j + k) + suffix (real instances).

The generalized form over `(j, k)` avoids the "shift" trick, which fails
when public keys are indexed by position (`pks.getD j`). Instead, the IH
works because `(j+1) + k = j + (k+1)` preserves the `pks.getD` index. 

theorem CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop_decomp_real_gen (P : PKEScheme) (pks : List P.PK) (j k : ℕ) (msgs : List (List P.M)) (_hk : k < msgs.length) : MI_hybridLoop P pks (j + k) j msgs = (MI_sampleN P k msgs).bind fun (pre : List (List P.C)) => (MT_CPA_real P (pks.getD (j + k) (defPK P)) (msgs.getD k [])).bind fun (cs : List P.C) => (MI_encList P pks (j + k + 1) (List.drop (k + 1) msgs)).bind fun (suf : List (List P.C)) => Core.SPComp.pure (pre ++ [cs] ++ suf)

Generalized decomposition with real core at position j + k.

theorem CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop_decomp_ideal_gen (P : PKEScheme) (pks : List P.PK) (j k : ℕ) (msgs : List (List P.M)) (_hk : k < msgs.length) : MI_hybridLoop P pks (j + k + 1) j msgs = (MI_sampleN P k msgs).bind fun (pre : List (List P.C)) => (MT_CPA_ideal P (msgs.getD k [])).bind fun (cs : List P.C) => (MI_encList P pks (j + k + 1) (List.drop (k + 1) msgs)).bind fun (suf : List (List P.C)) => Core.SPComp.pure (pre ++ [cs] ++ suf)

Generalized decomposition with ideal core at position j + k.

theorem CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop_decomp_real (P : PKEScheme) (pks : List P.PK) (i : ℕ) (msgs : List (List P.M)) (hi : i < msgs.length) : MI_hybridLoop P pks i 0 msgs = (MI_sampleN P i msgs).bind fun (pre : List (List P.C)) => (MT_CPA_real P (pks.getD i (defPK P)) (msgs.getD i [])).bind fun (cs : List P.C) => (MI_encList P pks (i + 1) (List.drop (i + 1) msgs)).bind fun (suf : List (List P.C)) => Core.SPComp.pure (pre ++ [cs] ++ suf)

Decomposition with real core, specialized to position 0.

theorem CatCrypt.Examples.PKE.MultiInstance.MI_hybridLoop_decomp_ideal (P : PKEScheme) (pks : List P.PK) (i : ℕ) (msgs : List (List P.M)) (hi : i < msgs.length) : MI_hybridLoop P pks (i + 1) 0 msgs = (MI_sampleN P i msgs).bind fun (pre : List (List P.C)) => (MT_CPA_ideal P (msgs.getD i [])).bind fun (cs : List P.C) => (MI_encList P pks (i + 1) (List.drop (i + 1) msgs)).bind fun (suf : List (List P.C)) => Core.SPComp.pure (pre ++ [cs] ++ suf)

Decomposition with ideal core, specialized to position 0.

The SLIDE Adversary (Instance Dimension)

noncomputable def CatCrypt.Examples.PKE.MultiInstance.MI_slideAdv (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) (i : ℕ) (A : List (List P.C) → Core.SPComp Bool) (cs : List P.C) : Core.SPComp Bool

SLIDE adversary for the instance dimension: embeds a single instance's ciphertext list into the multi-instance context.

Equations

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

Per-Step Advantage Bound

theorem CatCrypt.Examples.PKE.MultiInstance.MI_step_eq (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) (i : ℕ) (hi : i < msgs.length) (A : List (List P.C) → Core.SPComp Bool) (hP : P.IsPure) : Crypto.AdvantageA (MI_hybrid P pks msgs i) (MI_hybrid P pks msgs (i + 1)) A = MT_CPA_Advantage P (pks.getD i (defPK P)) (msgs.getD i []) (MI_slideAdv P pks msgs i A)

Per-step advantage equality: adjacent MI hybrids differ by one MT-CPA$ query.

theorem CatCrypt.Examples.PKE.MultiInstance.MI_step_bound (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) (i : ℕ) (hi : i < msgs.length) (A : List (List P.C) → Core.SPComp Bool) (hP : P.IsPure) : Crypto.AdvantageA (MI_hybrid P pks msgs i) (MI_hybrid P pks msgs (i + 1)) A ≤ MT_CPA_Advantage P (pks.getD i (defPK P)) (msgs.getD i []) (MI_slideAdv P pks msgs i A)

Per-step advantage bound (≤ version).

Main Reduction Theorems

theorem CatCrypt.Examples.PKE.MultiInstance.Adv_MI_MT_CPA (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) (ε : ENNReal) (A : List (List P.C) → Core.SPComp Bool) (hP : P.IsPure) (hMT : ∀ i < msgs.length, MT_CPA_Advantage P (pks.getD i (defPK P)) (msgs.getD i []) (MI_slideAdv P pks msgs i A) ≤ ε) : MI_Advantage P pks msgs A ≤ ↑msgs.length * ε

Multi-instance to single-instance reduction (CSF 2025, Case Study 2).

theorem CatCrypt.Examples.PKE.MultiInstance.Adv_MI_direct (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) (ε : ENNReal) (A : List (List P.C) → Core.SPComp Bool) (hstep : ∀ i < msgs.length, Crypto.AdvantageA (MI_hybrid P pks msgs i) (MI_hybrid P pks msgs (i + 1)) A ≤ ε) : MI_Advantage P pks msgs A ≤ ↑msgs.length * ε

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

theorem CatCrypt.Examples.PKE.MultiInstance.Adv_MI_MT_CPA_nested (P : PKEScheme) (pks : List P.PK) (msgs : List (List P.M)) (q : ℕ) (ε : ENNReal) (A : List (List P.C) → Core.SPComp Bool) (hP : P.IsPure) (hMT : ∀ i < msgs.length, MT_CPA_Advantage P (pks.getD i (defPK P)) (msgs.getD i []) (MI_slideAdv P pks msgs i A) ≤ ↑q * ε) : MI_Advantage P pks msgs A ≤ ↑msgs.length * ↑q * ε

Nested hybrid composition (CSF 2025, combining Cases 1 & 2).