OpdsCredentials

--------------------------- MODULE OpdsCredentials --------------------------- (***************************************************************************) (* OPDS credential lifecycle for happybook. *) (* *) (* Models the D1 table *) (* opds_credentials(user_id PRIMARY KEY, password UNIQUE, created_at) *) (* as a set of <<user, password>> pairs, and the operations: *) (* *) (* - Enable/Regenerate: INSERT ... ON CONFLICT(user_id) DO UPDATE SET *) (* password = new. Each attempt is one atomic SQL statement; if the *) (* fresh password collides with ANOTHER user's UNIQUE password the *) (* statement fails with no effect and the caller retries with a new *) (* random password, up to MaxAttempts times. *) (* - Revoke: DELETE by user_id. *) (* - Basic-auth read: atomic SELECT user_id WHERE password = p; the *) (* request then acts as the returned user. *) (* *) (* Invariants: *) (* - PasswordsUnique: no two users ever hold the same password. *) (* - AtMostOneCredPerUser: user_id is a primary key. *) (* - AuthSound: an auth check with password p only ever resolves to a *) (* user whose current password is p (so after regenerate/revoke the *) (* old password no longer authenticates). *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Users, \* small set of user ids Passwords, \* small password space, so generate-collisions occur MaxAttempts, \* retry budget for the regenerate loop (3 in the code) NoAuth \* model value: "no auth result pending" VARIABLES table, \* subset of Users \X Passwords: the opds_credentials 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 Passwords /\ regen \in [Users -> RegenStates] /\ lastAuth \in [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 password p that 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, p) == /\ regen[u].active /\ ~\E v \in Users \ {u} : <<v, p>> \in table /\ table' = {r \in table : r[1] # u} \cup {<<u, p>>} /\ regen' = [regen EXCEPT ![u].active = FALSE] /\ lastAuth' = NoAuth (* One upsert attempt whose generated password p is already held by a *) (* different user: the UNIQUE(password) constraint rejects the statement, *) (* which has no effect on the table. The caller retries until the budget *) (* is exhausted, then gives up (surfacing an error to the user). *) UpsertCollision(u, p) == /\ regen[u].active /\ \E v \in Users \ {u} : <<v, p>> \in table /\ regen' = [regen EXCEPT ![u] = [active |-> regen[u].tries + 1 < MaxAttempts, tries |-> regen[u].tries + 1]] /\ lastAuth' = NoAuth /\ UNCHANGED table (* DELETE FROM opds_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 WHERE password = p, hit case: record the *) (* resolution so AuthSound can inspect it in the post-state. *) AuthHit(p) == /\ \E u \in Users : <<u, p>> \in table /\ lastAuth' = [pw |-> p, user |-> CHOOSE u \in Users : <<u, p>> \in table] /\ UNCHANGED <<table, regen>> (* SELECT miss: the request is rejected with 401. *) AuthMiss(p) == /\ ~\E u \in Users : <<u, p>> \in table /\ lastAuth' = NoAuth /\ UNCHANGED <<table, regen>> Next == \/ \E u \in Users : StartRegen(u) \/ Revoke(u) \/ \E u \in Users, p \in Passwords : UpsertOk(u, p) \/ UpsertCollision(u, p) \/ \E p \in Passwords : AuthHit(p) \/ AuthMiss(p) Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- (* UNIQUE(password): no two rows share a password. *) PasswordsUnique == \A p \in Passwords : Cardinality({r \in table : r[2] = p}) <= 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 password. *) AuthSound == lastAuth = NoAuth \/ <<lastAuth.user, lastAuth.pw>> \in table =============================================================================

SPECIFICATION Spec CONSTANTS Users = {u1, u2, u3} Passwords = {p1, p2, p3} MaxAttempts = 3 NoAuth = NoAuth INVARIANTS TypeOK PasswordsUnique AtMostOneCredPerUser AuthSound CHECK_DEADLOCK FALSE