KosyncCredentials

-------------------------- MODULE KosyncCredentials -------------------------- (***************************************************************************) (* KOReader progress-sync (kosync) credential lifecycle for happybook. *) (* *) (* Models the D1 table *) (* kosync_credentials(user_id PRIMARY KEY, username UNIQUE NOT NULL, *) (* password NOT NULL, created_at) *) (* as a set of <<user, username, password>> triples, and the operations: *) (* *) (* - Enable/Regenerate: generate a fresh random (username, password) *) (* pair and INSERT ... ON CONFLICT(user_id) DO UPDATE SET username, *) (* password. Each attempt is one atomic SQL statement; if the fresh *) (* username collides with ANOTHER user's UNIQUE username the *) (* statement fails with no effect and the caller retries with fresh *) (* random values, up to MaxAttempts times, then gives up. *) (* - Revoke: DELETE by user_id. *) (* - Auth (KOReader request): atomic SELECT user_id, password WHERE *) (* username = n, then compare md5(password) with the presented key. *) (* Abstractly: auth succeeds for (n, p) iff <<u, n, p>> is a current *) (* row, and the request then acts as u. *) (* *) (* Invariants: *) (* - UsernamesUnique: no two users ever hold the same username. *) (* - AtMostOneCredPerUser: user_id is a primary key. *) (* - AuthSound: an auth check with (username, password) only ever *) (* resolves to the user whose current row is exactly that pair (so *) (* after regenerate/revoke the old pair no longer authenticates, and *) (* a username can never authenticate as the wrong user). *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Users, \* small set of user ids Usernames, \* small username space, so generate-collisions occur Passwords, \* small password space MaxAttempts, \* retry budget for the regenerate loop (3 in the code) NoAuth \* model value: "no auth result pending" VARIABLES table, \* subset of Users \X Usernames \X Passwords: the rows regen, \* per-user state of an in-flight enable/regenerate call lastAuth \* result of the auth SELECT taken in the previous step vars == <<table, regen, lastAuth>> RegenStates == [active : BOOLEAN, tries : 0..MaxAttempts] TypeOK == /\ table \subseteq Users \X Usernames \X Passwords /\ regen \in [Users -> RegenStates] /\ lastAuth \in [name : Usernames, pw : Passwords, user : Users] \cup {NoAuth} Init == /\ table = {} /\ regen = [u \in Users |-> [active |-> FALSE, tries |-> 0]] /\ lastAuth = NoAuth ----------------------------------------------------------------------------- (* A request begins an enable/regenerate for user u. *) StartRegen(u) == /\ ~regen[u].active /\ regen' = [regen EXCEPT ![u] = [active |-> TRUE, tries |-> 0]] /\ lastAuth' = NoAuth /\ UNCHANGED table (* One upsert attempt with freshly generated pair (n, p) whose username *) (* does not collide with another user's row: the atomic INSERT ... ON *) (* CONFLICT replaces u's row (if any) and the call returns. *) UpsertOk(u, n, p) == /\ regen[u].active /\ ~\E r \in table : r[1] # u /\ r[2] = n /\ table' = {r \in table : r[1] # u} \cup {<<u, n, p>>} /\ regen' = [regen EXCEPT ![u].active = FALSE] /\ lastAuth' = NoAuth (* One upsert attempt whose generated username n is already held by a *) (* different user: the UNIQUE(username) constraint rejects the statement, *) (* which has no effect on the table. The caller retries with fresh *) (* random values until the budget is exhausted, then gives up (surfacing *) (* an error to the user). *) UpsertCollision(u, n) == /\ regen[u].active /\ \E r \in table : r[1] # u /\ r[2] = n /\ regen' = [regen EXCEPT ![u] = [active |-> regen[u].tries + 1 < MaxAttempts, tries |-> regen[u].tries + 1]] /\ lastAuth' = NoAuth /\ UNCHANGED table (* DELETE FROM kosync_credentials WHERE user_id = u. May interleave with *) (* anything, including another request's in-flight regenerate. *) Revoke(u) == /\ table' = {r \in table : r[1] # u} /\ lastAuth' = NoAuth /\ UNCHANGED regen (* Atomic SELECT user_id, password WHERE username = n plus the md5 key *) (* comparison, hit case: record the resolution so AuthSound can inspect *) (* it in the post-state. *) AuthHit(n, p) == /\ \E u \in Users : <<u, n, p>> \in table /\ lastAuth' = [name |-> n, pw |-> p, user |-> CHOOSE u \in Users : <<u, n, p>> \in table] /\ UNCHANGED <<table, regen>> (* SELECT miss or key mismatch: the request is rejected with 401. *) AuthMiss(n, p) == /\ ~\E u \in Users : <<u, n, p>> \in table /\ lastAuth' = NoAuth /\ UNCHANGED <<table, regen>> Next == \/ \E u \in Users : StartRegen(u) \/ Revoke(u) \/ \E u \in Users, n \in Usernames, p \in Passwords : UpsertOk(u, n, p) \/ \E u \in Users, n \in Usernames : UpsertCollision(u, n) \/ \E n \in Usernames, p \in Passwords : AuthHit(n, p) \/ AuthMiss(n, p) Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- (* UNIQUE(username): no two rows share a username. *) UsernamesUnique == \A n \in Usernames : Cardinality({r \in table : r[2] = n}) <= 1 (* PRIMARY KEY(user_id): no two rows share a user. *) AtMostOneCredPerUser == \A u \in Users : Cardinality({r \in table : r[1] = u}) <= 1 (* Whenever an auth SELECT resolved to a user, that user's current row *) (* carries exactly the presented username and password. *) AuthSound == lastAuth = NoAuth \/ <<lastAuth.user, lastAuth.name, lastAuth.pw>> \in table =============================================================================

SPECIFICATION Spec CONSTANTS Users = {u1, u2} Usernames = {n1, n2} Passwords = {p1, p2} MaxAttempts = 3 NoAuth = NoAuth INVARIANTS TypeOK UsernamesUnique AtMostOneCredPerUser AuthSound CHECK_DEADLOCK FALSE