OpenMonkeyAuth

-------------------------- MODULE OpenMonkeyAuth -------------------------- (***************************************************************************) (* First-party auth ceremony for OpenMonkey. *) (* *) (* Login/register UI is served first-party (openmonkey.proc.io) and calls *) (* the auth service's raw API from the browser. All ceremony kinds *) (* (WebAuthn passkey create/get, HKDF account-key signature, silent *) (* device-key login) share one shape, modeled as a single abstract *) (* ceremony: *) (* *) (* Issue - GET /v1/{register,login}/options hands the browser a fresh *) (* challenge bound to the requesting principal. *) (* Verify - POST /v1/{register,login}/verify (or /v1/key/...): the *) (* server accepts a challenge only if it is fresh (never used) *) (* and no older than TTL, consumes it, and creates a session. *) (* The session cookie replaces any prior one for that user. *) (* Logout - POST /v1/logout destroys the session. *) (* *) (* Sessions and the trust model are unchanged from the hosted-pages *) (* design: the auth service issues and validates sessions; the app API *) (* forwards the first-party session cookie to /v1/whoami, an access gate *) (* that is exactly "session active", so it needs no extra state here. *) (* CORS/cross-subdomain transport is not state and is out of scope. *) (* *) (* Safety-only, finite model. The real 5-minute challenge TTL is *) (* abstracted to TTL clock ticks against a bounded clock. Challenge *) (* identities are ordered slots allocated lowest-free-slot first *) (* (symmetry breaking). NoChal (= 0) marks "no session". *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Users, \* set of principals (model values) NumChallenges, \* number of challenge identity slots MaxClock, \* clock bound TTL, \* challenge lifetime in ticks (abstracts 5 minutes) NULL \* model value: "no owner" ASSUME NumChallenges \in Nat /\ NumChallenges >= 1 ASSUME MaxClock \in Nat /\ TTL \in Nat /\ TTL < MaxClock Chals == 1..NumChallenges NoChal == 0 VARIABLES clock, \* 0..MaxClock chalOwner, \* [Chals -> Users \cup {NULL}] principal it was issued to chalIssued, \* [Chals -> 0..MaxClock] issue time chalVerifiedAt, \* [Chals -> 0..MaxClock] consume time (used only) chalState, \* [Chals -> {"none","fresh","used"}] sessionChal \* [Users -> Chals \cup {NoChal}] challenge backing the \* user's active session; NoChal = logged out vars == <<clock, chalOwner, chalIssued, chalVerifiedAt, chalState, sessionChal>> Init == /\ clock = 0 /\ chalOwner = [c \in Chals |-> NULL] /\ chalIssued = [c \in Chals |-> 0] /\ chalVerifiedAt = [c \in Chals |-> 0] /\ chalState = [c \in Chals |-> "none"] /\ sessionChal = [u \in Users |-> NoChal] Tick == /\ clock < MaxClock /\ clock' = clock + 1 /\ UNCHANGED <<chalOwner, chalIssued, chalVerifiedAt, chalState, sessionChal>> \* Browser fetches ceremony options; server mints a challenge bound to u. \* Lowest-free-slot allocation breaks challenge-labeling symmetry. Issue(u, c) == /\ chalState[c] = "none" /\ \A x \in 1..(c - 1) : chalState[x] # "none" /\ chalOwner' = [chalOwner EXCEPT ![c] = u] /\ chalIssued' = [chalIssued EXCEPT ![c] = clock] /\ chalState' = [chalState EXCEPT ![c] = "fresh"] /\ UNCHANGED <<clock, chalVerifiedAt, sessionChal>> \* Server-side verify: accepts only a fresh, same-owner, unexpired \* challenge; consumes it (single use) and creates the session. A new \* login replaces any existing session cookie for that user. Verify(u, c) == /\ chalState[c] = "fresh" /\ chalOwner[c] = u /\ clock - chalIssued[c] <= TTL /\ chalState' = [chalState EXCEPT ![c] = "used"] /\ chalVerifiedAt' = [chalVerifiedAt EXCEPT ![c] = clock] /\ sessionChal' = [sessionChal EXCEPT ![u] = c] /\ UNCHANGED <<clock, chalOwner, chalIssued>> \* POST /v1/logout destroys the session server-side. Logout(u) == /\ sessionChal[u] # NoChal /\ sessionChal' = [sessionChal EXCEPT ![u] = NoChal] /\ UNCHANGED <<clock, chalOwner, chalIssued, chalVerifiedAt, chalState>> Next == \/ Tick \/ \E u \in Users : \/ Logout(u) \/ \E c \in Chals : Issue(u, c) \/ Verify(u, c) Spec == Init /\ [][Next]_vars (***************************************************************************) (* Invariants *) (***************************************************************************) TypeOK == /\ clock \in 0..MaxClock /\ chalOwner \in [Chals -> Users \cup {NULL}] /\ chalIssued \in [Chals -> 0..MaxClock] /\ chalVerifiedAt \in [Chals -> 0..MaxClock] /\ chalState \in [Chals -> {"none", "fresh", "used"}] /\ sessionChal \in [Users -> Chals \cup {NoChal}] \* 1. Every active session is backed by a consumed challenge that was \* issued to exactly that principal. No session without a completed \* ceremony, and never on someone else's challenge. SessionBackedByOwnChallenge == \A u \in Users : sessionChal[u] # NoChal => /\ chalState[sessionChal[u]] = "used" /\ chalOwner[sessionChal[u]] = u \* 2. A challenge backs at most one session (single use across users; \* within a user a re-login replaces the session). ChallengeSingleUse == \A u1 \in Users, u2 \in Users : (u1 # u2 /\ sessionChal[u1] # NoChal) => sessionChal[u1] # sessionChal[u2] \* 3. Every consumed challenge was verified within TTL of issuance: \* expired challenges never create sessions. VerifiedWithinTTL == \A c \in Chals : chalState[c] = "used" => /\ chalVerifiedAt[c] >= chalIssued[c] /\ chalVerifiedAt[c] - chalIssued[c] <= TTL (***************************************************************************) (* Action properties *) (***************************************************************************) \* A consumed challenge is consumed forever: no replay of used challenges. NoChallengeReplay == [][\A c \in Chals : chalState[c] = "used" => chalState'[c] = "used"]_vars \* Challenge bindings are immutable once issued. ChallengeBindingImmutable == [][\A c \in Chals : chalState[c] # "none" => /\ chalOwner'[c] = chalOwner[c] /\ chalIssued'[c] = chalIssued[c]]_vars =============================================================================

SPECIFICATION Spec CONSTANTS Users = {u1, u2} NumChallenges = 2 MaxClock = 3 TTL = 1 NULL = NULL INVARIANTS TypeOK SessionBackedByOwnChallenge ChallengeSingleUse VerifiedWithinTTL PROPERTIES NoChallengeReplay ChallengeBindingImmutable CHECK_DEADLOCK FALSE