Post 3: authority that changes during operation (agent-controls series)

[williamzujkowski]

Post 3 in the agent-controls series: authority that changes during operation

Where the series stands

• Part 1 — expressed agent
  guardrails as machine-checkable OSCAL, and proved the gate ran.
• Part 2 — proved the
  gate is correct for every input, with Dafny plus a Rego twin plus
  differential testing.

Both posts assume something they never state: the policy is fixed.
The gate evaluates a tool call against a static allowlist and returns
allow or deny. That is the right simplification for parts 1 and 2, and
it is also the thing that breaks next.

The gap this post fills

Six active IETF drafts on agent authorization were read against a
working control-plane implementation. Two defects recur in all six:

1. Authority is modeled as issued state, not current state. A token
   still valid by expiry and call-count stays valid even after the
   conditions that justified it have changed — the sandbox posture
   shifted, a reviewer blocked, runtime behavior diverged from the
   approved plan. Enforcement checks the signature, not the world.
2. Demotion does not exist. Every draft models grant and revoke.
   None models the middle. An agent that fails review is often still
   useful at a lower authority level, and no specification says how to
   put it there.

Public drafts, if the post wants to cite them (read the live body before
quoting any section number — these readings are second-hand and
unverified):

Draft	Rev
draft-liu-agent-operation-authorization	02
draft-chen-agent-decoupled-authorization-model	00
draft-ni-a2a-ai-agent-security-requirements	01
draft-song-oauth-ai-agent-collaborate-authz	02

Bodies at https://www.ietf.org/archive/id/<draft-name>-<rev>.txt.

The specific technical hook

draft-liu-...-02 carries a policy_id claim referencing an OPA policy
by identifier. Without a content-addressed digest, the audit evidence
can later point at a different policy body under the same ID.

OSCAL has the identical defect. An implemented-requirement points
at a control by identifier; nothing content-addresses the control text
or the policy body actually in force at assessment time. Two
communities, two layers, same referential weakness. That observation
bridges this series back to Part 1 and is probably the strongest single
paragraph available.

A second hook: scope narrowing is not mode narrowing

Delegation models prevent an agent from widening scope. None of them
constrain mode. "Modify one file" at enforce authority and "recommend
a patch" at suggest authority target the same resource and the same
operation family with completely different blast radius.

Candidate thesis

A proved gate is only as good as the policy it enforces, and the
policy is the part that has to change while the agent is running.
Both OSCAL assessment and the current agent-authorization drafts
assume point-in-time evaluation against an identifier — and that
assumption breaks for an actor whose trustworthiness changes during
operation.

Falsifiable, contested, and it earns its place by attacking the
previous two posts rather than restating them. Part 2 already did this
to Part 1 successfully; the series has a working pattern.

What would make it concrete

The obvious extension to
oscal-agent-controls:
an authority mode carried alongside the policy tuple, a demotion path
that is not full revocation, and a Dafny lemma along the lines of
"an agent cannot act above its current authority mode, and a demotion
takes effect before the next decision." That is the same trick as Part
2 applied to a moving target, and it keeps the series' promise that
everything shown actually runs.

Constraints (unchanged from #413)

Describe the approach generically. No internal control counts, no
control IDs from the internal overlay, no internal repo or project
names, no employer specifics. nexus-agents is public and may be named
and linked. Synthetic namespaces and fake tool names throughout, as in
Parts 1 and 2 — that convention worked and the NDA audit on both posts
came back completely clean.

Run the pre-publish gate before pushing.

[williamzujkowski]

Written and merged: The Policy Is the Part That Moves (#484), backed by oscal-agent-controls#1.

Implementation first, prose second — the code was proving before the post was drafted.

Both load-bearing claims verified against the live drafts rather than the issue's summary, which flagged its own readings as second-hand. The policy_id defect is real: the draft defines it as "a string that serves as an OPA policy reference and MUST match a registered policy in the AS", and every integrity mention in the document is a JWS signature over the token, never over the policy body it points at. Demotion genuinely does not exist: revoke/revocation occur 13 times across the four drafts, demote/downgrade/step-down zero times.

Two corrections to the issue as filed. It says six drafts were read but lists four, so the post claims four. And "every draft models grant and revoke" understates the finding — two of the four don't model revocation either, which makes the point stronger than written.

What now runs: verify/Authority.dfy (authority modes, digest-bound grants, demotion), an independent Rego twin, decide_bound()/demote()/policy_digest() in the Python monitor, and a 324-case differential test across three implementations that agree on every case. Six lemmas discharged, including DemotionCannotWiden and GrantBoundToPolicyBody. Gate: 26 Dafny obligations, 12 OPA tests, 13 pytest.

The best part of the post is a proof failure. DemotionTakesEffectImmediately didn't verify first time — the property was over-claimed and needed a digest-match precondition, because when the policy body has also rotated the call denies for a different reason. Every test I'd have written holds the policy constant and varies the mode, which is exactly where my wrong claim happens to be true. That leads the proof section instead of the five lemmas that passed.

Also caught two defects in my own draft before merge: I'd dated it a week in the future (the same impossible-date defect the archive audit spent weeks removing), and written "eleven times" for a count that came from grep -c — lines containing a match, not occurrences. Real figure 13. Both fixed.