Textbook UC vocabulary over the abstract open-system theory

This file gives a thin, presentation-layer reading of the abstract OpenTheory / execution infrastructure in the standard Canetti-style UC vocabulary: Protocol, Functionality, Adversary, Environment, Simulator, and an explicit execution experiment EXEC.

The point of this file is faithfulness. The contextual-equivalence form ObservedCompEmulates sem ε π F quantifies uniformly over arbitrary plugs K : T.Plug Δ under a user-chosen observation semantics. That is mathematically useful, but it is not by itself the textbook execution experiment. The paper-level form UCSecure exec ε π F fixes that by taking an explicit Execution T and using ∀ A. ∃ S. ∀ Z-quantification over real-world adversaries A, simulators S, and environments Z.

The bridge observedCompEmulates_toUCSecure_id (this file) shows that semantic emulation implies textbook UC security with the identity simulator S := A, exposing a single plug K(A, Z) : T.Plug Δ.toPort via OpenTheory.plug_wire_left and then applying ObservedCompEmulates at that plug.

The converse direction (textbook UC implies plug-level ObservedCompUCSecure) goes through Canetti's dummy-adversary theorem and is packaged as the reusable capability HasDummyAdversaryFactor.

Main definitions

• ProtocolBoundary: a pair of port boundaries (main, adv) for the environment-facing and adversary-facing sides of a protocol.
• ProtocolBoundary.toPort: the combined main ⊗ adv port boundary.
• Protocol T Δ, Functionality T Δ: open systems exposing Δ.toPort.
• Adversary T Δ back: an open system at swap Δ.adv ⊗ back; the back-channel back carries communication between the adversary and the environment.
• Environment T Δ back: an open system at swap Δ.main ⊗ swap back, which is definitionally a T.Plug (Δ.main ⊗ back).
• Simulator T Δ back: a function from real-world adversaries to ideal-world adversaries on the same back-channel.
• dummyAdversary: the canonical bidirectional relay idWire Δ.adv : Adversary T Δ Δ.adv from HasIdWire.
• EXEC π A Z: the closed system T.close (T.wire π A) Z.
• Execution T: a concrete distributional interpretation of closed systems as UC execution outputs.
• UCSecure exec ε π F: textbook computational UC security ∀ back A. ∃ S. ∀ Z. exec.distAdvantage (EXEC π A Z) (EXEC F S Z) ≤ ε.

Main results

• observedCompEmulates_toUCSecure_id: ObservedCompEmulates sem ε π F implies UCSecure (Execution.ofSemantics sem) ε π F with the identity simulator S := A.

Standard UC roles

structure Interaction.UC.Standard.ProtocolBoundary : Type 1

A protocol's boundary signature: a pair of port boundaries recording the two directed interfaces a protocol exposes.

• main is the interface to the environment / honest parties (inputs in, outputs out).
• adv is the interface to the adversary / network (network packets, scheduling tokens, leakage, etc.).

Both sides are full PortBoundarys rather than bare Interfaces because each direction generally carries traffic in both directions.

• main : PortBoundary

  Interface to the environment / honest parties.

• adv : PortBoundary

  Interface to the adversary / network.

@[reducible, inline]

abbrev Interaction.UC.Standard.ProtocolBoundary.toPort (Δ : ProtocolBoundary) : PortBoundary

The combined main ⊗ adv port boundary of a protocol.

@[reducible, inline]

abbrev Interaction.UC.Standard.Protocol (T : OpenTheory) (Δ : ProtocolBoundary) : Type u

A protocol is an open system exposing its full (main ⊗ adv) boundary.

@[reducible, inline]

abbrev Interaction.UC.Standard.Functionality (T : OpenTheory) (Δ : ProtocolBoundary) : Type u

A functionality is the ideal-world counterpart of a protocol; the same type, used as the trusted reference object.

@[reducible, inline]

abbrev Interaction.UC.Standard.Adversary (T : OpenTheory) (Δ : ProtocolBoundary) (back : PortBoundary) : Type u

An adversary speaks to the protocol over the swapped adv side and to the environment over a back-channel back.

@[reducible, inline]

abbrev Interaction.UC.Standard.Environment (T : OpenTheory) (Δ : ProtocolBoundary) (back : PortBoundary) : Type u

An environment speaks to the protocol over the swapped main side and to the adversary over the swapped back-channel. By definitional equality of swap and tensor, this is exactly a T.Plug (PortBoundary.tensor Δ.main back).

@[reducible, inline]

abbrev Interaction.UC.Standard.Simulator (T : OpenTheory) (Δ : ProtocolBoundary) (back : PortBoundary) : Type u

A simulator maps a real-world adversary to an ideal-world adversary on the same back-channel.

This is the lightweight presentation form. A more structural variant keeps the simulator as an open system on Δ.adv ⊗ swap Δ.adv and applies it via wire; both variants are interconvertible in any compact-closed OpenTheory.

def Interaction.UC.Standard.dummyAdversary {T : OpenTheory} [T.HasIdWire] (Δ : ProtocolBoundary) : Adversary T Δ Δ.adv

The dummy adversary: the canonical bidirectional relay between the adversary's view of the protocol (swap Δ.adv) and the environment's view of that same channel (Δ.adv on the back-channel). It is the coevaluation idWire Δ.adv provided by HasIdWire.

The execution experiment

def Interaction.UC.Standard.EXEC {T : OpenTheory} {Δ : ProtocolBoundary} {back : PortBoundary} (π : Protocol T Δ) (A : Adversary T Δ back) (Z : Environment T Δ back) : T.Closed

EXEC π A Z is the closed-system execution obtained by wiring the protocol π to the adversary A along their shared adv boundary, and then closing the result against the environment Z.

By definitional equality of swap (X ⊗ Y) with swap X ⊗ swap Y, the type of Z is exactly the T.Plug of the wired result, so no explicit boundary transport is needed.

Textbook UC security

def Interaction.UC.Standard.UCSecure {T : OpenTheory} (exec : Execution T) (ε : ℝ) {Δ : ProtocolBoundary} (π F : Protocol T Δ) : Prop

UCSecure exec ε π F is the textbook computational UC security statement: for every adversary A, there exists a simulator S such that no environment Z can distinguish the real-world execution EXEC π A Z from the ideal-world execution EXEC F S Z with advantage greater than ε.

The quantifier structure ∀ back A. ∃ S. ∀ Z is exactly Canetti's formulation; in particular, the simulator may depend on the adversary but not on the environment. The back-channel back is universally quantified to allow the environment-adversary side-channel to be arbitrary.

Bridge from observed emulation

theorem Interaction.UC.Standard.observedCompEmulates_toUCSecure_id {T : OpenTheory} [T.HasPlugWireFactor] {sem : Semantics T} {ε : ℝ} {Δ : ProtocolBoundary} {π F : Protocol T Δ} (h : ObservedCompEmulates sem ε π F) : UCSecure (Execution.ofSemantics sem) ε π F

Computational emulation ObservedCompEmulates sem ε π F implies textbook UC security for the observation-induced execution Execution.ofSemantics sem, with the identity simulator S := A. The existential simulator is witnessed by the real-world adversary itself.

The proof rewrites both EXEC π A Z and EXEC F A Z via OpenTheory.plug_wire_left, exposing the same plug K(A, Z) : T.Plug Δ.toPort on both sides, and then applies the ObservedCompEmulates hypothesis at that single plug.

class Interaction.UC.Standard.HasDummyAdversaryFactor (T : OpenTheory) extends T.IsCompactClosed : Type (max 1 u)

Structural capability for Canetti's dummy-adversary factorization.

Compact closure gives the wiring primitives, but the textbook-to-plug UC direction also needs a decomposition principle for arbitrary plugs into an adversary/environment pair. The concrete syntax models can provide that principle as an instance of this class.

• map_id {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W
• map_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)
• map_par {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (f₁.tensor f₂) (T.par W₁ W₂) = T.par (T.map f₁ W₁) (T.map f₂ W₂)
• map_wire {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.map (f₁.tensor f₂) (T.wire W₁ W₂) = T.wire (T.map (f₁.tensor (PortBoundary.Hom.id Γ)) W₁) (T.map ((PortBoundary.Hom.id Γ.swap).tensor f₂) W₂)
• map_plug {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) (K : T.Obj Δ₂.swap) : T.plug (T.map f W) K = T.plug W (T.map f.swap K)
• unit : T.Obj PortBoundary.empty
• par_assoc {Δ₁ Δ₂ Δ₃ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) (W₃ : T.Obj Δ₃) : T.map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom (T.par (T.par W₁ W₂) W₃) = T.par W₁ (T.par W₂ W₃)
• par_comm {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom (T.par W₁ W₂) = T.par W₂ W₁
• par_leftUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyLeft Δ).toHom (T.par HasUnit.unit W) = W
• par_rightUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyRight Δ).toHom (T.par W HasUnit.unit) = W
• wire_assoc {Δ₁ Γ₁ Γ₂ Δ₃ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ₁)) (W₂ : T.Obj (Γ₁.swap.tensor Γ₂)) (W₃ : T.Obj (Γ₂.swap.tensor Δ₃)) : T.wire (T.wire W₁ W₂) W₃ = T.wire W₁ (T.wire W₂ W₃)
• wire_par_superpose {Δ₁ Δ₂ Γ Δ₃ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj (Δ₂.tensor Γ)) (W₃ : T.Obj (Γ.swap.tensor Δ₃)) : T.wire (T.map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Γ).symm.toHom (T.par W₁ W₂)) W₃ = T.map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).symm.toHom (T.par W₁ (T.wire W₂ W₃))
• wire_comm {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire W₁ W₂ = T.map (PortBoundary.Equiv.tensorComm Δ₂ Δ₁).toHom (T.wire (T.map (PortBoundary.Equiv.tensorComm Γ.swap Δ₂).toHom W₂) (T.map (PortBoundary.Equiv.tensorComm Δ₁ Γ).toHom W₁))
• idWire (Γ : PortBoundary) : T.Obj (Γ.swap.tensor Γ)
• wire_idWire (Γ : PortBoundary) {Δ₂ : PortBoundary} (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire (HasIdWire.idWire Γ) W₂ = W₂
• wire_idWire_right (Γ : PortBoundary) {Δ₁ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) : T.wire W₁ (HasIdWire.idWire Γ) = W₁
• unit_eq : HasUnit.unit = T.map (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (HasIdWire.idWire PortBoundary.empty)
• toObservedCompUCSecure_dummy {sem : Semantics T} {ε : ℝ} {Δ : ProtocolBoundary} {π F : Protocol T Δ} : UCSecure (Execution.ofSemantics sem) ε π F → ∃ (SimSpace : Type u) (simulate : SimSpace → T.Plug Δ.toPort → T.Plug Δ.toPort), ObservedCompUCSecure sem ε π F SimSpace simulate

theorem Interaction.UC.Standard.ucSecure_toObservedCompUCSecure_dummy {T : OpenTheory} [HasDummyAdversaryFactor T] {sem : Semantics T} {ε : ℝ} {Δ : ProtocolBoundary} {π F : Protocol T Δ} (h : UCSecure (Execution.ofSemantics sem) ε π F) : ∃ (SimSpace : Type u) (simulate : SimSpace → T.Plug Δ.toPort → T.Plug Δ.toPort), ObservedCompUCSecure sem ε π F SimSpace simulate

Dummy-adversary direction.

Textbook UC security UCSecure exec ε π F implies the plug-level simulator-based form ObservedCompUCSecure: given the existential simulator from UCSecure instantiated at the dummy adversary, one constructs a T.Plug Δ.toPort-level simulator by repackaging the adversary-environment pair through the zig-zag identity wire_idWire_right.

This is the content of Canetti's dummy-adversary theorem (cf. Canetti '01, Thm 4.16). The non-formalized structural decomposition is now an explicit reusable assumption, HasDummyAdversaryFactor, rather than a local proof hole.