Higher-Categorical Semantics of an Agentic Web-Site Protocol: Non-Exclusive Rights, Site Virtual Machines, and Doubly-Authorized Expiring Tokens
Author: Anonymous. *Agent assistance disclosed:* drafted with an AI agent under the direction of the (anonymous) responsible human author.
Status labels. Each result is tagged [Proved] (complete proof here or mechanized in the accompanying Lean file), [Sketch] (proof outline, details routine but unchecked), or [Conjecture]. No external results are cited beyond standard textbook facts (sheaves on a site, Lawvere theories, Grothendieck construction, IND-CPA/PRF definitions).
1. Setting
An *agentic site* $S$ exposes resources to software agents $a$ acting for human owners $o(a)$, governed by a site operator $\sigma$. We give three layers: (i) a sheaf of interaction rights, (ii) an algebraic theory whose models are the site virtual machine (VM) and whose shell scripts are interpretations, (iii) an authorization protocol presented as a 2-category whose security properties are invariants of its path space.
2. Non-exclusive interaction rights as sheaves
Let $\mathcal{R}$ be the poset of resource scopes (paths, endpoints, scope strings), ordered by inclusion, with the Grothendieck topology $J$ in which a family $\{U_i \subseteq U\}$ covers iff $\bigcup U_i = U$. Define the presheaf $$\mathrm{Perm}: \mathcal{R}^{op} \to \mathbf{Set},\qquad \mathrm{Perm}(U) = \{\,(p, g)\ :\ p \text{ a principal},\ g \text{ a grant valid on all of } U\,\}$$ with restriction $\mathrm{Perm}(U)\to\mathrm{Perm}(V)$ for $V\subseteq U$.
Proposition 2.1 [Sketch]. If grants are determined by their pointwise validity (a grant on $U$ is a compatible family of grants on points of $U$), then $\mathrm{Perm}$ is a $J$-sheaf: compatible local grants glue uniquely.
Non-exclusivity. A policy is *exclusive* on $U$ if the fibre $\mathrm{Perm}(U)\to \mathrm{Res}(U)$ over each resource is a subsingleton (at most one principal). Non-exclusive rights are those where this fails: the operator's right and the user's right coexist. Formally, the *rights object* for parties $P$ is the coproduct-of-holders presheaf $\coprod_{p\in P} \mathrm{Perm}_p$ mapped into resources by the codiagonal $\nabla$; exclusivity is the condition that $\nabla$ is a monomorphism. The terms of a typical agentic site ("operator retains non-exclusive use rights; user retains ownership") are exactly a non-mono $\nabla$ with the user's sub-presheaf $\mathrm{Perm}_{user}\hookrightarrow$ total rights retaining all ownership sections.
Proposition 2.2 [Proved]. Exclusivity is local: $\nabla$ is mono iff it is mono on every cover. (Monos of sheaves are detected stalkwise/locally; for the poset site this is elementary.)
Higher refinement. Replacing $\mathbf{Set}$ by $\infty$-groupoids, $\mathrm{Perm}$ becomes an $\infty$-sheaf whose higher cells are *delegation equivalences* (two grants identified by a revocable delegation chain). Then $\pi_0$ recovers the set-level policy and $\pi_1$ at a section records the automorphisms (re-delegations) of a grant. [Conjecture 2.3] For delegation graphs without cycles of revocation, $\mathrm{Perm}$ is 0-truncated, i.e. no higher information is lost by the set-level model.
3. Skills and the site as a virtual machine
Let $\mathbb{T}_S$ be the Lawvere theory (finite-product category) generated by the site's operations, e.g. search: Query -> List(Note), get: Slug -> Note, submit: Key x Draft -> Receipt, status: Receipt -> Status, with equations such as idempotence of reads ($\mathrm{get}\circ\Delta$ coherence) and status(submit(k,d)) = pending immediately after creation. Effects (network, failure, rate limiting) are handled by the monad $T = \mathrm{State}_{\mathrm{srv}} \circ \mathrm{Exc}_{\{400,401,403,404,409,429,503\}}$ on the client side.
- The site VM is a model $M: \mathbb{T}_S \to \mathbf{Kl}(T)$, product preserving.
- A skill is a morphism of theories $\phi: \mathbb{T}_{task}\to \mathbb{T}_S$ (an interpretation of a task language in site operations); composing gives a model $M\circ\phi$ of the task theory.
- A shell script is a concrete presentation of $\phi$: each command is a term of $\mathbb{T}_S$; pipes are composition in $\mathbf{Kl}(T)$.
Proposition 3.1 [Proved, standard]. Skills compose: theory morphisms compose, and precomposition preserves models. The category of skills is $\mathbf{Law}/\mathbb{T}_S$.
Installation as base change. An installer is a map $\iota$ from a client environment to one providing the skill's free variables (binaries, SITE_BASE, key file). Installation is pullback of the skill along $\iota$; idempotent installers correspond to $\iota$ factoring through a retraction. The accompanying skill/ directory gives a concrete installer and scripts; install.sh is idempotent [Proved by inspection: it overwrites fixed paths only].
4. The double-authorization protocol
4.1 States and transitions
Protocol states for one agent–owner pair (writing $t$ for wall time, $e$ for expiry): $$\mathsf{Idle}\xrightarrow{\ \mathrm{req}\ }\mathsf{Pending}_o\xrightarrow{\ \mathrm{conf}_o\ }\mathsf{Pending}_\sigma\xrightarrow{\ \mathrm{appr}_\sigma\ }\mathsf{Claimable}\xrightarrow{\ \mathrm{claim}\ }\mathsf{Active}(e)$$ with $\mathrm{renew}: \mathsf{Active}(e)\to\mathsf{Active}(e')$ permitted only when $t<e$, $\mathrm{tick}: \mathsf{Active}(e)\to\mathsf{Expired}$ when $t\ge e$, $\mathsf{Expired}\to\mathsf{Idle}$, and rejection/denial edges to $\mathsf{Idle}$. Request triggers an email to the owner with a confirmation URL; $\mathrm{appr}_\sigma$ triggers an email to the owner containing the one-time claim URL $u = \mathrm{base}/\mathrm{claim}/r$ with $r\leftarrow\{0,1\}^{256}$.
4.2 The 2-category $\mathbf{Auth}$
Let $\mathbf{Auth}$ be the 2-category whose objects are states, 1-cells are finite transition paths, and 2-cells are *approval witnesses*: a 2-cell $\alpha: \gamma\Rightarrow\gamma'$ exists between parallel paths when $\gamma'$ is obtained from $\gamma$ by commuting independent events (e.g. reordering an unrelated renewal of a different agent). Approvals $\mathrm{conf}_o,\mathrm{appr}_\sigma$ are generating 1-cells *labelled* by signatures from distinct principals; the labelling is a 2-functor $\lambda:\mathbf{Auth}\to \mathbf{B}(\mathcal{P}(\{o,\sigma\}),\cup)$ into the delooping of the join-semilattice of approvers (a one-object 2-category with only identity 2-cells).
Homotopy type of authorization. The classifying space $|N\,\mathbf{Auth}(\mathsf{Idle},\mathsf{Claimable})|$ of the hom-category records all ways of becoming claimable up to commuting. **Theorem 4.1 [Proved; Lean claim_requires_both]. Every 1-cell $\mathsf{Idle}\to\mathsf{Claimable}$ satisfies $\lambda(\gamma)=\{o,\sigma\}$. Hence the hom-category maps into the full subcategory over $\{o,\sigma\}$; the space of authorization paths is contractible onto its approval label**, i.e. $\lambda$ is constant on the path space. *Proof:* by induction on paths: the only edge into $\mathsf{Claimable}$ is $\mathrm{appr}_\sigma$, from $\mathsf{Pending}_\sigma$, whose only incoming edge is $\mathrm{conf}_o$, and every path to $\mathsf{Idle}$ resets the label. $\square$
Remark (order of approvals). Because the protocol fixes owner-first, the hom-groupoid is in fact discrete with one component; a symmetric variant (either order) would give a hom-groupoid whose two orders are connected by a 2-cell, a "square" filling $S^0\to D^1$ — the higher cell says the two orders are *equivalent* authorizations. [Proved for the finite model, trivial.]
4.3 Time: token lifetimes as a sheaf on $\mathbb{R}$
Let $\mathcal{O}(\mathbb{R}_{\ge0})$ be opens of time. The *validity sheaf* $\mathcal{V}(W)=\{k : k \text{ valid at every } t\in W\}$. A token with issuance $s$ and expiry $e$ is a section over $[s,e)$ (half-open intervals generate; we use the sheaf on the Alexandrov/interval site). Renewal extends a section: given $k\in\mathcal{V}([s,e))$ and $t<e$, renewal produces $k'\in\mathcal{V}([t,e'))$ with $k|_{[t,e)}=k'|_{[t,e)}$, so they glue to a section over $[s,e')$. Proposition 4.2 [Proved]. Gluing requires overlap: renewal at $t\ge e$ yields intervals $[s,e)$ and $[t,e')$ with empty intersection *and* a gap or point of non-validity $[e,t]$; no section over $[s,e')$ exists. Hence *a renewal chain is a connected section; expiry is a disconnection*, and $\pi_0$ of the support of $\mathcal V$ for an agent counts the number of full double-approval rounds needed.
In topos terms: work in $\mathbf{Sh}(\mathbb{R}_{\ge0})$; the proposition "the agent is authorized" is a truth value $\llbracket \mathrm{Auth}\rrbracket\in\Omega$, an open set of times. Expiry-forces-restart says: every connected component of $\llbracket\mathrm{Auth}\rrbracket$ begins with a claim event, which is preceded by both approvals (combine 4.1 and 4.2) [Proved for the discrete-time Lean model; Sketch for continuous time].
4.4 One-time-ness as linearity
Model the claim URL as a resource in a linear (symmetric monoidal closed, non-cartesian) category: $\mathrm{claim}: \mathsf{URL}\otimes \mathsf{Req}\to \mathsf{Key}$ with no diagonal $\mathsf{URL}\to\mathsf{URL}\otimes\mathsf{URL}$. Operationally the server maintains a set $U$ of live token hashes, and $\mathrm{claim}$ performs an atomic compare-and-delete. **Theorem 4.3 [Proved; Lean single_use].** In any execution, at most one claim on a given $r$ succeeds. The categorical statement—no derivation duplicates $\mathsf{URL}$—is the soundness of the linear typing w.r.t. the compare-and-delete semantics. Concurrency: atomicity is an *assumption* on the store (e.g. a transactional delete); without it the theorem is false.
Note: GET/HEAD on the URL must be side-effect-free (email scanners prefetch links); only POST consumes. This is the observation that a non-linear *read* $\mathsf{URL}\to\mathsf{URL}\otimes\mathsf{Info}$ is allowed iff it does not touch the key component.
4.5 Unguessability
Let $r\leftarrow\{0,1\}^{n}$ uniformly, $n=256$, stored only as $H(r)$. Theorem 4.4 [Proved, elementary]. An adversary making $q$ online guesses against $L$ live tokens succeeds with probability $\le qL/2^{n}$. If instead $r=F_K(\mathrm{ctr})$ for a PRF $F$, success is $\le qL/2^n+\mathrm{Adv}^{\mathrm{prf}}_F(\mathcal B)$ by a standard hybrid [Sketch]. Semantic security of the email channel is *not* provided by the protocol: anyone reading the owner's mailbox within the claim window can claim. We state this as an explicit trust assumption $\mathsf{A_{mail}}$.
4.6 Security theorems (summary)
Under assumptions: atomic store ($\mathsf{A_{atom}}$), monotone trusted clock ($\mathsf{A_{clk}}$), owner mailbox confidentiality ($\mathsf{A_{mail}}$), authenticity of the owner-confirmation and operator-approval endpoints ($\mathsf{A_{auth}}$):
1. No claim without both approvals. [Proved, Lean] 2. Single use. [Proved, Lean, given $\mathsf{A_{atom}}$] 3. Renewal only before expiry. [Proved, Lean] 4. Expiry forces restart: after expiry, reaching $\mathsf{Active}$ again requires a fresh $\mathrm{conf}_o$ and $\mathrm{appr}_\sigma$. [Proved, Lean] 5. Unguessability. $\le qL2^{-256}$ online. [Proved] 6. Composition across sessions (parallel agents as a tensor of protocol 2-categories, security preserved): [Conjecture; plausible via a UC-style argument, not attempted].
5. Higher-topos view
Put everything in $\mathcal{X}=\mathbf{Sh}_\infty(\mathcal{R}\times\mathcal{O}(\mathbb{R}_{\ge0}))$. Rights (Sec. 2), the validity sheaf (Sec. 4.3), and the VM model (Sec. 3, as an internal product-preserving functor) live in one $\infty$-topos. The protocol state machine is an internal $(\infty,2)$-category whose hom-$\infty$-groupoids are the authorization path spaces; Theorem 4.1 says the approval-label map from these to the discrete object $\mathcal{P}(\{o,\sigma\})$ is constant at the top element. [Conjecture 5.1] The descent (gluing) of authorization across resource covers holds: an agent authorized on each $U_i$ with compatible tokens is authorized on $\bigcup U_i$ — true if tokens are scope-sets, false if scopes are not closed under union, so a precise condition is needed.
6. Artifacts
lean/AuthProtocol.lean— discrete-time state machine and proofs of 4.6(1–4) (Lean 4 core, type-checks with Lean 4.35.0, no sorry). Caveat: the Lean statements are step-local (e.g. the two steps enteringclaimablemust be confOwner then apprOperator;activerejects further claims); lifting them to whole traces is the induction in Thm 4.1, not yet mechanized.skill/install.sh— idempotent installer for the site-VM skill.skill/bin/sitevm— dispatcher interpreting $\mathbb{T}_S$ operations as HTTP calls (search,get,submit,status,enroll,claim,renew-check).skill/SKILL.md— skill manifest.
7. Limitations
No mechanized treatment of the $\infty$-categorical statements; the continuous-time and PRF claims are sketches; the email channel is trusted; denial-of-service and phishing of approval URLs are out of scope.