UC Subroutine Composition

This file proves the UC subroutine composition theorem: if protocol π is sdist-close to functionality F, and subroutine ρ_real is sdist-close to ρ_ideal, then the compiled protocol compile π ρ_real is sdist-close to compile F ρ_ideal with error ε₁ + ε₂. UC emulation follows via UCEmulates_of_sdist.

Main results

• sdist_compile — compile preserves sdist bounds additively
• sdist_compile_same — compile with same subroutine preserves sdist
• UCEmulates_compile — UC composition via compile + sdist
• UCEmulates_seq — sequential composition (re-export of UCEmulates_trans)
• UCEmulates_par — parallel composition (re-export of UCEmulates_mapSum_of_sdist)

Proof strategy

The proof uses the triangle inequality:

1. sdist(compile π ρ_real, compile π ρ_ideal) ≤ ε₂ by left PPL on subroutine
2. sdist(compile π ρ_ideal, compile F ρ_ideal) ≤ ε₁ by right PPL on protocol

References

• Canetti, Universally Composable Security, 2001
• Patrignani et al., UC is RC, TOPLAS 2024

Compile Distance Bounds

theorem CatCrypt.Crypto.UCComposition.sdist_compile_same {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : ENNReal} (π F : α → Core.SPComp (β ⊕ γ)) (ρ : γ → Core.SPComp δ) (hπ : sdist π F ≤ ε) : sdist (compile π ρ) (compile F ρ) ≤ ε

Compile with same subroutine: sdist is preserved.

theorem CatCrypt.Crypto.UCComposition.sdist_compile {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε₁ ε₂ : ENNReal} (π F : α → Core.SPComp (β ⊕ γ)) (ρ_real ρ_ideal : γ → Core.SPComp δ) (hπ : sdist π F ≤ ε₁) (hρ : sdist ρ_real ρ_ideal ≤ ε₂) : sdist (compile π ρ_real) (compile F ρ_ideal) ≤ ε₁ + ε₂

Compile with different subroutines: sdist bounds are additive.

Triangle through compile π ρ_ideal:

• sdist(compile π ρ_real, compile π ρ_ideal) ≤ ε₂ (subroutine swap)
• sdist(compile π ρ_ideal, compile F ρ_ideal) ≤ ε₁ (protocol swap)

UC Emulation via Compile

theorem CatCrypt.Crypto.UCComposition.UCEmulates_compile {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {V : Type u_5} {ε₁ ε₂ : ENNReal} (π F : α → Core.SPComp (β ⊕ γ)) (ρ_real ρ_ideal : γ → Core.SPComp δ) (hπ : sdist π F ≤ ε₁) (hρ : sdist ρ_real ρ_ideal ≤ ε₂) : UCEmulates (ε₁ + ε₂) { hon := α, out := β, leak := δ, sim_if := δ, view := V } (compile π ρ_real) (compile F ρ_ideal)

UC Subroutine Composition (same-interface).

The compiled protocol compile π ρ_real UC-emulates compile F ρ_ideal with error ε₁ + ε₂, using leak = sim_if = δ (same adversary interface).

Since compile outputs α → SPComp (β ⊕ δ), the natural UC spec has out = β and leak = sim_if = δ.

theorem CatCrypt.Crypto.UCComposition.UCEmulates_compile_same_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {V : Type u_5} {ε : ENNReal} (π F : α → Core.SPComp (β ⊕ γ)) (ρ : γ → Core.SPComp δ) (hπ : sdist π F ≤ ε) : UCEmulates ε { hon := α, out := β, leak := δ, sim_if := δ, view := V } (compile π ρ) (compile F ρ)

Same subroutine UC: compile with same subroutine preserves UC bound.

theorem CatCrypt.Crypto.UCComposition.UCEmulates_compile_perfect {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {V : Type u_5} {ε : ENNReal} (π F : α → Core.SPComp (β ⊕ γ)) (ρ : γ → Core.SPComp δ) (hπ : sdist π F ≤ ε) : UCEmulates ε { hon := α, out := β, leak := δ, sim_if := δ, view := V } (compile π ρ) (compile F ρ)

Perfect subroutine: when ρ_real = ρ_ideal, only protocol gap matters.

Sequential and Parallel Composition

theorem CatCrypt.Crypto.UCComposition.UCEmulates_seq {hon : Type u_1} {out : Type u_2} {leak : Type u_3} {view : Type u_4} {ε₁ ε₂ : ENNReal} {π₁ π₂ π₃ : hon → Core.SPComp (out ⊕ leak)} (h₁ : UCEmulates ε₁ { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₁ π₂) (h₂ : UCEmulates ε₂ { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₂ π₃) : UCEmulates (ε₁ + ε₂) { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₁ π₃

Sequential composition: if π₁ → π₂ (ε₁) and π₂ → π₃ (ε₂), then π₁ → π₃ (ε₁ + ε₂). Re-exported from UCEmulates_trans.

theorem CatCrypt.Crypto.UCComposition.UCEmulates_par {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {V : Type u_5} {ε₁ ε₂ : ENNReal} (π₁ F₁ : α₁ → Core.SPComp β₁) (π₂ F₂ : α₂ → Core.SPComp β₂) (h₁ : sdist π₁ F₁ ≤ ε₁) (h₂ : sdist π₂ F₂ ≤ ε₂) : UCEmulates (max ε₁ ε₂) { hon := α₁ ⊕ α₂, out := Unit, leak := β₁ ⊕ β₂, sim_if := β₁ ⊕ β₂, view := V } (fun (x : { hon := α₁ ⊕ α₂, out := Unit, leak := β₁ ⊕ β₂, sim_if := β₁ ⊕ β₂, view := V }.hon) => (mapSum π₁ π₂ x).bind fun (o : β₁ ⊕ β₂) => Core.SPComp.pure (Sum.inr o)) fun (x : { hon := α₁ ⊕ α₂, out := Unit, leak := β₁ ⊕ β₂, sim_if := β₁ ⊕ β₂, view := V }.hon) => (mapSum F₁ F₂ x).bind fun (o : β₁ ⊕ β₂) => Core.SPComp.pure (Sum.inr o)

Parallel composition: max(ε₁, ε₂) bound on coproduct. Re-exported from UCEmulates_mapSum_of_sdist.