--------------------------- MODULE BylineDelegation --------------------------- (***************************************************************************) (* Safety model of an AAuth-style delegation server: a root person spawns *) (* agents whose identity is delegated from the person, and a resource *) (* serves deploys only along a chain that traces back to a live grant. *) (* *) (* Lifecycle modeled (mirroring a Worker + D1 implementation): *) (* *) (* - Spawn: the person creates an agent (pending), a delegation grant *) (* (person -> agent, scope deploy, active), and a single-use bootstrap *) (* token with a TTL. *) (* - Redeem: the bootstrap token is consumed by ONE atomic conditional *) (* UPDATE (redeemed_at IS NULL AND not expired); the winner binds the *) (* public key it presented to the agent (jkt) and receives an agent *) (* token bound to that key (cnf.jwk). The bootstrap string travels *) (* over the network, so a thief who observed it may race the redeem *) (* with its OWN key. Single-use means exactly one of {owner, thief} *) (* wins and the loser fails loudly. This is the accepted *) (* possession-based window, mitigated operationally by the short TTL *) (* and by delivering the token over a private channel (e.g. a k8s *) (* Secret); a thief victory is loud (the owner cannot bind), not an *) (* invariant violation. *) (* - IssueResource: the resource challenges a signed agent request with *) (* a resource token naming the agent and the presenting key's jkt. *) (* - MintAuth (person /token): mints an auth token only if the *) (* presenting key's jkt equals the agent's bound jkt AND the agent is *) (* active AND an unrevoked grant (person, agent, scope) exists. *) (* Resource tokens are single-use via a jti table (atomic *) (* insert-or-nothing), so replaying one mints at most one auth token. *) (* Faithful detail: the jti is consumed BEFORE the grant read, so a *) (* presentation that fails the grant check still burns the jti *) (* (BurnJti) -- an availability cost, never a safety one. *) (* - BeginAccess / CommitAccess (resource /client/v4): exchanges a valid *) (* auth token (cnf.jkt must equal the presenting key's jkt) for an *) (* opaque access token row. The grant is read, then the row is *) (* inserted WITHOUT re-checking -- two-phase on purpose, matching the *) (* code: a revocation may land in between, so an access token row can *) (* exist whose grant is already revoked. That is safe only because... *) (* - UseAccess: every USE of the access token re-joins to the grant at *) (* decision time (revoked_at IS NULL). The use log records the grant *) (* state observed at decision time; RevokedGrantNeverServes is the *) (* load-bearing invariant that forces this per-request join instead *) (* of trusting token expiry. *) (* *) (* Expiry is modeled as a simple state transition (active -> expired), *) (* not with clocks. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Agents, \* pool of agent identities the person may spawn Keys, \* signing keypairs (a key stands for possession of its private half) ThiefKeys, \* keys held by the network observer, never by an owner pod BootTokens, \* pool of single-use bootstrap-token identities ResTokens, \* pool of resource-token identities (jti) AuthTokens, \* pool of auth-token identities AccTokens, \* pool of opaque access-token identities NoKey, \* model value: "no key bound" NoAgent, \* model value: "no agent" NoRes \* model value: "no resource token" ASSUME ThiefKeys \subseteq Keys ASSUME NoKey \notin Keys ASSUME NoAgent \notin Agents ASSUME NoRes \notin ResTokens OwnerKeys == Keys \ ThiefKeys AgentStates == {"free", "pending", "active"} GrantStates == {"none", "active", "revoked"} BootStates == {"free", "issued", "redeemed", "expired"} ResStates == {"free", "issued", "redeemed", "expired"} TokStates == {"free", "active", "expired"} VARIABLES agentSt, \* Agents -> lifecycle state (free = not yet spawned) agentJkt, \* Agents -> key bound at redeem time (the stored jkt), or NoKey grantSt, \* Agents -> state of THE grant (1 person, scope deploy => one grant per agent) bootSt, \* BootTokens -> lifecycle state bootAgent, \* BootTokens -> agent the bootstrap was minted for stolen, \* subset of BootTokens whose string a thief has observed creds, \* subset of Agents \X Keys: agent token bound to key + private key possession redemptions, \* subset of BootTokens \X Keys: history of successful redeems (for SingleUseBootstrap) resSt, \* ResTokens -> lifecycle state ("redeemed" = jti row inserted) resAgent, \* ResTokens -> agent claim resKey, \* ResTokens -> agent_jkt claim (key that signed the challenged request) authSt, \* AuthTokens -> lifecycle state authAgent, \* AuthTokens -> agent the token authorizes (via cnf.jkt + grant) authKey, \* AuthTokens -> cnf.jkt authRes, \* AuthTokens -> resource token (jti) the auth token was minted from accSt, \* AccTokens -> lifecycle state accAgent, \* AccTokens -> agent the opaque row is bound to (row also carries person+grant) inflightAcc, \* AuthTokens -> 0..1 : access mints past the grant read, before the insert useLog \* history of access-token authorization decisions: the decision \* (ok) and the grant state observed at decision time (gst) vars == <> TypeOK == /\ agentSt \in [Agents -> AgentStates] /\ agentJkt \in [Agents -> Keys \cup {NoKey}] /\ grantSt \in [Agents -> GrantStates] /\ bootSt \in [BootTokens -> BootStates] /\ bootAgent \in [BootTokens -> Agents \cup {NoAgent}] /\ stolen \subseteq BootTokens /\ creds \subseteq (Agents \X Keys) /\ redemptions \subseteq (BootTokens \X Keys) /\ resSt \in [ResTokens -> ResStates] /\ resAgent \in [ResTokens -> Agents \cup {NoAgent}] /\ resKey \in [ResTokens -> Keys \cup {NoKey}] /\ authSt \in [AuthTokens -> TokStates] /\ authAgent \in [AuthTokens -> Agents \cup {NoAgent}] /\ authKey \in [AuthTokens -> Keys \cup {NoKey}] /\ authRes \in [AuthTokens -> ResTokens \cup {NoRes}] /\ accSt \in [AccTokens -> TokStates] /\ accAgent \in [AccTokens -> Agents \cup {NoAgent}] /\ inflightAcc \in [AuthTokens -> 0..1] /\ useLog \subseteq [ok: BOOLEAN, gst: GrantStates] Init == /\ agentSt = [a \in Agents |-> "free"] /\ agentJkt = [a \in Agents |-> NoKey] /\ grantSt = [a \in Agents |-> "none"] /\ bootSt = [b \in BootTokens |-> "free"] /\ bootAgent = [b \in BootTokens |-> NoAgent] /\ stolen = {} /\ creds = {} /\ redemptions = {} /\ resSt = [r \in ResTokens |-> "free"] /\ resAgent = [r \in ResTokens |-> NoAgent] /\ resKey = [r \in ResTokens |-> NoKey] /\ authSt = [t \in AuthTokens |-> "free"] /\ authAgent = [t \in AuthTokens |-> NoAgent] /\ authKey = [t \in AuthTokens |-> NoKey] /\ authRes = [t \in AuthTokens |-> NoRes] /\ accSt = [x \in AccTokens |-> "free"] /\ accAgent = [x \in AccTokens |-> NoAgent] /\ inflightAcc = [t \in AuthTokens |-> 0] /\ useLog = {} (***************************************************************************) (* The person spawns an agent: one D1 batch inserts the agent row *) (* (pending), the delegation grant (active), and the bootstrap token. *) (***************************************************************************) Spawn(a, b) == /\ agentSt[a] = "free" /\ bootSt[b] = "free" /\ agentSt' = [agentSt EXCEPT ![a] = "pending"] /\ grantSt' = [grantSt EXCEPT ![a] = "active"] /\ bootSt' = [bootSt EXCEPT ![b] = "issued"] /\ bootAgent' = [bootAgent EXCEPT ![b] = a] /\ UNCHANGED <> \* The bootstrap string crosses the network; a thief observes it. StealBoot(b) == /\ bootSt[b] = "issued" /\ b \notin stolen /\ stolen' = stolen \cup {b} /\ UNCHANGED <> \* Bootstrap TTL elapses before redemption. ExpireBoot(b) == /\ bootSt[b] = "issued" /\ bootSt' = [bootSt EXCEPT ![b] = "expired"] /\ UNCHANGED <> (***************************************************************************) (* POST /api/agents/redeem: the atomic conditional UPDATE *) (* UPDATE bootstrap_tokens SET redeemed_at = now *) (* WHERE token_hash = ? AND redeemed_at IS NULL AND expires_at > now *) (* Exactly one caller wins; the winner binds ITS key to the agent and *) (* receives an agent token bound to that key. An owner pod redeems with *) (* an owner key; a thief needs to have observed the string and redeems *) (* with a thief key. The loser's UPDATE changes 0 rows: loud 403. *) (***************************************************************************) Redeem(b, k) == /\ bootSt[b] = "issued" /\ (k \in ThiefKeys) => (b \in stolen) /\ LET a == bootAgent[b] IN /\ bootSt' = [bootSt EXCEPT ![b] = "redeemed"] /\ agentJkt' = [agentJkt EXCEPT ![a] = k] /\ agentSt' = [agentSt EXCEPT ![a] = "active"] /\ creds' = creds \cup {<>} /\ redemptions' = redemptions \cup {<>} /\ UNCHANGED <> \* The person revokes the delegation grant. RevokeGrant(a) == /\ grantSt[a] = "active" /\ grantSt' = [grantSt EXCEPT ![a] = "revoked"] /\ UNCHANGED <> (***************************************************************************) (* Resource rung 1: a signed request with no auth token is challenged *) (* with a resource token naming the requesting agent and the jkt of the *) (* key that signed the request. No DB state is consulted here. *) (***************************************************************************) IssueResource(r, a, k) == /\ resSt[r] = "free" /\ <> \in creds /\ resSt' = [resSt EXCEPT ![r] = "issued"] /\ resAgent' = [resAgent EXCEPT ![r] = a] /\ resKey' = [resKey EXCEPT ![r] = k] /\ UNCHANGED <> \* Resource token TTL elapses; verifyJwt rejects it before the jti insert. ExpireRes(r) == /\ resSt[r] = "issued" /\ resSt' = [resSt EXCEPT ![r] = "expired"] /\ UNCHANGED <> (***************************************************************************) (* Person /token, successful path. Signature and claim checks (agent, *) (* agent_jkt) pass, the jti insert-or-nothing wins, and the grant join *) (* grants g JOIN agents a WHERE g.agent_id = ? AND g.scope = ? *) (* AND g.revoked_at IS NULL AND a.status = 'active' AND a.jkt = ? *) (* finds a live row. The jti insert is atomic (ON CONFLICT DO NOTHING *) (* with changes = 1 required), so two concurrent replays of one resource *) (* token cannot both reach the mint: the insert IS the decision point, *) (* which is why this action can be modeled atomically. *) (***************************************************************************) MintAuth(r, k, t) == /\ resSt[r] = "issued" /\ <> \in creds \* signed request as that agent, key k /\ k = resKey[r] \* agent_jkt claim = verified.jkt /\ agentJkt[resAgent[r]] = k \* a.jkt = verified.jkt in the join /\ agentSt[resAgent[r]] = "active" /\ grantSt[resAgent[r]] = "active" /\ authSt[t] = "free" /\ resSt' = [resSt EXCEPT ![r] = "redeemed"] /\ authSt' = [authSt EXCEPT ![t] = "active"] /\ authAgent' = [authAgent EXCEPT ![t] = resAgent[r]] /\ authKey' = [authKey EXCEPT ![t] = k] /\ authRes' = [authRes EXCEPT ![t] = r] /\ UNCHANGED <> \* Person /token, grant-check failure AFTER the jti insert: the code \* consumes the jti first, then reads the grant; a revoked grant (or \* inactive agent) 403s but the resource token is already burned. \* Availability cost only -- no token is minted. BurnJti(r, k) == /\ resSt[r] = "issued" /\ <> \in creds /\ k = resKey[r] /\ ~( /\ agentJkt[resAgent[r]] = k /\ agentSt[resAgent[r]] = "active" /\ grantSt[resAgent[r]] = "active" ) /\ resSt' = [resSt EXCEPT ![r] = "redeemed"] /\ UNCHANGED <> \* Auth token TTL elapses (600 s in the implementation). ExpireAuth(t) == /\ authSt[t] = "active" /\ authSt' = [authSt EXCEPT ![t] = "expired"] /\ UNCHANGED <> (***************************************************************************) (* Resource rung 2, read phase: auth token verified (typ, aud, exp), *) (* cnf.jkt equals the presenting key's jkt, and the grant read *) (* grants g JOIN agents a WHERE g.person_id = ? AND g.agent_id = ? *) (* AND g.scope = ? AND g.revoked_at IS NULL AND a.status = 'active' *) (* sees a live row. The access-token INSERT is a separate statement *) (* with no grant re-check (CommitAccess below), so a revocation landing *) (* between read and insert yields an access-token row whose grant is *) (* already revoked. The design accepts this: authorization happens at *) (* USE time (UseAccess re-joins), never at mint time. *) (***************************************************************************) BeginAccess(t, k) == /\ authSt[t] = "active" /\ <> \in creds /\ k = authKey[t] \* cnf.jkt = verified.jkt /\ agentSt[authAgent[t]] = "active" /\ grantSt[authAgent[t]] = "active" /\ inflightAcc[t] = 0 /\ inflightAcc' = [inflightAcc EXCEPT ![t] = 1] /\ UNCHANGED <> \* Rung 2, write phase: the opaque access-token row is inserted with the \* agent/person/grant read earlier; the grant may have been revoked in \* between (see BeginAccess comment). CommitAccess(t, x) == /\ inflightAcc[t] = 1 /\ accSt[x] = "free" /\ accSt' = [accSt EXCEPT ![x] = "active"] /\ accAgent' = [accAgent EXCEPT ![x] = authAgent[t]] /\ inflightAcc' = [inflightAcc EXCEPT ![t] = 0] /\ UNCHANGED <> \* Access token TTL elapses (expires_at row check). ExpireAcc(x) == /\ accSt[x] = "active" /\ accSt' = [accSt EXCEPT ![x] = "expired"] /\ UNCHANGED <> (***************************************************************************) (* Resource rung 3: a request bears the opaque access token. The row is *) (* re-joined to grants and agents at decision time: *) (* access_tokens t JOIN grants g ON g.id = t.grant_id *) (* JOIN agents a ON a.id = t.agent_id *) (* WHERE t.token_hash = ? AND t.expires_at > now *) (* AND g.revoked_at IS NULL AND a.status = 'active' *) (* The decision and the grant state observed at decision time are logged. *) (***************************************************************************) UseAccess(x) == /\ accSt[x] # "free" /\ LET g == grantSt[accAgent[x]] ok == /\ accSt[x] = "active" /\ g = "active" /\ agentSt[accAgent[x]] = "active" IN useLog' = useLog \cup {[ok |-> ok, gst |-> g]} /\ UNCHANGED <> Next == \/ \E a \in Agents, b \in BootTokens : Spawn(a, b) \/ \E b \in BootTokens : StealBoot(b) \/ \E b \in BootTokens : ExpireBoot(b) \/ \E b \in BootTokens, k \in Keys : Redeem(b, k) \/ \E a \in Agents : RevokeGrant(a) \/ \E r \in ResTokens, a \in Agents, k \in Keys : IssueResource(r, a, k) \/ \E r \in ResTokens : ExpireRes(r) \/ \E r \in ResTokens, k \in Keys, t \in AuthTokens : MintAuth(r, k, t) \/ \E r \in ResTokens, k \in Keys : BurnJti(r, k) \/ \E t \in AuthTokens : ExpireAuth(t) \/ \E t \in AuthTokens, k \in Keys : BeginAccess(t, k) \/ \E t \in AuthTokens, x \in AccTokens : CommitAccess(t, x) \/ \E x \in AccTokens : ExpireAcc(x) \/ \E x \in AccTokens : UseAccess(x) Spec == Init /\ [][Next]_vars -------------------------------------------------------------------------------- (* Invariants *) \* (1) A bootstrap token binds at most one key ever: the atomic conditional \* UPDATE admits exactly one winner, so at most one agent-token issuance \* per bootstrap. Owner and thief can race; they cannot both win. SingleUseBootstrap == \A b \in BootTokens : \A k1, k2 \in Keys : (<> \in redemptions /\ <> \in redemptions) => k1 = k2 \* (2) Every minted auth token's cnf.jkt equals the jkt bound to its agent \* at redeem time. agentJkt is written exactly once (there is one \* bootstrap per agent and Redeem is its only writer), so the current \* binding IS the redeem-time binding. KeyBinding == \A t \in AuthTokens : authSt[t] # "free" => authKey[t] = agentJkt[authAgent[t]] \* (3) Every auth/access token that exists traces to a grant created by the \* root person for that agent and scope (grant rows are created only by \* Spawn and never deleted; "none" means no grant was ever created). AuthTracesToGrant == /\ \A t \in AuthTokens : authSt[t] # "free" => grantSt[authAgent[t]] # "none" /\ \A x \in AccTokens : accSt[x] # "free" => grantSt[accAgent[x]] # "none" \* (4) The load-bearing one: every use-log entry marked ok observed grant \* state = active at decision time. This forces the per-request join \* to grants; a design that trusted access-token expiry instead (serve \* iff accSt = "active") would violate it via RevokeGrant ; UseAccess. RevokedGrantNeverServes == \A e \in useLog : e.ok => e.gst = "active" \* (5) A resource token (jti) mints at most one auth token: the jti table \* insert-or-nothing admits exactly one redemption per jti. SingleRedemptionPerResourceToken == \A t1, t2 \in AuthTokens : (t1 # t2 /\ authSt[t1] # "free" /\ authSt[t2] # "free") => authRes[t1] # authRes[t2] ================================================================================