Universal Composability (UC) Security

This file defines UC security at Level 1 (information-theoretic): no complexity bounds.

Main definitions

• UCSpec — specification of UC interfaces (honest, output, leak, sim_if, view)
• mapSum — parallel composition on Sum (= tensor in KlSPComp)
• realWorld, idealWorld — real and ideal world executions
• UCEmulates — UC emulation with statistical error ε
• UCEmulatesPerfect — perfect UC emulation (ε = 0)

Main results

• mapSum_pure_left — mapSum pure g (.inl a) = pure (.inl a)
• UCEmulates_of_sdist — same-interface: sdist ≤ ε → UCEmulates ε
• UCEmulates_of_dummy — dummy adversary sufficiency
• UCEmulates_trans — transitivity (same-interface, via simulator chaining)

UC vs sdist

UC emulation (Canetti-style ∀ A ∃ S) is strictly weaker than sdist ≤ ε. The implication sdist ≤ ε → UCEmulates ε holds (take S = A), but the reverse is false because the simulator can transform the leak channel. (The robust-hyperproperty (RHP) equivalence is developed separately.)

Sub-SMC structure (same-interface case)

When leak = sim_if (same adversary interface), UC emulation inherits the sub-SMC structure from sdist:

• UCEmulates_refl — identity: any protocol emulates itself
• UCEmulates_trans — composition: simulator chaining gives additive bounds
• Tensor: follows from sdist_mapSum_le via UCEmulates_of_sdist

For the general case (different interfaces), the categorical structure is richer — it involves a 2-categorical notion where simulators are 2-cells.

Concurrent UC (forthcoming)

This file provides single-shot, non-interactive UC emulation. The concurrent (reactive) layer — UCEmulatesConcurrent* over the ITreeN interaction-tree monad, with the Kantorovich-distance and stateful variants — will be included in core in a forthcoming revision; it currently lives in the parent development under CatCrypt/Crypto/UCMonad/.

UC Specification

structure CatCrypt.Crypto.UCSpec : Type (max (max (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1)) (u_4 + 1)) (u_5 + 1))

A UC specification bundles the types of the various interfaces.

• hon : honest input interface
• out : honest output interface
• leak : adversary interface (real world leakage)
• sim_if : simulator interface (ideal world)
• view : adversary/simulator observable output

• hon : Type u_1
• out : Type u_2
• leak : Type u_3
• sim_if : Type u_4
• view : Type u_5

Parallel Composition on Sum

noncomputable def CatCrypt.Crypto.mapSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → Core.SPComp β) (g : γ → Core.SPComp δ) : α ⊕ γ → Core.SPComp (β ⊕ δ)

Concrete parallel composition on Sum (= tensor ⊗ in KlSPComp). Applies f on .inl and g on .inr.

Equations

• CatCrypt.Crypto.mapSum f g (Sum.inl a) = CatCrypt.Core.SPComp.map Sum.inl (f a)
• CatCrypt.Crypto.mapSum f g (Sum.inr c) = CatCrypt.Core.SPComp.map Sum.inr (g c)

@[simp]

theorem CatCrypt.Crypto.mapSum_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → Core.SPComp β) (g : γ → Core.SPComp δ) (a : α) : mapSum f g (Sum.inl a) = Core.SPComp.map Sum.inl (f a)

@[simp]

theorem CatCrypt.Crypto.mapSum_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → Core.SPComp β) (g : γ → Core.SPComp δ) (c : γ) : mapSum f g (Sum.inr c) = Core.SPComp.map Sum.inr (g c)

@[simp]

theorem CatCrypt.Crypto.mapSum_pure_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → Core.SPComp γ) (a : α) : mapSum Core.SPComp.pure g (Sum.inl a) = Core.SPComp.pure (Sum.inl a)

@[simp]

theorem CatCrypt.Crypto.mapSum_pure_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Core.SPComp β) (c : γ) : mapSum f Core.SPComp.pure (Sum.inr c) = Core.SPComp.pure (Sum.inr c)

@[simp]

theorem CatCrypt.Crypto.mapSum_pure_pure {α : Type u_1} {β : Type u_2} : mapSum Core.SPComp.pure Core.SPComp.pure = Core.SPComp.pure

mapSum pure pure = pure (identity on Sum).

theorem CatCrypt.Crypto.mapSum_eq_tensorHom {α₁ α₂ β₁ β₂ : Type} (f : α₁ → Core.SPComp α₂) (g : β₁ → Core.SPComp β₂) : mapSum f g = fun (x : have this := α₁ ⊕ β₁; this) => (Core.KlSPComp.wkR f β₁ x).bind (Core.KlSPComp.wkL α₂ g)

mapSum f g equals the KlSPComp tensor product wkR f ≫ wkL g.

Real and Ideal Worlds

noncomputable def CatCrypt.Crypto.realWorld (spec : UCSpec) (π : spec.hon → Core.SPComp (spec.out ⊕ spec.leak)) (A : spec.leak → Core.SPComp spec.view) (Z : spec.out ⊕ spec.view → Core.SPComp Bool) : spec.hon → Core.SPComp Bool

Real world: Z ∘ₖ (id ⊕ A) ∘ₖ π.

Equations

• CatCrypt.Crypto.realWorld spec π A Z a = ((π a).bind (CatCrypt.Crypto.mapSum CatCrypt.Core.SPComp.pure A)).bind Z

noncomputable def CatCrypt.Crypto.idealWorld (spec : UCSpec) (F : spec.hon → Core.SPComp (spec.out ⊕ spec.sim_if)) (S : spec.sim_if → Core.SPComp spec.view) (Z : spec.out ⊕ spec.view → Core.SPComp Bool) : spec.hon → Core.SPComp Bool

Ideal world: Z ∘ₖ (id ⊕ S) ∘ₖ F.

Equations

• CatCrypt.Crypto.idealWorld spec F S Z a = ((F a).bind (CatCrypt.Crypto.mapSum CatCrypt.Core.SPComp.pure S)).bind Z

UC Emulation

def CatCrypt.Crypto.UCEmulates (ε : ENNReal) (spec : UCSpec) (π : spec.hon → Core.SPComp (spec.out ⊕ spec.leak)) (F : spec.hon → Core.SPComp (spec.out ⊕ spec.sim_if)) : Prop

Protocol π UC-emulates ideal functionality F with statistical error ε.

For ALL adversaries A, there EXISTS a simulator S such that the sdist of the post-adversary views is ≤ ε. The environment Z is absorbed into sdist's distinguisher supremum.

Equations

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

def CatCrypt.Crypto.UCEmulatesPerfect (spec : UCSpec) (π : spec.hon → Core.SPComp (spec.out ⊕ spec.leak)) (F : spec.hon → Core.SPComp (spec.out ⊕ spec.sim_if)) : Prop

Perfect UC emulation: ε = 0.

Equations

• CatCrypt.Crypto.UCEmulatesPerfect spec π F = CatCrypt.Crypto.UCEmulates 0 spec π F

Basic Theorems

theorem CatCrypt.Crypto.UCEmulates_of_sdist {out : Type u_1} {leak : Type u_2} (ε : ENNReal) {view : Type u_3} {hon : Type u_4} (π F : hon → Core.SPComp (out ⊕ leak)) (h : sdist π F ≤ ε) : UCEmulates ε { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π F

Same-interface UC: if sdist π F ≤ ε, then UCEmulates ε with S = A. When leak = sim_if, the simulator is just the adversary itself.

theorem CatCrypt.Crypto.UCEmulates_mono {spec : UCSpec} {π : spec.hon → Core.SPComp (spec.out ⊕ spec.leak)} {F : spec.hon → Core.SPComp (spec.out ⊕ spec.sim_if)} {ε₁ ε₂ : ENNReal} (h : UCEmulates ε₁ spec π F) (hle : ε₁ ≤ ε₂) : UCEmulates ε₂ spec π F

Monotonicity: UC emulation with tighter bound implies looser bound.

theorem CatCrypt.Crypto.UCEmulates_of_dummy {hon : Type u_1} {out : Type u_2} {leak : Type u_3} (ε : ENNReal) (π F : hon → Core.SPComp (out ⊕ leak)) (h : sdist π F ≤ ε) (view : Type u_4) (A : leak → Core.SPComp view) : ∃ (S : leak → Core.SPComp view), (sdist (fun (a : hon) => (π a).bind (mapSum Core.SPComp.pure A)) fun (a : hon) => (F a).bind (mapSum Core.SPComp.pure S)) ≤ ε

Dummy adversary sufficiency (same-interface case: view = leak).

If UC holds against the identity adversary, it holds against ALL adversaries. The key idea: given adversary A, absorb it into the distinguisher.

theorem CatCrypt.Crypto.UCEmulates_refl {hon : Type u_1} {out : Type u_2} {leak : Type u_3} {view : Type u_4} (π : hon → Core.SPComp (out ⊕ leak)) : UCEmulates 0 { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π π

Reflexivity: any protocol UC-emulates itself perfectly (same-interface).

theorem CatCrypt.Crypto.UCEmulates_trans {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 } π₁ π₃

Transitivity of UC emulation (same-interface case).

Given adversary A, chain simulators: h₁ gives S₁ for A, h₂ gives S₂ for S₁. The triangle inequality on sdist gives the additive bound. This is the composition property for the UC sub-SMC.

Heterogeneous Transitivity

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

Heterogeneous transitivity: compose UC bounds across different leak types. Given π₁ ──UC(ε₁)──▶ π₂ (leak₁ → leak₂) and π₂ ──UC(ε₂)──▶ π₃ (leak₂ → sim_if), we get π₁ ──UC(ε₁+ε₂)──▶ π₃ (leak₁ → sim_if). The middle type leak₂ is consumed.

theorem CatCrypt.Crypto.UCEmulates_trans_hetero₃ {hon : Type u_1} {out : Type u_2} {l₁ : Type u_3} {l₂ : Type u_4} {l₃ : Type u_5} {sim : Type u_6} {view : Type u_7} {ε₁ ε₂ ε₃ : ENNReal} {π₁ : hon → Core.SPComp (out ⊕ l₁)} {π₂ : hon → Core.SPComp (out ⊕ l₂)} {π₃ : hon → Core.SPComp (out ⊕ l₃)} {π₄ : hon → Core.SPComp (out ⊕ sim)} (h₁ : UCEmulates ε₁ { hon := hon, out := out, leak := l₁, sim_if := l₂, view := view } π₁ π₂) (h₂ : UCEmulates ε₂ { hon := hon, out := out, leak := l₂, sim_if := l₃, view := view } π₂ π₃) (h₃ : UCEmulates ε₃ { hon := hon, out := out, leak := l₃, sim_if := sim, view := view } π₃ π₄) : UCEmulates (ε₁ + ε₂ + ε₃) { hon := hon, out := out, leak := l₁, sim_if := sim, view := view } π₁ π₄

Heterogeneous transitivity for 3-step pipelines.

Oracle-Game UC Emulation

def CatCrypt.Crypto.GameUCEmulates (ε : ENNReal) {OracleIf : Type u_1} (G_real G_ideal : (OracleIf → Core.SPComp Bool) → Core.SPComp Bool) : Prop

UC emulation for oracle-based (interactive) games.

Many cryptographic security definitions give the adversary oracle access to a set of operations (e.g., encryption, decryption, key generation). The game constructs the oracles and hands them to the adversary, who produces a distinguishing bit.

GameUCEmulates ε G_real G_ideal says that no adversary can distinguish the real game from the ideal game with advantage greater than ε.

This generalizes UCEmulates to the reactive/oracle setting where the adversary interacts via multiple adaptive queries rather than receiving a single output.

Equations

• CatCrypt.Crypto.GameUCEmulates ε G_real G_ideal = ∀ (A : OracleIf → CatCrypt.Core.SPComp Bool), CatCrypt.Crypto.Advantage (G_real A) (G_ideal A) ≤ ε

theorem CatCrypt.Crypto.GameUCEmulates_refl {OracleIf : Type u_1} (G : (OracleIf → Core.SPComp Bool) → Core.SPComp Bool) : GameUCEmulates 0 G G

Reflexivity: any game trivially emulates itself.

theorem CatCrypt.Crypto.GameUCEmulates_mono {OracleIf : Type u_1} {G_real G_ideal : (OracleIf → Core.SPComp Bool) → Core.SPComp Bool} {ε₁ ε₂ : ENNReal} (h : GameUCEmulates ε₁ G_real G_ideal) (hle : ε₁ ≤ ε₂) : GameUCEmulates ε₂ G_real G_ideal

Monotonicity: tighter bound implies looser bound.

theorem CatCrypt.Crypto.GameUCEmulates_trans {OracleIf : Type u_1} {G₁ G₂ G₃ : (OracleIf → Core.SPComp Bool) → Core.SPComp Bool} {ε₁ ε₂ : ENNReal} (h₁ : GameUCEmulates ε₁ G₁ G₂) (h₂ : GameUCEmulates ε₂ G₂ G₃) : GameUCEmulates (ε₁ + ε₂) G₁ G₃

Transitivity via triangle inequality.

theorem CatCrypt.Crypto.GameUCEmulates_sym {OracleIf : Type u_1} {G_real G_ideal : (OracleIf → Core.SPComp Bool) → Core.SPComp Bool} {ε : ENNReal} (h : GameUCEmulates ε G_real G_ideal) : GameUCEmulates ε G_ideal G_real

Symmetry: swapping real and ideal preserves the bound.