Token refinement pilot

Phase 5 connects three deliberately different descriptions of one narrow property: the per-boot lifecycle of the FIDO pinUvAuthToken and its persistent credential-management grant. It does not establish whole-firmware formal verification, cross-reset refinement, or liveness.

The three tiers

• A is formal/RSKeyTokenAbstract.tla: 44 states and an outcome-labelled AllowedEventRel. Next is its existential closure, not a second relation.
• B is formal/RSKeySecurityState.tla. TLC checks native INSTANCE refinement in TokenRefinement.cfg, and checks labelled outcomes separately in TokenRefinementOutcome.cfg.
• C is (FidoState, TokenPersistentView). The persistent view contains exactly EF_PIN and EF_PAUTHTOKEN. EF_ALWAYS_UV is excluded: it decides when UV is required, but it is not token-lifecycle state. A therefore over-approximates the no-PIN state when the runtime flag is enabled.

The TLA+ module owns AStates, Ops, Outcomes, and AllowedRelation. scripts/export_token_relation.py only captures TLA+-serialized values; scripts/generate_token_edges.py generates the Rust enums, AState, and exact bitset. The exhaustive host test checks all 69,696 tuples. The current export is 44 states, 12 operations, 3 outcomes, and 1,039 allowed edges; these are printed facts, not hand-maintained requirements.

Concrete domain and boot boundary

InitC is the real boot shape relevant to this projection: FidoState::new, the valid BootState lock/warm restoration performed by AppletHandler::new, and clientPIN initialization. Initialization rerolls secret bytes but leaves the abstract token retired. ValidBootInput bounds the restored mismatch byte by PIN_MISMATCH_LIMIT; the board decoder clamps older or corrupt scratch values to that range.

ValidPersistent admits all four presence combinations of EF_PIN and EF_PAUTHTOKEN. This is intentional, including grant && !pinSet: since 0x09CB ensure_seed writes the grant record with no PIN behind it, so that shape is the factory state and the state after every completed reset, and firmware before 0x08BF or a torn reset could leave it too. Because A observes only record presence, not record contents, no older-firmware version assumption is needed for R0p. Every projected write and power cut remains inside those four states.

wf_concrete(F, P) requires the production permission shapes represented by B, live(F) => P.pin_set, a retired token to have no permission or rp binding, and an rp binding to imply a live token. R2a checks InitC; R2b checks inductiveness without kani::assume. R3a checks the initial map and R3b checks every bounded named concrete step against the generated relation.

Reset evidence table

There is no Compatible premise. No additional boot restriction was found; R0a uses only ValidBootInput. M7-Q1 and M7-Q2 are hardware-evidence tasks, not assumptions silently added to the refinement theorem.

Outcomes and completeness

Outcomes are labels, not A variables. Authorized on a dead-token stutter is therefore still a distinct, forbidden tuple. R1o checks B action labels, while the emulator trace carries outcome_raw copied from the real CTAP response. The validator derives possible B outcomes independently and accepts only consensus: one singleton equal to δC. Multiple interpretations are AMBIGUOUS, never a selected witness; formal/floors.txt ratchets their count.

assurance/token_refinement.toml and scripts/token_refinement_gate.py enforce the three completeness axes across the tree: volatile writers of the token, persistent writers for the keys derived from TokenPersistentView, and authorization outcome producers. Every vocabulary the scan matches on is read out of the tree — the token’s own field list, the PERM_* constants, the Fs methods that reach a storage mutation, the fields and permissions abstract_token really reads, and the crate’s module graph — so a new field, permission or store method arrives as an unowned site rather than as silence. Each entry then carries its disposition: step names the abstract Step it implements, stutter moves security-visible state A does not observe, out-of-scope is a real gate outside A’s vocabulary, and the gate derives which of those a site can be from what it writes.

Three of them are configuration-conditional, and the column field names the docs/assurance-matrix.md column that makes them so. The panel’s set-PIN and PIN-check doors onto EF_PIN exist only where firmware-display pulls in rsk-display; the authenticatorLargeBlobs write gate — the one authorization decision on a permission bit A has no word for — is dead in the largeblob-ext column, because CTAP 2.3 §12.4 forbids serving both large-blob designs and the dispatch is guarded on it.

assurance-trace exposes verification artifacts to the host emulator and is never a firmware feature. check.sh poisons every assurance-only module in a throwaway tree, proves the poison reaches a host feature build but not firmware, and requires the pristine and poisoned firmware images to be byte-identical.

Reproduce

nix develop -c ./scripts/token_refinement.sh --check
nix develop -c ./formal/run-tlc.sh TokenRefinement.cfg
nix develop -c ./formal/run-tlc.sh TokenRefinementOutcome.cfg
nix develop -c ./scripts/kani.sh state

The state/outcome mutants, wrong generated edge tests, broken-stop test, dead-token authorized stutter test, and ambiguous-consensus test are part of the same tree. Cross-reset behavior remains phase 6.