-------------------------- 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

=============================================================================