Authenticated Actor (C17)

Table of contents

Authenticated Actor (C17)

A regulated composition that wires Credential (the authentication surface — “does this presented material belong to this principal?”) and Actor Identity (the attestation surface — “who authorized this action, and can you prove it?”) under a single principal, owning the three concepts neither atom specifies because each is freestanding: (1) revocation cascade — revoking the principal’s authentication credential closes the attestation surface, so a revoked login can no longer produce new signed attestations; (2) secret-surface separation — the authentication verifier (a login key) and the attestation key (a signing key) are distinct key surfaces the composition never cross-routes; and (3) namespace binding — the Credential principal_ref and the Actor Identity actor_ref are bound bijectively to one principal, so every attestation an actor produces resolves back to the authenticated principal. The load-bearing emergent guarantee is the revocation cascade: the composition gates attest_as_actor on the bound credential’s live Active status, read atomically with the attestation write, so authority to sign flows from a currently-valid login rather than from a one-time binding. This composition does not revoke credentials, register actors in the actor registry, or evaluate authorization — each is named, not absorbed.

Intent

Two freestanding atoms answer two adjacent but distinct questions about a principal. Credential answers “did the right material arrive — does this presented secret match what was registered for this principal?” and produces a momentary verified signal. Actor Identity answers “can a future verifier confirm this actor authorized this specific action?” and produces a durable, non-repudiable attestation. Each is correctly specified without naming the other (Credential’s specification names no other atom; Actor Identity’s verify validates a proof against the actor registry’s public material, not against any credential record). Yet the moment both exist for the same principal, three concepts arise that belong to neither atom alone — concepts that were surfaced not by a thought experiment but by a real implementation. The Attributed Permissions Admin demo conflated a single secret to serve as both the login credential and the attestation signing key (demos/attributed-permissions-admin/CORNERS.md §Cross-atom identity surface aliasing), and in doing so exposed three questions the library could not answer: does revoking a login revoke the ability to sign? must the two secret surfaces be distinct? and are the principal_ref and actor_ref namespaces bound to one principal or free to diverge? This composition is the structure that answers them.

The first and load-bearing concept is the revocation cascade, and it is the outbound-authority counterpart to Login’s session cascade. Login (C13) makes a revoked credential’s sessions die: revoking a credential and calling revoke_sessions_for_credential walks the derived-session set and terminates each. Authenticated Actor makes a revoked credential’s attestation surface die: once the principal’s authentication credential is revoked, the composition refuses to produce new attestations for the bound actor. The asymmetry between the two cascades is itself load-bearing. A session is mutable, live state with an active set to walk; the cascade is an enumeration-and-revoke. An attestation is an immutable, point-in-time record — there is no active-attestation set to retract, and retracting one would be wrong: a validly-authorized attestation made before revocation must remain valid (Actor Identity’s non-repudiation contract is conditional on credential integrity at attestation time, not perpetually). The only coherent cascade for an immutable record surface is forward closure: the composition stops producing new attestations the instant the gating credential leaves Active. That forward closure is the emergent guarantee this composition owns.

The second concept is secret-surface separation. The authentication credential’s stored form is a verifier — a one-way artifact (a salted password hash, an encoded public key) from which the original secret cannot be recovered (Credential Invariant 8) and which Credential never exposes in any output (Credential’s Outputs and Feedback sections — the stored verifier is not an output field). An attestation key is a signing surface — material that produces a verifiable proof of authorship. A password hash is not a signing key; the surfaces are structurally different, and conflating them (as the demo did, for demo simplicity) is an architectural error, not a conforming shortcut. The composition forecloses the cross-routing half of this structurally — attest_as_actor takes a distinct attestation credential and never reads or re-purposes the Credential verifier (which is, by Invariant 8, not even available to read) — and names the distinct-provisioning half as a deployment obligation, because no records check can prove that two opaque secrets are cryptographically distinct.

The third concept is namespace binding. Attestations are attributed to actor_ref; sessions and credentials are keyed on principal_ref. If the two namespaces are allowed to diverge, an audit record attributed to one identity surface cannot be reconciled to the session or credential record on the other — a forensic reconstruction problem. The composition binds the two namespaces bijectively: each authenticated actor is one (principal_ref, actor_ref) pair, recorded at registration and immutable thereafter, so an attestation’s actor_ref always resolves to exactly one authenticated principal_ref and vice versa.

This is a composition, not a new primitive. Credential and Actor Identity are unchanged; Authenticated Actor is the wiring that makes them coherent for a single principal. It introduces emergent actions — register_authenticated_actor, attest_as_actor, and the read-only verify_actor_attestation — that belong to no single constituent and exist only because the two atoms are wired together. What it is not: it is not the credential-revocation surface (the identity-management surface calls Credential.revoke; this composition provides the downstream gate, exactly as Login provides the downstream session cascade without initiating the revocation); it is not the actor registry that provisions the attestation key’s public material (an Actor Registry / Identity Provisioning concept Actor Identity already defers to); it is not an authorization surface deciding what the authenticated actor may do (Permissions); and it is not a session manager (Login). Each is named in Edge cases.

Summary

Authenticated Actor is a composition — a specification that wires two freestanding patterns together — that ties a principal’s login to their signature. One pattern, Credential, checks that a presented secret belongs to a principal (the login). The other, Actor Identity, produces an attestation: a permanent, checkable record that a specific actor authorized a specific action (the signature). On their own, neither pattern knows about the other, which leaves three questions unanswered when the same person has both — and this composition answers all three. First and most important: if you revoke someone’s login, can they still produce new signatures? Here the answer is no. The composition checks, every time an actor goes to sign, that their login credential is still active, and it makes that check at the same instant it records the signature, so a revocation can’t slip through a gap. Crucially, signatures made before the revocation stay valid — they were properly authorized at the time, and erasing them would be wrong — so the cascade only closes the door going forward; it never rewrites the past. Second: the login secret and the signing key are kept as two separate things; the composition never uses one as the other (a password hash is not a signing key). Third: the login identity and the signing identity are locked together as one principal, so any signature can always be traced back to the person who logged in.

The composition’s defining emergent guarantee — a property that appears only when the two patterns are combined, belonging to neither alone — is that revocation cascade: a revoked login closes the signing surface. Its most common uses are regulated systems where the same person both logs in and signs actions of consequence: a clinician authenticating and then electronically signing a controlled-substance prescription, a bank officer logging in and attesting a wire approval, a developer authenticating and signing a release commit at a regulated software vendor. Any system where revoking someone’s access must also stop them from producing new signed authorizations — and where an auditor must be able to trace each signature to the authenticated identity behind it — is a candidate for this composition.

Composes

Credential — the authentication surface and the gating constituent. register_authenticated_actor calls Credential.register(principal_ref, credential_material, credential_type, expires_at?) → credential_id | rejected(invalid-request | duplicate-active-credential | storage-failure) to establish the principal’s authentication credential. attest_as_actor does not call Credential.verify (which would require re-presenting the login secret on every signature); instead it performs a read-only status query against the credential store — is there an Active credential for this (principal_ref, credential_type) pair? — exactly as Login’s login step 3 reads the store directly (Credential’s Feedback section states the credential store is queryable to composing patterns). The composition does not call Credential.rotate or Credential.revoke — those are the identity-management surface’s actions; the composition provides only the downstream attest-surface cascade, never the credential revocation itself. The gate keys on the (principal_ref, credential_type) pair rather than a fixed credential_id, so a rotation (which produces a successor Active credential — Credential Invariant 6) keeps the surface open while a revocation (which leaves no Active credential — Credential Invariant 4) closes it.
Actor Identity — the attestation surface. attest_as_actor calls Actor Identity.attest(action_ref, actor_ref, attest_credential) → attestation_id | rejected(invalid-request | invalid-credential | storage-failure) to produce the non-repudiable record, passing the bound actor_ref (resolved from the namespace binding) and the caller-supplied attestation credential (the signing key — distinct from the authentication credential_material, never the Credential verifier). verify_actor_attestation calls Actor Identity.verify(attestation_id) → verified | failed-verification(proof-invalid | actor-unknown-in-registry | registry-unavailable) | not-known as a read-only pass-through, additionally resolving the verified attestation’s actor_ref back to its bound principal_ref. The composition does not register the actor’s public material in the actor registry — that is the Actor Registry / Identity Provisioning concept Actor Identity already names as forthcoming; attest surfaces a registry-unknown actor_ref through its own outcomes.

The Credential store (credential records) and the Actor Identity attestation store (attestations) are owned by their respective constituent instances. Authenticated Actor owns no constituent state — it indexes across the two with its own emergent maps (principal_to_actor, actor_to_principal, below) and a composition-layer attest log, and the attestations themselves are the regulated record of record (no Audit Trail substrate is in the cut — see Edge cases, No Audit Trail substrate).

A surface this composition needs that no constituent provides is the bijective binding between the authentication namespace (principal_ref) and the attestation namespace (actor_ref). Credential keys on principal_ref; Actor Identity keys on actor_ref; neither relates the two. This is a composition-introduced surface at Authenticated Actor’s layer (one of the four legitimate capability-provenance sources — see pressure-testing.md §Capability provenance), realized by the two emergent maps below.

Composition logic

Composition state

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

principal_to_actor — map from principal_ref to {actor_ref, credential_type, credential_id, bound_at}. Populated atomically by register_authenticated_actor after Credential.register succeeds; immutable thereafter (no action rebinds an existing principal). credential_type is the gating type — the credential type whose Active status the attest gate consults — and credential_id is the initial credential record for traceability; the gate keys on the (principal_ref, credential_type) pair (not the fixed credential_id) so that a rotation successor keeps the surface open. This is the namespace-binding index: it records that a principal was bound to an actor, under which gating credential type, and when.
actor_to_principal — reverse map from actor_ref to principal_ref, maintained as the strict inverse of principal_to_actor and written in the same atomic step. Used by verify_actor_attestation to resolve a verified attestation’s actor_ref back to its authenticated principal_ref without a full scan. Immutable once written.

attest_log — append-only record of every attest_as_actor call, whether it produced an attestation or was refused. Each entry carries: entry_id (opaque, system-generated), principal_ref, actor_ref (null when the call failed before the binding resolved), action_ref, outcome (one of: success not-bound credential-not-active(observed_status) invalid-attest-credential attest-failed invalid-request) — where observed_status is the status of the most-recent credential record for the (principal_ref, credential_type) pair (Revoked Expired Rotated), the absence of any Active credential being what closed the gate, attestation_id (present only on success; null otherwise), attempted_at. This log is the composition’s own composition-layer query surface; the attestation store is the non-repudiable record of record for the successful signatures it references. The two are redundant by design, exactly as Login pairs its login_event_log with the Audit Trail — but here the tamper-evident external-auditor surface is the attestation store itself, not a separate Audit Trail.

The credential store and the attestation store are owned by their constituent instances; the composition duplicates neither.

Configuration

attest_surface_separation — a deployment-declared obligation (default enforced) asserting that the attestation key material an actor presents to attest_as_actor is provisioned as distinct key material from the authentication credential_material registered through Credential. This is the declaring source (capability provenance) for Invariant 2’s distinct-provisioning half: the composition forecloses cross-routing structurally (it never feeds Credential material into Actor Identity.attest), and the deployment attests that the two surfaces are independently provisioned. Whether the two opaque secrets are cryptographically distinct cannot be checked from the composition’s records, so this obligation’s satisfaction is an externally-clearable check (Generation acceptance). A deployment that sets this to anything other than enforced is declaring the demo-grade aliasing the CORNERS finding flagged, and forfeits Invariant 2.
gating_credential_type_default — the default credential_type used as the gating type when register_authenticated_actor is not given one explicitly. Deployment-configurable; must be a non-empty string. A deployment whose principals authenticate with a single primary credential type (e.g. "password" or "fido2") sets this once; deployments binding a specific non-default type supply it per registration.

Primitive policies

The composition takes string-typed inputs at its action boundaries; each is validated at this layer or by a constituent.

principal_ref — opaque reference to the authenticated principal; the key of principal_to_actor. Must contain at least one non-whitespace character (invalid-request). Passed to Credential.register and used in the credential-store status read. Equality is opaque byte-identity; never normalized or case-folded (inherited from Credential’s opaque-principal_ref discipline).
actor_ref — opaque reference to the attesting actor in the actor registry; the key of actor_to_principal. Must be non-empty. Passed to Actor Identity.attest. Byte-identity equality; never normalized. The composition does not validate that the actor_ref exists in the registry — Actor Identity.attest/verify surface a registry-unknown actor through their own outcomes.
credential_type — caller-supplied (or defaulted) label selecting the gating credential type; the value Credential uses to enforce its one-active-per-(principal_ref, credential_type) rule. Non-empty; opaque; never normalized at this layer.
credential_material — the raw authentication secret, consumed by Credential.register and never persisted (Credential Invariant 8). The composition passes it through without inspection.
attest_credential — the raw attestation signing material, consumed by Actor Identity.attest and never persisted (Actor Identity’s credential-consumed-not-stored discipline). The composition passes it through without inspection and never substitutes the authentication credential_material or the Credential verifier for it (Invariant 2).
action_ref — opaque reference to the action being attested; passed through to Actor Identity.attest. Non-empty; byte-identity; the composition does not interpret it (action-content immutability is handled at the host layer, inherited from Actor Identity).
attestation_id — opaque Actor Identity handle; the argument verify_actor_attestation resolves. 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 intake (register_authenticated_actor), one emergent gated-attest (attest_as_actor), and one read-only query (verify_actor_attestation).

Uniform constituent-rejection mapping. Every constituent call below maps its rejection taxonomy to a composition-boundary code as named in each step. Where a constituent rejection arrives before any irreversible effect, it surfaces as a clean pre-state rejection that leaves no emergent state populated; the composition writes its attest_log entry (for attest_as_actor) or no map (for register_authenticated_actor) accordingly.

`register_authenticated_actor`

register_authenticated_actor(principal_ref, actor_ref, credential_material, credential_type?, expires_at?) →
  {credential_id, actor_ref, bound_at}
 | rejected(
   invalid-request
  | namespace-conflict
  | duplicate-active-credential
  | storage-failure
  )

Binds an actor_ref to a principal_ref and registers the principal’s authentication credential, establishing the namespace binding and the gating credential together. Steps:

Validate: principal_ref, actor_ref, credential_material each non-empty; credential_type (or gating_credential_type_default) non-empty; expires_at, if supplied, a future timestamp. Any violation → rejected(invalid-request). Stop.
Namespace-conflict guard (the bijection precondition). If principal_ref is already a key of principal_to_actor, or actor_ref is already a key of actor_to_principal, → rejected(namespace-conflict); nothing is written. This enforces the bijection at the boundary: neither namespace may be double-bound (Invariant 3).
Call Credential.register(principal_ref, credential_material, credential_type, expires_at?). Map duplicate-active-credential → rejected(duplicate-active-credential) (the principal already holds an Active credential of this type — the caller rotates rather than re-registers, per Credential’s own contract), invalid-request → rejected(invalid-request), storage-failure → rejected(storage-failure). On any rejection, no binding is written. On success, obtain credential_id.
Atomically write principal_to_actor[principal_ref] = {actor_ref, credential_type, credential_id, bound_at = now} and the strict inverse actor_to_principal[actor_ref] = principal_ref. (The two writes share one transaction; a discrepancy between them is evidence of a failed atomic write — Invariant 3.) If this write fails after the credential was registered → rejected(storage-failure), with the orphaned credential (registered, unbound) surfaced as a finding per the Cross-store consistency under partial failure edge case.
Return {credential_id, actor_ref, bound_at}. The principal is now an authenticated actor: it can authenticate (via the credential) and attest (via the bound actor surface, gated on the credential’s Active status).

`attest_as_actor`

attest_as_actor(principal_ref, action_ref, attest_credential) →
  attestation_id
 | rejected(
   invalid-request
  | not-bound
  | credential-not-active
  | invalid-attest-credential
  | attest-failed
  )

Produces a non-repudiable attestation for the bound actor, only if the principal’s authentication credential is currently Active — the revocation cascade, enforced as a forward gate. This action is the composition’s load-bearing surface. Steps:

Validate: principal_ref, action_ref, attest_credential each non-empty. Any violation → append attest_log entry {outcome: invalid-request, actor_ref: null, attestation_id: null}; return rejected(invalid-request). Stop.
Resolve the binding: principal_to_actor[principal_ref] → {actor_ref, credential_type}. Absent → append attest_log {outcome: not-bound, actor_ref: null}; return rejected(not-bound). Stop. (not-bound is structurally distinct from credential-not-active: the principal was never an authenticated actor, versus the principal was bound but its credential is no longer Active.)
The cascade gate (read the credential status and attest atomically). Read the credential store for an Active credential for (principal_ref, credential_type). If none exists — because the credential was revoked (Credential Invariant 4), expired (Invariant 11), or rotated without a current Active successor — append attest_log {outcome: credential-not-active(observed_status), actor_ref}; return rejected(credential-not-active). Stop. The status read and the Actor Identity.attest call in step 4 are one serialized critical section keyed on principal_ref (implementations serialize on principal_ref, exactly as Login serializes its cascade on credential_id and Defensible Retention serializes hold-check-and-purge on record_ref) — and because Credential.revoke is issued outside this composition (on the credential record, not through a composition action), the serialization point that makes it contend is the gating (principal_ref, credential_type) credential record itself: the gate reads that record’s status under, and the attestation commits while holding, the same record lock an externally-issued Credential.revoke must acquire to transition it (the per-pair lock Credential’s active-uniqueness constraint already imposes — Credential Invariant 2), so a revoke is ordered strictly before or after the section, never inside it. Equivalently, an implementation may re-validate the credential’s Active status under that lock at attest-commit; a composition-local principal_ref mutex that the external revoke does not contend on is not sufficient. No concurrent Credential.revoke may interleave between the status read and the attestation write such that an attestation is produced while the credential is non-Active. This atomicity is the load-bearing concurrency claim (Invariant 1) and the formal-model subject; a non-atomic check-then-attest is the time-of-check-to-time-of-use (TOCTOU) hazard the buggy twin demonstrates.
Call Actor Identity.attest(action_ref, actor_ref, attest_credential) — passing the bound actor_ref (never a caller-supplied actor reference) and the caller-supplied attestation credential (never the authentication credential_material or the Credential verifier — Invariant 2). Map invalid-credential → rejected(invalid-attest-credential) (the signing material did not validate against the actor registry’s public material for actor_ref), invalid-request → rejected(invalid-request), storage-failure → rejected(attest-failed). On any rejection, append the corresponding attest_log entry with attestation_id: null; return the mapped rejection. On success, obtain attestation_id.
Append attest_log {outcome: success, principal_ref, actor_ref, action_ref, attestation_id, attempted_at: now}. Return attestation_id. The attestation is recorded in the Actor Identity store under the bound actor, immutably (Actor Identity Invariant 1), and remains valid independent of any later credential revocation (Actor Identity Invariant 8 — non-repudiation conditional on credential integrity at attestation time).

`verify_actor_attestation` (read-only)

verify_actor_attestation(attestation_id) →
  {result, actor_ref?, principal_ref?}

where result ∈ { verified | failed-verification(proof-invalid | actor-unknown-in-registry | registry-unavailable) | not-known }.

The read-only surface an auditor uses to verify an attestation and resolve the authenticated principal behind it. Steps: call Actor Identity.verify(attestation_id). On not-known, return {result: not-known} (no actor_ref to resolve). On any other result, read the attestation’s actor_ref and resolve actor_to_principal[actor_ref] → principal_ref (absent → principal_ref omitted, surfaced as a binding-integrity finding: an attestation exists for an actor_ref the composition did not bind, see Edge cases Attestations for unbound actors). Return {result, actor_ref, principal_ref?}. No state is changed — this is a pure read, mirroring Actor Identity’s read-only verify. Logging who verified an attestation and when is a composing access-log concept (Edge cases — Auditing verification reads), named rather than absorbed.

The load-bearing wiring decision — the revocation cascade is forward closure of the attest gate, read atomically with the attestation write

The composition’s structural reason to exist is the revocation cascade, and it is defended in four parts.

Principle. Revoking a principal’s authentication credential must close that principal’s attestation surface: a revoked login must not be able to produce new signed attestations. The composition gates attest_as_actor on the bound credential’s live Active status, read atomically with the attestation write — so the authority to sign flows from a currently-valid login, not from a one-time binding made when the actor was first registered.

Likely objection. Two objections a sharp reviewer raises. First: why not let Actor Identity refuse attestations for revoked principals itself, or cascade the revocation the way Login revokes sessions? Second: if the gate is just a status read followed by an attest call, doesn’t a concurrent revocation between the two steps let a revoked credential still sign?

Mechanism that resolves it. To the first: Actor Identity validates the attestation credential against the actor registry’s public material and has no knowledge of the Credential atom — it structurally cannot see a credential revocation, so the gate cannot live inside it. And the cascade cannot be a revoke-the-set operation as in Login, because there is no active-attestation set to walk: attestations are immutable, point-in-time records (Actor Identity Invariant 1), and retracting a validly-made one would be wrong (Actor Identity Invariant 8 makes non-repudiation conditional on credential integrity at attestation time, not perpetually — an attestation made while the credential was Active was validly authorized and stays valid). The only coherent cascade for an immutable record surface is forward closure: stop producing new attestations once the credential leaves Active. To the second: the status read and the Actor Identity.attest call are one serialized critical section keyed on principal_ref (Action wiring step 3), so no Credential.revoke interleaves between check and attest; and revocation absorbing (Credential Invariant 4) plus terminal-state absorbing (Invariant 5) and expiry absorbing (Invariant 11) guarantee that once the credential is non-Active, no Active credential exists for the pair, so the gate stays closed for every subsequent call. The TOCTOU window the non-atomic reading would open is exactly what the formal model’s buggy twin demonstrates is unsafe.

Result. A revoked (or expired, or rotated-without-current-successor) login cannot produce new attestations through the composition (Invariant 1); pre-revocation attestations remain valid and immutable, which is correct because they were validly authorized when made; and the cascade requires no new active-state machinery — it is the structural consequence of gating on a constituent’s own terminal-absorbing invariants, with the composition supplying only the atomic check-and-attest and the namespace binding the gate reads.

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 — Revocation cascade / attest-surface closure (load-bearing). No attestation is produced by attest_as_actor for a bound principal whose gating credential is not Active at the time the attestation is written; equivalently, once a bound principal’s (principal_ref, credential_type) credential leaves Active (revoked, expired, or rotated without a current Active successor), the composition produces no further attestations for that principal until a new Active credential is registered (which, the binding being immutable, belongs to re-registration / rebinding). The guarantee is forward-closing: it constrains new attestations, not the immutability or validity of attestations already made (those rest on Actor Identity Invariants 1 and 8). This is the load-bearing concurrency/safety claim and the formal-model subject; the model verifies that the atomic check-and-attest admits no reachable state in which an attestation is written under a non-Active credential, and the buggy twin shows the non-atomic check-then-attest TOCTOU does. Rests on: Credential Invariant 4 (revocation absorbing), Invariant 5 (terminal-state absorbing), and Invariant 11 (expiry absorbing) — the named constituent invariants guaranteeing no Active credential exists for the pair once terminal; the composition-introduced atomic check-and-attest critical section (Action wiring, attest_as_actor step 3, serialized on principal_ref); the credential-store status-read capability (Credential’s Feedback section — the store is queryable to composing patterns); and the principal_to_actor namespace binding (composition-introduced surface) that supplies the (principal_ref, credential_type) pair the gate reads.
Invariant 2 — Secret-surface separation. The authentication credential surface (Credential’s stored verifier, a one-way artifact) and the attestation credential surface (the signing material Actor Identity.attest consumes, validated against the actor registry’s public material) are distinct key surfaces; the composition never presents the authentication credential_material, nor anything derived from the Credential verifier, as the attest_credential, and never the reverse. The cross-routing half is foreclosed structurally: attest_as_actor accepts a distinct attest_credential argument and never reads the Credential verifier — which is one-way (Credential Invariant 8) and never exposed in any output (Credential’s Outputs/Feedback discipline), and therefore neither usable nor even available to re-purpose. The distinct-provisioning half — that the two opaque secrets are independently provisioned and cryptographically distinct — is a deployment obligation the records cannot confirm, stated as an obligation with verification routed to an externally-clearable check. Rests on: Credential Invariant 8 (credential material never persisted; the stored verifier is a one-way artifact from which the raw secret cannot be recovered) together with Credential’s Outputs/Feedback discipline (the stored verifier is never exposed in any output) — the two jointly make the verifier unusable and unavailable as a signing key; Actor Identity’s credential-consumed-not-stored discipline (declared in its Inputs, Behavior, and Decision-points — the attestation credential is consumed at attest and never persisted; this is a behavioral commitment, not one of its nine numbered invariants); and the deployment-declared attest_surface_separation configuration capability (Configuration) backing the distinct-provisioning obligation. This is the spec-level closure of the CORNERS §Cross-atom identity surface aliasing finding (a single secret aliased for both surfaces).
Invariant 3 — Namespace binding (principal ⇔ actor bijection). Each bound principal has exactly one (principal_ref, actor_ref) pair: principal_to_actor and actor_to_principal are strict inverses, neither namespace is double-bound (the register_authenticated_actor namespace-conflict guard), and a binding is immutable once written (no action rebinds). Consequently every attestation produced through attest_as_actor carries the actor_ref bound to the authenticating principal_ref, and verify_actor_attestation resolves any verified attestation’s actor_ref back to exactly one principal_ref. Defended in-line: register_authenticated_actor writes both maps in one atomic step (step 4) behind the conflict guard (step 2); attest_as_actor passes only the bound actor_ref (step 4), never a caller-supplied one. Rests on: the composition-introduced principal_to_actor / actor_to_principal maps and the namespace-conflict guard, plus Credential Invariant 1 (registration immutability) and Actor Identity Invariant 1 (attestation immutability) for the immutability of the bound endpoints.
Invariant 4 — Attestation traceability and attest-log completeness. Every attest_as_actor call produces exactly one attest_log entry, and every entry whose outcome is success carries a non-null attestation_id resolvable in the Actor Identity store and a non-null actor_ref equal to principal_to_actor[principal_ref].actor_ref; every non-success entry carries attestation_id: null. An auditor can therefore trace any composition-produced attestation to the authenticated principal that produced it, and reconcile every successful attestation against an attest-log entry, from the composition’s own state. Defended in-line: each branch of attest_as_actor appends exactly one entry (steps 1–5). Rests on: the composition-introduced attest_log append discipline and the principal_to_actor binding; the attestation it references rests on Actor Identity Invariant 9 (attestation durability).
Invariant 5 — Constituent invariants preserved. All Credential invariants (1–11) hold over the credential store, and all Actor Identity invariants (1–9) hold over the attestation store. Authenticated Actor weakens no constituent invariant; it adds a gate and a binding, neither of which mutates constituent state outside the constituents’ own actions. Rests on: each constituent’s own Generation acceptance bar over its store instance.

Invariant 1 (revocation cascade) is the emergent guarantee the composition exists to provide; Invariant 2 (secret-surface separation) and Invariant 3 (namespace binding) are the two structural conditions that make the cascade and its audit trail meaningful — separation keeps the gated surface and the signing surface from collapsing into one, and the bijection lets every signature resolve to the authenticated identity the gate protects. Invariant 4 makes the attest surface auditable from the composition’s own records; Invariant 5 preserves every constituent guarantee underneath.

Examples

Walkthrough — register, attest, then revoke-and-fail, end to end

A regulated software vendor authenticates developers and requires every release commit to be signed. It deploys Authenticated Actor with gating_credential_type_default = "fido2" and attest_surface_separation = enforced.

Registration. The identity-management surface registers developer dev_smith: register_authenticated_actor(principal_ref = "dev_smith", actor_ref = "actor_smith", credential_material = <fido2-attestation-object>, credential_type = "fido2"). The namespace-conflict guard passes (neither namespace is bound); Credential.register returns credential_id = "cred_s01"; principal_to_actor["dev_smith"] = {actor_ref: "actor_smith", credential_type: "fido2", credential_id: "cred_s01", bound_at} and actor_to_principal["actor_smith"] = "dev_smith" are written atomically. Returns {credential_id: "cred_s01", actor_ref: "actor_smith", bound_at}.
Attestation while Active. The developer signs a release commit with their separate hardware signing key: attest_as_actor(principal_ref = "dev_smith", action_ref = "commit_c44a", attest_credential = <hardware-signing-key>). Step 2 resolves actor_smith. Step 3 reads the credential store: an Active fido2 credential exists for ("dev_smith", "fido2") → gate open. Step 4 calls Actor Identity.attest("commit_c44a", "actor_smith", <hardware-signing-key>) → attestation_id = "att_a17". Step 5 logs success. Returns att_a17. The continuous-integration system later calls verify_actor_attestation("att_a17") → {result: verified, actor_ref: "actor_smith", principal_ref: "dev_smith"} before merging — the signature verifies and resolves to the authenticated developer.
Revocation closes the surface. Security determines cred_s01 was compromised. The identity-management surface calls Credential.revoke("cred_s01", revoked_by_ref = "security_team", reason = "key-compromise") — cred_s01 is now Revoked (Credential Invariant 4). No call into Authenticated Actor is required to “cascade”: the next attestation attempt is refused structurally. attest_as_actor("dev_smith", "commit_c45b", <hardware-signing-key>) → step 3 reads the credential store, finds no Active credential for ("dev_smith", "fido2") → appends attest_log {outcome: credential-not-active(Revoked)}; returns rejected(credential-not-active). The revoked login can no longer sign (Invariant 1). The earlier att_a17 remains verified — it was validly authorized before revocation (Actor Identity Invariant 8).

Domain example — rotation keeps the surface open

The same developer’s hardware authenticator is replaced under the 12-month rotation policy. The identity-management surface calls Credential.rotate("cred_s01", <new-fido2-object>) → "cred_s02" (cred_s01 → Rotated, cred_s02 → Active, same ("dev_smith", "fido2") pair — Credential Invariants 2 and 6). No rebinding is needed: attest_as_actor("dev_smith", "commit_c46c", <hardware-signing-key>) → step 3 finds an Active credential for the pair (the rotation successor) → gate open → attestation produced. The gate keys on the (principal_ref, credential_type) pair, not the fixed credential_id, precisely so that a rotation (the actor is still legitimate) keeps the surface open while a revocation (the actor’s authority is withdrawn) closes it. This is the load-bearing distinction between Credential Invariant 6 (rotation non-mutation, new Active successor) and Invariant 4 (revocation absorbing, no Active successor).

Rejection path — namespace conflict and unbound attest

Namespace conflict. A second registration reuses an already-bound actor: register_authenticated_actor("dev_jones", "actor_smith", <material>, "fido2") → step 2 finds actor_smith already in actor_to_principal → rejected(namespace-conflict); no credential is registered, no binding written. The bijection (Invariant 3) is preserved: actor_smith stays bound to exactly dev_smith.
Attest for an unbound principal. attest_as_actor("dev_unknown", "action_x", <key>) for a principal never registered through the composition → step 2 finds no binding → attest_log {outcome: not-bound}; rejected(not-bound). This is distinct from credential-not-active: the principal was never an authenticated actor at all.
Invalid attestation credential. attest_as_actor("dev_smith", "commit_c47d", <wrong-signing-key>) while the credential is Active → gate open, but Actor Identity.attest returns invalid-credential (the signing material does not validate against the registry’s public material for actor_smith) → attest_log {outcome: invalid-attest-credential}; rejected(invalid-attest-credential). The gate (authentication still valid) and the attest check (signing key valid) are independent surfaces — secret-surface separation in action (Invariant 2).

Regulated adversarial scenarios

Three scenarios the composition must survive in regulated contexts.

Regulator audit — “prove this signed action was authorized by a principal whose login was valid at signing time, and trace the signature to that login.” An auditor examines attestation att_a17. verify_actor_attestation("att_a17") returns {verified, actor_ref: "actor_smith", principal_ref: "dev_smith"} — the proof verifies (Actor Identity Invariants 2 and 3) and resolves to the authenticated principal via the namespace binding (Invariant 3). The auditor reads the credential store for ("dev_smith", "fido2") and confirms cred_s01 was Active at att_a17.attested_at (it was revoked later). The attest-log entry for att_a17 corroborates the timeline (Invariant 4). Every claim is answered from the composition’s records plus the two constituent stores — no developer narration. The structural guarantee that a revoked login could not have produced a new signature after revocation is Invariant 1.

Disputed signature — the principal claims they did not authorize an action. dev_smith disputes commit_c44a. The investigator calls verify_actor_attestation("att_a17"): verified binds actor_smith to commit_c44a at attested_at (Actor Identity Invariant 8). The namespace binding resolves actor_smith to dev_smith (Invariant 3). The dispute cannot be sustained without claiming credential compromise — which is exactly the boundary Actor Identity Invariant 8 names (non-repudiation conditional on credential integrity), routed to a Compromise Disclosure composing pattern. The investigator additionally confirms, from the credential store, that cred_s01 was Active at signing time, so the signature was produced through a valid login surface — Invariant 1’s gate was satisfied at the time.

Breach investigation — “during the compromise window, was any new signature produced after we revoked the credential?” A security team revoked cred_s01 at T_revoke and asks whether the attacker produced signatures afterward. They query the attest_log for dev_smith entries after T_revoke: every such entry shows outcome: credential-not-active(Revoked) and a null attestation_id — the gate refused them (Invariant 1). A success entry after T_revoke would be the smoking gun, and Invariant 1 forecloses it structurally: the atomic check-and-attest admits no state in which an attestation is written under a Revoked credential. Any attestation in the Actor Identity store for actor_smith carries an attested_at at or before T_revoke; the forward-closure boundary is the revocation timestamp, and the attest_log is the records-alone evidence of every refused post-revocation attempt.

Generation acceptance

A derived implementation of Authenticated Actor is acceptable — in the regulator-acceptance sense — when an external auditor, given the composition’s emergent state (principal_to_actor, actor_to_principal, attest_log) plus the Credential store and the Actor Identity attestation store, can do all of the following without recourse to source code, runbooks, or developer narration. The composition carries no Audit Trail substrate (see Edge cases), so the records-clearable checks read the attestation store — itself the non-repudiable record — and the composition’s emergent state, rather than an Audit-Trail traversal.

Records-clearable checks

Namespace-binding bijection. Confirm principal_to_actor and actor_to_principal are strict inverses (every principal → {actor, …} has actor → principal, and vice versa), and that no actor_ref or principal_ref appears as a key in its map more than once. A discrepancy is a failed atomic write or a bijection violation (Invariant 3).
Attest-surface closure (the cascade). For every attest_log entry with outcome: success and attestation_id = A, confirm that the credential for (principal_ref, credential_type) was Active at the entry’s attempted_at — i.e. no credential record for the pair shows a terminal transition (revoked_at / expiry / rotated_at without a current Active successor) at or before that timestamp such that no Active credential existed. A success entry whose credential was non-Active at attest time is a conformance failure (Invariant 1). Conversely, confirm every attest_log entry with outcome: credential-not-active(...) corresponds to a (principal_ref, credential_type) pair with no Active credential at attempted_at.
Attestation traceability. For every attest_log success entry, confirm attestation_id resolves in the Actor Identity store, that Actor Identity.verify returns verified for it (under the current registry view, or failed-verification(proof-invalid) only where the registry’s public material has since rotated — handled at the registry layer, not a composition defect), and that its actor_ref equals principal_to_actor[principal_ref].actor_ref. An attestation referenced by a success entry but absent from the store, or carrying a different actor_ref, is a conformance failure (Invariant 4).
Attest-log completeness. Confirm every successful attestation in the Actor Identity store attributed to a bound actor_ref has a corresponding attest_log success entry, and that no success entry lacks an attestation_id. A bound-actor attestation with no log entry is a finding (Invariant 4); an attestation in the store for an actor_ref absent from actor_to_principal is the attestations-for-unbound-actors anomaly (Edge cases).
Constituent Generation acceptance bars. Verify Credential’s six checks over the credential store and Actor Identity’s five checks over the attestation store. The composition’s invariants depend on the correctness of the constituents’ invariants (Invariant 5).

Externally-clearable checks

These questions arise around the composition 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 two secret surfaces are genuinely distinct key material. The composition forecloses cross-routing structurally, but whether the deployment provisioned the authentication credential and the attestation signing key as cryptographically distinct material (rather than aliasing one for both, the CORNERS finding) cannot be confirmed from the records — the verifier is one-way and the secrets are opaque. This is the load-bearing separation audit-gap, cleared by the deployment’s key-provisioning evidence and the attest_surface_separation = enforced declaration (Invariant 2).
Whether the actor_ref was correctly provisioned in the actor registry. The composition binds an actor_ref and surfaces registry errors through attest/verify, but whether the registry holds the correct public material for that actor is the Actor Registry / Identity Provisioning concept (Edge cases).
Whether the authenticated actor was authorized to take the attested action. The composition attributes who authorized an action (the attestation) but does not gate whether they were permitted to — that requires a Permissions instance (Edge cases — Authorization is a composing concept).
Whether a credential later determined compromised invalidates prior attestations. Invariant 1 closes the surface forward; retroactive reinterpretation of attestations made during a compromise window is a Compromise Disclosure composing concept (Actor Identity Invariant 8’s named boundary), not a property the composition’s records resolve.

Edge cases and explicit non-goals

No Audit Trail substrate — the attestations are the regulated record. Login wires an Audit Trail to record its login/logout/cascade events; Authenticated Actor deliberately does not (the approved cut is Credential + Actor Identity, two atoms). It can afford to, because Actor Identity attestations are themselves the non-repudiable, regulator-grade records of the actions they attest — the composition’s success outputs are tamper-resistant proofs, not mere log lines. The attest_log is the composition-layer query surface (the analog of Login’s login_event_log), and the attestation store is the external-auditor surface. A deployment that needs tamper-evident logging of the binding and gate operations themselves (registrations, refused attest attempts) composes Audit Trail above this composition — a named composing concept, not absorbed, exactly as Login keeps lockout out of its cut.
The composition does not revoke credentials. attest_as_actor’s cascade is the downstream consequence of a revocation performed elsewhere; the composition never calls Credential.revoke. The identity-management surface (or a compromise-response process) revokes the credential through Credential’s own surface; the composition’s gate then closes the attest surface structurally. A deployment that wants to also terminate the principal’s live sessions on revocation wires Login’s revoke_sessions_for_credential in parallel — the two cascades (sessions die, attest surface closes) are independent downstream consequences of the same Credential.revoke, each owned by its own composition.
No active-attestation revocation — the cascade is forward-closure only. Unlike Login’s session cascade, there is no set of “active attestations” to retract: attestations are immutable point-in-time records (Actor Identity Invariant 1), and an attestation made under a then-Active credential stays valid by design (Actor Identity Invariant 8). The cascade therefore closes the surface going forward and never rewrites the past. A deployment that needs prior attestations reinterpreted as untrustworthy after a compromise composes a Compromise Disclosure pattern, which produces new reinterpretation records rather than mutating the attestation store.
Actor registration is not owned here. The composition binds an actor_ref that must already exist in the actor registry with valid public material; it does not register the actor or its attestation key. Actor registration, key rotation in the registry, and registry availability are the Actor Registry / Identity Provisioning concept Actor Identity already names as forthcoming. The composition surfaces a registry-unknown actor through Actor Identity.attest/verify outcomes (invalid-attest-credential, failed-verification(actor-unknown-in-registry | registry-unavailable)).
Authorization is a composing concept. Whether the authenticated actor was permitted to take the attested action is distinct from whether they authorized it. The composition attributes authorization (the attestation answers who); it composes no Permissions instance and does not gate what the actor may do. A deployment that needs authorization wires a Permissions check ahead of attest_as_actor, exactly as Login leaves logout authorization to a composing Permissions layer.
Rebinding and re-registration. A binding is immutable (Invariant 3); the composition exposes no action to rebind an existing principal_ref to a different actor_ref or to point the gate at a different credential type. A principal whose credential was revoked and who needs to attest again requires a fresh Active credential under the bound (principal_ref, credential_type) pair — re-registration of the credential through Credential’s surface (the gate then reopens), not a rebinding. Changing the actor binding itself (a different actor_ref) is a deliberate non-goal: it would let the audit identity behind a principal shift, defeating the namespace-binding invariant. Deployments needing actor re-keying do so through the actor registry, preserving the actor_ref.
Attestations for unbound actors. An attestation in the Actor Identity store for an actor_ref absent from actor_to_principal is a binding-integrity anomaly: it indicates an attestation was produced for that actor outside this composition (Actor Identity is freestanding and may be called directly), so the composition cannot resolve its principal_ref. verify_actor_attestation returns verified with principal_ref omitted and the case is surfaced as a finding. The honest boundary: the namespace binding (Invariant 3) and traceability (Invariant 4) cover exactly the attestations produced through this composition; an out-of-band Actor Identity.attest call is invisible to the binding, exactly as a credential registered outside the composition is invisible to the gate.
Cross-store consistency under partial failure. register_authenticated_actor writes to the credential store (Credential.register) and then the composition’s binding maps. If the binding write fails after the credential was registered, the result is an orphaned credential (registered, unbound): the composition returns rejected(storage-failure) and surfaces the orphan as a finding to be reconciled (rebind, or revoke the orphaned credential). attest_as_actor writes only to the attestation store (one Actor Identity.attest call) plus the append-only attest_log; the attest and the log append are ordered so a log entry without a successful attestation is impossible for success (the attestation_id is obtained before the entry is written), and an attestation without a log entry is the traceability finding check 4 catches. There is no multi-irreversible-write atomicity hazard on the attest path — the single irreversible effect is the immutable attestation, and the gate precedes it.
Concurrency. Two concurrent attest_as_actor calls for the same principal_ref each run their own atomic check-and-attest critical section (serialized on principal_ref); both may succeed (two distinct attestations — Actor Identity has no at-most-one constraint, and two signed actions are two valid records), and neither can sign under a non-Active credential. A concurrent Credential.revoke and attest_as_actor are serialized by the critical section — which serializes on the gating (principal_ref, credential_type) credential record (the row Credential.revoke transitions and Credential Invariant 2 already locks), so the externally-issued revoke contends on the same point rather than on a composition-local handle: the attest either observes the credential Active and completes, or observes it non-Active and refuses — there is no interleaving in which an attestation is written under a revoked credential (Invariant 1; the formal model verifies this and its buggy twin shows the non-atomic reading is unsafe). Two concurrent register_authenticated_actor calls for overlapping namespaces are serialized by the namespace-conflict guard plus Credential’s own active-uniqueness constraint (Credential Invariant 2): at most one succeeds for a given pair.
Clock semantics. bound_at and attempted_at are best-effort wall-time annotations read from the deployment’s clock (inherited from Credential’s and Actor Identity’s clock-source treatment); attested_at on the attestation is set by Actor Identity. The cascade’s correctness does not depend on clock honesty — it depends on the credential’s Active-vs-terminal status at attest time, a state check, not a timestamp comparison. Deployments needing verifiable signing time compose Trusted Timestamping (RFC 3161 — the Internet standard for trusted time-stamping), per Actor Identity’s own edge case.
Auditing verification reads. verify_actor_attestation records nothing — it is a pure read, mirroring Actor Identity’s read-only verify. Logging who verified an attestation and when is a composing access-log concept, named rather than absorbed.

Standards references

Authenticated Actor is the structural form of the requirement that authentication and non-repudiable attestation be bound under one principal, with revocation of the former closing the latter. Its primary anchors:

NIST (National Institute of Standards and Technology — US federal standards body) SP 800-63B §5.2 (Authenticator Lifecycle — Binding, Revocation, and Reauthentication) — the requirement that a revoked authenticator can no longer be used to establish authority. The revocation cascade (Invariant 1) is the structural form: a revoked authentication credential closes the actor’s attestation surface, so authority to sign flows from a currently-valid authenticator.
NIST SP 800-57 Part 1 (Recommendation for Key Management — General) — key-usage separation: a key used for one purpose (authentication) should not serve another (signing/attestation). Secret-surface separation (Invariant 2) is the composition-level expression of the key-separation principle.
PCI DSS (Payment Card Industry Data Security Standard — the card networks’ mandatory security rules for cardholder data) Requirement 8.6 (management of authentication factors and their binding to individual accounts) — authentication factors must be bound to a specific identity and managed through their lifecycle; the namespace binding (Invariant 3) and the revocation cascade (Invariant 1) are the structural mechanisms for the bind-and-revoke lifecycle of a payment-system actor.
FIPS 140-3 (Federal Information Processing Standard — Security Requirements for Cryptographic Modules) — the standard for the cryptographic modules that hold and operate signing keys; the distinct-key-surface obligation (Invariant 2, externally-clearable) is where a deployment’s FIPS 140-3-validated module provisioning is the cleared evidence that the attestation key is genuinely separate material.

Authenticated Actor inherits the broader standards compliance of its constituents:

Through Credential: NIST SP 800-63B (authenticator and verifier requirements — stored verifiers, not raw secrets), FIDO2 / WebAuthn (phishing-resistant authenticator binding), PCI DSS Requirement 8, ISO/IEC 27001 §A.9.4 (system and application access control), GDPR (EU General Data Protection Regulation) Article 32 (security of processing — the verifier-not-material discipline). The revocation-absorbing and terminal-absorbing invariants the cascade rests on are Credential’s.
Through Actor Identity: NIST SP 800-63-3 (identity and authenticator assurance), eIDAS Regulation (EU 910/2014 — qualified electronic signatures), FIPS 186-5 (Digital Signature Standard), 21 CFR (US Code of Federal Regulations) Part 11 (FDA electronic records and signatures — uniquely attributable, repudiation-resistant signatures), DEA EPCS (US Drug Enforcement Administration — Electronic Prescriptions for Controlled Substances; 21 CFR §1311 — two-factor cryptographic attestation for controlled-substance prescriptions), HIPAA (US Health Insurance Portability and Accountability Act) §164.312(d) (person or entity authentication), SOX (Sarbanes-Oxley Act) §302/§404 (officer certifications and internal-control evidence). The non-repudiation contract the cascade preserves forward is Actor Identity’s.

Status

grounded on Final Critique 4 — 2026-06-10 (drafted 2026-06-10; three-round baseline + author Final Critique complete — three foundational + four refining findings closed in-pattern, foundational to zero; formal-layer vote YES and the derived TLA+ — Temporal Logic of Actions — model + buggy twin verified in tools/harness/, so the formal prerequisite is discharged; Phase 4 Opus Happy-Torvalds-X2 fresh-reader clearance gate cleared in a fresh session 2026-06-10 (Final Critique 4) — foundational findings at zero, five refining findings folded, the correct TLA+ model re-verified at 16 states and the buggy twin re-rejected on Inv1_NoSignAfterRevoke). Drafted against the approved C17 architectural cut — Credential (the authentication/gating surface) + Actor Identity (the attestation surface) — answering the three CORNERS §Cross-atom identity surface aliasing questions as three emergent invariants: the revocation cascade (forward closure of the attest gate, the load-bearing claim), secret-surface separation, and namespace binding. Regulated-pattern conventions (Regulated adversarial scenarios; Generation acceptance, with the records-clearable / externally-clearable split adapted to a composition whose record-of-record is the attestation store rather than an Audit Trail) baked in from the first draft, inherited from the methodology directly per pressure-testing.md §Regulated-pattern conventions. With the author gating review, the verified formal model and its buggy twin, and the fresh-reader Phase 4 clearance gate all cleared at zero foundational findings, the pattern is grounded on Final Critique 4.

Lineage notes

Regulated composition (composes two regulated atoms — Credential and Actor Identity — both carrying the security overlay). The two regulated-overlay conventions — Regulated adversarial scenarios and Generation acceptance (with the records-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 references are Login (C13) for the revocation-cascade shape (Authenticated Actor is Login’s outbound-attestation counterpart — Login revokes the derived session set; C17 forward-closes the attest surface) and the TLA+ TOCTOU buggy-twin discipline, Attributed Permissions Admin for the two-atom compliance-pairing shape and the attestation-attribution surface, and Immutable Transaction Ledger (C6) for the compact single-load-bearing-invariant TLA+ model + buggy-twin structure. The motivating gap is demos/attributed-permissions-admin/CORNERS.md §Cross-atom identity surface aliasing, whose three questions (revocation cascade, secret interchangeability, audit identity unification) become this composition’s three emergent invariants.

Structural milestone. This composition retires the two Authenticated Actor *(forthcoming)* references in the atom corpus — in atoms/credential.md and atoms/actor-identity.md — each of which named the three invariants this composition owns and pointed at the CORNERS finding. At grounding (this Phase 4 gate — Final Critique 4, 2026-06-10), each atom’s *(partially resolved)* marker is removed; the references were already live links at drafting (both atoms point at this file), so this change only retires the status markers in atoms/credential.md and atoms/actor-identity.md.

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 (Credential Invariants 4/5/11 and the queryable-store status read for the cascade; Credential Invariant 8 and Actor Identity’s credential-consumed discipline for secret-surface separation; Credential Invariant 1 and Actor Identity Invariant 1 for the binding’s immutable endpoints; Actor Identity Invariant 9 for traceability’s durable attestation), the deployment-declared attest_surface_separation configuration capability (the distinct-provisioning half of Invariant 2), and composition-introduced surfaces (the atomic check-and-attest critical section; the principal_to_actor / actor_to_principal maps; the attest_log append discipline). No invariant rests on an ambient “the system can…”. In particular, the cascade gate is not attributed to Actor Identity (which cannot see a credential revocation) — it is a composition-introduced atomic critical section resting on Credential’s terminal-absorbing invariants, 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 — cascade gate mis-attributed to Actor Identity — foundational (Pass 2 EOS, capability-provenance / FC5-1 class). An early draft phrased the cascade as “Actor Identity refuses attestation when the credential is revoked,” pinning a capability on a constituent that does not expose it — Actor Identity validates against the actor registry and has no knowledge of the Credential atom. → Reframed as a composition-introduced atomic check-and-attest critical section resting on Credential Invariants 4/5/11 and the credential-store status read (a queryable-store capability Credential’s Feedback section declares); the gate lives at the composition layer, named explicitly. This is the round’s foundational soundness fix.
F2 — TOCTOU window in the check-then-attest gate unaddressed — foundational (Pass 3). The draft read the credential status and then called Actor Identity.attest as two steps without stating their atomicity; a concurrent Credential.revoke between them would let a revoked credential still sign — defeating Invariant 1, the composition’s entire reason to exist. → Action wiring step 3 now names the status-read-and-attest as one serialized critical section keyed on principal_ref (mirroring Login’s cascade serialization and Defensible Retention’s hold-check-and-purge), and Invariant 1 is stated as the atomicity claim the formal model verifies (with the non-atomic reading as the buggy twin).
F3 — rotation conflated with revocation; gate keyed on credential_id — foundational (Pass 3). An early gate keyed on the bound credential_id, which a rotation (new successor credential_id, Credential Invariant 6) would render non-Active, wrongly closing the surface for a legitimate rotated actor. → The gate keys on the (principal_ref, credential_type) pair so a rotation successor keeps the surface open (the actor is still legitimate) while a revocation closes it (Credential Invariant 4 vs 6); the binding stores credential_type as the gating type and credential_id for traceability only. Rotation walkthrough added.
F4 — secret-surface separation overclaimed as fully structural — refining (Pass 3). The draft asserted the composition guarantees the two secrets are distinct, but no records check can prove two opaque secrets are cryptographically distinct. → Invariant 2 split into the cross-routing half (foreclosed structurally — the composition never reads the one-way Credential verifier, which Invariant 8 makes unavailable) and the distinct-provisioning half (a deployment obligation backed by the attest_surface_separation config capability and routed to an externally-clearable check).
F5 — not-bound and credential-not-active conflated in the attest rejection vocabulary — refining (Pass 1 / Pass 3). An early signature returned a single failure for “can’t attest,” hiding the load-bearing distinction between “never an authenticated actor” and “was bound but the credential is no longer Active.” → Two named rejections, with the attest_log outcome vocabulary distinguishing them and the breach-investigation scenario exercising credential-not-active(Revoked).
F6 — Generation acceptance split named “Audit-Trail-traversal-clearable” with no Audit Trail in the cut — refining (Pass 1). The canonical split names an Audit-Trail traversal; C17 has no Audit Trail. → The split is adapted to “records-clearable” (the attestation store — itself the record of record — plus the emergent maps and attest_log) and “externally-clearable,” with the adaptation stated and the No Audit Trail substrate edge case defending why the attestations suffice.
F7 — TLA+ and TOCTOU 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 cascade gate is housed at the composition layer rather than mis-attributed to a constituent. Pass 2 confirmed the three externalizations a fresh reader is most likely to probe — actor registration (the Actor Registry concern), authorization (no Permissions in the cut), and Compromise Disclosure (forward-closure only) — 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 revocation cascade (Invariant 1) is a load-bearing concurrency/safety claim: under interleaving of Credential.revoke and attest_as_actor, no reachable state may exist in which an attestation is written for a principal whose gating credential is non-Active — a TOCTOU-class claim of exactly the shape Credential’s own credential-buggy-toctou.tla and Capacity Constraint’s TOCTOU twin verify. The other two emergent invariants are not TLA+-class: secret-surface separation (Invariant 2) is a structural/by-construction + deployment-obligation argument with no temporal dimension, and namespace binding (Invariant 3) is a structural bijection better suited to a relational (Alloy) surface or by-construction maintenance — both are scoped out of the temporal model exactly as Login scoped its non-cascade invariants and C6 scoped to its single binding-bijection claim. Traceability (Invariant 4) is a single-write-path records-shape argument; Invariant 5 is each constituent’s own bar.

Formal model — 2026-06-10: TLA+ authored and verified; formal layer discharged. Derived model authenticated-actor.tla with config authenticated-actor.cfg, checked via tools/harness/ (the repo’s tla-checker WASM — WebAssembly — checker; no Java). What it checks: per bound principal p, three variables — credStatus[p] ∈ {Active, Revoked} (the gating credential’s status), attested[p] (whether the composition has produced an attestation for p), and a global signedAfterRevoke flag computed from the actual credential status observed at each attest commit (derived from history, not tracked independently — avoiding the begged-question pitfall). The load-bearing Invariant 1 is Inv1_NoSignAfterRevoke == signedAfterRevoke = FALSE — no attestation is ever committed while the gating credential is non-Active. The CORRECT model performs the status-check and the attest commit as a single atomic action (AttestAtomic, guarded on credStatus[p] = "Active", computing signedAfterRevoke from the observed status), alongside Revoke(p); the property holds across all reachable states. Bounds/saturation: Principals = {p1, p2}; the property is per-principal-local, so the state space saturates quickly — raising to {p1, p2, p3} adds no new behavior class (each principal’s check-and-attest-vs-revoke interleaving is independent). Buggy twin: authenticated-actor-buggy.tla splits the gate into a latched CheckGate(p) (records the gate passed while Active) and a separate CommitAttest(p) (writes the attestation if the gate latch is set) — the non-atomic check-then-attest the Concurrency edge case and Invariant 1 warn against. The interleaving CheckGate(p) → Revoke(p) → CommitAttest(p) commits an attestation while credStatus[p] = Revoked, setting signedAfterRevoke = TRUE; TLC rejects the twin on Inv1_NoSignAfterRevoke. 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 status-read and the attest to be one serialized critical section (Action wiring step 3), which is exactly the atomic/non-atomic distinction between the correct model and the twin. Canonical English unchanged. The secret-surface separation (Invariant 2) and namespace binding (Invariant 3) are deliberately out of model scope (structural / deployment-obligation properties; see the vote). Reproduce: cd tools/harness && node check.mjs ../../compositions/authenticated-actor.tla (and … -buggy.tla --buggy).

Opus clearance gate — Happy Torvalds X2 — 2026-06-10 (Claude Opus, claude-opus-4-8): clean of foundational findings; five refining findings folded; foundational at zero; grounds on Final Critique 4. Run in a fresh session against the committed spec, fresh-reader discipline throughout (only this spec, the methodology pass-question sections, the two constituent specs — atoms/credential.md and atoms/actor-identity.md — and the three .tla files read; this pattern’s own Lineage “closed” claims were not trusted — every load-bearing claim was re-derived from the spec body and the constituent specs). All three passes run; Pass 1 (GRID) and Pass 2 (EOS) at standard intensity, Pass 3 (Linus) at X2.

Formal layer re-verified mechanically. node check.mjs ../../compositions/authenticated-actor.tla → CORRECT model holds at 16 states (all invariants hold); node check.mjs ../../compositions/authenticated-actor-buggy.tla --buggy → twin REJECTED on Inv1_NoSignAfterRevoke (17 states) — the green is non-vacuous on the load-bearing invariant. The prose edits below are all out-of-model (wording/citation/acronym); the .tla and .cfg are unchanged and re-verify as above.

Capability provenance re-derived head-on against the constituent specs (not trusted from this pattern’s self-check). Confirmed present, with the cited numbers and meanings, in the constituents as written: Credential Invariant 4 (revocation absorbing), Invariant 5 (terminal-state absorbing), Invariant 11 (expiry absorbing) — each stating no Active credential survives for the pair once terminal (the (principal_ref, credential_type) “no Active exists” conclusion they carry rests in turn on Credential Invariant 2, active uniqueness, which they cite internally); Credential Invariant 8 (raw material never persisted; verifier one-way) plus Credential’s Outputs/Feedback discipline (verifier never exposed) for secret-surface separation; Credential Invariant 1 and Actor Identity Invariant 1 for the binding’s immutable endpoints; Actor Identity Invariant 9 for traceability’s durable attestation; Actor Identity Invariants 2/3 (action/actor binding) and Invariant 6 (self-containment — verify consults only the attestation’s fields and the actor registry’s public material) for why the gate cannot live in Actor Identity. Action signatures verified to match exactly: Credential.register/rotate/revoke and Actor Identity.attest/verify. The credential-store status-read capability is genuinely declared (Credential Feedback: “the credential store is queryable … to authorized administrative surfaces”; Behavior: “composing patterns … may query the credential store directly”). The cascade gate is confirmed housed at the composition layer, not mis-attributed to Actor Identity (which structurally cannot see a credential revocation) — no FC5-1-class mis-attribution, no ambient dependency. The four load-bearing stress points each re-derived from the spec body and found soundly handled: (1) the TOCTOU — the safety property is formally verified under atomicity, and the cascade is correctly forward-closure, not a set-revocation (attestations are immutable per Actor Identity Inv 1/8, so there is no active-attestation set to walk); (2) secret-surface separation — cross-routing foreclosed structurally, distinct-provisioning honestly an externally-clearable deployment obligation; (3) namespace bijection — register-time conflict guard + atomic strict-inverse writes + immutability; (4) capability provenance — every Rests on: clause resolves to a declared source. Per-finding format F-id — short name — class → fix:

FC4-1 — TOCTOU serialization point under-named — refining (Pass 3, determinism leak / “two engineers” posture). The critical section was described as “keyed on principal_ref” (a composition-local handle), but Credential.revoke is issued outside the composition on the credential record; a literal composition-local mutex would not exclude the external revoke, leaving the TOCTOU open. The safety requirement and its formal verification were already present, so this sharpens rather than adds. → Action wiring step 3 and the Concurrency edge case now name the shared serialization point as the gating (principal_ref, credential_type) credential record — the row Credential.revoke transitions and Credential Invariant 2 already locks — so the external revoke provably contends (or, equivalently, the gate re-validates Active status under that lock at attest-commit).
FC4-2 — verifier-non-exposure mis-cited to Credential Invariant 8 — refining (Pass 2, capability-provenance cite precision). Three passages (Intent, Invariant 2 inline, Invariant 2 Rests on:) attributed “the verifier is never exposed in any output” to Credential Invariant 8, whose text covers raw-material non-persistence and verifier one-wayness; verifier-non-exposure is declared in Credential’s Outputs/Feedback/State. The capability is declared (not an undeclared dependency), so the dependency is sound — only the citation needed correcting. → Split the citation: Invariant 8 for one-wayness, Credential’s Outputs/Feedback for non-exposure.
FC4-3 — “Invariant set” overstates Actor Identity’s consumed-not-stored discipline — refining (Pass 2, cite precision). Invariant 2’s Rests on: located the credential-consumed-not-stored discipline in “its Behavior section and Invariant set,” but no numbered Actor Identity invariant states it — it is an Inputs/Behavior/Decision-points behavioral commitment. → Reworded to cite Inputs/Behavior/Decision-points and note it is a behavioral commitment, not one of the nine numbered invariants.
FC4-4 — DEA / EPCS unglossed at first use — refining (Pass 1, acronym discipline). → Spelled out “US Drug Enforcement Administration — Electronic Prescriptions for Controlled Substances” at first use in Standards references.

FC4-5 — observed_status value set not pinned — refining (Pass 3, primitive-policy completeness). The attest_log credential-not-active(observed_status) outcome did not state what observed_status reports when several terminal credential records exist for the pair. The load-bearing behavior (gate closed) is unaffected, but the records-clearable surface is sharper with it pinned. → Defined observed_status as the most-recent credential record’s status for the pair (Revoked Expired Rotated), the absence of any Active credential being what closed the gate.

Foundational findings: zero. Grounds on Final Critique 4. The two structural-milestone forthcoming-references to this composition were already live links at drafting; their *(partially resolved)* status markers in atoms/credential.md and atoms/actor-identity.md are retired in this same change.