Contextual emulation and UC security

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

Main definitions

• Emulates T real ideal ObsEq says that the open system real emulates ideal in theory T whenever, for every valid plug (context), the resulting closed systems are observationally equivalent.

• UCSecure T protocol ideal ObsEq 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 observationally equivalent to the closed real system.

Basic properties

• Emulates.refl and Emulates.trans follow immediately from the corresponding properties of the observation relation ObsEq.

• 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 (requires a lawful theory).

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.

structure Interaction.UC.Emulates {T : OpenTheory} {Δ : PortBoundary} (real ideal : T.Obj Δ) (ObsEq : T.Closed → T.Closed → Prop) : Prop

Emulates T real ideal ObsEq asserts that real contextually emulates ideal in the open-composition theory T.

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

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

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

theorem Interaction.UC.Emulates.refl {T : OpenTheory} {Δ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} (hRefl : ∀ (c : T.Closed), ObsEq c c) (W : T.Obj Δ) : Emulates W W ObsEq

Every open system emulates itself, provided the observation relation is reflexive.

theorem Interaction.UC.Emulates.trans {T : OpenTheory} {Δ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} (hTrans : ∀ (a b c : T.Closed), ObsEq a b → ObsEq b c → ObsEq a c) {W₁ W₂ W₃ : T.Obj Δ} (h₁₂ : Emulates W₁ W₂ ObsEq) (h₂₃ : Emulates W₂ W₃ ObsEq) : Emulates W₁ W₃ ObsEq

Emulation composes transitively, provided the observation relation is transitive.

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

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} {ObsEq : T.Closed → T.Closed → Prop} {real ideal : T.Obj Δ} (h : Emulates real ideal ObsEq) (K : T.Plug Δ) : ObsEq (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.

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.CompactClosed] {Δ₁ Δ₂ : 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.CompactClosed] {Δ₁ Δ₂ : 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.CompactClosed] {Δ₁ Γ Δ₂ : 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.CompactClosed] {Δ₁ Γ Δ₂ : 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.CompactClosed] {Δ : 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.

theorem Interaction.UC.Emulates.par_left {T : OpenTheory} [T.CompactClosed] {Δ₁ Δ₂ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} {real₁ ideal₁ : T.Obj Δ₁} (h₁ : Emulates real₁ ideal₁ ObsEq) (W₂ : T.Obj Δ₂) : Emulates (T.par real₁ W₂) (T.par ideal₁ W₂) ObsEq

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.CompactClosed] {Δ₁ Δ₂ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} (W₁ : T.Obj Δ₁) {real₂ ideal₂ : T.Obj Δ₂} (h₂ : Emulates real₂ ideal₂ ObsEq) : Emulates (T.par W₁ real₂) (T.par W₁ ideal₂) ObsEq

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.CompactClosed] {Δ₁ Δ₂ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} (hTrans : ∀ (a b c : T.Closed), ObsEq a b → ObsEq b c → ObsEq a c) {real₁ ideal₁ : T.Obj Δ₁} {real₂ ideal₂ : T.Obj Δ₂} (h₁ : Emulates real₁ ideal₁ ObsEq) (h₂ : Emulates real₂ ideal₂ ObsEq) : Emulates (T.par real₁ real₂) (T.par ideal₁ ideal₂) ObsEq

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.CompactClosed] {Δ₁ Γ Δ₂ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} {real₁ ideal₁ : T.Obj (Δ₁.tensor Γ)} (h₁ : Emulates real₁ ideal₁ ObsEq) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : Emulates (T.wire real₁ W₂) (T.wire ideal₁ W₂) ObsEq

Replacing the left factor of a wiring preserves emulation.

theorem Interaction.UC.Emulates.wire_right {T : OpenTheory} [T.CompactClosed] {Δ₁ Γ Δ₂ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} (W₁ : T.Obj (Δ₁.tensor Γ)) {real₂ ideal₂ : T.Obj (Γ.swap.tensor Δ₂)} (h₂ : Emulates real₂ ideal₂ ObsEq) : Emulates (T.wire W₁ real₂) (T.wire W₁ ideal₂) ObsEq

Replacing the right factor of a wiring preserves emulation.

theorem Interaction.UC.Emulates.wire_compose {T : OpenTheory} [T.CompactClosed] {Δ₁ Γ Δ₂ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} (hTrans : ∀ (a b c : T.Closed), ObsEq a b → ObsEq b c → ObsEq a c) {real₁ ideal₁ : T.Obj (Δ₁.tensor Γ)} {real₂ ideal₂ : T.Obj (Γ.swap.tensor Δ₂)} (h₁ : Emulates real₁ ideal₁ ObsEq) (h₂ : Emulates real₂ ideal₂ ObsEq) : Emulates (T.wire real₁ real₂) (T.wire ideal₁ ideal₂) ObsEq

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.CompactClosed] {Δ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} (W : T.Obj Δ) {K₁ K₂ : T.Obj Δ.swap} (hK : Emulates K₁ K₂ ObsEq) : ObsEq (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.CompactClosed] {Δ : PortBoundary} {ObsEq : T.Closed → T.Closed → Prop} (hTrans : ∀ (a b c : T.Closed), ObsEq a b → ObsEq b c → ObsEq a c) {real ideal : T.Obj Δ} {K_real K_ideal : T.Obj Δ.swap} (hProt : Emulates real ideal ObsEq) (hEnv : Emulates K_real K_ideal ObsEq) : ObsEq (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 Δ) (ObsEq : T.Closed → T.Closed → Prop) (SimSpace : Type u_1) (simulate : SimSpace → T.Plug Δ → T.Plug Δ) : Prop

UCSecure T protocol ideal ObsEq 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 observationally equivalent 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 Δ} {ObsEq : T.Closed → T.Closed → Prop} (h : Emulates protocol ideal ObsEq) : UCSecure protocol ideal ObsEq 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 Δ} {ObsEq : T.Closed → T.Closed → Prop} (hSec : UCSecure protocol ideal ObsEq PUnit.{u_1 + 1} fun (x : PUnit.{u_1 + 1}) (K : T.Plug Δ) => K) : Emulates protocol ideal ObsEq

UC security with identity simulation recovers emulation.