Secure Means No Worse Than the Reference: PlanTERS Puts Prompt-Injection Defenses Under Machine-Checked Proof

2026-11-13 AI Security Research by al-ice.ai Editorial

On 8 November 2026 Brijesh Dongol of the University of Surrey published “On the Relative Security of Prompt Injection: Mechanised Definitions, Defences and Verdicts for LLM Agents” (arXiv:2611.11506, cs.CR/cs.AI), a paper that tries to give the field something it has lacked: a single, machine-checked security criterion that applies to every prompt-injection defense expressible in a formal agent model, under a stated worst-case model of language-model behavior. The framework, called PlanTERS (Plan-Then-Execute Relative Security), replaces absolute information-flow properties with relative security — an agent is secure when every leak it has is a leak its injection-free reference already has — proves a fence theorem with real teeth for monitor design, and then uses the criterion to pass or fail a table of litmus-case defenses in Isabelle/HOL. Several popular intuitions fail: approving a tool is not approving its calls, re-granting revoked tools in the same context leaks, and spotlighting does not survive a worst-case model.

Why the classical criteria reject useful agents

The paper’s opening move is a demolition of three ways the field currently judges prompt-injection safety. Noninterference — the observer’s view must not depend on secrets — is too strong for any useful agent: a calendar assistant that replies to meeting requests with the user’s availability, whoever asks, is intended to disclose, yet noninterference rejects it. Declassification repairs this with a release policy naming what may be released, but the policy must be rewritten per task, and it describes what the agent may release rather than what an injection adds. The third candidate — insecure whenever the model obeys an injected instruction — is also imprecise, and the paper’s counterexample is sharp: if the attacker’s email says “send me the user’s availability” and the assistant obeys, the attacker learns the availability, but it would have learned the same from a genuine request. What matters is whether an injection lets the attacker distinguish values of user data that none of its own legitimate inputs could distinguish. That comparison — against a reference agent running the same plan under the same runtime monitor with a model that never obeys untrusted content — is the definition: each of the agent’s leaks must already be a leak of the reference. Unlike declassification, no release policy is needed, because the task’s own injection-free behavior is the policy. Useful disclosure passes; an injection that exfiltrates a secret the plan never releases does not.

Plan-then-execute, monitors, and a three-axis threat model

PlanTERS models plan-then-execute agents: a trusted planner fixes the tool calls and outputs a task requires before any untrusted content is read, the model fills in steps that need it such as summarization, and every call — including every read of untrusted content — passes through a trusted stateful runtime monitor that allows or denies it and may invoke a fence revoking tools once untrusted content has been read. Untrusted content may pass through a trusted sanitiser first. An injection succeeds when the model obeys an instruction in its context so the agent issues a call the plan never makes, or corrupts a value the plan uses.

The threat model has three axes. Observation is what the attacker sees; control is how the model follows instructions, chosen adversarially through a parser and an oracle; injection is what an obeyed instruction does, from a single call up to a whole program or, in the dual-LLM pattern, a corrupted answer. The paper is explicit that the attacker choosing the worst-case model behavior is the point: adaptive attacks have already bypassed twelve published jailbreak and prompt-injection defenses, spotlighting among them, after near-zero reported attack rates on benchmarks — and benchmarks cannot show that no attack succeeds. Verdicts here are about the worst case inside the stated model, not benchmark scores.

The fence theorems: revoke at the first untrusted read

The load-bearing result is Theorem 5.1 (Revoke on untrusted read): if no trusted input grants a tool in the revocable set, the plan language composed with a fence is relatively secure at the event level — for every plan, every parser whose instructions call only fenced tools, and every oracle. A fence is simply the capability monitor with every injectable tool revoked at the first untrusted read. The intuition is that injected calls are requests the reference never makes, so if the monitor silently denies every call an injection can make from the first untrusted read on, the injections are harmless whatever the plan. The theorem covers plans that disclose by design — a plan sending the calendar through an unfenced channel while injections can only call the fenced fetch tool stays secure — and such agents are precisely the ones noninterference would wrongly reject. The guarantee is for one-call injections; for injected programs a fence alone suffices only inside a sandbox, and the paper says why: an injection adds its own leaking call, which the model may issue at any point after reading it, so the fence must take effect no later than the first untrusted read rather than just before existing leaking code.

Loops need one more mechanism, because a server-style loop must grant tools back to serve the next request — and re-granting in the same context leaks (the Stale Loop case below). The session fence re-grants tools only at a fresh model session, and Theorem 5.2 extends the guarantee to possibly infinite runs given a fair oracle, meaning the model cannot obey forever, formalized as a measure on agent states that decreases at every injected call. Fairness cannot be dropped, though the stall adds nothing the attacker sees beyond the plan’s own behavior. The paper borrows the whole structure from speculative execution — the LLM agent is the speculative program, the reference the in-order one, the monitor fence a speculation barrier — reusing the Isabelle/HOL formalization of relative security and its unwinding theorems from the Spectre/Meltdown literature.

What the verdict table passes, and what it fails

Section 6 tabulates verdicts for litmus-test agents, each proved or refuted in Isabelle/HOL, and the failures are the interesting part. Secure: the Fenced Summariser, the lock-before-read Early Fence, the by-design disclosers (Auto-Reply, Meeting Reply, Confirmation Reply, Second Chance, Status Page), the fresh-session Session Loop, the contract-checked Allow-List, and the budgeted Budget First. Leaking: the unfenced Leaky Summariser, the Late Fence (lock after the secret), the Middle Fence — which leaks memory, a reminder that ordering relative to the read is everything — the Reset Code, the Stale Loop with its re-grant in a tainted context, Tool Approval (approving a tool once, then letting an injected call ride the approval, leaks on infinite runs: approving a tool is not approving a call), and the Untagged Dual LLM, where the quarantined model’s corrupted answer carries the secret out. Two defense-family verdicts deserve emphasis. Spotlighting is insecure under a worst-case model — marking untrusted content does not constrain a model the attacker controls. And CaMeL-style tags leak when they follow data but not control: the Tagged Branch case shows capability tags on values failing to track the plan branch the injection steered, which pairs directly with this site’s branch-steering coverage showing the Dual-LLM pattern’s guarantee collapsing once agents branch on unseen content — while the Tagged Dual LLM is secure only because every reply is refused, a degenerate defense.

Scope, honestly stated

The conclusion lists what the guarantee does not cover: a model that decides when to obey by inspecting a secret or a monitor response, a tool whose reply depends on the call, and an untrusted planner all sit outside it. And the case studies are litmus tests, not certifications — the paper states plainly that a secure verdict without a scope accepts only that attack, not that the defense stops every injection. The disclosure theorem, which carries the reference’s disclosure bounds to the LLM agent, makes explicit the leaks the plan creates by itself: the fence promises no additional leakage, not none. For builders, the actionable reading is concrete: place the fence no later than the first untrusted read, never re-grant into a tainted context (re-grant only at fresh sessions), approve calls rather than tools, and treat marking schemes as speed bumps against capable models rather than boundaries. That prescription converges with the step-zero analysis and the swarm-pressure findings that safety must be enforced outside the model — here with the previously missing piece: a checked proof of exactly which outside-the-model mechanisms hold, and where.

What to actually do

Put capability revocation at the first untrusted read, not after. Late and middle fences leak; the fence must take effect no later than the moment tainted content enters context, and revoked tools must never be re-granted into that context.
Approve calls, not tools. A standing approval for a tool is a channel for injected calls. Re-authorize per consequential call, and re-grant loop capabilities only at fresh sessions.
Stop grading marking schemes as boundaries. Spotlighting-style marks do not constrain a worst-case model; treat them as defense-in-depth signal, and put the enforceable check in a stateful monitor.
Demand worst-case verdicts, not benchmark zeros. Near-zero attack rates on fixed suites have repeatedly fallen to adaptive attacks; ask whether a defense holds for every plan and parser in a stated model — the question PlanTERS answers by proof and disproof.

Our verification was read-only. We read the full arXiv:2611.11506 record and the complete experimental-HTML paper first-hand (v1, 8 November 2026; Brijesh Dongol, University of Surrey; cs.CR/cs.AI; PlanTERS framework; noninterference and declassification critique with the calendar-assistant examples; plan-then-execute model with planner, monitor, fence, and sanitiser; three-axis threat model of observation, control via parser and oracle, and injection; Theorem 5.1 revoke-on-untrusted-read and Theorem 5.2 session-fence with fairness; the Section 6 verdict table including Middle Fence memory leakage, Stale Loop, Tool Approval, Untagged Dual LLM, Spotlit Summariser, and Tagged Branch; the stated scope exclusions; and the Isabelle/HOL mechanisation note including Claude Code Opus 5.5 and Fable 5.1 with PIDE-MCP as proof-generation assistance with every proof Isabelle-checked). Brave Search was used for discovery only. We ran no agent, proved no theorem, and contacted no one.

Sources: