Momentary corruption: the CJSV22 corruption model

This file ships the momentary corruption model: the canonical adaptive corruption model with refresh-based healing introduced in Canetti, Jain, Swanberg, Varia, Universally Composable End-to-End Secure Messaging (CRYPTO 2022, §3.2). All names live under the MomentaryCorruption.* namespace so it is unambiguous which model (in the sense of CorruptionModel) is in scope.

The model captures:

• Adaptive compromise. The environment may issue compromise(m) for any machine m at any time, marking m's current epoch as compromised in the adversary's view.
• Refresh-based healing. A subsequent refresh(m) advances m's epoch counter and clears the current corrupted snapshot flag; future epochs are not (yet) compromised. This is the structural ingredient that lets the framework derive post-compromise security as a healing theorem rather than as an axiom.

The bundled value MomentaryCorruption.model Sid Pid is a CorruptionModel whose Event is Alphabet Sid Pid and whose State is State Sid Pid (the two-flag plus epoch tracking).

Contents

• Alphabet Sid Pid — inductive event alphabet compromise(m) | refresh(m), indexed by MachineId Sid Pid.
• Epoch — the per-machine refresh counter (a ℕ abbrev).
• State Sid Pid — two-flag corruption tracking (corrupted, compromised) plus the per-machine epoch counter.
• State.applyCompromise / State.applyRefresh — the canonical deterministic updates triggered by alphabet events.
• react — the Alphabet → State → ProbComp State reaction driving the model's EnvAction.
• envAction — the canonical EnvAction Alphabet State for the model.
• model Sid Pid — the bundled CorruptionModel value.
• Process Sid Pid Δ — the corruption-aware open-process abbreviation: EnvOpenProcess of a MachineProcess with this model's env channel.
• MachineProcess.withMomentaryCorruption — the standard wrapping that turns a MachineProcess into a Process.

Universe constraint

Sid and Pid live in Type (i.e. Type 0) because State participates in ProbComp-valued reactions and ProbComp : Type → Type. Concrete protocol identity types (ℕ, String, etc.) all satisfy this bound. The two OpenProcess universes (v, w) are exposed.

Additive design

The model is standalone: nothing here is threaded into OpenNodeProfile. Existing OpenProcess constructions are untouched. The corruption-aware composition operators (par / wire / plug lifted from OpenTheory) and the four *.corrupt forwarding lemmas (CJSV22 §4.2) live in a downstream layer that consumes Process and the model's bundled envAction; this file ships only the data and the per-event reactions.

Decidability

All comparisons are over MachineId (which derives DecidableEq from [DecidableEq Sid] [DecidableEq Pid]) and over Epoch = ℕ. The deterministic state updates require [DecidableEq Sid] [DecidableEq Pid]; the alphabet, state, and process types themselves do not.

Alphabet and epoch

inductive Interaction.UC.MomentaryCorruption.Alphabet (Sid Pid : Type) : Type

The momentary-corruption event alphabet.

• compromise m snapshots the current state of machine m into the adversary's view: a leakage observer (declared separately, e.g. via SnapshotLeakable) fires, and the current epoch of m is marked compromised in the bookkeeping state.
• refresh m advances the epoch counter for m and clears the current snapshot flag. After a refresh, future epochs of m are not (yet) compromised; the protocol's forward-secrecy mechanism gets a chance to heal.

The pair (compromise, refresh) is what makes corruption momentary (rather than persistent): at any point the environment may compromise a machine, and a subsequent refresh recovers post-compromise security for future epochs.

• compromise {Sid Pid : Type} (m : MachineId Sid Pid) : Alphabet Sid Pid

  Snapshot the current state of m into the adversary's view.

• refresh {Sid Pid : Type} (m : MachineId Sid Pid) : Alphabet Sid Pid

  Advance the epoch counter of m, enabling forward healing.

def Interaction.UC.MomentaryCorruption.instDecidableEqAlphabet.decEq {Sid✝ Pid✝ : Type} [DecidableEq Sid✝] [DecidableEq Pid✝] (x✝ x✝¹ : Alphabet Sid✝ Pid✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Interaction.UC.MomentaryCorruption.instDecidableEqAlphabet {Sid✝ Pid✝ : Type} [DecidableEq Sid✝] [DecidableEq Pid✝] : DecidableEq (Alphabet Sid✝ Pid✝)

def Interaction.UC.MomentaryCorruption.Alphabet.target {Sid Pid : Type} : Alphabet Sid Pid → MachineId Sid Pid

The machine targeted by an event.

@[simp]

theorem Interaction.UC.MomentaryCorruption.Alphabet.target_compromise {Sid Pid : Type} (m : MachineId Sid Pid) : (compromise m).target = m

@[simp]

theorem Interaction.UC.MomentaryCorruption.Alphabet.target_refresh {Sid Pid : Type} (m : MachineId Sid Pid) : (refresh m).target = m

@[reducible, inline]

abbrev Interaction.UC.MomentaryCorruption.Epoch : Type

Epoch indexes the per-machine refresh cycles.

A flat ℕ is the simplest concrete choice: refresh counts as epoch m += 1. Richer protocols (e.g. Signal's asymmetric ratchet with separate sending and receiving counters) can wrap this in their own Epoch-isomorphic type; the model only requires DecidableEq and a way to advance.

Bookkeeping state

structure Interaction.UC.MomentaryCorruption.State (Sid Pid : Type) : Type

State Sid Pid packages the two-flag corruption tracking that the model carries between events.

• corrupted m = true iff the current state of m has been snapshotted by the adversary at least once and not refreshed since. Mutated by compromise m (sets true) and refresh m (sets false).
• compromised m e = true iff the secrets for epoch e of m are in the adversary's view. Strictly accumulating: a compromise event sets compromised m (current_epoch m); epochs once compromised stay compromised forever.
• epoch m is m's current refresh counter. Mutated by refresh m (increments by one).

The two flags corrupted and compromised are deliberately independent:

• corrupted m may be false while compromised m e holds for some past e: the adversary saw that epoch's secret, but the machine has since refreshed and now has a fresh secret.
• corrupted m may be true while compromised m e' is false for some future e': a forward-secret key schedule may forward-decrypt only a bounded window from a current compromise.

Two flags, two distinct purposes. The naming deliberately avoids the ambiguous "exposed", which would collide with OpenTheory's boundary-exposure terminology.

• corrupted : MachineId Sid Pid → Bool

  Per-machine snapshot flag, mutated by compromise and refresh.

• compromised : MachineId Sid Pid → Epoch → Bool

  Per-(machine, epoch) leak flag, monotonically accumulating.

• epoch : MachineId Sid Pid → Epoch

  Per-machine refresh counter, advanced by refresh.

theorem Interaction.UC.MomentaryCorruption.State.ext {Sid Pid : Type} {x y : State Sid Pid} (corrupted : x.corrupted = y.corrupted) (compromised : x.compromised = y.compromised) (epoch : x.epoch = y.epoch) : x = y

theorem Interaction.UC.MomentaryCorruption.State.ext_iff {Sid Pid : Type} {x y : State Sid Pid} : x = y ↔ x.corrupted = y.corrupted ∧ x.compromised = y.compromised ∧ x.epoch = y.epoch

def Interaction.UC.MomentaryCorruption.State.init {Sid Pid : Type} : State Sid Pid

The fully-honest initial state: nothing corrupted, nothing compromised, every machine at epoch zero.

@[implicit_reducible]

instance Interaction.UC.MomentaryCorruption.State.instInhabited {Sid Pid : Type} : Inhabited (State Sid Pid)

@[simp]

theorem Interaction.UC.MomentaryCorruption.State.corrupted_init {Sid Pid : Type} (m : MachineId Sid Pid) : init.corrupted m = false

@[simp]

theorem Interaction.UC.MomentaryCorruption.State.compromised_init {Sid Pid : Type} (m : MachineId Sid Pid) (e : Epoch) : init.compromised m e = false

@[simp]

theorem Interaction.UC.MomentaryCorruption.State.epoch_init {Sid Pid : Type} (m : MachineId Sid Pid) : init.epoch m = 0

def Interaction.UC.MomentaryCorruption.State.applyCompromise {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : State Sid Pid

Apply compromise m to the bookkeeping state: set corrupted m and mark the current epoch of m as compromised. The epoch counter is not advanced.

This is a deterministic update, so the value lives in the underlying State; the canonical EnvAction reaction wraps it via pure.

def Interaction.UC.MomentaryCorruption.State.applyRefresh {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : State Sid Pid

Apply refresh m to the bookkeeping state: clear corrupted m and advance the epoch counter of m by one. Past compromised flags are preserved (they are historical and accumulate).

After a refresh, future events on m write into the new epoch; this is the structural ingredient that lets the model derive PCS (post-compromise security) as a healing theorem rather than as an axiom.

@[simp]

theorem Interaction.UC.MomentaryCorruption.State.corrupted_applyCompromise_self {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : (applyCompromise m cs).corrupted m = true

theorem Interaction.UC.MomentaryCorruption.State.corrupted_applyCompromise_of_ne {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] {m m' : MachineId Sid Pid} (h : m' ≠ m) (cs : State Sid Pid) : (applyCompromise m cs).corrupted m' = cs.corrupted m'

@[simp]

theorem Interaction.UC.MomentaryCorruption.State.corrupted_applyRefresh_self {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : (applyRefresh m cs).corrupted m = false

theorem Interaction.UC.MomentaryCorruption.State.corrupted_applyRefresh_of_ne {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] {m m' : MachineId Sid Pid} (h : m' ≠ m) (cs : State Sid Pid) : (applyRefresh m cs).corrupted m' = cs.corrupted m'

@[simp]

theorem Interaction.UC.MomentaryCorruption.State.epoch_applyCompromise {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : (applyCompromise m cs).epoch = cs.epoch

@[simp]

theorem Interaction.UC.MomentaryCorruption.State.epoch_applyRefresh_self {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : (applyRefresh m cs).epoch m = cs.epoch m + 1

theorem Interaction.UC.MomentaryCorruption.State.epoch_applyRefresh_of_ne {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] {m m' : MachineId Sid Pid} (h : m' ≠ m) (cs : State Sid Pid) : (applyRefresh m cs).epoch m' = cs.epoch m'

theorem Interaction.UC.MomentaryCorruption.State.compromised_applyCompromise_self_currentEpoch {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : (applyCompromise m cs).compromised m (cs.epoch m) = true

theorem Interaction.UC.MomentaryCorruption.State.compromised_applyCompromise_of_compromised {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] {cs : State Sid Pid} {m m' : MachineId Sid Pid} {e : Epoch} (h : cs.compromised m' e = true) : (applyCompromise m cs).compromised m' e = true

compromise is monotone: once an epoch is in the adversary's view, it stays in the adversary's view. This is the structural fact that makes PCS (post-compromise security) about future epochs rather than about un-leaking past ones.

@[simp]

theorem Interaction.UC.MomentaryCorruption.State.compromised_applyRefresh {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : (applyRefresh m cs).compromised = cs.compromised

refresh preserves all past compromise flags.

Reaction and bundled model

def Interaction.UC.MomentaryCorruption.react {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (s : Alphabet Sid Pid) (cs : State Sid Pid) : ProbComp (State Sid Pid)

The canonical EnvAction reaction for the momentary-corruption alphabet: compromise snapshots, refresh advances the epoch.

This is the baseline used by every protocol that opts in to momentary corruption. Protocols that need richer per-event behaviour (e.g. simulator-controlled randomization on compromise, or a non-trivial leakage function) build their own EnvAction rather than overriding individual branches here.

def Interaction.UC.MomentaryCorruption.envAction {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] : EnvAction (Alphabet Sid Pid) (State Sid Pid)

The canonical momentary-corruption EnvAction.

@[simp]

theorem Interaction.UC.MomentaryCorruption.react_compromise {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : react (Alphabet.compromise m) cs = pure (State.applyCompromise m cs)

@[simp]

theorem Interaction.UC.MomentaryCorruption.react_refresh {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] (m : MachineId Sid Pid) (cs : State Sid Pid) : react (Alphabet.refresh m) cs = pure (State.applyRefresh m cs)

@[simp]

theorem Interaction.UC.MomentaryCorruption.envAction_react {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] : envAction.react = react

def Interaction.UC.MomentaryCorruption.model (Sid Pid : Type) [DecidableEq Sid] [DecidableEq Pid] : CorruptionModel

The momentary-corruption model bundled as a CorruptionModel.

Use this when you want to talk about the model abstractly through the CorruptionModel API — for instance, when stating a lemma that is generic over corruption models but instantiated to the momentary case at a use site.

@[simp]

theorem Interaction.UC.MomentaryCorruption.model_Event {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] : (model Sid Pid).Event = Alphabet Sid Pid

@[simp]

theorem Interaction.UC.MomentaryCorruption.model_State {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] : (model Sid Pid).State = State Sid Pid

@[simp]

theorem Interaction.UC.MomentaryCorruption.model_envAction {Sid Pid : Type} [DecidableEq Sid] [DecidableEq Pid] : (model Sid Pid).envAction = envAction

Canonical corruption-aware open process

@[reducible, inline]

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

Process Sid Pid Δ is the canonical open process for the momentary-corruption model: a MachineProcess Sid Pid Δ paired with this model's env channel.

Type-level definition does not depend on [DecidableEq Sid] [DecidableEq Pid]; the typeclass requirements only appear when one constructs the env action's reaction (e.g. via MachineProcess.withMomentaryCorruption).

def Interaction.UC.MachineProcess.withMomentaryCorruption {Sid Pid : Type} {m : Type w → Type w'} {Δ : PortBoundary} [DecidableEq Sid] [DecidableEq Pid] (P : MachineProcess Sid Pid m Δ) : MomentaryCorruption.Process Sid Pid m Δ

Wrap a MachineProcess Sid Pid Δ with the canonical momentary-corruption env channel, yielding a MomentaryCorruption.Process.

This is the standard inhabitant: compromise(m) snapshots m's current epoch into the adversary's view (sets corrupted m and compromised m (epoch m)), and refresh(m) advances m's epoch counter and clears corrupted m.

Protocols that need richer per-event behaviour (e.g. simulator-controlled randomization on compromise, or a non-trivial leakage function that depends on the protocol state) build their EnvOpenProcess directly with a bespoke EnvAction rather than going through this wrapping.

@[simp]

theorem Interaction.UC.MachineProcess.process_withMomentaryCorruption {Sid Pid : Type} {m : Type w → Type w'} {Δ : PortBoundary} [DecidableEq Sid] [DecidableEq Pid] (P : MachineProcess Sid Pid m Δ) : P.withMomentaryCorruption.process = P

@[simp]

theorem Interaction.UC.MachineProcess.envAction_withMomentaryCorruption {Sid Pid : Type} {m : Type w → Type w'} {Δ : PortBoundary} [DecidableEq Sid] [DecidableEq Pid] (P : MachineProcess Sid Pid m Δ) : P.withMomentaryCorruption.envAction = MomentaryCorruption.envAction

@[simp]

theorem Interaction.UC.MachineProcess.react_withMomentaryCorruption_compromise {Sid Pid : Type} {m : Type w → Type w'} {Δ : PortBoundary} [DecidableEq Sid] [DecidableEq Pid] (P : MachineProcess Sid Pid m Δ) (mid : MachineId Sid Pid) (cs : MomentaryCorruption.State Sid Pid) : EnvOpenProcess.react P.withMomentaryCorruption (MomentaryCorruption.Alphabet.compromise mid) cs = pure (MomentaryCorruption.State.applyCompromise mid cs)

@[simp]

theorem Interaction.UC.MachineProcess.react_withMomentaryCorruption_refresh {Sid Pid : Type} {m : Type w → Type w'} {Δ : PortBoundary} [DecidableEq Sid] [DecidableEq Pid] (P : MachineProcess Sid Pid m Δ) (mid : MachineId Sid Pid) (cs : MomentaryCorruption.State Sid Pid) : EnvOpenProcess.react P.withMomentaryCorruption (MomentaryCorruption.Alphabet.refresh mid) cs = pure (MomentaryCorruption.State.applyRefresh mid cs)