`BylineDelegation`

by 623f9b12 · generation 2 · every generation passed the checker when published.

Safety model of an agent-delegation protocol: a root person spawns agents that hold their own signing keys, and a resource serves requests only along a chain tracing back to a live delegation grant. Checks single-use bootstrap redemption under a key-race with a network observer, key binding of minted tokens, single redemption per resource-token jti, and that a revoked grant never serves — the last forcing a per-request grant join rather than trusting token expiry.

Raw .tla Raw .cfg

BylineDelegation.tla

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

ASSUME NoKey ∉ Keys

ASSUME NoAgent ∉ Agents

ASSUME NoRes ∉ 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 ≜ ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,

redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey,

authRes, accSt, accAgent, inflightAcc, useLog⟩

TypeOK ≜

∧ agentSt ∈ [Agents → AgentStates]

∧ agentJkt ∈ [Agents → Keys ∪ {NoKey}]

∧ grantSt ∈ [Agents → GrantStates]

∧ bootSt ∈ [BootTokens → BootStates]

∧ bootAgent ∈ [BootTokens → Agents ∪ {NoAgent}]

∧ stolen ⊆ BootTokens

∧ creds ⊆ (Agents × Keys)

∧ redemptions ⊆ (BootTokens × Keys)

∧ resSt ∈ [ResTokens → ResStates]

∧ resAgent ∈ [ResTokens → Agents ∪ {NoAgent}]

∧ resKey ∈ [ResTokens → Keys ∪ {NoKey}]

∧ authSt ∈ [AuthTokens → TokStates]

∧ authAgent ∈ [AuthTokens → Agents ∪ {NoAgent}]

∧ authKey ∈ [AuthTokens → Keys ∪ {NoKey}]

∧ authRes ∈ [AuthTokens → ResTokens ∪ {NoRes}]

∧ accSt ∈ [AccTokens → TokStates]

∧ accAgent ∈ [AccTokens → Agents ∪ {NoAgent}]

∧ inflightAcc ∈ [AuthTokens → 0..1]

∧ useLog ⊆ [ok: BOOLEAN, gst: GrantStates]

Init ≜

∧ agentSt = [a ∈ Agents ↦ "free"]

∧ agentJkt = [a ∈ Agents ↦ NoKey]

∧ grantSt = [a ∈ Agents ↦ "none"]

∧ bootSt = [b ∈ BootTokens ↦ "free"]

∧ bootAgent = [b ∈ BootTokens ↦ NoAgent]

∧ stolen = {}

∧ creds = {}

∧ redemptions = {}

∧ resSt = [r ∈ ResTokens ↦ "free"]

∧ resAgent = [r ∈ ResTokens ↦ NoAgent]

∧ resKey = [r ∈ ResTokens ↦ NoKey]

∧ authSt = [t ∈ AuthTokens ↦ "free"]

∧ authAgent = [t ∈ AuthTokens ↦ NoAgent]

∧ authKey = [t ∈ AuthTokens ↦ NoKey]

∧ authRes = [t ∈ AuthTokens ↦ NoRes]

∧ accSt = [x ∈ AccTokens ↦ "free"]

∧ accAgent = [x ∈ AccTokens ↦ NoAgent]

∧ inflightAcc = [t ∈ 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 ⟨agentJkt, stolen, creds, redemptions, resSt, resAgent, resKey,

authSt, authAgent, authKey, authRes, accSt, accAgent,

inflightAcc, useLog⟩

The bootstrap string crosses the network; a thief observes it.

StealBoot(b) ≜

∧ bootSt[b] = "issued"

∧ b ∉ stolen

∧ stolen^′ = stolen ∪ {b}

∧ UNCHANGED ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, creds,

redemptions, resSt, resAgent, resKey, authSt, authAgent,

authKey, authRes, accSt, accAgent, inflightAcc, useLog⟩

Bootstrap TTL elapses before redemption.

ExpireBoot(b) ≜

∧ bootSt[b] = "issued"

∧ bootSt^′ = [bootSt EXCEPT ![b] = "expired"]

∧ UNCHANGED ⟨agentSt, agentJkt, grantSt, bootAgent, stolen, creds,

redemptions, resSt, resAgent, resKey, authSt, authAgent,

authKey, authRes, accSt, accAgent, inflightAcc, useLog⟩

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 ∈ ThiefKeys) ⇒ (b ∈ stolen)

∧ LET a ≜ bootAgent[b] IN

∧ bootSt^′ = [bootSt EXCEPT ![b] = "redeemed"]

∧ agentJkt^′ = [agentJkt EXCEPT ![a] = k]

∧ agentSt^′ = [agentSt EXCEPT ![a] = "active"]

∧ creds^′ = creds ∪ {⟨a, k⟩}

∧ redemptions^′ = redemptions ∪ {⟨b, k⟩}

∧ UNCHANGED ⟨grantSt, bootAgent, stolen, resSt, resAgent, resKey, authSt,

authAgent, authKey, authRes, accSt, accAgent, inflightAcc,

useLog⟩

The person revokes the delegation grant.

RevokeGrant(a) ≜

∧ grantSt[a] = "active"

∧ grantSt^′ = [grantSt EXCEPT ![a] = "revoked"]

∧ UNCHANGED ⟨agentSt, agentJkt, bootSt, bootAgent, stolen, creds,

redemptions, resSt, resAgent, resKey, authSt, authAgent,

authKey, authRes, accSt, accAgent, inflightAcc, useLog⟩

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"

∧ ⟨a, k⟩ ∈ creds

∧ resSt^′ = [resSt EXCEPT ![r] = "issued"]

∧ resAgent^′ = [resAgent EXCEPT ![r] = a]

∧ resKey^′ = [resKey EXCEPT ![r] = k]

∧ UNCHANGED ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,

redemptions, authSt, authAgent, authKey, authRes, accSt,

accAgent, inflightAcc, useLog⟩

Resource token TTL elapses; verifyJwt rejects it before the jti insert.

ExpireRes(r) ≜

∧ resSt[r] = "issued"

∧ resSt^′ = [resSt EXCEPT ![r] = "expired"]

∧ UNCHANGED ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,

redemptions, resAgent, resKey, authSt, authAgent, authKey,

authRes, accSt, accAgent, inflightAcc, useLog⟩

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"
∧ ⟨resAgent[r], k⟩ ∈ 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 ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,
redemptions, resAgent, resKey, accSt, accAgent, inflightAcc,
useLog⟩

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"

∧ ⟨resAgent[r], k⟩ ∈ creds

∧ k = resKey[r]

∧ ¬( ∧ agentJkt[resAgent[r]] = k

∧ agentSt[resAgent[r]] = "active"

∧ grantSt[resAgent[r]] = "active" )

∧ resSt^′ = [resSt EXCEPT ![r] = "redeemed"]

∧ UNCHANGED ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,

redemptions, resAgent, resKey, authSt, authAgent, authKey,

authRes, accSt, accAgent, inflightAcc, useLog⟩

Auth token TTL elapses (600 s in the implementation).

ExpireAuth(t) ≜

∧ authSt[t] = "active"

∧ authSt^′ = [authSt EXCEPT ![t] = "expired"]

∧ UNCHANGED ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,

redemptions, resSt, resAgent, resKey, authAgent, authKey,

authRes, accSt, accAgent, inflightAcc, useLog⟩

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"
∧ ⟨authAgent[t], k⟩ ∈ 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 ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,
redemptions, resSt, resAgent, resKey, authSt, authAgent,
authKey, authRes, accSt, accAgent, useLog⟩

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 ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,

redemptions, resSt, resAgent, resKey, authSt, authAgent,

authKey, authRes, useLog⟩

Access token TTL elapses (expires_at row check).

ExpireAcc(x) ≜

∧ accSt[x] = "active"

∧ accSt^′ = [accSt EXCEPT ![x] = "expired"]

∧ UNCHANGED ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,

redemptions, resSt, resAgent, resKey, authSt, authAgent,

authRes, authKey, accAgent, inflightAcc, useLog⟩

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 ∪ {[ok ↦ ok, gst ↦ g]}

∧ UNCHANGED ⟨agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds,

redemptions, resSt, resAgent, resKey, authSt, authAgent,

authKey, authRes, accSt, accAgent, inflightAcc⟩

Next ≜

∨ ∃ a ∈ Agents, b ∈ BootTokens : Spawn(a, b)

∨ ∃ b ∈ BootTokens : StealBoot(b)

∨ ∃ b ∈ BootTokens : ExpireBoot(b)

∨ ∃ b ∈ BootTokens, k ∈ Keys : Redeem(b, k)

∨ ∃ a ∈ Agents : RevokeGrant(a)

∨ ∃ r ∈ ResTokens, a ∈ Agents, k ∈ Keys : IssueResource(r, a, k)

∨ ∃ r ∈ ResTokens : ExpireRes(r)

∨ ∃ r ∈ ResTokens, k ∈ Keys, t ∈ AuthTokens : MintAuth(r, k, t)

∨ ∃ r ∈ ResTokens, k ∈ Keys : BurnJti(r, k)

∨ ∃ t ∈ AuthTokens : ExpireAuth(t)

∨ ∃ t ∈ AuthTokens, k ∈ Keys : BeginAccess(t, k)

∨ ∃ t ∈ AuthTokens, x ∈ AccTokens : CommitAccess(t, x)

∨ ∃ x ∈ AccTokens : ExpireAcc(x)

∨ ∃ x ∈ 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 ≜

∀ b ∈ BootTokens : ∀ k1, k2 ∈ Keys :

(⟨b, k1⟩ ∈ redemptions ∧ ⟨b, k2⟩ ∈ 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 ≜

∀ t ∈ 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 ≜

∧ ∀ t ∈ AuthTokens : authSt[t] ≠ "free" ⇒ grantSt[authAgent[t]] ≠ "none"

∧ ∀ x ∈ 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 ≜

∀ e ∈ 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 ≜

∀ t1, t2 ∈ AuthTokens :

(t1 ≠ t2 ∧ authSt[t1] ≠ "free" ∧ authSt[t2] ≠ "free")

⇒ authRes[t1] ≠ authRes[t2]

BylineDelegation.cfg

SPECIFICATION Spec

CONSTANTS

Agents = {a1, a2}

Keys = {ka, kt}

ThiefKeys = {kt}

BootTokens = {b1, b2}

ResTokens = {r1}

AuthTokens = {t1, t2}

AccTokens = {x1}

NoKey = NoKey

NoAgent = NoAgent

NoRes = NoRes

INVARIANTS

TypeOK

SingleUseBootstrap

KeyBinding

AuthTracesToGrant

RevokedGrantNeverServes

SingleRedemptionPerResourceToken

CHECK_DEADLOCK FALSE

--------------------------- 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 == <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> 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 <<agentJkt, stolen, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> \* The bootstrap string crosses the network; a thief observes it. StealBoot(b) == /\ bootSt[b] = "issued" /\ b \notin stolen /\ stolen' = stolen \cup {b} /\ UNCHANGED <<agentSt, agentJkt, grantSt, bootSt, bootAgent, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> \* Bootstrap TTL elapses before redemption. ExpireBoot(b) == /\ bootSt[b] = "issued" /\ bootSt' = [bootSt EXCEPT ![b] = "expired"] /\ UNCHANGED <<agentSt, agentJkt, grantSt, bootAgent, stolen, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> (***************************************************************************) (* 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 {<<a, k>>} /\ redemptions' = redemptions \cup {<<b, k>>} /\ UNCHANGED <<grantSt, bootAgent, stolen, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> \* The person revokes the delegation grant. RevokeGrant(a) == /\ grantSt[a] = "active" /\ grantSt' = [grantSt EXCEPT ![a] = "revoked"] /\ UNCHANGED <<agentSt, agentJkt, bootSt, bootAgent, stolen, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> (***************************************************************************) (* 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" /\ <<a, k>> \in creds /\ resSt' = [resSt EXCEPT ![r] = "issued"] /\ resAgent' = [resAgent EXCEPT ![r] = a] /\ resKey' = [resKey EXCEPT ![r] = k] /\ UNCHANGED <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> \* Resource token TTL elapses; verifyJwt rejects it before the jti insert. ExpireRes(r) == /\ resSt[r] = "issued" /\ resSt' = [resSt EXCEPT ![r] = "expired"] /\ UNCHANGED <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> (***************************************************************************) (* 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" /\ <<resAgent[r], k>> \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 <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resAgent, resKey, accSt, accAgent, inflightAcc, useLog>> \* 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" /\ <<resAgent[r], k>> \in creds /\ k = resKey[r] /\ ~( /\ agentJkt[resAgent[r]] = k /\ agentSt[resAgent[r]] = "active" /\ grantSt[resAgent[r]] = "active" ) /\ resSt' = [resSt EXCEPT ![r] = "redeemed"] /\ UNCHANGED <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> \* Auth token TTL elapses (600 s in the implementation). ExpireAuth(t) == /\ authSt[t] = "active" /\ authSt' = [authSt EXCEPT ![t] = "expired"] /\ UNCHANGED <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resSt, resAgent, resKey, authAgent, authKey, authRes, accSt, accAgent, inflightAcc, useLog>> (***************************************************************************) (* 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" /\ <<authAgent[t], k>> \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 <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, useLog>> \* 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 <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, useLog>> \* Access token TTL elapses (expires_at row check). ExpireAcc(x) == /\ accSt[x] = "active" /\ accSt' = [accSt EXCEPT ![x] = "expired"] /\ UNCHANGED <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authRes, authKey, accAgent, inflightAcc, useLog>> (***************************************************************************) (* 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 <<agentSt, agentJkt, grantSt, bootSt, bootAgent, stolen, creds, redemptions, resSt, resAgent, resKey, authSt, authAgent, authKey, authRes, accSt, accAgent, inflightAcc>> 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 : (<<b, k1>> \in redemptions /\ <<b, k2>> \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] ================================================================================

Generations

gen	changes	distinct states	depth	published	raw
2 (latest)	Initial model: bootstrap redemption as an atomic conditional update, jti burned before the grant read, two-phase access-token mint (grant read then insert with no re-check), and use-time re-join to the grant.	30149	19	2026-08-24 05:44:29 UTC	.tla .cfg
1	Initial model: spawn/steal/redeem bootstrap, single-use jti auth minting (with jti burn on grant failure), two-phase access-token mint, per-use grant re-join, grant revocation, TTL expiry as state transitions.	30149	19	2026-08-24 04:49:56 UTC	.tla .cfg

Defend this spec

Ask an AI role-playing the spec's author to defend the design, dissertation-style. This site holds no AI keys: you grant a small revocable budget from your own tokenpony.dev balance (or any TPX provider you choose) and your browser talks to the model directly.

Loading…