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 ObservedCompEmulates 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 (AsympObservedCompEmulates), 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 result type observed at the closed-system boundary;
4. a run : T.Closed → m Result that extracts the probabilistic game associated to each closed system.

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

• coin-flip-only protocols with m = ProbComp and SPMFSemantics.ofMonadLift 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 ObservedCompEmulates 0 statement against an SPMF Unit that carries a real failure mass.

Main definitions

• Semantics T bundles a result type, a surface monad, its sub-probabilistic semantics, and a run function extracting a game from each closed system.
• Semantics.evalDist is the SPMF Result denotation of a closed system.
• Semantics.distAdvantage is the total variation distance between two such denotations.
• Execution T is a closed-system execution experiment consumed by textbook UC statements.
• ObservedCompEmulates sem ε real ideal asserts that for every environment (plug), the distinguishing advantage between the real and ideal closed systems is at most ε.
• AsympObservedCompEmulates is the asymptotic variant: for every PPT adversary choosing environments, the advantage is negligible in the security parameter.
• ObservedCompUCSecure sem ε protocol ideal SimSpace simulate is the simulator-based variant with bounded advantage.

Main results

• ObservedCompEmulates.refl: advantage zero against itself.
• ObservedCompEmulates.triangle: transitivity with additive advantage bounds.
• ObservedCompEmulates.map_invariance: boundary adaptation preserves the bound.
• ObservedCompEmulates.par_compose, wire_compose, plug_compose: advantages add under parallel, wired, and plugged composition.
• ObservedCompUCSecure.toObservedCompEmulates_id: simulator-based security with the identity simulator recovers computational emulation.
• AsympObservedCompEmulates.par_compose, wire_compose, plug_compose: asymptotic composition from pointwise negligible bounds.
• observedDistGame: constructs the SecurityGame whose advantage is the UC distinguishing advantage.
• AsympObservedCompEmulates.iff_secureAgainst: AsympObservedCompEmulates 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;
• Result is the externally visible output type;
• run extracts an m Result game from each closed system.

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

• Result : Type

  Externally visible output type of the closed-system observation.

• 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 self.Result

  The probabilistic game extracted from a closed system.

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

The external SPMF 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 visible SPMF 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

Closed-system executions

structure Interaction.UC.Execution (T : OpenTheory) : Type (max 1 u)

A concrete UC execution semantics for a structural open theory.

Unlike Semantics, which keeps the surface monad and observer used to derive a distribution, Execution stores only the externally visible closed-system experiment. Paper-level UC statements should consume this type so that the chosen execution experiment is explicit.

• Result : Type

  Externally visible output type of the closed UC experiment.

• eval : T.Closed → SPMF self.Result

  Distributional interpretation of a closed system.

noncomputable def Interaction.UC.Execution.ofSemantics {T : OpenTheory} (sem : Semantics T) : Execution T

The observation-relative execution induced by a bundled Semantics.

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

Distinguishing advantage between closed executions.

@[simp]

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

theorem Interaction.UC.Execution.distAdvantage_ofSemantics {T : OpenTheory} (sem : Semantics T) (p q : T.Closed) : (ofSemantics sem).distAdvantage p q = sem.distAdvantage p q

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

ObservedCompEmulates 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.ObservedCompEmulates.refl {T : OpenTheory} (sem : Semantics T) {Δ : PortBoundary} (W : T.Obj Δ) : ObservedCompEmulates sem 0 W W

Every system computationally emulates itself with advantage zero.

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

Computational emulation composes transitively with additive advantage bounds (triangle inequality on total variation distance).

theorem Interaction.UC.ObservedCompEmulates.map_invariance {T : OpenTheory} [T.IsLawfulPlug] {sem : Semantics T} {ε : ℝ} {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) {real ideal : T.Obj Δ₁} (h : ObservedCompEmulates sem ε real ideal) : ObservedCompEmulates 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.ObservedCompEmulates.mono {T : OpenTheory} {sem : Semantics T} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) {Δ : PortBoundary} {real ideal : T.Obj Δ} (h : ObservedCompEmulates sem ε₁ real ideal) : ObservedCompEmulates sem ε₂ real ideal

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

Composition

theorem Interaction.UC.ObservedCompEmulates.par_left {T : OpenTheory} [T.HasPlugWireFactor] {sem : Semantics T} {ε : ℝ} {Δ₁ Δ₂ : PortBoundary} {real₁ ideal₁ : T.Obj Δ₁} (h₁ : ObservedCompEmulates sem ε real₁ ideal₁) (W₂ : T.Obj Δ₂) : ObservedCompEmulates 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.ObservedCompEmulates.par_right {T : OpenTheory} [T.HasPlugWireFactor] {sem : Semantics T} {ε : ℝ} {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) {real₂ ideal₂ : T.Obj Δ₂} (h₂ : ObservedCompEmulates sem ε real₂ ideal₂) : ObservedCompEmulates 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.ObservedCompEmulates.par_compose {T : OpenTheory} [T.HasPlugWireFactor] {sem : Semantics T} {ε₁ ε₂ : ℝ} {Δ₁ Δ₂ : PortBoundary} {real₁ ideal₁ : T.Obj Δ₁} {real₂ ideal₂ : T.Obj Δ₂} (h₁ : ObservedCompEmulates sem ε₁ real₁ ideal₁) (h₂ : ObservedCompEmulates sem ε₂ real₂ ideal₂) : ObservedCompEmulates sem (ε₁ + ε₂) (T.par real₁ real₂) (T.par ideal₁ ideal₂)

Computational UC composition for par: advantages add.

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

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

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

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

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

Computational UC composition for wire: advantages add.

theorem Interaction.UC.ObservedCompEmulates.plug_compose {T : OpenTheory} [T.HasPlugWireFactor] {sem : Semantics T} {ε₁ ε₂ : ℝ} {Δ : PortBoundary} {real ideal : T.Obj Δ} {K_real K_ideal : T.Obj Δ.swap} (hProt : ObservedCompEmulates sem ε₁ real ideal) (hEnv : ObservedCompEmulates 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.ObservedCompUCSecure {T : OpenTheory} (sem : Semantics T) (ε : ℝ) {Δ : PortBoundary} (protocol ideal : T.Obj Δ) (SimSpace : Type u_1) (simulate : SimSpace → T.Plug Δ → T.Plug Δ) : Prop

ObservedCompUCSecure 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.ObservedCompEmulates.toObservedCompUCSecure {T : OpenTheory} {sem : Semantics T} {ε : ℝ} {Δ : PortBoundary} {protocol ideal : T.Obj Δ} (h : ObservedCompEmulates sem ε protocol ideal) : ObservedCompUCSecure 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.ObservedCompUCSecure.toObservedCompEmulates_id {T : OpenTheory} {sem : Semantics T} {ε : ℝ} {Δ : PortBoundary} {protocol ideal : T.Obj Δ} (hSec : ObservedCompUCSecure sem ε protocol ideal PUnit.{u_1 + 1} fun (x : PUnit.{u_1 + 1}) (K : T.Plug Δ) => K) : ObservedCompEmulates sem ε protocol ideal

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

Asymptotic computational emulation

def Interaction.UC.AsympObservedCompEmulates (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

AsympObservedCompEmulates 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.AsympObservedCompEmulates.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) : AsympObservedCompEmulates 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.AsympObservedCompEmulates.of_observedCompEmulates {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 : ℕ), ObservedCompEmulates (sem n) (ε n) (real n) (ideal n)) : AsympObservedCompEmulates T sem real ideal Adv isPPT env

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

Asymptotic composition

theorem Interaction.UC.AsympObservedCompEmulates.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 : ℕ), ObservedCompEmulates (sem n) (ε₁ n) (real₁ n) (ideal₁ n)) (h₂ : ∀ (n : ℕ), ObservedCompEmulates (sem n) (ε₂ n) (real₂ n) (ideal₂ n)) : AsympObservedCompEmulates 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.AsympObservedCompEmulates.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 : ℕ), ObservedCompEmulates (sem n) (ε₁ n) (real₁ n) (ideal₁ n)) (h₂ : ∀ (n : ℕ), ObservedCompEmulates (sem n) (ε₂ n) (real₂ n) (ideal₂ n)) : AsympObservedCompEmulates 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.AsympObservedCompEmulates.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 : ℕ), ObservedCompEmulates (sem n) (ε₁ n) (real n) (ideal n)) (hEnv : ∀ (n : ℕ), ObservedCompEmulates (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.observedDistGame (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.AsympObservedCompEmulates.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 Δ} : AsympObservedCompEmulates T sem real ideal Adv isPPT env ↔ (observedDistGame T sem real ideal env).secureAgainst isPPT

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

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 ≤ (observedDistGame T sem real ideal env).advantage (reduce A) n) (hUC : AsympObservedCompEmulates 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.