Contextual emulation and UC security

This file defines the core judgments for Universally Composable (UC) security at the abstract OpenTheory level.

Main definitions

• Observation T bundles a binary relation on closed systems together with a proof that it is an equivalence relation. UC judgments are parameterized uniformly over Observation T so that reflexivity, symmetry, and transitivity are always available without per-call hypotheses.

• Emulates real ideal Obs says that the open system real emulates ideal whenever, for every valid plug (context), the resulting closed systems are related by Obs.rel.

• UCSecure protocol ideal Obs SimSpace simulate is the existential simulator variant: there exists a simulator that transforms any context so that the closed ideal system (with the simulated context) is Obs.rel-related to the closed real system.

The canonical Observation.eq T instantiates the framework with perfect syntactic equality on closed systems; downstream layers (e.g. open process isos, asymptotic computational indistinguishability) supply their own Observation constructors.

Basic properties

• Emulates.refl and Emulates.trans are immediate consequences of the bundled Equivalence proof in Observation.

• Emulates.map_invariance shows that adapting both sides of an emulation along the same boundary morphism preserves the emulation (requires a lawful theory).

• Emulates.plug_invariance shows that plugging both sides of an emulation with the same additional context preserves the emulation.

UC composition theorems

• Emulates.par_compose: parallel composition preserves emulation.
• Emulates.wire_compose: wired composition preserves emulation.
• Emulates.plug_compose: both protocol and environment emulation compose to yield observational equivalence of the closed systems.

These rely on structural factorization lemmas (close_par_left, close_par_right, close_wire_left, close_wire_right, plug_comm) that capture monoidal coherence identities, derived from the CompactClosed axioms.

Design note: why Observation requires a full Equivalence

Bundling the equivalence proof into Observation lets every UC theorem quantify over a single parameter Obs : Observation T rather than threading a relation plus separate hRefl/hTrans/hSymm hypotheses. The cost is that observation relations which are not equivalences (e.g. the fixed-ε computational distinguishability relation fun c₁ c₂ => distAdvantage (sem c₁) (sem c₂) ≤ ε, which fails transitivity because the triangle inequality only gives 2ε) cannot be packaged as Observation T. The intended bridge from computational security to abstract Emulates therefore lives at the asymptotic level (where negligible distance is closed under sums and is a genuine equivalence), not at the fixed-ε level.

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

Observation T bundles a binary relation on the closed systems of an open theory T together with a proof that it is an equivalence relation.

This is the parameter slot through which different security flavors (perfect, statistical, asymptotic computational) plug into the abstract UC judgments Emulates and UCSecure.

• rel : T.Closed → T.Closed → Prop

  The underlying binary relation on closed systems.

• equiv : Equivalence self.rel

  The relation is an equivalence (reflexive, symmetric, transitive).

def Interaction.UC.Observation.eq (T : OpenTheory) : Observation T

Perfect syntactic equality on closed systems is an observation relation.

@[simp]

theorem Interaction.UC.Observation.eq_rel {T : OpenTheory} {c₁ c₂ : T.Closed} : (eq T).rel c₁ c₂ ↔ c₁ = c₂

structure Interaction.UC.Emulates {T : OpenTheory} {Δ : PortBoundary} (real ideal : T.Obj Δ) (Obs : Observation T) : Prop

Emulates real ideal Obs asserts that real contextually emulates ideal in the open-composition theory T, judged by the observation relation Obs : Observation T.

For every plug K : T.Plug Δ, the closed compositions T.close real K and T.close ideal K are related by Obs.rel.

This is the definitional core of UC security: no environment can distinguish real from ideal under the chosen observation.

• compare (K : T.Plug Δ) : Obs.rel (T.close real K) (T.close ideal K)

theorem Interaction.UC.Emulates.refl {T : OpenTheory} {Δ : PortBoundary} (Obs : Observation T) (W : T.Obj Δ) : Emulates W W Obs

Every open system emulates itself.

theorem Interaction.UC.Emulates.symm {T : OpenTheory} {Δ : PortBoundary} {Obs : Observation T} {W₁ W₂ : T.Obj Δ} (h : Emulates W₁ W₂ Obs) : Emulates W₂ W₁ Obs

Emulation is symmetric.

theorem Interaction.UC.Emulates.trans {T : OpenTheory} {Δ : PortBoundary} {Obs : Observation T} {W₁ W₂ W₃ : T.Obj Δ} (h₁₂ : Emulates W₁ W₂ Obs) (h₂₃ : Emulates W₂ W₃ Obs) : Emulates W₁ W₃ Obs

Emulation composes transitively.

theorem Interaction.UC.Emulates.map_invariance {T : OpenTheory} [T.IsLawfulPlug] {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} (f : Δ₁.Hom Δ₂) {real ideal : T.Obj Δ₁} (h : Emulates real ideal Obs) : Emulates (T.map f real) (T.map f ideal) Obs

Adapting both sides of an emulation along the same boundary morphism preserves the emulation, provided the theory has lawful map and plug.

The key identity used is plug (map f W) K = plug W (map (swap f) K), which is the map_plug naturality law.

theorem Interaction.UC.Emulates.plug_invariance {T : OpenTheory} {Δ : PortBoundary} {Obs : Observation T} {real ideal : T.Obj Δ} (h : Emulates real ideal Obs) (K : T.Plug Δ) : Obs.rel (T.close real K) (T.close ideal K)

Plugging both sides of an emulation with the same additional context preserves the emulation.

If real emulates ideal and we close both against the same plug K, the resulting closed systems are still observationally equivalent. This is immediate from the definition.

Structural factorization of close under composition

def Interaction.UC.OpenTheory.parContextLeft {T : OpenTheory} {Δ₁ Δ₂ : PortBoundary} (W₂ : T.Obj Δ₂) (K : T.Plug (Δ₁.tensor Δ₂)) : T.Plug Δ₁

The effective plug for the left component of a parallel composition.

Given W₂ : T.Obj Δ₂ and K : T.Plug (tensor Δ₁ Δ₂), wire them together through the Δ₂ boundary to obtain a plug for Δ₁ alone.

def Interaction.UC.OpenTheory.parContextRight {T : OpenTheory} {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (K : T.Plug (Δ₁.tensor Δ₂)) : T.Plug Δ₂

The effective plug for the right component of a parallel composition.

Given W₁ : T.Obj Δ₁ and K : T.Plug (tensor Δ₁ Δ₂), wire them together through the Δ₁ boundary to obtain a plug for Δ₂ alone.

theorem Interaction.UC.OpenTheory.close_par_left {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) (K : T.Plug (Δ₁.tensor Δ₂)) : T.close (T.par W₁ W₂) K = T.close W₁ (parContextLeft W₂ K)

Closing a parallel composition factors through the left component.

This captures the string-diagram identity: plugging par W₁ W₂ against K is the same as plugging W₁ against the residual context formed by wiring W₂ into K.

theorem Interaction.UC.OpenTheory.close_par_right {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) (K : T.Plug (Δ₁.tensor Δ₂)) : T.close (T.par W₁ W₂) K = T.close W₂ (parContextRight W₁ K)

Closing a parallel composition factors through the right component.

def Interaction.UC.OpenTheory.wireContextLeft {T : OpenTheory} {Δ₁ Γ Δ₂ : PortBoundary} (W₂ : T.Obj (Γ.swap.tensor Δ₂)) (K : T.Plug (Δ₁.tensor Δ₂)) : T.Plug (Δ₁.tensor Γ)

The effective plug for the left factor of a wiring.

Given W₂ : T.Obj (tensor (swap Γ) Δ₂) and K : T.Plug (tensor Δ₁ Δ₂), wire them together through the Δ₂ boundary to obtain a plug for tensor Δ₁ Γ.

def Interaction.UC.OpenTheory.wireContextRight {T : OpenTheory} {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) (K : T.Plug (Δ₁.tensor Δ₂)) : T.Plug (Γ.swap.tensor Δ₂)

The effective plug for the right factor of a wiring.

Given W₁ : T.Obj (tensor Δ₁ Γ) and K : T.Plug (tensor Δ₁ Δ₂), wire them together through the Δ₁ boundary to obtain a plug for tensor (swap Γ) Δ₂.

theorem Interaction.UC.OpenTheory.close_wire_left {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) (K : T.Plug (Δ₁.tensor Δ₂)) : T.close (T.wire W₁ W₂) K = T.close W₁ (wireContextLeft W₂ K)

Closing a wired composition factors through the left component.

theorem Interaction.UC.OpenTheory.close_wire_right {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) (K : T.Plug (Δ₁.tensor Δ₂)) : T.close (T.wire W₁ W₂) K = T.close W₂ (wireContextRight W₁ K)

Closing a wired composition factors through the right component.

theorem Interaction.UC.OpenTheory.plug_comm {T : OpenTheory} [T.HasPlugWireFactor] {Δ : PortBoundary} (W : T.Obj Δ) (K : T.Obj Δ.swap) : T.plug W K = T.plug K W

plug is symmetric: the protocol and context roles are interchangeable.

This follows from plug_eq_wire plus commutativity of wire via par_comm.

UC composition theorems

theorem Interaction.UC.Emulates.par_left {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} {real₁ ideal₁ : T.Obj Δ₁} (h₁ : Emulates real₁ ideal₁ Obs) (W₂ : T.Obj Δ₂) : Emulates (T.par real₁ W₂) (T.par ideal₁ W₂) Obs

Replacing the left component of a parallel composition preserves emulation, with the right component and environment held fixed.

theorem Interaction.UC.Emulates.par_right {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} (W₁ : T.Obj Δ₁) {real₂ ideal₂ : T.Obj Δ₂} (h₂ : Emulates real₂ ideal₂ Obs) : Emulates (T.par W₁ real₂) (T.par W₁ ideal₂) Obs

Replacing the right component of a parallel composition preserves emulation, with the left component and environment held fixed.

theorem Interaction.UC.Emulates.par_compose {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Δ₂ : PortBoundary} {Obs : Observation T} {real₁ ideal₁ : T.Obj Δ₁} {real₂ ideal₂ : T.Obj Δ₂} (h₁ : Emulates real₁ ideal₁ Obs) (h₂ : Emulates real₂ ideal₂ Obs) : Emulates (T.par real₁ real₂) (T.par ideal₁ ideal₂) Obs

UC composition theorem for par: if each component emulates its ideal, then their parallel composition emulates the parallel composition of ideals.

The proof uses a hybrid argument through T.par ideal₁ real₂, with each step reducing to emulation of a single component via close_par_left / close_par_right.

theorem Interaction.UC.Emulates.wire_left {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} {real₁ ideal₁ : T.Obj (Δ₁.tensor Γ)} (h₁ : Emulates real₁ ideal₁ Obs) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : Emulates (T.wire real₁ W₂) (T.wire ideal₁ W₂) Obs

Replacing the left factor of a wiring preserves emulation.

theorem Interaction.UC.Emulates.wire_right {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} (W₁ : T.Obj (Δ₁.tensor Γ)) {real₂ ideal₂ : T.Obj (Γ.swap.tensor Δ₂)} (h₂ : Emulates real₂ ideal₂ Obs) : Emulates (T.wire W₁ real₂) (T.wire W₁ ideal₂) Obs

Replacing the right factor of a wiring preserves emulation.

theorem Interaction.UC.Emulates.wire_compose {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Γ Δ₂ : PortBoundary} {Obs : Observation T} {real₁ ideal₁ : T.Obj (Δ₁.tensor Γ)} {real₂ ideal₂ : T.Obj (Γ.swap.tensor Δ₂)} (h₁ : Emulates real₁ ideal₁ Obs) (h₂ : Emulates real₂ ideal₂ Obs) : Emulates (T.wire real₁ real₂) (T.wire ideal₁ ideal₂) Obs

UC composition theorem for wire: if each factor emulates its ideal, then their wired composition emulates the wired ideal.

theorem Interaction.UC.Emulates.plug_right {T : OpenTheory} [T.HasPlugWireFactor] {Δ : PortBoundary} {Obs : Observation T} (W : T.Obj Δ) {K₁ K₂ : T.Obj Δ.swap} (hK : Emulates K₁ K₂ Obs) : Obs.rel (T.close W K₁) (T.close W K₂)

Replacing the plug (environment) while keeping the protocol fixed preserves observational equivalence, using plug_comm to swap the protocol/environment roles.

theorem Interaction.UC.Emulates.plug_compose {T : OpenTheory} [T.HasPlugWireFactor] {Δ : PortBoundary} {Obs : Observation T} {real ideal : T.Obj Δ} {K_real K_ideal : T.Obj Δ.swap} (hProt : Emulates real ideal Obs) (hEnv : Emulates K_real K_ideal Obs) : Obs.rel (T.close real K_real) (T.close ideal K_ideal)

UC composition theorem for plug: if the protocol emulates its ideal and the environment emulates its ideal, then the closed real-world execution is observationally equivalent to the closed ideal-world execution.

The proof uses a hybrid through T.close ideal K_real: step 1 is plug_invariance (same environment, different protocol) and step 2 is plug_right (same protocol, different environment).

def Interaction.UC.UCSecure {T : OpenTheory} {Δ : PortBoundary} (protocol ideal : T.Obj Δ) (Obs : Observation T) (SimSpace : Type u_1) (simulate : SimSpace → T.Plug Δ → T.Plug Δ) : Prop

UCSecure protocol ideal Obs SimSpace simulate is the UC security statement with an existential simulator.

There exists a simulator parameter s : SimSpace such that for every context K, the closed real-world execution T.close protocol K is related (under Obs.rel) to the closed ideal-world execution T.close ideal (simulate s K).

The simulator simulate s transforms the context rather than the ideal functionality, following the standard UC convention: the simulator acts as a wrapper around the honest context to make the ideal world look like the real world.

theorem Interaction.UC.Emulates.toUCSecure {T : OpenTheory} {Δ : PortBoundary} {protocol ideal : T.Obj Δ} {Obs : Observation T} (h : Emulates protocol ideal Obs) : UCSecure protocol ideal Obs PUnit.{u_1 + 1} fun (x : PUnit.{u_1 + 1}) (K : T.Plug Δ) => K

Emulation implies UC security with the trivial (identity) simulator.

theorem Interaction.UC.UCSecure.toEmulates_id {T : OpenTheory} {Δ : PortBoundary} {protocol ideal : T.Obj Δ} {Obs : Observation T} (hSec : UCSecure protocol ideal Obs PUnit.{u_1 + 1} fun (x : PUnit.{u_1 + 1}) (K : T.Plug Δ) => K) : Emulates protocol ideal Obs

UC security with identity simulation recovers emulation.