Machine identity for UC composition

This file introduces MachineId Sid Pid, the (sid, pid) machine identity used to address protocol participants in CJSV22-style universal composition (Canetti, Jain, Swanberg, Varia, Universally Composable End-to-End Secure Messaging, CRYPTO 2022). A machine is identified by a session identifier sid : Sid and a party identifier pid : Pid. Within a single instantiated session, party identifiers distinguish participants; across sessions, the session identifier scopes who is allowed to talk to whom.

The framework's OpenProcess Party Δ is generic in its participant type Party. Specializing Party := MachineId Sid Pid recovers the CJSV22 surface where every protocol input and output is keyed by a (sid, pid) pair. The abbreviation MachineProcess Sid Pid Δ names that specialization.

MachineId is intentionally additive: nothing in the existing UC layer mentions it, and protocols that already use a flat Party continue to work unchanged. New work that needs session-aware identity (forward security, post-compromise security, multi-session composition) instantiates Party := MachineId Sid Pid and uses the helpers below.

Per-process access control and subroutine respecting

This file also introduces the access-control vocabulary required by the CJSV22 subroutine respecting condition:

• HasAccessControl P. A typeclass over OpenProcess Party Δ carrying allowed : Interface.RoutedPacket Δ.In Party → Bool. The default-open instance HasAccessControl.allowAll is provided for protocols whose security is not sensitive to per-machine input filtering.
• MachineProcess.allowSameSession owner P. The canonical CJSV22 filter on a MachineProcess: admit a routed packet iff its sender shares a session with owner (per MachineId.sameSession).
• MachineProcess.SubroutineRespectingAt sid P. A Prop-valued property saying every reachable step's decoration only attributes controllers in session sid. Built recursively over Spec.Decoration via OpenNodeProfile.SessionCoherentAtMove and DecorationSessionCoherentAt.

These three pieces are additive on top of the existing OpenProcess surface: no existing construction site is touched, and the predicate SubroutineRespectingAt reads off the controller annotations already carried by OpenNodeContext.

Deferred follow-up

The runtime integration that consults HasAccessControl from BoundaryAction.inputDecode is deliberately deferred to the corruption layer, which already needs to touch the boundary surface for EnvAction dispatch. Until that integration lands, HasAccessControl is a declarative contract that downstream constructions thread by hand: the typeclass exposes the per-process allowed predicate, but no construction in this file enforces it against the runtime. Consumers that need the contract enforced should filter incoming routed packets explicitly through allowed at the appropriate boundary surface.

structure Interaction.UC.MachineId (Sid Pid : Type u) : Type u

MachineId Sid Pid is the standard (sid, pid) machine identity from CJSV22's universal composition with global subroutines.

Two machines are equal iff both their session identifier and party identifier agree. Decidable equality is derived from decidable equality on Sid and Pid.

The session identifier Sid is left abstract so users can pick the structure that fits their composition style: a flat Nat or String for single-level sessions, or a List String / prefix tree when nested subsessions need to be addressed by hierarchical paths (the standard CJSV22 idiom for spawned subprotocols).

• sid : Sid
• pid : Pid

def Interaction.UC.instDecidableEqMachineId.decEq {Sid✝ Pid✝ : Type u_1} [DecidableEq Sid✝] [DecidableEq Pid✝] (x✝ x✝¹ : MachineId Sid✝ Pid✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Interaction.UC.instDecidableEqMachineId {Sid✝ Pid✝ : Type u_1} [DecidableEq Sid✝] [DecidableEq Pid✝] : DecidableEq (MachineId Sid✝ Pid✝)

theorem Interaction.UC.MachineId.ext_iff {Sid Pid : Type u} {m₁ m₂ : MachineId Sid Pid} : m₁ = m₂ ↔ m₁.sid = m₂.sid ∧ m₁.pid = m₂.pid

theorem Interaction.UC.MachineId.ext {Sid Pid : Type u} {m₁ m₂ : MachineId Sid Pid} (hsid : m₁.sid = m₂.sid) (hpid : m₁.pid = m₂.pid) : m₁ = m₂

def Interaction.UC.MachineId.sameSession {Sid Pid : Type u} [DecidableEq Sid] (m₁ m₂ : MachineId Sid Pid) : Bool

Two machines belong to the same protocol session iff their session identifiers agree.

This is the syntactic ingredient of CJSV22's "subroutine respecting" check: within a subroutine respecting protocol, a machine routes inbound and outbound messages only between machines sharing its sid.

@[simp]

theorem Interaction.UC.MachineId.sameSession_self {Sid Pid : Type u} [DecidableEq Sid] (m : MachineId Sid Pid) : m.sameSession m = true

theorem Interaction.UC.MachineId.sameSession_iff {Sid Pid : Type u} [DecidableEq Sid] (m₁ m₂ : MachineId Sid Pid) : m₁.sameSession m₂ = true ↔ m₁.sid = m₂.sid

theorem Interaction.UC.MachineId.sameSession_comm {Sid Pid : Type u} [DecidableEq Sid] (m₁ m₂ : MachineId Sid Pid) : m₁.sameSession m₂ = m₂.sameSession m₁

theorem Interaction.UC.MachineId.sameSession_trans {Sid Pid : Type u} [DecidableEq Sid] {m₁ m₂ m₃ : MachineId Sid Pid} (h₁₂ : m₁.sameSession m₂ = true) (h₂₃ : m₂.sameSession m₃ = true) : m₁.sameSession m₃ = true

@[reducible, inline]

abbrev Interaction.UC.MachineProcess (Sid Pid : Type u) (m : Type w → Type w') (Δ : PortBoundary) : Type (max (max (max u (v + 1)) (w + 1)) w')

MachineProcess Sid Pid Δ is the specialization of OpenProcess to processes whose participants are identified by (sid, pid) machine identities.

This is the canonical type for protocols written in the CJSV22 idiom: every input and output packet is keyed by a MachineId Sid Pid, and session-scoped composition operates uniformly over this type.

Existing examples that use a flat Party are unaffected; only protocols that need session-aware identity instantiate this abbreviation.

Per-process access control

class Interaction.UC.HasAccessControl {Party : Type u} {m : Type w → Type w'} {Δ : PortBoundary} (P : OpenProcess m Party Δ) : Type u

HasAccessControl P is the per-process predicate deciding which routed inbound packets are admissible to the open process P.

For an open process P : OpenProcess Party Δ, an instance supplies allowed : Interface.RoutedPacket Δ.In Party → Bool. The runtime layer consults this typeclass when delivering inbound packets: a packet is forwarded to P only when allowed rp = true.

The default for new instances is allow everything (HasAccessControl.allowAll). Protocols that need sender-aware filtering provide a more restrictive instance. The canonical CJSV22-style filter (MachineProcess.allowSameSession) admits a packet iff its sender shares a session with the process owner, recovering the access-control fragment of the subroutine respecting condition (CJSV22 §2.3).

The runtime integration into BoundaryAction.inputDecode is deliberately not wired up in this slice: the typeclass exists as a forward-compatible vocabulary that downstream layers (notably the F2 corruption work) consume. Until that integration lands, HasAccessControl is a declarative contract that downstream constructions must thread by hand.

• allowed : Δ.In.RoutedPacket Party → Bool

@[reducible]

def Interaction.UC.HasAccessControl.allowAll {Party : Type u} {m : Type w → Type w'} {Δ : PortBoundary} (P : OpenProcess m Party Δ) : HasAccessControl P

The trivial allow-all access control: every routed packet is admissible.

Useful for protocols whose security does not depend on per-machine input filtering, and as the canonical baseline against which more restrictive instances are compared.

@[simp]

theorem Interaction.UC.HasAccessControl.allowed_allowAll {Party : Type u} {m : Type w → Type w'} {Δ : PortBoundary} (P : OpenProcess m Party Δ) (rp : Δ.In.RoutedPacket Party) : allowed P rp = true

@[reducible]

def Interaction.UC.MachineProcess.allowSameSession {Sid Pid : Type u} {m : Type w → Type w'} {Δ : PortBoundary} [DecidableEq Sid] (owner : MachineId Sid Pid) (P : MachineProcess Sid Pid m Δ) : HasAccessControl P

The canonical CJSV22 same-session access control on a MachineProcess.

MachineProcess.allowSameSession owner P admits a routed packet iff its sender shares a session with owner (per MachineId.sameSession).

This is the access-control fragment of the subroutine respecting condition (CJSV22 §2.3): a machine (s, p) only accepts inputs from senders whose session identifier is also s. Combined with a sender-aware emit (delivered by F2), this recovers the full structural same-session discipline.

@[simp]

theorem Interaction.UC.MachineProcess.allowed_allowSameSession {Sid Pid : Type u} {m : Type w → Type w'} {Δ : PortBoundary} [DecidableEq Sid] (owner : MachineId Sid Pid) (P : MachineProcess Sid Pid m Δ) (rp : Δ.In.RoutedPacket (MachineId Sid Pid)) : HasAccessControl.allowed P rp = rp.sender.sameSession owner

Subroutine respecting predicate

def Interaction.UC.OpenNodeProfile.SessionCoherentAtMove {Sid Pid : Type u} {Δ : PortBoundary} {X : Type w} (sid : Sid) (ons : OpenNodeProfile (MachineId Sid Pid) Δ X) (x : X) : Prop

A node semantics is session-coherent at sid for a chosen move x iff every controller listed by the node for that move resides in session sid.

This is the per-move check used by DecorationSessionCoherentAt: at the node where x is chosen, every machine credited as a controller of x must share the protocol's session identifier.

def Interaction.UC.DecorationSessionCoherentAt {Sid Pid : Type u} {Δ : PortBoundary} (sid : Sid) {spec : Spec} : Spec.Decoration (OpenNodeContext (MachineId Sid Pid) Δ) spec → spec.Transcript → Prop

A spec decoration is session-coherent at sid along a chosen transcript iff every visited node attributes only controllers in session sid.

This is the recursive companion to OpenNodeProfile.SessionCoherentAtMove, modeled directly on IsSilentDecoration: the predicate walks the same transcript path through the decoration tree and accumulates the per-node coherence checks.

def Interaction.UC.MachineProcess.SubroutineRespectingAt {Sid Pid : Type u} {m : Type w → Type w'} {Δ : PortBoundary} (sid : Sid) (P : MachineProcess Sid Pid m Δ) : Prop

A MachineProcess is subroutine respecting at sid iff every step from every reachable state, along every transcript path, only attributes controllers in session sid.

This is the controller-side fragment of CJSV22's subroutine respecting condition. The sender-side fragment (every emitted / accepted RoutedPacket has sender in session sid) lives at the BoundaryAction integration layer and is enforced by future HasAccessControl instances installed via MachineProcess.allowSameSession.

@[simp]

theorem Interaction.UC.DecorationSessionCoherentAt_done {Sid Pid : Type u} {Δ : PortBoundary} (sid : Sid) (d : Spec.Decoration (OpenNodeContext (MachineId Sid Pid) Δ) Spec.done) (tr : Spec.done.Transcript) : DecorationSessionCoherentAt sid d tr

@[simp]

theorem Interaction.UC.DecorationSessionCoherentAt_node {Sid Pid : Type u} {Δ : PortBoundary} (sid : Sid) {Moves : Type w} {residual : Moves → Spec} (d : Spec.Decoration (OpenNodeContext (MachineId Sid Pid) Δ) (Spec.node Moves residual)) (x : Moves) (tr : (residual x).Transcript) : DecorationSessionCoherentAt sid d ⟨x, tr⟩ ↔ OpenNodeProfile.SessionCoherentAtMove sid d.1 x ∧ DecorationSessionCoherentAt sid (d.2 x) tr