On the Relative Security of Prompt Injection: Mechanised Definitions, Defences and Verdicts for LLM Agents

Summary

This paper proposes relative security for LLM agents that read untrusted content: an agent counts as secure if every leak it has is also a leak of a reference agent that never obeys injected instructions. The authors present PlanTERS, a framework built on a small agent language with runtime monitors and attacker models, and prove in Isabelle/HOL that revoking injectable tools after the first untrusted read makes every plan relatively secure at the event level on finite runs, extending to possibly infinite runs under a fairness condition.

Mitigation

The source describes a fence theorem: revoking injectable tools at the first untrusted read, and never granting them back, makes every plan relatively secure at the event level on finite runs, for model behaviours where each injection is a single call and the model obeys on a schedule fixed in advance; with a fairness condition, this extends to possibly infinite runs.

Topics

• Prompt injection and jailbreaks

Related items

• LowHelp defend against memory poisoning in Amazon Bedrock AgentCore with multi-layer write validationSimilar attack · AWS Security Blog
• InfoCan the Confidence and Decisions of System 1 Models Be Trusted? An Explainability and Perturbation Audit of Jev-Style Decision ModelsSimilar attack · Arxiv (cs.CR + cs.CL + cs.LG)
• InfoHarness Matters: Measuring and Dissecting Security Resilience in Web AgentsSimilar attack · Arxiv (cs.CR + cs.CL + cs.LG)
• MediumTop MCP security resources — November 2026Similar attack · Adversa AI Blog
• InfoScaling Adaptive Prompt Injection Attacks with Agent SwarmsSimilar attack · Arxiv (cs.CR + cs.CL + cs.LG)