Actor Suspension (C18)

Table of contents

Actor Suspension (C18)

A regulated composition: when an actor must be deactivated — a departing employee, a compromised account, a contractor whose engagement ended — every surface through which that actor can still act must be closed in one operation, and the closure must be provable from the records. C18 is Login’s outbound-side counterpart: where Login wires credential-verification to session-issuance on the way in, C18 wires actor-suspension to the revocation of every active Permissions grant and every active Session on the way out, attests the whole act through one tamper-evident Audit Trail event, and (optionally) revokes the actor’s Credential so it cannot re-authenticate. It composes Actor Identity (the actor whose Active→Suspended lifecycle the composition introduces), Permissions, Session, and Audit Trail as a substrate (reaching Event Log + Actor Identity + Tamper Evidence + Retention Window transitively); Credential is an optional fifth constituent. Three emergent invariants: atomicity of multi-surface revocation — after suspend_actor succeeds, the actor has zero active grants and zero active sessions, committed as one transaction with no partial state (the load-bearing claim); audit completeness — the actor.suspended event enumerates every grant_id and session_token revoked; and suspension cascade ordering — the Active→Suspended transition gates the cascade, and a second suspend_actor against an already-Suspended actor is a no-op. The default posture is all-or-nothing under one transaction.

Intent

Every system that distinguishes actors eventually has to un-distinguish one. An employee leaves; a credential is found in a paste dump; a contractor’s engagement ends; an account shows the signature of a takeover. The obligation that follows is deceptively simple to state and notoriously easy to botch: cut off every way that actor can still act, now, and be able to prove afterward that you did. The botch is always the same shape — access is revoked on one surface but not another. The session cookie is invalidated but the API token’s permission grant is still active; the role is removed but a long-lived session keeps working; the login credential is disabled but a service grant the actor still holds quietly authorizes a scheduled job. Each gap is a half-open door, and a half-suspended actor is more dangerous than an un-suspended one, because the system and its operators believe the actor is locked out.

This is the friction C18 exists to resolve, and naming it precisely keeps the composition honest: C18 is not an “account deactivation feature”; it is a multi-surface atomic de-authorization with a records-alone completeness proof. An actor’s ability to act is spread across two independent authorization surfaces that no single atom relates: Permissions holds the grants that say what the actor may do, and Session holds the live authenticated channels that say the actor is currently acting. Revoking one without the other leaves a door open. Worse, each surface has its own multiplicity — an actor may hold many grants (issued at different times, by different grantors) and many sessions (one per device) — so closure on each surface is itself an enumerate-then-revoke-each operation, exactly the mass-revocation pattern Permissions names as the composing system’s responsibility (“enumerate all active grants where grant.subject_ref = departing_subject, then call revoke(grant_id) for each”) and Session supports through its principal_ref-queryable store (“revoke all sessions for this account”). The structure that snapshots both surfaces, revokes every member of both, sets the actor’s suspension state, and seals the whole act as one attributed, tamper-evident record belongs to no single constituent. It belongs to the composition, and this composition is that structure.

C18 is Login’s mirror image, and the symmetry is load-bearing. Login (C13) is the inbound wiring: Credential.verify → Session.issue, with the emergent cascade that revoking a credential terminates the derived sessions. C18 is the outbound wiring: suspend → revoke every grant + revoke every session, with the emergent guarantee that suspension closes all surfaces at once. Login’s cascade walks an active-session set under a snapshot and tolerates partial completion (a per-session storage failure is logged and the cascade continues — partial revocation beats none). C18 makes the opposite default choice, and the difference is deliberate: a suspension that half-completes leaves an ambiguous security state, so C18’s default is all-or-nothing under one transaction — the actor is either fully de-authorized or the operation visibly fails and is retried, never silently half-done. The same TOCTOU (time-of-check-to-time-of-use) race Login surfaced as finding FC1 in its Final Critique 4 — a concurrent terminal transition during the cascade — recurs here and is resolved the same way: a grant or session the cascade targets that another process already revoked is found already-terminal and counted, not re-revoked.

This is a composition, not a new primitive. Actor Identity, Permissions, Session, and Audit Trail are unchanged; C18 is the wiring that makes them coherent as one suspension surface. It introduces emergent actions — suspend_actor, the read-only suspension_report, and the thin reinstate_actor — and an emergent state machine the constituents do not carry: the actor’s Active → Suspended lifecycle. Actor Identity is the attestation atom, with a single Attested state and no actor lifecycle (it explicitly defers actor registration, deactivation, and suspension to a forthcoming Actor Registry / Identity Provisioning pattern); the Active/Suspended state is therefore a composition-introduced surface C18 owns, not a state read from any constituent.

What the composition is not: it is not the issuance surface — it revokes grants and sessions but never issues them (Permissions.grant and Session.issue are called elsewhere), so it cannot, by itself, prevent a new grant or session being created for a suspended actor after the cascade snapshot (a named composing-layer obligation, exactly as Login’s cascade is snapshot-scoped); it is not the actor registry that provisions actor identities; it is not an authorization-policy engine deciding whether an actor should be suspended (that is wired ahead of suspend_actor at the administrative / Multi-Party Approval layer); and it does not restore access on reinstatement — reinstate_actor lifts the suspension state but never un-revokes a terminal grant or session (re-provisioning is the issuance layer’s job). Each is named explicitly in Edge cases.

Summary

Actor Suspension is a regulated composition — a specification that wires several freestanding patterns together — that does one job thoroughly: when you need to cut off an actor (a departing employee, a hacked account, a contractor who’s done), it closes every door at once and leaves proof. The problem it solves is the classic security gap where someone’s access is pulled in one place but not another — their login is disabled but a permission grant still works, or their role is removed but an open session keeps going. C18 makes that impossible by treating suspension as a single all-or-nothing action: it finds every active permission grant the actor holds and every active login session they have, revokes all of them together, marks the actor as suspended, and writes one tamper-proof audit record that lists every grant and session it revoked. If any part of that can’t complete, the whole thing rolls back and nothing changes — because a half-suspended actor (some access cut, some not) is worse than one who wasn’t touched, since everyone would wrongly believe they were locked out. Optionally, it also revokes the actor’s login credential so they can’t sign back in.

It is the exact mirror of the Login pattern: Login wires up “check the credential, then start a session” on the way in; this wires up “suspend the actor, then revoke every grant and every session” on the way out. The composition’s defining emergent guarantee — a property that exists only when the patterns are combined — is that single multi-surface revocation: after a successful suspension, the actor provably holds zero active grants and zero active sessions, and the audit record names every one that was revoked. Its common uses are exactly the moments compliance regimes care about most: offboarding a terminated employee (the access must be removed promptly and provably), responding to a compromised account, and ending a third-party’s access. Any system that must deactivate an actor across multiple access surfaces at once — and prove from the records that nothing was missed — is a candidate for this composition.

Composes

Actor Identity — the identity of the actor being suspended. C18 introduces the actor’s Active → Suspended lifecycle as a composition-introduced state machine, because Actor Identity carries no lifecycle state of its own (a single Attested state, with actor registration / deactivation / suspension explicitly deferred to a forthcoming Actor Registry / Identity Provisioning pattern). The actor_ref is the suspension subject and the join key across the two authorization surfaces. C18 does not mutate any attestation (they are immutable — Actor Identity Invariant 1); the attestation surface enters via the Audit Trail substrate, which attests the actor.suspended event under the suspending operator’s credential.
Permissions — the grant surface, used in both directions. Read: suspend_actor enumerates the actor’s active grants by querying the grant store for {grant_id} where subject_ref = actor_ref and status = Active (the grant store is queryable; Permissions’ Behavior section exposes per-grant fields to composing systems). Write: the cascade calls Permissions.revoke(grant_id) → ok | rejected(not-known | not-active | storage-failure) for each enumerated grant — Permissions provides no bulk-revoke surface, and naming the per-grant enumerate-then-revoke as the composing system’s responsibility is Permissions’ own Mass revocation on subject deprovisioning edge case. C18 is that composing system. A revoke reaching an already-not-active grant (a concurrent revocation) is the benign TOCTOU case (below), not an error.
Session — the live-channel surface, used in both directions. Read: suspend_actor enumerates the actor’s active sessions by querying the session store for {session_token} where principal_ref = actor_ref and status = Active (Session’s store is principal_ref-queryable precisely to support “show all active sessions for this account” and “revoke all sessions for this account” administrative operations). Write: the cascade calls Session.revoke(session_token, revoked_by_ref = suspended_by_ref, reason) → revoked | rejected(invalid-request | already-terminal | not-known | storage-failure) for each active session. A session that became terminal between the snapshot and the revoke returns already-terminal — the benign TOCTOU case, counted as skipped exactly as Login’s Final Critique 4 (finding FC1) handles it.
Audit Trail — the regulated-audit substrate: C18 names it the way an atom is named and reaches Event Log, Actor Identity, Tamper Evidence, and Retention Window transitively through it (per the Compositions of compositions convention — see spec-format.md), maintaining one Audit Trail instance for all suspension events. C18 records the actor.suspended event by calling AuditTrail.record_action(action_ref, actor_ref, credential, data) → event_id | rejected(invalid-credential | invalid-request | recording-failure) directly on the one Audit Trail instance the substrate carries — the established substrate-composition pattern (Multi-Party Approval and C7 record their own events on the Audit Trail their substrate carries). The capability is Audit Trail’s own declared record_action and its Invariant 1 (attribution coverage), reached through the named substrate — not an ambient reach-through. The event’s data carries the complete enumeration of every revoked grant_id and session_token (Invariant 2). The substrate seals the event (Tamper Evidence) and governs its retention (Retention Window) so the suspension record outlives the access it closed.
Credential (optional fifth constituent) — when composed, the cascade additionally calls Credential.revoke(credential_id, revoked_by_ref = suspended_by_ref, reason) → revoked | rejected(...) on the actor’s authentication credential so the suspended actor cannot re-authenticate to establish a new session. This closes the re-entry door the grant/session revocation alone leaves open (revoking current sessions does not stop a new login). When Credential is not composed, closing that door is a named composing obligation (the deployment revokes the credential through Login’s surface, or wires C18 with Credential). Including Credential makes C18 the full outbound counterpart to Login’s inbound Credential.verify → Session.issue.

The Permissions grant store, the Session store, and (when composed) the Credential store are owned by their respective constituent instances; the Event Log, Actor Identity attestation store, Tamper Evidence seal store, and Retention Window store are owned by the Audit Trail substrate. C18 owns no constituent state — it owns the emergent actor_suspension_state map and indexes the suspension events through the substrate.

A surface C18 needs that crosses the two authorization surfaces is the unified actor namespace: the actor_ref must be the same identity under which the actor holds Permissions grants (as subject_ref) and Session sessions (as principal_ref). This unification is the precise concept the Authenticated Actor (C17) composition establishes as a principal_ref ↔ actor_ref bijection, and the precise gap demos/attributed-permissions-admin/CORNERS.md §Cross-atom identity surface aliasing flags when it diverges. C18 names the unification as a deployment precondition (Configuration) — satisfied by C17 as a named composing peer or by deployment convention — rather than composing C17 directly; the enumeration’s correctness is conditional on it, an externally-clearable check (Generation acceptance).

Composition logic

Composition state

The composition owns emergent state that wires the constituents into one suspension surface. None of this state belongs to a single constituent.

actor_suspension_state — map from actor_ref to {state, suspended_at?, suspended_by_ref?, reason?, suspension_event_id?} where state ∈ {Active, Suspended}. An actor_ref absent from the map is treated as Active (the default — no suspension has been recorded). Populated/transitioned by suspend_actor (Active → Suspended) and reinstate_actor (Suspended → Active). This is the composition-introduced actor lifecycle the constituents do not carry. The suspension_event_id binds the Suspended state to the sealed actor.suspended Audit Trail event that enumerates what was revoked.

suspension_log — append-only record of every suspend_actor and reinstate_actor call, whether it transitioned, was a no-op, or failed. Each entry: entry_id (opaque, system-generated), actor_ref, operation (suspend reinstate), outcome (suspended reinstated already-suspended already-active revocation-failure(surface) recording-failure invalid-request), revoked_grants (the grant_id set, on success), revoked_sessions (the session_token set, on success), suspension_event_id?, attempted_at. This is the composition’s composition-layer query surface; the Audit Trail substrate is the tamper-evident external-auditor record of the same suspension events. The two are redundant by design, exactly as Login pairs its login_event_log with the Audit Trail.

The actor’s grants live in the Permissions store, its sessions in the Session store, its (optional) credential in the Credential store, and the suspension events in the Audit Trail substrate. C18 duplicates none of them; it transitions the suspension state and binds each suspension to the sealed event that records the revoked set.

The enumerated active set for an actor_ref — its active grants and active sessions — is not stored as standing state; it is computed at suspension time by querying the Permissions and Session stores. The sealed actor.suspended event’s enumerated {revoked_grants, revoked_sessions} is the durable, records-alone snapshot of that set at suspension time.

Configuration

unified_actor_namespace — a deployment-declared precondition (default enforced) asserting that the actor_ref C18 suspends is the same identity value under which the actor holds Permissions grants (as subject_ref) and Session sessions (as principal_ref). This is the declaring source (capability provenance) for the enumeration’s correctness: C18 enumerates subject_ref = actor_ref grants and principal_ref = actor_ref sessions, which is complete only if the namespaces coincide. A deployment satisfies this via the Authenticated Actor (C17) principal_ref ↔ actor_ref binding (a named composing peer) or by convention; whether the namespaces actually coincide is an externally-clearable check (Generation acceptance). A deployment whose namespaces diverge under-enumerates and produces an incomplete suspension — the audit-gap the CORNERS finding flags.
revoke_credential_on_suspend — whether the cascade also revokes the actor’s authentication credential (requires the optional Credential constituent). Default true when Credential is composed; absent otherwise. When false or Credential is uncomposed, closing the re-authentication door is a named composing obligation (Edge cases — Re-authentication after suspension).
audit_trail_retention_policy — inherited, not re-configured. C18 records its actor.suspended / actor.reinstated events on the Audit Trail substrate, which carries the host’s regulatory retention policy; record_action takes the policy via the substrate’s configured value. The suspension events should persist at least as long as the longest retention obligation over the access they closed — often longer, for post-offboarding dispute defensibility (the access is gone; the proof it was lawfully closed must outlive it).
partial_failure_posture — all-or-nothing (default) or best-effort. The default rolls the whole cascade back on any constituent revoke failure (no partial state — Invariant 1). best-effort (the Login-style posture, for deployments that prefer maximal closure over atomicity) continues the cascade on a per-surface failure, records the failure, and surfaces a revocation-failure(surface) finding — explicitly weakening Invariant 1 to snapshot-scoped-best-effort. The default is all-or-nothing precisely because a half-suspended actor is a worse security state than a cleanly-failed one.

Primitive policies

actor_ref — opaque reference to the actor being suspended; the key of actor_suspension_state and the join key (= subject_ref = principal_ref under unified_actor_namespace). Must contain at least one non-whitespace character (invalid-request). Byte-identity equality; never normalized.
suspended_by_ref — non-empty reference to the operator performing the suspension; flows to Session.revoke (as revoked_by_ref), Credential.revoke (as revoked_by_ref), and AuditTrail.record_action (as actor_ref), so the records attribute the suspension to one operator. Whether suspended_by_ref is authorized to suspend actors is a named composing concept (Edge cases — Suspension authorization), exactly as Login leaves logout authorization to a composing layer.
credential — the suspending operator’s opaque credential, consumed by AuditTrail.record_action (and the Actor Identity reached through the substrate) to attest the suspension event; never persisted by C18.
reason — non-empty string naming why the actor is suspended; carried into each Session.revoke / Credential.revoke reason and the actor.suspended event. Mandatory (a suspension without a stated reason is a compliance finding — Permissions, Session, and Credential each require a non-empty reason on revoke).
grant_id / session_token / credential_id — opaque constituent handles surfaced by the enumeration; passed to the respective revoke. Opaque; never normalized.

No primitive is case-sensitivity-normalized at the composition layer; deployments wanting normalization wire it at the calling layer before invoking composition actions.

Action wiring

The composition exposes three actions: one emergent multi-surface suspension (suspend_actor), one read-only query (suspension_report), and one thin lifecycle-reversal (reinstate_actor).

Uniform constituent-rejection mapping. Each constituent revoke maps its rejection taxonomy as named per step. Under the all-or-nothing posture, any non-benign revoke failure aborts the transaction and rolls back (no partial state); under best-effort, it is recorded and the cascade continues. A Permissions.revoke → not-active or Session.revoke → already-terminal is benign in both postures — the target is already terminal, which is the cascade’s goal (the TOCTOU already-terminal case), counted as skipped, never an abort.

`suspend_actor`

suspend_actor(actor_ref, suspended_by_ref, credential, reason) →
  {suspended, revoked_grants, revoked_sessions, revoked_credential?, event_id}
 | rejected(
   invalid-request
  | already-suspended
  | revocation-failure
  | recording-failure
  )

Suspends an actor by atomically revoking every active Permissions grant and every active Session (and, optionally, the actor’s Credential), transitioning the actor to Suspended, and sealing the complete revoked set into one attributed Audit Trail event. Steps:

Validate: actor_ref, suspended_by_ref, credential, reason each non-empty. Any violation → append suspension_log {operation: suspend, outcome: invalid-request}; return rejected(invalid-request). Stop.
Suspension-state gate (Active → Suspended; the cascade ordering, Invariant 3). Read actor_suspension_state[actor_ref]. If state = Suspended → append suspension_log {outcome: already-suspended}; return rejected(already-suspended) and change no state — the cascade does not re-run (no-op on already-Suspended; the second suspension is idempotent). An actor_ref absent from the map is Active and proceeds.
Snapshot the active set (read-only, atomic with the cascade). Enumerate the actor’s active grants G = {grant_id : subject_ref = actor_ref ∧ status = Active} from the Permissions store and active sessions S = {session_token : principal_ref = actor_ref ∧ status = Active} from the Session store. The snapshot read and the cascade writes in steps 4–6 are one serialized transaction keyed on actor_ref (the host transaction boundary, exactly as Login’s cascade and Audit Trail’s cascade-on-purge commit in one transactional boundary), so no concurrently-issued grant or session is half-covered: a grant/session created after the snapshot is not in G/S and is not covered by this suspension (snapshot-scoped — Invariant 1’s stated bound, and the Suspension is snapshot-scoped edge case). An empty G and S is a valid suspension (an actor with no active access is still recorded as Suspended) — distinct from any failure.
Cascade — revoke every member of both surfaces (and optionally the credential). Within the transaction:
- For each grant_id ∈ G: Permissions.revoke(grant_id). ok → add to revoked_grants. not-active (a concurrent revocation already terminalized it) → benign, add to revoked_grants (the goal is met). not-known → an enumeration/store inconsistency (a grant the query returned but the store no longer knows — structurally near-impossible, since Permissions never deletes grants, Invariant 10): treated as a non-benign failure, handled exactly as storage-failure — abort and return rejected(revocation-failure) under all-or-nothing, or record revocation-failure(permissions) and continue under best-effort — and additionally surfaced as a high-priority store-inconsistency finding in suspension_log. storage-failure → abort under all-or-nothing (roll back; the grant stays whatever it was), or record revocation-failure(permissions) and continue under best-effort.
- For each session_token ∈ S: Session.revoke(session_token, revoked_by_ref = suspended_by_ref, reason). revoked → add to revoked_sessions. already-terminal (the TOCTOU already-terminal case — a concurrent logout/expiry/cascade terminalized it) → benign, add to revoked_sessions. not-known → enumeration/store inconsistency (structurally near-impossible — Session is durable, Invariant 9): a non-benign failure handled exactly as the grant case — abort and return rejected(revocation-failure) under all-or-nothing, or record revocation-failure(session) and continue under best-effort — and surfaced as a high-priority store-inconsistency finding in suspension_log. storage-failure → abort under all-or-nothing, or record revocation-failure(session) and continue under best-effort.
- If revoke_credential_on_suspend and Credential is composed: Credential.revoke(credential_id, revoked_by_ref = suspended_by_ref, reason). revoked → set revoked_credential = credential_id. already-terminal → benign (already revoked/rotated/expired). storage-failure → abort / record per posture.
Transition and bind (still within the transaction). Set actor_suspension_state[actor_ref] = {state: Suspended, suspended_at: now, suspended_by_ref, reason, suspension_event_id: <pending>}.
Seal the act — record_action carrying the complete enumeration (Invariant 2). Call AuditTrail.record_action(action_ref = actor.suspended, actor_ref = suspended_by_ref, credential, data = {suspended_actor: actor_ref, revoked_grants, revoked_sessions, revoked_credential?, reason, suspended_at = now}) → event_id; set suspension_event_id = event_id. The data carries the complete revoked set (or, for a very large set, a cryptographic digest of it — mechanism-neutral exactly as C6/C7 treat their large payloads), so the enumeration is sealed and tamper-evident: a later silent edit to the recorded set breaks the seal. Map the substrate’s rejection: invalid-credential / invalid-request / recording-failure → abort under all-or-nothing (roll back the whole cascade — the suspension never happened, retry against intact state) and return rejected(recording-failure); under best-effort the revokes have already committed and the orphan (revoked access with no sealed suspension event) is handled per the Cross-store consistency under partial failure edge case.
Commit the transaction. Append suspension_log {operation: suspend, outcome: suspended, revoked_grants, revoked_sessions, suspension_event_id: event_id}. Return {suspended, revoked_grants, revoked_sessions, revoked_credential?, event_id}. The actor is now Suspended with zero active grants and zero active sessions (Invariant 1).

`suspension_report` (read-only)

suspension_report(actor_ref) →
  {state, suspended_at?, suspended_by_ref?, reason?, revoked_grants?, revoked_sessions?, suspension_event_id?}
 | rejected(invalid-request)

The read-only surface an auditor, operator, or the actor themselves uses to read an actor’s suspension status and, if Suspended, the complete set that was revoked. Resolves actor_suspension_state[actor_ref]: absent or Active → {state: Active}; Suspended → the full suspension record including suspended_at, suspended_by_ref, reason, the suspension_event_id, and the enumerated revoked_grants / revoked_sessions (read from the sealed event the suspension_event_id binds, the authoritative record). No Audit Trail event is produced — a pure read. Logging who read a suspension report belongs to a composing access-log concept, named rather than absorbed.

`reinstate_actor`

reinstate_actor(actor_ref, reinstated_by_ref, credential, reason) →
  {reinstated, event_id}
 | rejected(invalid-request | already-active | recording-failure)

Lifts an actor’s suspension by transitioning Suspended → Active and recording an attributed actor.reinstated event. It does not restore any revoked grant or session — those are terminal in their constituents (Permissions Invariant 3, Session Invariant 4) and cannot be un-revoked; re-authorizing the actor means issuing fresh grants and sessions through the issuance layer, which is not C18’s surface. Steps: validate inputs (invalid-request); if state ≠ Suspended → rejected(already-active) (no-op); else record AuditTrail.record_action(action_ref = actor.reinstated, actor_ref = reinstated_by_ref, credential, data = {reinstated_actor: actor_ref, reason, reinstated_at = now}) → event_id, then set actor_suspension_state[actor_ref] = {state: Active} (atomic with the event); append suspension_log; return {reinstated, event_id}. Reinstatement is the state-machine’s reverse edge only — re-provisioning access is the composing layer’s job (Edge cases — Reinstatement does not restore access).

The load-bearing wiring decision — multi-surface revocation is atomic and complete; suspension gates the cascade

The composition’s structural reason to exist has two halves.

Half 1 — every active grant and every active session is revoked in one all-or-nothing transaction. suspend_actor snapshots both authorization surfaces, revokes every member of both (and optionally the credential), transitions the actor to Suspended, and seals the complete revoked set — all in one transaction; on any non-benign failure the whole act rolls back.

Principle. An actor’s ability to act is spread across two independent surfaces (grants and sessions), each with its own multiplicity; closing the actor out requires closing both surfaces completely, and a partial close is a worse state than no close because it is invisible. Likely objection: why not revoke grants and sessions independently — let an admin call Permissions.revoke per grant and Session.revoke per session — rather than wrapping them in one composition action? Mechanism that resolves it: because independent revocation has no completeness guarantee and no atomicity — an admin who revokes the grants but forgets a session, or whose session-revocation step fails midway, leaves a half-open actor and no record that the closure was incomplete. C18 snapshots both surfaces, revokes every enumerated member within one transaction keyed on actor_ref, and, on any non-benign constituent failure, rolls the whole cascade back (the all-or-nothing default) — so the post-condition is crisp: the actor is either fully de-authorized (zero active grants, zero active sessions) or unchanged and the operation visibly failed. A benign already-terminal target (a concurrent revocation) is counted toward the goal, not treated as a failure, so a TOCTOU race does not spuriously abort. Result: after suspend_actor returns success, the actor provably holds zero active grants and zero active sessions, committed atomically — the multi-surface completeness no single constituent provides, and the opposite of Login’s deliberately best-effort cascade because suspension’s failure mode (a half-open door) is more dangerous than its retry cost.

Half 2 — the Active→Suspended transition gates the cascade, and the sealed event records exactly what was closed. The cascade runs only on the Active→Suspended edge (a second suspension is a no-op), and the actor.suspended event enumerates every revoked grant_id and session_token.

Principle. The suspension must be idempotent (running it twice must not double-revoke or produce two conflicting records) and its completeness must be provable from the records alone. Likely objection: doesn’t recording the whole revoked set duplicate what the Permissions and Session stores already show (each revoked grant/session carries its own revoked_at)? Mechanism that resolves it: the per-constituent revocation records show that each grant/session was revoked, but only the composition knows they were revoked as one suspension act and which set constituted “the actor’s access at suspension time.” The Active→Suspended gate (step 2) makes the cascade fire exactly once — a second suspend_actor sees Suspended and returns already-suspended without re-running — and the sealed actor.suspended event binds the complete {revoked_grants, revoked_sessions} enumeration into one tamper-evident record, so an auditor reads one event and sees the whole closure, not a scatter of independently-revoked records they must reassemble and hope is complete. Result: the suspension is idempotent (gated on the state transition) and its completeness is records-alone provable (the sealed enumeration), resting on the substrate’s Tamper Evidence so a later attempt to shrink the recorded set to hide a missed surface breaks the seal.

Composition-level invariants

These invariants emerge from the composition; none belongs to a single constituent. Each invariant’s Rests on: clause is its capability-provenance record (see pressure-testing.md §Capability provenance): every clause traces to a declared source — a named constituent invariant or action, a deployment-declared configuration capability, or a composition-introduced surface this composition owns.

Invariant 1 — Atomicity of multi-surface revocation (load-bearing). After suspend_actor(actor_ref, …) returns success, the actor holds zero active grants (no Active Permissions grant with subject_ref = actor_ref) and zero active sessions (no Active Session with principal_ref = actor_ref) over the snapshot taken in step 3, and the transition + cascade + sealed event committed as one transaction — there is no reachable success state in which the actor is Suspended while an enumerated grant or session remains Active. Snapshot-scoped, modulo concurrent issuance: a grant or session created after the step-3 snapshot is not covered by this suspension (the composition revokes but never issues, so it cannot block a concurrent Permissions.grant / Session.issue); closing that gap is the composing-layer obligation to gate issuance on actor_suspension_state (Edge cases — Suspension is snapshot-scoped), exactly as Login’s cascade is snapshot-scoped. Under the all-or-nothing posture, a non-benign constituent-revoke or audit-write failure rolls the whole cascade back, so a failed suspend_actor leaves the actor unchanged (not partially suspended). This is the load-bearing concurrency/atomicity claim and the formal-model subject; the model verifies that the atomic cascade admits no Suspended-with-active-access state, and the buggy twin shows a non-atomic multi-surface revocation reaches exactly that partial state. Rests on: Permissions revoke + Invariant 2 (status monotonicity Active→Revoked) + Invariant 8 (revoked grants confer no permission); Session revoke + Invariant 4 (revocation absorbing); the Permissions subject_ref-queryable grant store and Session principal_ref-queryable session store (the enumeration capabilities both atoms declare); the composition-introduced one-transaction cascade (Action wiring steps 3–7) and the unified_actor_namespace configuration capability (the enumeration’s join correctness).
Invariant 2 — Audit completeness. Every successful suspend_actor produces exactly one actor.suspended Audit Trail event whose data enumerates every grant_id in revoked_grants and every session_token in revoked_sessions (and revoked_credential when applicable) — the complete set the cascade closed, with no revoked surface omitted from the record. The enumeration is part of the sealed event payload, so an auditor can confirm the suspension’s completeness from one tamper-evident record. Defended in-line: step 6 carries the complete {revoked_grants, revoked_sessions} (or its digest) into the record_action data, committed in the same transaction as the revokes (step 7). Rests on: Audit Trail record_action and Invariant 1 (attribution coverage) reached through the named substrate, the substrate’s Tamper Evidence sealing (so the enumeration cannot be silently shrunk), and the composition-introduced cascade that assembles the complete set before sealing.
Invariant 3 — Suspension cascade ordering. The cascade runs only on the Active → Suspended transition: suspend_actor against an actor already in Suspended returns already-suspended and changes no state (no second cascade, no second event, no double-revoke), and the suspension state is monotonic on the suspend edge (an Active actor with a recorded suspension is Suspended until reinstate_actor explicitly reverses it). The benign TOCTOU case — a grant/session the cascade targets that a concurrent process already terminalized — is counted toward completion (not-active/already-terminal → skipped, not aborted), mirroring Login’s Final Critique 4 (finding FC1) already-terminal handling. Defended in-line: step 2’s state gate rejects an already-Suspended actor before any cascade; step 4 treats already-terminal targets as benign. Rests on: the composition-introduced actor_suspension_state gate (Action wiring step 2) and the benign-already-terminal mapping (step 4), with the terminal-target semantics resting on Permissions Invariant 3 (revocation terminal) and Session Invariant 5 (terminal-state absorbing).
Invariant 4 — Constituent invariants preserved. All Permissions invariants (1–10) hold over the grant store, all Session invariants (1–11) hold over the session store, all Actor Identity invariants (1–9) hold over the attestation store, all Audit Trail composition-level invariants (1–8) hold over the substrate (and transitively all Event Log, Retention Window, and Tamper Evidence invariants), and — when composed — all Credential invariants (1–11) hold over the credential store. C18 weakens no constituent invariant; it revokes through each constituent’s own revoke and records through the substrate’s own record_action. Rests on: each constituent’s own Generation acceptance bar over its store instance.

Invariant 1 (atomic multi-surface revocation) is the emergent guarantee the composition exists to provide; Invariant 2 (audit completeness) is what makes that guarantee provable from one sealed record; Invariant 3 (cascade ordering) makes the suspension idempotent and orders the cascade behind the state transition. Invariant 4 preserves every constituent guarantee underneath.

Examples

Walkthrough — offboarding a departing employee, end to end

A bank deploys C18 over its access surfaces with unified_actor_namespace = enforced (the actor_ref is the employee’s directory identity, used as subject_ref for grants and principal_ref for sessions, bound via C17), partial_failure_posture = all-or-nothing, Credential composed with revoke_credential_on_suspend = true, and the substrate’s audit_trail_retention_policy = sox_7_year.

Suspension trigger. An employee resigns; HR’s offboarding workflow calls suspend_actor(actor_ref = "emp_4821", suspended_by_ref = "hr_offboard_svc", credential = <svc-cred>, reason = "employment-ended-2026-06-10").
State gate. actor_suspension_state["emp_4821"] is absent → Active → proceed (Invariant 3).
Snapshot. The Permissions store yields three active grants for subject_ref = "emp_4821": g_finread, g_wireinit, g_reports. The Session store yields two active sessions for principal_ref = "emp_4821": tok_laptop, tok_phone. The snapshot and the cascade below run in one transaction keyed on emp_4821.
Cascade. Permissions.revoke(g_finread) → ok; revoke(g_wireinit) → ok; revoke(g_reports) → ok (revoked_grants = {g_finread, g_wireinit, g_reports}). Session.revoke(tok_laptop, "hr_offboard_svc", "employment-ended-2026-06-10") → revoked; revoke(tok_phone, …) → revoked (revoked_sessions = {tok_laptop, tok_phone}). Credential.revoke(cred_emp4821, "hr_offboard_svc", …) → revoked (revoked_credential = cred_emp4821).
Transition + seal. actor_suspension_state["emp_4821"] = {Suspended, suspended_at, suspended_by_ref: "hr_offboard_svc", reason}; AuditTrail.record_action(actor.suspended, "hr_offboard_svc", <svc-cred>, data = {suspended_actor: "emp_4821", revoked_grants: {g_finread, g_wireinit, g_reports}, revoked_sessions: {tok_laptop, tok_phone}, revoked_credential: cred_emp4821, reason}) → ev_susp_001. Transaction commits.
Result. Returns {suspended, revoked_grants (3), revoked_sessions (2), revoked_credential, event_id: ev_susp_001}. emp_4821 now holds zero active grants and zero active sessions (Invariant 1); Permissions.permitted("emp_4821", "wire:initiate") → denied; Session.validate(tok_laptop) → invalid(revoked); and the revoked credential blocks re-authentication.

Domain example — compromised account, all-or-nothing abort and retry

A security team suspends a compromised account: suspend_actor("svc_8830", "soc_analyst_k", <cred>, "credential-in-paste-dump"). The snapshot finds five grants and one long-lived session. Mid-cascade, Session.revoke(tok_svc) returns storage-failure (the session store is briefly unreachable). Under all-or-nothing, the whole transaction rolls back: the five grant revocations are undone, the suspension state is not set, and suspension_log records {outcome: revocation-failure(session)}. suspend_actor returns rejected(revocation-failure). The account is left exactly as it was — not half-suspended — and the SOC (Security Operations Center) retries once the session store recovers, at which point the suspension completes atomically. The crisp post-condition (fully suspended or unchanged) is the all-or-nothing posture’s entire point.

Rejection path — already-suspended no-op, and the benign TOCTOU race

Already suspended (idempotent no-op). A retry of the offboarding call: suspend_actor("emp_4821", …) → step 2 finds state = Suspended → rejected(already-suspended); no second cascade, no double-revoke, no second event (Invariant 3). The single suspension from the first call stands.
Benign TOCTOU — concurrent logout during the cascade. While suspend_actor("emp_4821", …) is mid-cascade, the employee’s laptop client fires its own Session.revoke(tok_laptop) (a logout). The cascade’s Session.revoke(tok_laptop, …) then returns already-terminal — the session is already terminal, which is the cascade’s goal. C18 counts tok_laptop in revoked_sessions (the surface is closed) and does not abort. This mirrors Login’s Final Critique 4 (finding FC1) already-terminal handling: a concurrent terminal transition during the cascade is benign, not a failure.

Regulated adversarial scenarios

Three scenarios the composition must survive in regulated contexts.

Regulator audit — “prove this terminated employee’s access was fully and promptly removed.” A SOX (Sarbanes-Oxley Act) auditor examines emp_4821’s offboarding. suspension_report("emp_4821") returns Suspended with suspended_at, suspended_by_ref, and the enumerated revoked_grants (3) and revoked_sessions (2). The auditor reads the sealed actor.suspended event ev_susp_001 and confirms, via AuditTrail.verify_record, that the enumeration was not altered after the fact (Invariant 2, resting on the substrate’s Tamper Evidence). For each enumerated grant_id, the Permissions store shows status = Revoked with revoked_at at suspension time; for each session_token, the Session store shows Revoked. Invariant 1 is the structural answer: a Suspended actor has zero active grants and zero active sessions. The examiner consults no source code — every claim is verified from the records.

Disputed action — “this employee couldn’t have done that; we suspended them.” An action attributed to emp_4821 is dated after suspended_at. The investigator reads ev_susp_001: the suspension revoked every active grant and session at suspended_at, atomically (Invariant 1). If the disputed action used a session, Session.validate on that token returns invalid(revoked) with revoked_at at suspension time — the session could not have authorized an action afterward. If it used a grant, Permissions.permitted returns denied. The only way the action could post-date the suspension is a new grant/session issued after the snapshot — which suspension_report plus the issuance records would show, and which is the named snapshot-scoped gap (the composing layer’s obligation to gate issuance on the suspension state). The records bound the question precisely.

Breach investigation — “during the incident, was any suspended actor’s access incompletely closed?” An investigator suspects a suspension half-completed under load. They walk the actor.suspended events in the incident window and, for each, cross-check that every enumerated grant_id/session_token is terminal in its store and that no active grant/session for that actor_ref exists outside the enumerated set as of suspended_at. Invariant 1 forecloses a Suspended-with-active-access state under the all-or-nothing posture: a half-suspended actor is not a reachable success state (the formal model verifies this; the buggy twin shows the non-atomic alternative reaches it). A deployment running best-effort would instead surface revocation-failure(surface) findings in the suspension_log — the honest record of any surface that did not close, which the investigator reads directly. Because the enumeration is in the sealed event payload, an attempt to shrink it to hide a missed surface breaks the seal.

Generation acceptance

A derived implementation of C18 is acceptable — in the regulator-acceptance sense — when an external auditor, given the composition’s emergent state (actor_suspension_state, suspension_log) plus the Permissions, Session, (optional) Credential, and Audit Trail substrate stores, can do all of the following without recourse to source code, runbooks, or developer narration.

Audit-Trail-traversal-clearable checks

These checks an auditor answers by reading the composition’s records (including the Audit Trail substrate reached through it).

Suspension completeness (the multi-surface guarantee). For every actor in actor_suspension_state with state = Suspended, confirm that no Permissions grant with subject_ref = actor_ref is Active and no Session with principal_ref = actor_ref is Active — except grants/sessions whose granted_at/issued_at post-dates suspended_at (the snapshot-scoped concurrent-issuance gap, a composing-layer obligation, not a C18 defect). A Suspended actor with an active grant or session issued before suspended_at is a conformance failure (Invariant 1).
Audit enumeration completeness. For every Suspended actor, confirm exactly one actor.suspended event carries its suspension_event_id, that AuditTrail.verify_record returns verified for it, and that the event’s enumerated revoked_grants / revoked_sessions exactly equals the set of grants/sessions for that actor_ref showing revoked_at = suspended_at. A revoked-at-suspension grant or session absent from the sealed enumeration is a conformance failure (Invariant 2). The inverse: every grant_id/session_token in the enumeration resolves to a Revoked record.
Idempotence and ordering. Confirm the suspension_log shows at most one outcome: suspended per actor_ref between reinstatements, and that any suspend_actor against an already-Suspended actor recorded already-suspended with no corresponding second actor.suspended event (Invariant 3). Confirm actor_suspension_state transitions only Active→Suspended (via suspend_actor) and Suspended→Active (via reinstate_actor), each bound to a sealed event.
Attribution and reason completeness. For every actor.suspended event, confirm it is attributed (via the substrate’s Actor Identity) to the suspended_by_ref and carries a non-empty reason, and that each revoked Session and (optional) Credential record carries the same suspended_by_ref and reason. A suspension with no attributed operator or no reason is a conformance failure.
Constituent Generation acceptance bars. Verify Permissions’ five checks over the grant store, Session’s five checks over the session store, Audit Trail’s six checks over the substrate (transitively clearing Event Log, Actor Identity, Tamper Evidence, Retention Window), and — when composed — Credential’s six checks. C18’s invariants depend on the correctness of the constituents’ invariants (Invariant 4).

Externally-clearable checks

These questions arise around C18 but cannot be answered from its records alone — they are the composition’s named audit-gaps, each routed to the evidence that owns it.

Whether the actor_ref namespace truly coincides with the grant subject_ref and session principal_ref namespaces. C18’s enumeration (and hence Invariant 1’s completeness) is complete only under unified_actor_namespace; whether the deployment actually unified them — via C17’s binding or convention — requires the deployment’s identity-namespace evidence, not C18’s records. This is the load-bearing enumeration-completeness audit-gap (Edge cases — Unified actor namespace is a precondition); a divergent namespace under-enumerates silently.
Whether a new grant or session was issued after the suspension snapshot. Invariant 1 is snapshot-scoped; whether the composing layer correctly gated Permissions.grant / Session.issue on the suspension state (so a suspended actor acquired no new access) requires the issuance layer’s records, not C18’s (Edge cases — Suspension is snapshot-scoped).
Whether the suspended_by_ref was authorized to suspend the actor. C18 attributes who suspended but does not gate whether they were permitted to; that requires a Permissions instance scoped to suspension authority (Edge cases — Suspension authorization).
Whether re-authentication was actually blocked. When Credential is uncomposed or revoke_credential_on_suspend = false, whether the deployment closed the re-authentication door requires the credential/Login records, not C18’s (Edge cases — Re-authentication after suspension).

Edge cases and explicit non-goals

Suspension is snapshot-scoped; concurrent issuance is a composing-layer gap. Invariant 1’s completeness holds over the active set enumerated at the step-3 snapshot. C18 revokes but never issues; it cannot prevent a concurrent Permissions.grant or Session.issue from creating new access for the actor after the snapshot. This is the exact analog of Login’s snapshot-scoped cascade (Login Invariant 2): the composing layer that issues grants and sessions must gate issuance on actor_suspension_state (refuse to issue for a Suspended actor), which C18 exposes as a queryable surface (suspension_report). C18 closes the actor’s existing access atomically; keeping it closed against new issuance is the issuance layer’s obligation, and whether it did so is an externally-clearable check. A deployment that wants the suspension to be self-enforcing wires the issuance gate; C18 provides the state the gate reads.
Unified actor namespace is a precondition, not a guarantee. C18 enumerates subject_ref = actor_ref grants and principal_ref = actor_ref sessions; this is complete only if the three namespaces coincide. The composition names this as a deployment precondition (unified_actor_namespace, satisfied by C17’s principal_ref ↔ actor_ref binding or by convention) rather than verifying it — verifying that two opaque namespaces coincide is not a records-alone check at C18’s layer. A deployment whose namespaces diverge under-enumerates and produces a suspension that misses the actor’s access under the other namespace — the precise gap demos/attributed-permissions-admin/CORNERS.md §Cross-atom identity surface aliasing flags, here named as an externally-clearable check rather than papered over.
All-or-nothing vs. best-effort — a deliberate inversion of Login’s choice. Login’s cascade is best-effort (a per-session storage failure is logged and the cascade continues; partial revocation beats none). C18’s default is all-or-nothing (a non-benign failure rolls the whole cascade back). The inversion is deliberate and defended: Login is adding a constraint (revoking sessions on a credential already revoked), so more closure is strictly better; C18 is establishing a security post-condition (the actor is locked out), and a half-established post-condition is a false belief that is worse than a clean failure. A deployment that prefers Login’s maximal-closure posture sets partial_failure_posture = best-effort, which explicitly weakens Invariant 1 to snapshot-scoped-best-effort and surfaces revocation-failure(surface) findings — the honest record of any surface that did not close.
Cross-store consistency under partial failure (best-effort posture). Under all-or-nothing, the cascade is one transaction and there is no partial state — a failure rolls back. Under best-effort (or where the constituent stores genuinely cannot share a transaction, e.g. distributed deployments), the revokes may commit before the actor.suspended write fails, leaving revoked access with no sealed suspension event — an orphan. The implementation (a) retries the record_action until it lands, (b) surfaces the actor and the already-revoked set as a high-priority finding in suspension_log, and (c) marks the recovered event cascade_recovery = true so an auditor distinguishes a clean suspension from a recovered one. This mirrors C7’s two-layer orphan discipline; the difference is that C18’s grant/session revocations are not irreversible in the spoliation sense (a revoked grant is a terminal record, not a destroyed one), so the orphan is an audit-completeness gap, not a data-loss gap.
Reinstatement does not restore access. reinstate_actor lifts the Suspended state but never un-revokes a grant or session — those are terminal in Permissions (Invariant 3) and Session (Invariant 4) and cannot return to Active. Re-authorizing a reinstated actor means issuing fresh grants (Permissions.grant) and letting them establish new sessions (Login), which is the issuance layer’s surface, not C18’s. Reinstatement is the state-machine’s reverse edge only — it re-opens the actor to future provisioning; it does not reach back into the constituents’ terminal records. A deployment that needs the old access back re-grants it explicitly, which is the correct, auditable behavior (the new grants carry new granted_at timestamps and their own attributions).
Suspension authorization is a composing concept. Whether the suspended_by_ref is authorized to suspend a given actor is an inward-authorization question C18 does not gate — it composes no Permissions instance scoped to suspension authority (the cut is Actor Identity + Permissions-as-revocation-target + Session + Audit Trail). The operator is attributed cryptographically via the substrate’s Actor Identity, so an auditor can always answer who suspended the actor; whether they were permitted to requires a Permissions check (or a Multi-Party Approval gate for high-stakes suspensions) wired ahead of suspend_actor, exactly as C7 leaves operator authorization to a composing pattern.
Re-authentication after suspension. Revoking the actor’s active grants and sessions closes their current access but does not, by itself, stop a new login that would establish a fresh session. Closing that door is the optional Credential constituent’s job (revoke_credential_on_suspend = true revokes the authentication credential so re-authentication fails — Credential Invariant 4). When Credential is uncomposed, the deployment must revoke the credential through Login’s surface (Credential.revoke then optionally revoke_sessions_for_credential) in parallel — a named composing obligation, with whether it did so an externally-clearable check.
No bulk constituent surfaces — the cascade enumerates and revokes each. Permissions provides no bulk-revoke (its Mass revocation edge case names per-grant enumerate-then-revoke as the composing system’s job) and Session’s bulk revocation is likewise an enumerate-and-revoke over its principal_ref-queryable store. C18 is the composing pattern that performs both enumerations and the per-member revocations within one transaction — which is exactly why the atomicity and completeness guarantees (Invariants 1 and 2) live at the composition layer and not in either atom.
The actor lifecycle is composition-introduced. Actor Identity has a single Attested state and no actor lifecycle; the Active/Suspended state machine is C18’s own (a composition-introduced surface). C18 therefore does not — and cannot — read a “suspended” flag from Actor Identity; it owns actor_suspension_state. A deployment that also wants the actor’s attestation registry entry deactivated (so the actor cannot produce new attestations) composes that through the forthcoming Actor Registry / Identity Provisioning pattern, or — for the attest surface specifically — through Authenticated Actor (C17), whose revocation cascade closes the attest surface when the credential is revoked. C18 + C17 + Credential-revocation together close the full outbound surface (grants, sessions, attestation, re-authentication); C18 alone closes grants and sessions.
Suspending an actor with no active access. An actor_ref with no active grants and no active sessions (a typo, or an actor already de-provisioned) is a valid no-op suspension: the cascade revokes nothing, the actor transitions to Suspended, and the actor.suspended event records empty revoked_grants/revoked_sessions. This is meaningful (“we suspended an actor who held no active access”) and harmless; it is distinct from a failure. C18 does not reject it, mirroring Login’s revoke_sessions_for_credential returning {revoked: 0} for a credential with no sessions.
Concurrency. Two concurrent suspend_actor calls for the same actor_ref are serialized by the transaction keyed on actor_ref and the Active→Suspended gate: the first transitions and cascades; the second observes Suspended and returns already-suspended (Invariant 3). The benign TOCTOU race — a concurrent Session.revoke/logout or Permissions.revoke terminalizing a target the cascade also targets — is counted as skipped (already-terminal/not-active), not aborted, mirroring Login’s Final Critique 4 (finding FC1). A concurrent Permissions.grant/Session.issue after the snapshot is the snapshot-scoped gap above.
Clock semantics. suspended_at, reinstated_at, and attempted_at are best-effort wall-time annotations read from the substrate’s clock authority at record time (injected by the Audit Trail substrate, not sampled inside C18’s transition — logic-confinement, inherited from the substrate). The Event Log sequence_number (via the substrate) is the authoritative order source for the suspension events. The cascade’s correctness depends on the snapshot/transaction serialization, not on clock comparison.

Standards references

C18 is the structural form of the prompt-and-provable-removal-of-access requirement that every access-control regime imposes at offboarding, deprovisioning, and incident response. Its primary anchors:

NIST (National Institute of Standards and Technology — US federal standards body) SP 800-53 Rev. 5, AC-2(3) (Account Management — Disable Accounts) and AC-6(5) (Least Privilege — Privileged Accounts) — AC-2(3) requires disabling accounts on termination, when they pose a significant risk, or when no longer required; AC-6(5) requires that privileged access be removed when no longer authorized. suspend_actor’s atomic multi-surface revocation (Invariant 1) is the operational form of “disable the account across every surface it can act through,” and the sealed enumeration (Invariant 2) is the records-alone proof the control was applied.
SOX (Sarbanes-Oxley Act) §404 (Internal Control over Financial Reporting) — segregation of duties and access removal on role change are §404 controls; the actor.suspended event’s enumerated, attributed, tamper-evident record is the §404 evidence that a departing or reassigned actor’s access to financial systems was removed promptly and completely.
HIPAA (US Health Insurance Portability and Accountability Act) §164.308(a)(3)(ii)(C) (Termination Procedures) — the administrative safeguard requiring procedures for terminating access to electronic protected health information when a workforce member’s employment ends. C18 is the structural realization: the suspension closes every grant and session at once and proves it from the records.
PCI DSS (Payment Card Industry Data Security Standard — the card networks’ mandatory security rules for cardholder data) Requirement 8.1.3 (revoke access for terminated users immediately) — the requirement that access for terminated users be revoked immediately and completely. C18’s all-or-nothing multi-surface revocation and its sealed enumeration are the structural form of “immediately and completely, provably.”
ISO/IEC 27001 §A.9.2.6 (Removal or Adjustment of Access Rights) — the International Organization for Standardization / International Electrotechnical Commission control requiring that access rights be removed on termination or adjusted on change. The composition’s enumerate-and-revoke-each-surface cascade is the operational control; the suspension report and sealed event are the audit evidence.

C18 inherits the broader standards compliance of its constituents:

Through Permissions: NIST SP 800-53 AC-2/AC-3/AC-6, NIST SP 800-207 (Zero Trust), ISO/IEC 27001 §A.9, HIPAA §164.312(a)(1), SOX §404, PCI DSS Requirement 7 — the grant-revocation surface the cascade drives.
Through Session: NIST SP 800-63B §7 (Session Management), OWASP ASVS V3, HIPAA §164.312(a)(2)(iii) (automatic logoff) — the session-revocation surface.
Through the Audit Trail substrate (and transitively Event Log, Actor Identity, Tamper Evidence, Retention Window): SOX §404/§802, HIPAA §164.312(b)/§164.530(j), PCI DSS Requirement 10, 21 CFR (US Code of Federal Regulations) Part 11, SEC Rule 17a-4, ISO/IEC 27001 §A.12.4, GDPR (EU General Data Protection Regulation) Articles 30 and 32 — the attributed, retained, tamper-evident record the suspension event lands on.
Through the optional Credential: NIST SP 800-63B (authenticator revocation), PCI DSS Requirement 8 — the re-authentication door the optional credential revocation closes.

Status

grounded on Final Critique 4 — 2026-06-10 (2026-06-10) — three-round baseline + author Final Critique + the fresh-reader Phase 4 Opus Happy-Torvalds-X2 clearance gate all complete; foundational findings at zero (the gate folded five refining findings — see Lineage). Formal-layer vote YES and the derived TLA+ — Temporal Logic of Actions — model + buggy twin verified in tools/harness/ (the CORRECT model holds at 2 states; the buggy twin is rejected on Invariant 1), so the formal prerequisite is discharged. Drafted against the approved C18 architectural cut — Actor Identity (the suspended actor’s composition-introduced Active/Suspended lifecycle) + Permissions (grant-revocation target) + Session (session-revocation target) + Audit Trail (substrate → Event Log + Actor Identity + Tamper Evidence + Retention Window) + optional Credential — as Login’s outbound-side counterpart, with multi-surface atomic revocation, audit completeness, and cascade ordering as the load-bearing claims. Regulated-pattern conventions (Regulated adversarial scenarios; Generation acceptance with the Audit-Trail-traversal-clearable / externally-clearable split) baked in from the first draft, inherited from the methodology directly per pressure-testing.md §Regulated-pattern conventions. This is the status C7 and C17 sat at before their own Phase 4 gates; the fresh-reader gate (Opus, claude-opus-4-8, 2026-06-10) cleared with zero foundational findings, flipping this status to grounded on Final Critique 4, bumping the catalog counts, and promoting the roadmap entry.

Lineage notes

Regulated composition (composes regulated atoms and records regulated events on the Audit Trail substrate). The two regulated-overlay conventions — Regulated adversarial scenarios and Generation acceptance (with the Audit-Trail-traversal-clearable / externally-clearable split) — are inherited from the methodology directly (pressure-testing.md), baked in from the first draft, not re-derived from predecessor patterns. The primary structural reference is Login (C13): C18 is Login’s outbound-side counterpart, and it mirrors Login’s cascade structure (snapshot-scoped revocation), atomic-commit discipline (the cascade + audit write in one transaction), and TOCTOU handling (a concurrent terminal transition during the cascade is benign, the same already-terminal case Login’s Final Critique 4 (finding FC1) resolved) — inverting only Login’s best-effort posture to all-or-nothing because suspension’s failure mode is more dangerous. The substrate-composition shape (recording on the Audit Trail the substrate carries) follows Audit Trail, Multi-Party Approval, and C7; the TLA+ atomic-cascade + buggy-twin structure mirrors audit-trail.tla and login.tla. The motivating gap is the deprovisioning cascade Permissions’ Mass revocation on subject deprovisioning edge case and Actor Identity’s Actor lifecycle / Actor Registry note both anticipate.

Structural milestone. C18 is the composing pattern that Permissions’ Actor Registry / Identity Provisioning (forthcoming) note (“Deprovisioning an actor should cascade revocation of their grants; that cascade belongs to the composing system”) and Actor Identity’s actor-lifecycle deferral both anticipate. No atom carries an exact Actor Suspension *(forthcoming)* marker to retire (the anticipation is phrased as the Actor Registry concern), so C18 retires no named forthcoming-link; it realizes the named cascade obligation. It also stands as the outbound counterpart to Login (C13) and composes naturally with Authenticated Actor (C17) (which closes the attest surface) and Credential revocation to close the full outbound surface.

Capability-provenance self-check. Every emergent invariant’s Rests on: clause traces to one of the four declared sources (pressure-testing.md §Capability provenance): named constituent invariants/actions (Permissions revoke + Invariants 2/8 and the subject_ref-queryable store; Session revoke + Invariant 4 and the principal_ref-queryable store; Audit Trail record_action + Invariant 1 reached through the named substrate; Permissions Invariant 3 and Session Invariant 5 for the benign-terminal semantics), the deployment-declared unified_actor_namespace configuration capability (the enumeration’s join correctness), and composition-introduced surfaces (the one-transaction cascade; the actor_suspension_state gate; the suspension_log). No invariant rests on an ambient “the system can…”. In particular, the Active/Suspended lifecycle is not attributed to Actor Identity (which carries no lifecycle state) — it is a composition-introduced state machine, named explicitly to avoid the FC5-1-class capability mis-attribution.

Author gating review — 2026-06-10 (3×3 baseline + author Final Critique; author-led, not fresh-reader). The author ran the three passes (Pass 1 GRID — the nine-node structural-completeness framework; Pass 2 EOS — Essence of Software conceptual independence; Pass 3 Linus adversarial) across three rounds and consolidated an author Final-Critique-shaped closing pass. The grounding-granting fresh-reader Phase 4 gate is a separate step (pending, fresh session). Per-finding format F-id — short name — class → fix:

F1 — Active/Suspended lifecycle mis-attributed to Actor Identity — foundational (Pass 2 EOS, capability-provenance / FC5-1 class). An early draft read the actor’s suspension state “from Actor Identity,” but Actor Identity has a single Attested state and no lifecycle — it explicitly defers actor suspension to a forthcoming Actor Registry. → The Active/Suspended state machine is reframed as a composition-introduced surface (actor_suspension_state) C18 owns, named explicitly in Composes, Composition state, and the actor lifecycle is composition-introduced edge case. This is the round’s foundational soundness fix.
F2 — multi-surface revocation atomicity unstated; partial-state hazard unaddressed — foundational (Pass 3). The draft revoked grants then sessions as two steps without stating their atomicity, leaving a Suspended-with-active-session partial state reachable on a mid-cascade failure — exactly the half-open-door hazard the composition exists to foreclose. → Action wiring steps 3–7 are now one serialized transaction keyed on actor_ref with an explicit all-or-nothing default (roll back on any non-benign failure); Invariant 1 states the atomicity claim the formal model verifies (with the non-atomic multi-surface revocation as the buggy twin); the partial_failure_posture config and the Login-inversion rationale are added.
F3 — unified actor namespace assumed silently — foundational (Pass 2 EOS, capability-provenance). The enumeration (subject_ref = actor_ref, principal_ref = actor_ref) silently assumed the three namespaces coincide; if they diverge, the suspension under-enumerates — the exact CORNERS aliasing gap. → unified_actor_namespace added as a deployment-declared configuration capability (the declaring source for the enumeration’s join correctness), satisfied by C17’s binding or convention, with the divergence named as an externally-clearable check and a dedicated edge case.
F4 — benign TOCTOU (already-terminal target) conflated with failure — refining (Pass 3). The draft treated a Session.revoke → already-terminal (a concurrent logout during the cascade) as a failure that could abort the all-or-nothing transaction, which would let a benign race spuriously roll back a suspension. → Step 4 now treats not-active/already-terminal as benign (the surface is closed, the goal met), counted toward completion, never an abort — mirroring Login’s Final Critique 4 (finding FC1) already-terminal handling; Invariant 3 names it.
F5 — reinstatement implied access restoration — refining (Pass 3). An early reinstate_actor read as if it restored the revoked grants/sessions, but those are terminal in their constituents and cannot be un-revoked. → reinstate_actor is reframed as a thin state-flip (Suspended→Active) that explicitly does not restore access; re-provisioning is named as the issuance layer’s job (the Reinstatement does not restore access edge case).
F6 — snapshot-scoped bound not stated; concurrent issuance gap hidden — refining (Pass 3). Invariant 1 read as unconditional completeness, but C18 revokes and never issues, so a grant/session issued after the snapshot is uncovered. → Invariant 1 carries an explicit snapshot-scoped modulo-clause (parallel to Login Invariant 2), and the Suspension is snapshot-scoped edge case names the composing-layer obligation to gate issuance on the suspension state.
F7 — TLA+, TOCTOU, SOC acronyms unglossed at first body use — refining (Pass 1 acronym discipline). → Glossed at first occurrence.
Final Critique (author, X2 posture). Re-ran all three passes after the fixes. Foundational findings (F1, F2, F3) confirmed closed; the capability-provenance self-check re-verified every Rests on: clause resolves to a declared source with zero ambient dependencies, and confirmed the Active/Suspended lifecycle is housed at the composition layer rather than mis-attributed to a constituent. Pass 2 confirmed the externalizations a fresh reader is most likely to probe — suspension authorization (no Permissions-for-authorization in the cut), the actor registry (the lifecycle is C18’s own, the registry remains forthcoming), and re-provisioning (the issuance layer, not C18) — are EOS-clean. Foundational findings at zero. The pattern is author-clean but not yet grounded: grounding is gated on the fresh-reader Phase 4 Opus clearance gate (pending, separate session), per fresh-reader discipline.

Formal-layer vote: YES. The atomicity of multi-surface revocation (Invariant 1) is a load-bearing concurrency/safety claim: under interleaving of the cascade and concurrent revocations/issuance, no reachable success state may have a Suspended actor with an active grant or session — a multi-store atomic-cascade claim of exactly the shape login.tla (snapshot-scoped cascade) and audit-trail.tla (atomic cascade-on-purge, with the non-atomic twin showing a dangling partial) verify. Audit completeness (Invariant 2) is verified jointly (the sealed enumeration equals the revoked set in the atomic model). Cascade ordering / no-op-on-already-Suspended (Invariant 3) is the Active→Suspended gate’s idempotence, exercised by the model’s guard. Invariant 4 is each constituent’s own bar.

Formal model — 2026-06-10: TLA+ authored and verified; formal layer discharged. Derived model actor-suspension.tla with config actor-suspension.cfg, checked via tools/harness/ (the repo’s tla-checker WASM — WebAssembly — checker; no Java). What it checks: the actor’s two authorization surfaces are modeled as a set of grants Grants and sessions Sessions, each in {active, revoked}, plus a suspended flag and a per-surface audited set (the enumeration carried in the actor.suspended event). The CORRECT model performs the cascade as a single atomic action (SuspendAtomic, guarded on ~suspended — the Active→Suspended gate): it revokes every grant and every session, records the complete enumeration into auditedGrants/auditedSessions, and sets suspended in one step. The model (and its conjunction Safety) asserts the following, all holding across every reachable state: Invariant 1 in two forms — Inv1_Coherent (the state is either fully un-suspended with nothing audited, or fully suspended with everything revoked and everything audited — the atomic-cascade coherence form) and the load-bearing Inv1_FullyDeauthorized (suspended ⇒ every grant revoked ∧ every session revoked; no Suspended-with-active-access state) — and Invariant 2 (Inv2_AuditComplete — every revoked grant/session is enumerated in the audited set). Invariant 3 (cascade ordering / no-op-on-already-Suspended) is covered by-construction, not as a named assertion: the SuspendAtomic guard ~suspended disables a second suspend (exactly-once firing) and the model defines no action that clears suspended (monotonicity), so both hold structurally. Per the coverage cross-check this is recorded as an assumption rather than a verified property — promotable to an explicit check should a future edit add a suspended-clearing (reinstate) action to this model. Bounds/saturation: Grants = {g1, g2}, Sessions = {s1, s2}; the property is per-actor-local, so the atomic commit collapses the partial-state space — raising the surface counts adds no new behavior class (the atomicity, not the cardinality, is what is verified). Buggy twin: actor-suspension-buggy.tla splits the cascade into separate, interleavable sub-steps (RevokeGrants → RevokeSessions → RecordSuspended) with no transaction — the non-atomic multi-surface revocation the All-or-nothing edge case and Invariant 1 warn against. The interleaving RevokeGrants → RecordSuspended reaches suspended = TRUE while a session is still active (a half-open door); TLC rejects the twin on Invariant 1. (The committed .cfg lists Inv1_Coherent first, so the checker reports the violation on it — Invariant 0 in the harness output; Inv1_FullyDeauthorized is independently violated by the same Suspended-with-active state, confirmed by an isolated single-invariant run.) The twin is the vacuity guard — it proves the checker can fail on this property, so the correct model’s green is meaningful. Conflict-protocol outcome: none — the model corroborates the English; the spec already requires the cascade + transition + seal to commit as one transaction (Action wiring steps 3–7, all-or-nothing default), which is exactly the atomic/non-atomic distinction between the correct model and the twin. Canonical English unchanged. The snapshot-scoped concurrent-issuance gap, the best-effort posture, and the optional Credential surface are deliberately out of model scope (composing-layer obligation / configurable posture / optional constituent; see the vote and edge cases). Reproduce: cd tools/harness && node check.mjs ../../compositions/actor-suspension.tla (and … -buggy.tla --buggy).

Opus clearance gate — Happy Torvalds X2 — 2026-06-10 (claude-opus-4-8): clean of foundational findings; 5 refining folded; foundational at zero; grounds on Final Critique 4. Fresh-reader Phase 4 gate conducted with no author context — every “closed”/”verified” claim in the prior Lineage was re-derived from the spec body and the constituent specs rather than trusted. Pass 1 (GRID) and Pass 2 (EOS) at standard intensity; Pass 3 (Linus) at X2 depth, stressing multi-surface revocation atomicity, audit completeness, cascade ordering, capability provenance, and regulated-overlay completeness.

Cross-reference re-verification (head-on against the constituent specs). Every cited constituent invariant count and capability was confirmed against the source: Permissions 1–10 (Invariant 2 status-monotonicity, 3 revocation-terminal, 8 revoked-confer-no-permission; the subject_ref-queryable grant store; the Mass revocation on subject deprovisioning edge case verbatim); Session 1–11 (Invariant 4 revocation-absorbing, 5 terminal-absorbing; the principal_ref-queryable store with “revoke all sessions for this account”); Actor Identity 1–9 (Invariant 1 attestation-immutability; single Attested state, actor lifecycle explicitly deferred to a forthcoming Actor Registry — confirming the Active/Suspended lifecycle is composition-introduced, not mis-attributed); Audit Trail application-level 1–8 (Invariant 1 attribution-coverage; record_action / verify_record signatures); Credential 1–11 (Invariant 4 revocation-absorbing; revoke signature). The constituent action signatures C18 cites match their sources exactly, and the Generation-acceptance check counts C18 names (Permissions 5, Session 5, Audit Trail 6, Credential 6) are each correct.

Capability-provenance re-verification. Every emergent invariant’s Rests on: clause resolves to a declared source among the legitimate kinds: named constituent invariants/actions (Permissions revoke + Inv 2/3/8 + the queryable store; Session revoke + Inv 4/5 + the queryable store; Audit Trail record_action + Inv 1 + Tamper Evidence, reached through the named substrate — not an ambient reach-through), the deployment-declared unified_actor_namespace configuration capability (the enumeration’s join correctness — an honest config capability whose actual coincidence is routed to an externally-clearable check, per declared-is-not-verified), and composition-introduced surfaces (the one-transaction cascade; the actor_suspension_state gate). The Active/Suspended lifecycle is housed at the composition layer, and the snapshot-scoped concurrent-issuance gap is a named composing-layer obligation parallel to Login Invariant 2. Zero ambient/undeclared dependencies; zero FC5-1-class mis-attributions.

Harness re-verification (mechanical, re-run this session through tools/harness/check.mjs). CORRECT — node check.mjs ../../compositions/actor-suspension.tla → TLA+ actor-suspension.tla (states: 2) -> all invariants hold — PASS. BUGGY — node check.mjs ../../compositions/actor-suspension-buggy.tla --buggy → TLA+ actor-suspension-buggy.tla (states: 2) -> VIOLATION: Invariant 0 violated — PASS (twin correctly rejected; Invariant 0 is Inv1_Coherent, the first-listed Invariant-1 encoding — an isolated cfg checking only Inv1_FullyDeauthorized confirms the twin violates that invariant specifically). Bound-saturation bump: raising the surfaces to Grants = {g1,g2,g3} / Sessions = {s1,s2,s3} keeps the CORRECT model at 2 states, all invariants holding — the atomic commit collapses the partial-state space, so cardinality adds no behavior class (saturated). The model faithfully encodes Invariant 1 (no reachable Suspended-with-active state), is non-vacuous (suspended reaches TRUE, so the implication’s antecedent is exercised, and the twin proves the checker can fail), and the twin re-introduces a real non-atomic-cascade hazard.

Per-finding (F-id — short name — class → fix):

FC4-1 — already-terminal handling mis-cited as “Login’s Final Critique 1” — refining → Login has no Final Critique 1; the benign already-terminal / TOCTOU handling is Login finding FC1, surfaced in its Final Critique 4 (login.md). All seven citations corrected to “Login’s Final Critique 4 (finding FC1)”.
FC4-2 — Lineage named a model invariant (Inv3_SuspendMonotone) absent from the committed .tla — refining → the model checks Inv1_Coherent, Inv1_FullyDeauthorized, Inv2_AuditComplete (+ Safety); Invariant 3 is covered by-construction (the ~suspended guard + no suspended-clearing action). The Formal-model paragraph now names the actual constructs and records Invariant 3 as by-construction.
FC4-3 — twin-rejection over-specified to Inv1_FullyDeauthorized — refining → the committed .cfg lists Inv1_Coherent first, so the harness reports the violation on Invariant 0 (Inv1_Coherent); both encode Invariant 1 and both are violated. Paragraph corrected, with the isolated single-invariant confirmation noted.
FC4-4 — not-known revoke result under-mapped at the suspend_actor boundary — refining → step 4 named a revoke → not-known (enumeration/store inconsistency) only as “surfaced as a finding”; now stated as a non-benign failure (abort + rejected(revocation-failure) under all-or-nothing, recorded under best-effort) plus a high-priority suspension_log finding, for both the grant and session surfaces (the case is structurally near-impossible given Permissions Inv 10 / Session Inv 9).
FC4-5 — SOC unglossed at first body use — refining (Pass 1 acronym) → glossed “Security Operations Center (SOC)” at first use in the compromised-account domain example (the prior Lineage F7 claimed it closed, but it had not propagated).

Foundational findings: zero. Five refining findings folded in-pattern. Pass 1 (GRID) and Pass 2 (EOS) clean — the regulated overlay is complete (Regulated adversarial scenarios’ three classes: regulator audit / disputed action / breach investigation; Generation acceptance with the Audit-Trail-traversal-clearable / externally-clearable split), identity model and action signatures and rejection taxonomies are explicit, and examples cover the rejection and adversarial paths. At the 92%-good threshold (foundational density zero), C18 grounds on Final Critique 4.