TpxRefresh

---- MODULE TpxRefresh ---- (***************************************************************************) (* Client-side refresh-token rotation for the browser-direct TPX OAuth *) (* client (apps/web/src/lib/tpx.ts). *) (* *) (* The authorization server keeps ONE valid refresh-token generation *) (* (asGen). A refresh presenting the current generation succeeds and *) (* rotates it (asGen + 1); presenting a stale generation is reuse and *) (* REVOKES the whole grant permanently. Two browser tabs share one *) (* localStorage slot holding the latest known generation; each tab does *) (* read slot -> refresh -> write rotated token back. *) (* *) (* The constant UseLock selects the design: *) (* FALSE: tabs interleave freely between read, request, and write-back. *) (* TRUE: the read-refresh-write section is a cross-tab critical *) (* section (the Web Lock in accessToken()). *) (* *) (* With UseLock = FALSE, TLC violates GrantSurvives in 5 states — the *) (* lost-token race that makes the Web Lock necessary, not defensive: *) (* 1. init: asGen = 0, slot = 0 *) (* 2. Enter(t1): t1 reads slot, holds generation 0 *) (* 3. RefreshOK(t1): server rotates, asGen = 1; t1 holds 1, slot *) (* still 0 (t1 has not written back yet) *) (* 4. Enter(t2): t2 reads slot, holds STALE generation 0 *) (* 5. RefreshStale(t2): t2 presents 0 while asGen = 1 -> reuse *) (* detected, revoked = TRUE. GrantSurvives violated. *) (* (17 states generated, 14 distinct.) *) (* *) (* The checked-in TpxRefresh.cfg uses UseLock = TRUE and passes *) (* (51 states generated, 49 distinct, depth 13): with the critical *) (* section, an honest pair of tabs can never trip reuse detection. *) (***************************************************************************) EXTENDS Naturals, TLC CONSTANT UseLock MaxGen == 4 \* 2 tabs x 2 refreshes: 4 rotations suffice Tabs == {"t1", "t2"} MaxRefreshes == 2 \* per-tab refresh budget (bounds the model) NoTab == "none" Gens == 0..MaxGen VARIABLES asGen, \* authorization server: the one currently-valid refresh generation revoked, \* TRUE once the server detects reuse and kills the grant slot, \* shared storage slot: latest refresh generation known to clients lock, \* mutex holder (meaningful only when UseLock) tab \* per-tab client state vars == <<asGen, revoked, slot, lock, tab>> TabStates == [phase: {"idle", "read", "got"}, tok: Gens, done: 0..MaxRefreshes] TypeOK == /\ asGen \in Gens /\ revoked \in BOOLEAN /\ slot \in Gens /\ lock \in Tabs \cup {NoTab} /\ tab \in [Tabs -> TabStates] Init == /\ asGen = 0 /\ revoked = FALSE /\ slot = 0 /\ lock = NoTab /\ tab = [t \in Tabs |-> [phase |-> "idle", tok |-> 0, done |-> 0]] Release(t) == IF lock = t THEN NoTab ELSE lock (* Tab enters its refresh path: acquire the lock (a no-op when UseLock is *) (* FALSE) and read the shared slot. The Web Locks callback reads storage *) (* immediately on entry, so acquire+read is one step in both designs. *) Enter(t) == /\ tab[t].phase = "idle" /\ tab[t].done < MaxRefreshes /\ ~revoked /\ (UseLock => lock = NoTab) /\ lock' = IF UseLock THEN t ELSE lock /\ tab' = [tab EXCEPT ![t].phase = "read", ![t].tok = slot] /\ UNCHANGED <<asGen, revoked, slot>> (* Server: the presented token is current -> rotate and hand out the next *) (* generation. Request + response are one atomic step (the server's *) (* token endpoint is transactional). *) RefreshOK(t) == /\ tab[t].phase = "read" /\ ~revoked /\ tab[t].tok = asGen /\ asGen < MaxGen /\ asGen' = asGen + 1 /\ tab' = [tab EXCEPT ![t].phase = "got", ![t].tok = asGen + 1] /\ UNCHANGED <<revoked, slot, lock>> (* Server: the presented token is stale -> reuse detection revokes the *) (* grant. The client sees the rejection, drops its state, and releases *) (* the lock (tpx.ts clears tpx.tokens and throws NeedsGrantError). *) RefreshStale(t) == /\ tab[t].phase = "read" /\ tab[t].tok # asGen /\ revoked' = TRUE /\ tab' = [tab EXCEPT ![t].phase = "idle", ![t].tok = 0, ![t].done = @ + 1] /\ lock' = Release(t) /\ UNCHANGED <<asGen, slot>> (* Tab persists the rotated token to the shared slot and leaves the *) (* critical section. *) WriteBack(t) == /\ tab[t].phase = "got" /\ slot' = tab[t].tok /\ tab' = [tab EXCEPT ![t].phase = "idle", ![t].done = @ + 1] /\ lock' = Release(t) /\ UNCHANGED <<asGen, revoked>> Next == \E t \in Tabs : Enter(t) \/ RefreshOK(t) \/ RefreshStale(t) \/ WriteBack(t) Spec == Init /\ [][Next]_vars ---------------------------------------------------------------------------- (* Invariants *) (* Honest clients never trip reuse detection: the grant survives. *) GrantSurvives == ~revoked ====

SPECIFICATION Spec CONSTANT UseLock = TRUE INVARIANT TypeOK INVARIANT GrantSurvives CHECK_DEADLOCK FALSE