From 17d455a9bf223574b6f0ca71b19483cc6105e221 Mon Sep 17 00:00:00 2001 From: Dawn Date: Tue, 18 Aug 2026 11:32:56 -0400 Subject: [PATCH] docs(nip-fi): scope administrative expiry to the grant and stop rotation clearing it Two defects found by running a bounded state model of the composed core + LIFECYCLE machine in two encodings -- one holding every guard the documents state plus the guards a careful implementer would infer, one holding only the guards actually written. Both were invisible to four line-by-line readers because reading supplies the missing rule unconsciously. Defect 1: administrative expiry was escapable by rotation. LIFECYCLE said an expired binding "remains durable and occupies both sides of the core partial bijection", so it stays in the relation -- and core Rotate replaces one exact "active" binding with "a fresh binding version" while no document said the replacement inherits binding_not_after. Reading the expired binding as active let rotation authority alone clear a bound only expiry authority had set; reading it as inactive removed it from TargetEligible, letting ProvisionBinding double-bind the identity or bind the administratively terminated key to a different identity, violating FI-INV-01 -- the invariant LIFECYCLE was leaning on. FI-LC-ADMIN-EXPIRY did not detect either: core Rotate is authorized and version-checked, so the escape satisfied the oracle's own wording. Defect 2: nothing in the six files said what binding_not_after is a bound *on*. Two reviewers resolved it in opposite directions -- one grant-scoped, one identity-scoped -- and the readings differ by 25,200 reachable states. The identity-scoped reading also makes RetirePair followed by ordinary enrollment an escape, which under the grant-scoped reading is a legitimately new grant. Repairs: - Core Rotate states that it continues one grant onto a new key and preserves every profile-defined administrative bound as an opaque field core neither interprets nor clears. - LIFECYCLE declares the bound grant-scoped, names the transitions that establish a new grant carrying no prior bound, and points identity-scoped deadlines at the capability projection in authoritative local-policy state, which already carries the revocation-bound machinery such a deadline needs. Encoding one here instead would put an authorization-relevant deadline in a store with no revocation bound. - LIFECYCLE defines a binding with a reached bound as active for every core relation and eligibility test, closing the TargetEligible horn. - Binding-creating transitions must declare continuation or establishment; the two cases partition that set with no remainder, so a future profile cannot add a creator whose bound semantics are undefined. - FI-LC-ADMIN-EXPIRY gains the rotation-must-not-clear arm and the negative arm that retire-then-enroll yields an unbounded binding and is conformant, so the oracle no longer admits the violation it exists to catch. Verification of the shipped bytes, not the intent: re-encoding the model from this text gives 0 grant-scoped escapes (17,184 before) and 0 FI-INV-01/FI-INV-03 regressions over 282,528 states across all three enrollment policies. Each clause was mutated separately and each goes red only for its own clause -- dropping the Rotate carry restores 21,216 escapes, and dropping the active definition admits both FI-INV-01 violations. A clause that cannot be made to fail is not a guard. Co-authored-by: Tyler Longwell Signed-off-by: Tyler Longwell --- docs/nips/NIP-FI-LIFECYCLE.md | 41 ++++++++++++++++++++++++++++++----- docs/nips/NIP-FI.md | 6 ++++- 2 files changed, 41 insertions(+), 6 deletions(-) diff --git a/docs/nips/NIP-FI-LIFECYCLE.md b/docs/nips/NIP-FI-LIFECYCLE.md index c86f4a7a57..a4bc72d75c 100644 --- a/docs/nips/NIP-FI-LIFECYCLE.md +++ b/docs/nips/NIP-FI-LIFECYCLE.md @@ -51,6 +51,27 @@ It also permits a core binding to carry `binding_not_after`, an optional administrative deadline. The pending lineage names one exact retired pair and binding version. There is at most one pending lineage per identity. +`binding_not_after` bounds the grant represented by **one binding**; it is not a +bound on the identity. Rotation continues the same grant: the replacement binding +preserves the carried bound, and only expiry authority changes it. Retirement, +revocation, disablement, re-enablement, provisioning, and ordinary enrollment +establish a *new* grant that carries no prior bound — so retirement of a bound +pair followed by ordinary enrollment under `attested-key` or `tofu` policy yields +an unbounded binding, and that is conformant. A deadline that must survive the end +of a grant — an identity-scoped access bound — belongs in the capability +projection of authoritative local-policy state, which core already requires for +any projection whose removal must close authority within a declared bound and +which is reread at preparation, final admission, and every protected lease use. +`binding_not_after` is not that mechanism and cannot substitute for it: it does +not survive the end of the grant that carries it, so a deployment relying on it +for identity-scoped expiry cannot claim a revocation bound for that expiry +(`FI-LC-ADMIN-EXPIRY`). + +A binding carrying a reached bound is **active** for every core relation and +eligibility test in this profile and in core, including the core partial +bijection and `TargetEligible` below. It is ineligible for authorization, not +absent from the binding relation. + `X_D`, `Q_D`, and `binding_not_after` are deployment-local state. Their versions are revalidation dependencies, not contract identities. A change invalidates a prepared decision and every dependent lease unless complete final-admission @@ -88,6 +109,14 @@ MUST leave all authoritative state unchanged (`FI-LC-ATOMIC`). Lease invalidation MAY be delivered asynchronously, but authorization use after the commit MUST recheck the advanced dependency before allowing an operation. +Every transition that creates a binding MUST state whether it **continues** an +existing grant, and therefore preserves that grant's administrative bound, or +**establishes** a new grant carrying no prior bound. The two cases partition the +binding-creating transitions with no remainder: core rotation continues, and +provisioning, re-enablement, and ordinary enrollment establish. A profile that +adds a binding-creating transition without this declaration cannot claim +conformance (`FI-LC-CLAIM`). + `TargetEligible(i, k, allow_disabled)` means that `k` is not revoked, `(i, k)` is not retired, neither `i` nor `k` has an active binding, and `i` is not disabled unless `allow_disabled` is true. Every new target key requires fresh, @@ -168,9 +197,11 @@ SetAdministrativeExpiry(i, k, old_version, binding_not_after?): This transition changes neither side of the pair nor its provenance. Setting, replacing, or clearing the bound advances the binding version. At equality the binding is ineligible but remains durable and occupies both sides of the core -partial bijection. Only this or another applicable privileged transition can -restore access; ordinary authorization cannot renew the bound -(`FI-LC-ADMIN-EXPIRY`). +partial bijection. This transition is the only expiry authority: no other +transition in this profile or in core sets, replaces, or clears the bound, and +core rotation carries it onto the replacement binding unchanged. Only this or +another applicable privileged transition can restore access; ordinary +authorization cannot renew the bound (`FI-LC-ADMIN-EXPIRY`). ## One-shot lineage and concurrency @@ -195,7 +226,7 @@ denied case. | ID | Setup and required result | |---|---| -| `FI-LC-CLAIM` | For a fixed profile set, compare complete discovery bytes across attested-key, TOFU, and provisioned configurations and across lifecycle states: they are identical. If one protected ingress omits lifecycle gates or uses a different lifecycle lineage, the domain cannot advertise the profile and the uncovered ingress fails closed. | +| `FI-LC-CLAIM` | For a fixed profile set, compare complete discovery bytes across attested-key, TOFU, and provisioned configurations and across lifecycle states: they are identical. If one protected ingress omits lifecycle gates or uses a different lifecycle lineage, the domain cannot advertise the profile and the uncovered ingress fails closed. If any claimed profile defines a binding-creating transition that declares neither grant continuation nor grant establishment, the domain cannot advertise that profile. | | `FI-LC-ORDINARY-GATES` | Fresh assertion and proof for a disabled identity, an identity with pending lineage, and a binding at administrative-expiry equality each deny without changing lifecycle state. | | `FI-LC-AUTHORITY` | An ordinary assertion plus valid Nostr proof, but no transition-specific authority, cannot perform any transition; mutation of any authority-bound field denies. | | `FI-LC-ATOMIC` | Inject failure at each transition write boundary; no binding, tombstone, disabled fact, lineage, history entry, or dependency version is partially committed. | @@ -203,7 +234,7 @@ denied case. | `FI-LC-PROVISION` | Ordinary first use in provisioned mode denies; authorized provisioning creates one binding and no lease; later current ordinary admission may use it. | | `FI-LC-DISABLE` | Disabling an active identity atomically disables it, retires its exact pair, records exact lineage, and closes subsequent lease use; replay is idempotent and preserves lineage. | | `FI-LC-REENABLE` | Re-enablement creates an eligible proven binding in the same commit that clears disabled state; absent or wrong expected lineage and a clear-only attempt deny. | -| `FI-LC-ADMIN-EXPIRY` | Before the bound the binding may authorize; at equality it denies while still occupying the relation; only an authorized version-checked update changes the bound. | +| `FI-LC-ADMIN-EXPIRY` | Before the bound the binding may authorize; at equality it denies while still occupying the relation, so a target eligibility test for either side of that pair fails. Rotating the expired binding to a new key carries the bound: the replacement denies at the same instant. No non-expiry transition clears it. Only an authorized version-checked update by the expiry authority changes the bound. Conversely, retirement, revocation, or re-enablement of the bound pair followed by an authorized or ordinary new grant produces an unbounded binding, which is the required result and not an escape. | | `FI-LC-QD-ONCE` | Two concurrent re-enablings consume the same `Q_D` lineage; exactly one commits and the loser leaves every authoritative store unchanged. | | `FI-LC-RACE` | Race each transition against prepared ordinary admission and lease use; no operation authorizes after observing the advanced lifecycle or binding dependency. | diff --git a/docs/nips/NIP-FI.md b/docs/nips/NIP-FI.md index 310fe39df9..c9949d8742 100644 --- a/docs/nips/NIP-FI.md +++ b/docs/nips/NIP-FI.md @@ -416,7 +416,11 @@ any policy-required current matching issuer attestation. [FI-TRACE-LIFECYCLE-AUT non-retired target key, retires the old pair, and creates a fresh binding version. The replacement provenance is `attested-key` when current matching issuer attestation was validated and `provisioned` otherwise. Rotation does - not globally revoke the old key. + not globally revoke the old key. Rotation continues one grant onto a new key + rather than establishing a new one: the replacement preserves every + profile-defined administrative bound carried by the binding it replaces, as an + opaque field core neither interprets nor clears. Only the authority that set + such a bound can change it. [FI-TRACE-LIFECYCLE-AUTHORITY] Failure or stale state causes no partial mutation. Ordinary authorization cannot perform or undo these transitions. Extended disablement, re-enablement,