Computational observation layer for UC security

This file bridges the abstract UC judgments (Emulates, UCSecure) to concrete computational indistinguishability by instantiating the ObsEq parameter with distributional advantage bounds.

Main definitions

• Semantics T is a function extracting a ProbComp Unit game from each closed system in the theory T. This is the minimal bridge between the structural open-composition layer and the probabilistic crypto layer.

• CompEmulates sem ε real ideal asserts that for every environment (plug), the distinguishing advantage between the real and ideal closed systems is at most ε.

• AsympCompEmulates is the asymptotic variant: for every PPT adversary choosing environments, the advantage is negligible in the security parameter.

• CompUCSecure sem ε protocol ideal SimSpace simulate is the simulator-based variant with bounded advantage.

Main results

• CompEmulates.refl: advantage zero against itself.
• CompEmulates.triangle: transitivity with additive advantage bounds.
• CompEmulates.map_invariance: boundary adaptation preserves the bound.
• CompEmulates.par_compose, wire_compose, plug_compose: advantages add under parallel, wired, and plugged composition.
• CompEmulates.toEmulates: every CompEmulates yields an abstract Emulates for the induced observation relation.
• CompUCSecure.toCompEmulates: simulator-based security implies computational emulation when the simulator is the identity.
• AsympCompEmulates.par_compose, wire_compose, plug_compose: asymptotic composition from pointwise negligible bounds.
• ucDistGame: constructs the SecurityGame whose advantage is the UC distinguishing advantage.
• AsympCompEmulates.iff_secureAgainst: AsympCompEmulates is equivalent to security of the UC distinguishing game.

structure Interaction.UC.Semantics (T : OpenTheory) : Type u

Semantics T extracts a probabilistic game (ProbComp Unit) from each closed system in the open-composition theory T.

The Unit return type matches the convention used by ProbComp.distAdvantage: success is () and failure is ⊥. This is the minimal bridge needed to give computational meaning to the abstract Emulates judgment.

• run : T.Closed → ProbComp Unit

def Interaction.UC.CompEmulates {T : OpenTheory} (sem : Semantics T) (ε : ℝ) {Δ : PortBoundary} (real ideal : T.Obj Δ) : Prop

CompEmulates sem ε real ideal asserts that real computationally emulates ideal up to advantage ε under semantics sem.

For every plug K : T.Plug Δ, the distinguishing advantage between the real-world and ideal-world closed executions is at most ε.

def Interaction.UC.compObsEq {T : OpenTheory} (sem : Semantics T) (ε : ℝ) : T.Closed → T.Closed → Prop

The observation relation on closed systems induced by a semantics and an advantage bound: two closed systems are related when their distinguishing advantage is at most ε.

theorem Interaction.UC.CompEmulates.toEmulates {T : OpenTheory} {sem : Semantics T} {ε : ℝ} {Δ : PortBoundary} {real ideal : T.Obj Δ} (h : CompEmulates sem ε real ideal) : Emulates real ideal (compObsEq sem ε)

CompEmulates is an instance of abstract Emulates for the observation relation compObsEq sem ε.

theorem Interaction.UC.CompEmulates.refl {T : OpenTheory} (sem : Semantics T) {Δ : PortBoundary} (W : T.Obj Δ) : CompEmulates sem 0 W W

Every system computationally emulates itself with advantage zero.

theorem Interaction.UC.CompEmulates.triangle {T : OpenTheory} {sem : Semantics T} {ε₁ ε₂ : ℝ} {Δ : PortBoundary} {W₁ W₂ W₃ : T.Obj Δ} (h₁₂ : CompEmulates sem ε₁ W₁ W₂) (h₂₃ : CompEmulates sem ε₂ W₂ W₃) : CompEmulates sem (ε₁ + ε₂) W₁ W₃

Computational emulation composes transitively with additive advantage bounds (triangle inequality on distinguishing advantage).

theorem Interaction.UC.CompEmulates.map_invariance {T : OpenTheory} [T.IsLawfulPlug] {sem : Semantics T} {ε : ℝ} {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) {real ideal : T.Obj Δ₁} (h : CompEmulates sem ε real ideal) : CompEmulates sem ε (T.map f real) (T.map f ideal)

Adapting both sides of a computational emulation along the same boundary morphism preserves the advantage bound.

This is the computational specialization of Emulates.map_invariance. The key identity is plug (map f W) K = plug W (map (swap f) K).

theorem Interaction.UC.CompEmulates.mono {T : OpenTheory} {sem : Semantics T} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) {Δ : PortBoundary} {real ideal : T.Obj Δ} (h : CompEmulates sem ε₁ real ideal) : CompEmulates sem ε₂ real ideal

Weakening: if ε₁ ≤ ε₂ then CompEmulates sem ε₁ implies CompEmulates sem ε₂.

Composition

theorem Interaction.UC.CompEmulates.par_left {T : OpenTheory} [T.CompactClosed] {sem : Semantics T} {ε : ℝ} {Δ₁ Δ₂ : PortBoundary} {real₁ ideal₁ : T.Obj Δ₁} (h₁ : CompEmulates sem ε real₁ ideal₁) (W₂ : T.Obj Δ₂) : CompEmulates sem ε (T.par real₁ W₂) (T.par ideal₁ W₂)

Replacing the left component of a parallel composition preserves the computational emulation bound.

theorem Interaction.UC.CompEmulates.par_right {T : OpenTheory} [T.CompactClosed] {sem : Semantics T} {ε : ℝ} {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) {real₂ ideal₂ : T.Obj Δ₂} (h₂ : CompEmulates sem ε real₂ ideal₂) : CompEmulates sem ε (T.par W₁ real₂) (T.par W₁ ideal₂)

Replacing the right component of a parallel composition preserves the computational emulation bound.

theorem Interaction.UC.CompEmulates.par_compose {T : OpenTheory} [T.CompactClosed] {sem : Semantics T} {ε₁ ε₂ : ℝ} {Δ₁ Δ₂ : PortBoundary} {real₁ ideal₁ : T.Obj Δ₁} {real₂ ideal₂ : T.Obj Δ₂} (h₁ : CompEmulates sem ε₁ real₁ ideal₁) (h₂ : CompEmulates sem ε₂ real₂ ideal₂) : CompEmulates sem (ε₁ + ε₂) (T.par real₁ real₂) (T.par ideal₁ ideal₂)

Computational UC composition for par: advantages add.

theorem Interaction.UC.CompEmulates.wire_left {T : OpenTheory} [T.CompactClosed] {sem : Semantics T} {ε : ℝ} {Δ₁ Γ Δ₂ : PortBoundary} {real₁ ideal₁ : T.Obj (Δ₁.tensor Γ)} (h₁ : CompEmulates sem ε real₁ ideal₁) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : CompEmulates sem ε (T.wire real₁ W₂) (T.wire ideal₁ W₂)

Replacing the left factor of a wiring preserves the computational emulation bound.

theorem Interaction.UC.CompEmulates.wire_right {T : OpenTheory} [T.CompactClosed] {sem : Semantics T} {ε : ℝ} {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) {real₂ ideal₂ : T.Obj (Γ.swap.tensor Δ₂)} (h₂ : CompEmulates sem ε real₂ ideal₂) : CompEmulates sem ε (T.wire W₁ real₂) (T.wire W₁ ideal₂)

Replacing the right factor of a wiring preserves the computational emulation bound.

theorem Interaction.UC.CompEmulates.wire_compose {T : OpenTheory} [T.CompactClosed] {sem : Semantics T} {ε₁ ε₂ : ℝ} {Δ₁ Γ Δ₂ : PortBoundary} {real₁ ideal₁ : T.Obj (Δ₁.tensor Γ)} {real₂ ideal₂ : T.Obj (Γ.swap.tensor Δ₂)} (h₁ : CompEmulates sem ε₁ real₁ ideal₁) (h₂ : CompEmulates sem ε₂ real₂ ideal₂) : CompEmulates sem (ε₁ + ε₂) (T.wire real₁ real₂) (T.wire ideal₁ ideal₂)

Computational UC composition for wire: advantages add.

theorem Interaction.UC.CompEmulates.plug_compose {T : OpenTheory} [T.CompactClosed] {sem : Semantics T} {ε₁ ε₂ : ℝ} {Δ : PortBoundary} {real ideal : T.Obj Δ} {K_real K_ideal : T.Obj Δ.swap} (hProt : CompEmulates sem ε₁ real ideal) (hEnv : CompEmulates sem ε₂ K_real K_ideal) : (sem.run (T.close real K_real)).distAdvantage (sem.run (T.close ideal K_ideal)) ≤ ε₁ + ε₂

Computational UC composition for plug: when both the protocol and the environment emulate their ideals, the advantage of the closed real system vs. closed ideal system is bounded by the sum.

Simulator-based computational UC security

def Interaction.UC.CompUCSecure {T : OpenTheory} (sem : Semantics T) (ε : ℝ) {Δ : PortBoundary} (protocol ideal : T.Obj Δ) (SimSpace : Type u_1) (simulate : SimSpace → T.Plug Δ → T.Plug Δ) : Prop

CompUCSecure sem ε protocol ideal SimSpace simulate is the simulator-based UC security statement with bounded advantage.

There exists a simulator parameter s : SimSpace such that for every context K, the distinguishing advantage between the real execution and the simulated ideal execution is at most ε.

theorem Interaction.UC.CompEmulates.toCompUCSecure {T : OpenTheory} {sem : Semantics T} {ε : ℝ} {Δ : PortBoundary} {protocol ideal : T.Obj Δ} (h : CompEmulates sem ε protocol ideal) : CompUCSecure sem ε protocol ideal PUnit.{u_1 + 1} fun (x : PUnit.{u_1 + 1}) (K : T.Plug Δ) => K

Computational emulation implies simulator-based UC security with the trivial (identity) simulator.

theorem Interaction.UC.CompUCSecure.toCompEmulates_id {T : OpenTheory} {sem : Semantics T} {ε : ℝ} {Δ : PortBoundary} {protocol ideal : T.Obj Δ} (hSec : CompUCSecure sem ε protocol ideal PUnit.{u_1 + 1} fun (x : PUnit.{u_1 + 1}) (K : T.Plug Δ) => K) : CompEmulates sem ε protocol ideal

Simulator-based UC security with identity simulation recovers computational emulation.

Asymptotic computational emulation

def Interaction.UC.AsympCompEmulates (T : ℕ → OpenTheory) (sem : (n : ℕ) → Semantics (T n)) {Δ : PortBoundary} (real ideal : (n : ℕ) → (T n).Obj Δ) (Adv : Type u_1) (isPPT : Adv → Prop) (env : Adv → (n : ℕ) → (T n).Plug Δ) : Prop

AsympCompEmulates is the asymptotic version of computational emulation.

Given a family of theories T n indexed by security parameter n : ℕ, with corresponding semantics, real/ideal systems, and adversary-chosen environments, this asserts that every PPT adversary has negligible distinguishing advantage.

theorem Interaction.UC.AsympCompEmulates.of_pointwise_bound {T : ℕ → OpenTheory} {sem : (n : ℕ) → Semantics (T n)} {Δ : PortBoundary} {real ideal : (n : ℕ) → (T n).Obj Δ} {Adv : Type u_1} {isPPT : Adv → Prop} {env : Adv → (n : ℕ) → (T n).Plug Δ} (f : ℕ → ENNReal) (hf : negligible f) (hbound : ∀ (_A : Adv) (n : ℕ) (K : (T n).Plug Δ), ENNReal.ofReal (((sem n).run ((T n).close (real n) K)).distAdvantage ((sem n).run ((T n).close (ideal n) K))) ≤ f n) : AsympCompEmulates T sem real ideal Adv isPPT env

Pointwise bounded advantage implies asymptotic security: if at each security parameter the advantage is bounded by f n, and f is negligible, then the asymptotic emulation holds (for any adversary class).

theorem Interaction.UC.AsympCompEmulates.of_compEmulates {T : ℕ → OpenTheory} {sem : (n : ℕ) → Semantics (T n)} {Δ : PortBoundary} {real ideal : (n : ℕ) → (T n).Obj Δ} {Adv : Type u_1} {isPPT : Adv → Prop} {env : Adv → (n : ℕ) → (T n).Plug Δ} (ε : ℕ → ℝ) (hε : negligible fun (n : ℕ) => ENNReal.ofReal (ε n)) (hComp : ∀ (n : ℕ), CompEmulates (sem n) (ε n) (real n) (ideal n)) : AsympCompEmulates T sem real ideal Adv isPPT env

Convert a family of pointwise CompEmulates bounds into an asymptotic statement when the bound function is negligible.

Asymptotic composition

theorem Interaction.UC.AsympCompEmulates.par_compose {T : ℕ → OpenTheory} {sem : (n : ℕ) → Semantics (T n)} [(n : ℕ) → (T n).CompactClosed] {Δ₁ Δ₂ : PortBoundary} {real₁ ideal₁ : (n : ℕ) → (T n).Obj Δ₁} {real₂ ideal₂ : (n : ℕ) → (T n).Obj Δ₂} {Adv : Type u_1} {isPPT : Adv → Prop} {env : Adv → (n : ℕ) → (T n).Plug (Δ₁.tensor Δ₂)} (ε₁ ε₂ : ℕ → ℝ) (hε₁ : negligible fun (n : ℕ) => ENNReal.ofReal (ε₁ n)) (hε₂ : negligible fun (n : ℕ) => ENNReal.ofReal (ε₂ n)) (h₁ : ∀ (n : ℕ), CompEmulates (sem n) (ε₁ n) (real₁ n) (ideal₁ n)) (h₂ : ∀ (n : ℕ), CompEmulates (sem n) (ε₂ n) (real₂ n) (ideal₂ n)) : AsympCompEmulates T sem (fun (n : ℕ) => (T n).par (real₁ n) (real₂ n)) (fun (n : ℕ) => (T n).par (ideal₁ n) (ideal₂ n)) Adv isPPT env

Asymptotic UC composition for par: if each component's pointwise advantage is negligible, then the parallel composition also has negligible advantage.

theorem Interaction.UC.AsympCompEmulates.wire_compose {T : ℕ → OpenTheory} {sem : (n : ℕ) → Semantics (T n)} [(n : ℕ) → (T n).CompactClosed] {Δ₁ Γ Δ₂ : PortBoundary} {real₁ ideal₁ : (n : ℕ) → (T n).Obj (Δ₁.tensor Γ)} {real₂ ideal₂ : (n : ℕ) → (T n).Obj (Γ.swap.tensor Δ₂)} {Adv : Type u_1} {isPPT : Adv → Prop} {env : Adv → (n : ℕ) → (T n).Plug (Δ₁.tensor Δ₂)} (ε₁ ε₂ : ℕ → ℝ) (hε₁ : negligible fun (n : ℕ) => ENNReal.ofReal (ε₁ n)) (hε₂ : negligible fun (n : ℕ) => ENNReal.ofReal (ε₂ n)) (h₁ : ∀ (n : ℕ), CompEmulates (sem n) (ε₁ n) (real₁ n) (ideal₁ n)) (h₂ : ∀ (n : ℕ), CompEmulates (sem n) (ε₂ n) (real₂ n) (ideal₂ n)) : AsympCompEmulates T sem (fun (n : ℕ) => (T n).wire (real₁ n) (real₂ n)) (fun (n : ℕ) => (T n).wire (ideal₁ n) (ideal₂ n)) Adv isPPT env

Asymptotic UC composition for wire: if each factor's pointwise advantage is negligible, then the wired composition also has negligible advantage.

theorem Interaction.UC.AsympCompEmulates.plug_compose {T : ℕ → OpenTheory} {sem : (n : ℕ) → Semantics (T n)} [(n : ℕ) → (T n).CompactClosed] {Δ : PortBoundary} {real ideal : (n : ℕ) → (T n).Obj Δ} {K_real K_ideal : (n : ℕ) → (T n).Obj Δ.swap} (ε₁ ε₂ : ℕ → ℝ) (hε₁ : negligible fun (n : ℕ) => ENNReal.ofReal (ε₁ n)) (hε₂ : negligible fun (n : ℕ) => ENNReal.ofReal (ε₂ n)) (hProt : ∀ (n : ℕ), CompEmulates (sem n) (ε₁ n) (real n) (ideal n)) (hEnv : ∀ (n : ℕ), CompEmulates (sem n) (ε₂ n) (K_real n) (K_ideal n)) : negligible fun (n : ℕ) => ENNReal.ofReal (((sem n).run ((T n).close (real n) (K_real n))).distAdvantage ((sem n).run ((T n).close (ideal n) (K_ideal n))))

Asymptotic UC composition for plug: if both the protocol and the environment have negligible pointwise advantages, then the distinguishing advantage of the closed real vs. closed ideal system is negligible.

Bridge to SecurityGame

noncomputable def Interaction.UC.ucDistGame (T : ℕ → OpenTheory) (sem : (n : ℕ) → Semantics (T n)) {Δ : PortBoundary} (real ideal : (n : ℕ) → (T n).Obj Δ) {Adv : Type u_1} (env : Adv → (n : ℕ) → (T n).Plug Δ) : SecurityGame Adv

The UC distinguishing game: a SecurityGame whose advantage at adversary A and security parameter n is the distributional distance between the real and ideal closed executions under the environment chosen by A.

theorem Interaction.UC.AsympCompEmulates.iff_secureAgainst {T : ℕ → OpenTheory} {sem : (n : ℕ) → Semantics (T n)} {Δ : PortBoundary} {real ideal : (n : ℕ) → (T n).Obj Δ} {Adv : Type u_1} {isPPT : Adv → Prop} {env : Adv → (n : ℕ) → (T n).Plug Δ} : AsympCompEmulates T sem real ideal Adv isPPT env ↔ (ucDistGame T sem real ideal env).secureAgainst isPPT

AsympCompEmulates is exactly secureAgainst isPPT for the UC distinguishing game. This is definitional.

theorem Interaction.UC.ucDistGame_secureAgainst_of_asympCompEmulates {T : ℕ → OpenTheory} {sem : (n : ℕ) → Semantics (T n)} {Δ : PortBoundary} {real ideal : (n : ℕ) → (T n).Obj Δ} {Adv : Type u_1} {isPPT : Adv → Prop} {env : Adv → (n : ℕ) → (T n).Plug Δ} (h : AsympCompEmulates T sem real ideal Adv isPPT env) : (ucDistGame T sem real ideal env).secureAgainst isPPT

If real UC-emulates ideal, then the UC distinguishing game is secure against any adversary class. Uses the SecurityGame.secureAgainst vocabulary.

theorem Interaction.UC.SecurityGame.secureAgainst_of_ucEmulation {T : ℕ → OpenTheory} {sem : (n : ℕ) → Semantics (T n)} {Δ : PortBoundary} {real ideal : (n : ℕ) → (T n).Obj Δ} {Adv : Type u_1} {Adv' : Type u_2} {isPPT : Adv → Prop} {isPPT' : Adv' → Prop} {env : Adv' → (n : ℕ) → (T n).Plug Δ} {g : SecurityGame Adv} {reduce : Adv → Adv'} (hreduce : ∀ (A : Adv), isPPT A → isPPT' (reduce A)) (hbound : ∀ (A : Adv) (n : ℕ), g.advantage A n ≤ (ucDistGame T sem real ideal env).advantage (reduce A) n) (hUC : AsympCompEmulates T sem real ideal Adv' isPPT' env) : g.secureAgainst isPPT

UC security reduction: if security of g₁ reduces to UC-emulation of real by ideal, then g₁ is secure whenever UC-emulation holds.

This bridges SecurityGame.secureAgainst_of_reduction to the UC setting: given a reduction from a standard security game to the UC distinguishing game, UC-emulation implies security of the original game.