Gratos_Challenge

------------------------- MODULE Gratos_Challenge ------------------------- (***************************************************************************) (* Models the challenge-keyed pending-ceremony state in gratos-multi. *) (* *) (* KV keys are {reg,auth}_challenge:{tenant}:{challenge}: Issue writes a *) (* key (options endpoint), Verify consumes it (get + delete before *) (* verification), Expire models the 300s TTL. There is no separate *) (* correlation id — the challenge itself, recovered from the signed *) (* clientDataJSON, is the key. *) (* *) (* Checked properties: *) (* - NoReplay: a consumed (tenant, challenge) pair never re-enters *) (* pending, so a credential response can verify at most once. *) (* - Cross-tenant isolation is structural: Verify(t, ch) requires the *) (* pair for that tenant in pending; a challenge issued for another *) (* tenant can never be consumed under t (tenant-namespaced key). *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Tenants, Challenges VARIABLES pending, \* set of <<tenant, challenge>> currently live in KV consumed \* set of <<tenant, challenge>> that have been verified vars == <<pending, consumed>> Pairs == Tenants \X Challenges Init == /\ pending = {} /\ consumed = {} \* Options endpoint: mint a fresh challenge for a tenant. Challenges are \* 32 random bytes from @simplewebauthn/server, so a value never repeats — \* encoded here by excluding both live and already-consumed pairs. Issue(t, ch) == /\ <<t, ch>> \notin pending /\ <<t, ch>> \notin consumed /\ pending' = pending \cup {<<t, ch>>} /\ UNCHANGED consumed \* Verify endpoint: get + delete the KV key, atomically consuming the \* challenge before the WebAuthn verification runs. Verify(t, ch) == /\ <<t, ch>> \in pending /\ pending' = pending \ {<<t, ch>>} /\ consumed' = consumed \cup {<<t, ch>>} \* KV TTL: a pending challenge silently disappears after 300s. Expire(t, ch) == /\ <<t, ch>> \in pending /\ pending' = pending \ {<<t, ch>>} /\ UNCHANGED consumed Next == \E t \in Tenants, ch \in Challenges : Issue(t, ch) \/ Verify(t, ch) \/ Expire(t, ch) Spec == Init /\ [][Next]_vars TypeOK == /\ pending \subseteq Pairs /\ consumed \subseteq Pairs \* Single-use: once verified, a pair can never be live again, so a second \* POST of the same credential response always fails the KV lookup. NoReplay == pending \cap consumed = {} =============================================================================

SPECIFICATION Spec \* Quiescence is legal: with the finite challenge pool, a state where every \* (tenant, challenge) pair has been consumed has no enabled action. That is \* the never-repeats encoding running dry, not a stuck protocol. CHECK_DEADLOCK FALSE CONSTANTS Tenants = {t1, t2} Challenges = {c1, c2} INVARIANTS TypeOK NoReplay