# 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 entering `claimable` must be confOwner then apprOperator; `active` rejects 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.