Fair PPT security for asynchronous env-open processes

This file lifts the synchronous Concurrent.Fairness ticket machinery to the asynchronous runtime in AsyncRuntime.lean, and packages a fair-PPT computational security definition secureAgainstFair that quantifies over scheduler pairs satisfying user-specified PPT and fairness predicates.

Main definitions

• AsyncRun process envAction — an infinite execution of the async runtime, structured as in Concurrent.ProcessOver.Run but threading the runtime alphabet RuntimeEvent Event.
• Ticketed Party Δ Event State — an EnvOpenProcess paired with a stable ticket map for its underlying process steps. Lifts Concurrent.ProcessOver.Ticketed to the env-open setting.
• Ticketed.enabledAt / Ticketed.firedAt — process-side ticket predicates evaluated on AsyncRun.
• Ticketed.WeakFairOn / StrongFairOn / WeakFair / StrongFair — process-side fairness predicates lifted from Concurrent.Fairness.
• SchedulerPair Party m State Event — the joint adversary type for the async runtime: a process scheduler plus a sibling env scheduler.
• secureAgainstFair mkSem real ideal ε isPPT isFair — fair-PPT computational emulation: every scheduler pair that is both PPT and fair distinguishes real from ideal with advantage at most ε.
• asympSecureAgainstFair — security-parameter-indexed, negligible variant.

Design notes

The pair (isPPT, isFair) is intentionally orthogonal: PPT does not imply fair delivery (an efficient adversary may starve a process), and fair delivery does not imply PPT execution (a fair scheduler may take unbounded internal computation between firings).

Three different "fairness" notions in the literature are not collapsed here. Scheduler fairness (TLA+ WF/SF, this file) is the only one captured by isFair arguments below. UC resource fairness is a property of the protocol design, and cryptographic fair exchange is a security goal for specific protocols; both compose orthogonally with secureAgainstFair.

Process tickets are the only ticket category lifted in this file. Env tickets reduce to Event itself, but their fairness story is governed entirely by the env scheduler (i.e. by the isFair predicate the user supplies). Lifting a unified ticket type carrying both process and env tickets is a deliberate non-goal at this stage: the two sides have different enable conditions and different adversary-control attributions and are easier to reason about separately.

Universe constraints

The lifted security layer pins move types, env state, env event alphabets, and the underlying open-process universes to 0. This matches the universe constraints already imposed by AsyncRuntime.lean (which threads ProbComp : Type → Type through the runtime), and is required for (openTheory.{u, 0, 0} Party).Closed to be well-formed.

Async runs

structure Interaction.UC.AsyncRun {Γ : Spec.Node.Context} {State Event : Type} (process : Concurrent.ProcessOver Γ) (envAction : EnvAction Event State) : Type u_1

AsyncRun process envAction is an infinite execution of the asynchronous runtime threading the RuntimeEvent Event alphabet.

It mirrors Concurrent.ProcessOver.Run shape-for-shape, with three extensions that match runStepsAsync:

• state n is the joint runtime state at step n, i.e. the residual process state plus the env-action bookkeeping state.
• event n records which side fired at step n: a processTick consumes the procTranscript, while an envTick e consumes the envSample.
• next_state n enforces the coherence law of one async step: at process ticks the proc field advances by the chosen transcript; at env ticks the env state advances to the sampled new state.

This is a freer object than the runtime's randomized executions (it does not commit to a particular scheduler); fairness predicates are phrased over AsyncRun rather than over the runtime distribution, exactly as Concurrent.ProcessOver.Ticketed.WeakFair is phrased over ProcessOver.Run.

• state : ℕ → AsyncRuntimeState process.Proc State

  The joint runtime state at each step.

• event : ℕ → RuntimeEvent Event

  The runtime event chosen at each step.

• procTranscript (n : ℕ) : (process.step (self.state n).proc).spec.Transcript

  The process-side transcript chosen at each step. Only constrained to be coherent when event n = .processTick; left unconstrained in the env-tick branch.

• envSample : ℕ → State

  The env-state result sampled at each step. Only constrained to be coherent when event n = .envTick e.

• next_state (n : ℕ) : self.state (n + 1) = match self.event n with | RuntimeEvent.processTick => let __src := self.state n; { proc := (process.step (self.state n).proc).next (self.procTranscript n), envState := __src.envState } | RuntimeEvent.envTick e => let __src := self.state n; { proc := __src.proc, envState := self.envSample n }

  One-step coherence: at process ticks the proc field advances by the chosen transcript, at env ticks the env state advances to the sampled new state.

def Interaction.UC.AsyncRun.initial {Γ : Spec.Node.Context} {State Event : Type} {process : Concurrent.ProcessOver Γ} {envAction : EnvAction Event State} (run : AsyncRun process envAction) : AsyncRuntimeState process.Proc State

The initial joint runtime state of an async run.

def Interaction.UC.AsyncRun.head {Γ : Spec.Node.Context} {State Event : Type} {process : Concurrent.ProcessOver Γ} {envAction : EnvAction Event State} (run : AsyncRun process envAction) : RuntimeEvent Event

The first runtime event of an async run.

Ticketed env-open processes

structure Interaction.UC.Ticketed (Party : Type) (m : Type → Type) (Δ : PortBoundary) (Event State : Type) : Type 1

Ticketed Party Δ Event State packages an EnvOpenProcess with a stable ticket map for its underlying open process.

This lifts Concurrent.ProcessOver.Ticketed to the env-open setting. The env channel is not assigned tickets here: env events are scheduled by the environment and are represented in the runtime trace by their alphabet symbol directly. Process tickets are the obligations whose firing fairness predicates constrain.

The bundle pins all relevant universes to 0 to match the runtime layer in AsyncRuntime.lean.

• toEnvProcess : EnvOpenProcess m Party Δ Event State

  The underlying env-open process.

• Ticket : Type

  The stable obligation type.

• ticket : self.toEnvProcess.process.toProcess.Tickets self.Ticket

  The stable ticket assigned to each complete process-step transcript.

@[reducible]

def Interaction.UC.Ticketed.process {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) : OpenProcess m Party Δ

The underlying open process of a ticketed env-open process.

@[reducible]

def Interaction.UC.Ticketed.envAction {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) : EnvAction Event State

The env-action channel of a ticketed env-open process.

def Interaction.UC.Ticketed.enabledAt {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) (n : ℕ) : Prop

A process ticket is enabled at step n of an async run when some transcript through the current process spec carries that ticket.

Equivalent to the synchronous Concurrent.ProcessOver.Ticketed.enabledAt evaluated at the process state (run.state n).proc. The env state is irrelevant because tickets only label process-step obligations.

def Interaction.UC.Ticketed.firedAt {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) (n : ℕ) : Prop

A process ticket fires at step n of an async run when:

1. the runtime fired a processTick at step n, and
2. the chosen transcript carries that ticket.

Note the asymmetry with the synchronous firedAt: an envTick at step n cannot fire a process ticket, even though the recorded procTranscript n is still well-formed. This matches the operational reading that env ticks do not advance the process side.

def Interaction.UC.Ticketed.WeakFairOn {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) : Prop

Weak fairness for a single process ticket: continuously enabled implies fired infinitely often.

Lifts Concurrent.ProcessOver.Ticketed.WeakFairOn to async runs, with the additional processTick precondition baked into firedAt (so the env scheduler cannot vacuously satisfy weak fairness by firing nothing but env ticks).

def Interaction.UC.Ticketed.StrongFairOn {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) : Prop

Strong fairness for a single process ticket: enabled infinitely often implies fired infinitely often.

Lifts Concurrent.ProcessOver.Ticketed.StrongFairOn to async runs, with the same processTick precondition as WeakFairOn.

def Interaction.UC.Ticketed.WeakFair {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) : Prop

An async run is weakly fair when every process ticket is.

def Interaction.UC.Ticketed.StrongFair {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) : Prop

An async run is strongly fair when every process ticket is.

theorem Interaction.UC.Ticketed.fired_implies_enabled {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) (n : ℕ) : ticketed.firedAt run ticket n → ticketed.enabledAt run ticket n

A process ticket fired at step n is enabled at step n.

theorem Interaction.UC.Ticketed.weakFairOn_of_strongFairOn {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) : ticketed.StrongFairOn run ticket → ticketed.WeakFairOn run ticket

Strong fairness implies weak fairness on the same ticket.

theorem Interaction.UC.Ticketed.weakFair_of_strongFair {Party : Type} {m : Type → Type} {Δ : PortBoundary} {Event State : Type} (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) : ticketed.StrongFair run → ticketed.WeakFair run

Strong fairness implies weak fairness for the whole run.

Scheduler pairs

structure Interaction.UC.SchedulerPair (Party : Type u) (m : Type → Type) (schedulerSampler : m (ULift.{0, 0} Bool)) (State Event : Type) : Type (max 1 u)

SchedulerPair Party m State Event bundles the two sibling samplers driving the async runtime: a process scheduler and an env scheduler, each indexed by the closed open-theory process they will run against.

This is the natural "joint adversary" type for the async runtime: fair-PPT security definitions quantify over scheduler pairs.

• proc (p : (openTheory Party m schedulerSampler).Closed) : ProcessScheduler m p.Proc State fun (st : AsyncRuntimeState p.Proc State) => (p.step st.proc).spec

  The process-side sampler, indexed by closed processes.

• env (p : (openTheory Party m schedulerSampler).Closed) : EnvScheduler m p.Proc State Event

  The env-side sampler, indexed by closed processes.

Fair PPT security

def Interaction.UC.secureAgainstFair {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} (mkSem : SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)) {Δ : PortBoundary} (real ideal : (openTheory Party m schedulerSampler).Obj Δ) (ε : ℝ) (isPPT isFair : SchedulerPair Party m schedulerSampler State Event → Prop) : Prop

Fair-PPT computational emulation up to advantage ε.

mkSem is a scheduler-parametric Semantics constructor: given a scheduler pair, it produces a Semantics for the open-process theory openTheory.{u, 0, 0} Party. The canonical instantiation is

fun s => processSemanticsAsync Party close envAction
  initState init s.proc s.env fuel observe

isPPT is the user's PPT class on scheduler pairs (typically specialized to PolyQueries-style query bounds plus polynomial runtime). isFair is the user's fairness class (typically expressed in terms of Ticketed.WeakFair / StrongFair evaluated on every run the scheduler pair could induce).

The two predicates are intentionally orthogonal. PPT does not imply fair delivery, and fair delivery does not imply PPT execution. Conflating them would lose the standard safety/liveness vs. complexity split familiar from TLA+ and from the PIOA literature.

theorem Interaction.UC.secureAgainstFair.of_compEmulates {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} {mkSem : SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)} {Δ : PortBoundary} {real ideal : (openTheory Party m schedulerSampler).Obj Δ} {ε : ℝ} {isPPT isFair : SchedulerPair Party m schedulerSampler State Event → Prop} (h : ∀ (scheds : SchedulerPair Party m schedulerSampler State Event), CompEmulates (mkSem scheds) ε real ideal) : secureAgainstFair mkSem real ideal ε isPPT isFair

Uniform CompEmulates against every scheduler pair implies fair-PPT security against any choice of isPPT and isFair.

theorem Interaction.UC.secureAgainstFair.refl {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} {mkSem : SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)} {Δ : PortBoundary} (isPPT isFair : SchedulerPair Party m schedulerSampler State Event → Prop) (W : (openTheory Party m schedulerSampler).Obj Δ) : secureAgainstFair mkSem W W 0 isPPT isFair

Self-emulation: every scheduler pair's induced semantics distinguishes a system from itself with advantage zero.

theorem Interaction.UC.secureAgainstFair.mono {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} {mkSem : SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)} {Δ : PortBoundary} {real ideal : (openTheory Party m schedulerSampler).Obj Δ} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) {isPPT isFair : SchedulerPair Party m schedulerSampler State Event → Prop} (h : secureAgainstFair mkSem real ideal ε₁ isPPT isFair) : secureAgainstFair mkSem real ideal ε₂ isPPT isFair

Weakening on the advantage bound.

theorem Interaction.UC.secureAgainstFair.mono_isPPT {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} {mkSem : SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)} {Δ : PortBoundary} {real ideal : (openTheory Party m schedulerSampler).Obj Δ} {ε : ℝ} {isPPT₁ isPPT₂ : SchedulerPair Party m schedulerSampler State Event → Prop} (hPPT : ∀ (scheds : SchedulerPair Party m schedulerSampler State Event), isPPT₁ scheds → isPPT₂ scheds) {isFair : SchedulerPair Party m schedulerSampler State Event → Prop} (h : secureAgainstFair mkSem real ideal ε isPPT₂ isFair) : secureAgainstFair mkSem real ideal ε isPPT₁ isFair

Weakening on the PPT class: a smaller PPT class quantifies over fewer schedulers, so security against the larger class implies security against the smaller class.

theorem Interaction.UC.secureAgainstFair.mono_isFair {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} {mkSem : SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)} {Δ : PortBoundary} {real ideal : (openTheory Party m schedulerSampler).Obj Δ} {ε : ℝ} {isPPT isFair₁ isFair₂ : SchedulerPair Party m schedulerSampler State Event → Prop} (hFair : ∀ (scheds : SchedulerPair Party m schedulerSampler State Event), isFair₁ scheds → isFair₂ scheds) (h : secureAgainstFair mkSem real ideal ε isPPT isFair₂) : secureAgainstFair mkSem real ideal ε isPPT isFair₁

Weakening on the fairness class: a smaller fairness class quantifies over fewer schedulers, so security against the larger class implies security against the smaller class.

def Interaction.UC.asympSecureAgainstFair {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} {Δ : PortBoundary} (mkSem : ℕ → SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)) (real ideal : ℕ → (openTheory Party m schedulerSampler).Obj Δ) (Adv : Type u_1) (isPPT isFair : Adv → Prop) (extract : Adv → ℕ → SchedulerPair Party m schedulerSampler State Event × (openTheory Party m schedulerSampler).Plug Δ) : Prop

Asymptotic version of secureAgainstFair: a security-parameter indexed family of mkSem constructors and (real, ideal) pairs is fair-secure when every PPT, fair adversary has negligible distinguishing advantage in the security parameter.

The shape mirrors AsympCompEmulates from Computational.lean: the adversary type Adv is opaque, equipped with PPT and fairness predicates, plus an extract function producing the scheduler pair and the closing plug at each security parameter.

theorem Interaction.UC.asympSecureAgainstFair.of_pointwise_bound {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} {Δ : PortBoundary} {mkSem : ℕ → SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)} {real ideal : ℕ → (openTheory Party m schedulerSampler).Obj Δ} {Adv : Type u_1} {isPPT isFair : Adv → Prop} {extract : Adv → ℕ → SchedulerPair Party m schedulerSampler State Event × (openTheory Party m schedulerSampler).Plug Δ} (f : ℕ → ENNReal) (hf : negligible f) (hbound : ∀ (_A : Adv) (n : ℕ), ENNReal.ofReal ((mkSem n (extract _A n).1).distAdvantage ((openTheory Party m schedulerSampler).close (real n) (extract _A n).2) ((openTheory Party m schedulerSampler).close (ideal n) (extract _A n).2)) ≤ f n) : asympSecureAgainstFair mkSem real ideal Adv isPPT isFair extract

A pointwise bound on the distinguishing advantage by a negligible function implies asymptotic fair-PPT security.

theorem Interaction.UC.asympSecureAgainstFair.of_secureAgainstFair {Party : Type u} {m : Type → Type} {schedulerSampler : m (ULift.{0, 0} Bool)} {State Event : Type} {Δ : PortBoundary} {mkSem : ℕ → SchedulerPair Party m schedulerSampler State Event → Semantics (openTheory Party m schedulerSampler)} {real ideal : ℕ → (openTheory Party m schedulerSampler).Obj Δ} {Adv : Type u_1} {isPPT isFair : Adv → Prop} {extract : Adv → ℕ → SchedulerPair Party m schedulerSampler State Event × (openTheory Party m schedulerSampler).Plug Δ} (ε : ℕ → ℝ) (hε : negligible fun (n : ℕ) => ENNReal.ofReal (ε n)) (h : ∀ (n : ℕ), secureAgainstFair (mkSem n) (real n) (ideal n) (ε n) (fun (s : SchedulerPair Party m schedulerSampler State Event) => ∃ (A : Adv), isPPT A ∧ (extract A n).1 = s) fun (s : SchedulerPair Party m schedulerSampler State Event) => ∃ (A : Adv), isFair A ∧ (extract A n).1 = s) : asympSecureAgainstFair mkSem real ideal Adv isPPT isFair extract

A family of secureAgainstFair bounds with negligible advantage sequence implies asymptotic fair-PPT security.