Computational observation layer for UC security

This file gives a concrete computational reading of the abstract UC judgments (Emulates, UCSecure) in terms of distributional distinguishing advantage. It deliberately keeps the fixed-ε notion CompEmulates separate from the abstract Emulates-as-equivalence judgment, because the relation fun c₁ c₂ => tvDist (sem c₁) (sem c₂) ≤ ε is not transitive at fixed ε (the triangle inequality only gives 2ε) and therefore cannot be packaged as Observation T. The principled bridge to abstract Emulates lives at the asymptotic level (AsympCompEmulates), where sums of negligibles are still negligible.

Design: bundled sub-probabilistic semantics

A Semantics T bundles:

1. an ambient surface monad m : Type → Type in which closed systems are observed;
2. a SPMFSemantics m factoring computations in m through an internal semantic monad into an externally visible SPMF;
3. a run : T.Closed → m Unit that extracts the probabilistic game associated to each closed system.

The observation target is SPMF Unit, so the resulting denotation carries genuine failure mass. Distinguishing advantage is the total variation distance between the two resulting SPMF Unit distributions. This lets the same framework express:

• coin-flip-only protocols with m = ProbComp and SPMFSemantics.ofHasEvalSPMF ProbComp;
• protocols with shared oracles where m = OracleComp superSpec and the internal semantic monad is StateT σ ProbComp via simulateQ;
• observation-style semantics that deliberately introduce failure, for example by querying with OptionT ProbComp and guard-ing on a predicate over sampled values. This is how OTP-style privacy gets a CompEmulates 0 statement against an SPMF Unit that carries a real failure mass.

Main definitions

• Semantics T bundles a surface monad, its sub-probabilistic semantics, and a run function extracting a game from each closed system.
• Semantics.evalDist is the SPMF Unit denotation of a closed system.
• Semantics.distAdvantage is the total variation distance between two such denotations.
• 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.
• CompUCSecure.toCompEmulates_id: simulator-based security with the identity simulator recovers computational emulation.
• 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 (max 1 u)

Semantics T bundles a computational observation layer for closed systems in the open-composition theory T:

• m is the surface monad in which the observation is written;
• sem is a SPMFSemantics m giving m its sub-probabilistic meaning;
• run extracts a m Unit game from each closed system.

The visible denotation of a closed system is therefore a SPMF Unit, where the none branch records failure mass (for example, a guard that rejected the sampled value). Distinguishing advantage is total variation on those SPMF Unit distributions.

• m : Type → Type

  Surface monad in which closed systems are observed.

• instMonad : Monad self.m

  Monad structure on the surface monad.

• sem : SPMFSemantics self.m

  Bundled sub-probabilistic semantics for the surface monad. The internal semantic monad is kept in Type → Type so that every protocol (ProbComp, OracleComp superSpec, OptionT ProbComp, StateT σ ProbComp) fits uniformly.

• run : T.Closed → self.m Unit

  The probabilistic game extracted from a closed system.

noncomputable def Interaction.UC.Semantics.evalDist {T : OpenTheory} (S : Semantics T) (p : T.Closed) : SPMF Unit

The external SPMF Unit denotation of a closed system under S.

noncomputable def Interaction.UC.Semantics.distAdvantage {T : OpenTheory} (S : Semantics T) (p q : T.Closed) : ℝ

Distinguishing advantage between two closed systems under S, defined as the total variation distance of their SPMF Unit denotations.

@[simp]

theorem Interaction.UC.Semantics.distAdvantage_self {T : OpenTheory} (S : Semantics T) (p : T.Closed) : S.distAdvantage p p = 0

theorem Interaction.UC.Semantics.distAdvantage_comm {T : OpenTheory} (S : Semantics T) (p q : T.Closed) : S.distAdvantage p q = S.distAdvantage q p

theorem Interaction.UC.Semantics.distAdvantage_nonneg {T : OpenTheory} (S : Semantics T) (p q : T.Closed) : 0 ≤ S.distAdvantage p q

theorem Interaction.UC.Semantics.distAdvantage_triangle {T : OpenTheory} (S : Semantics T) (p q r : T.Closed) : S.distAdvantage p r ≤ S.distAdvantage p q + S.distAdvantage q r

theorem Interaction.UC.Semantics.distAdvantage_le_one {T : OpenTheory} (S : Semantics T) (p q : T.Closed) : S.distAdvantage p q ≤ 1

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 total variation distance between the real-world and ideal-world closed-system denotations is at most ε.

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 total variation distance).

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.HasPlugWireFactor] {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.HasPlugWireFactor] {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.HasPlugWireFactor] {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.HasPlugWireFactor] {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.HasPlugWireFactor] {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.HasPlugWireFactor] {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.HasPlugWireFactor] {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.distAdvantage (T.close real K_real) (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).distAdvantage ((T n).close (real n) K) ((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).HasPlugWireFactor] {Δ₁ Δ₂ : 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).HasPlugWireFactor] {Δ₁ Γ Δ₂ : 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).HasPlugWireFactor] {Δ : 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).distAdvantage ((T n).close (real n) (K_real n)) ((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 total variation 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.