Formal Security Analysis of Agent Protocol Composition

• URL: http://arxiv.org/abs/2606.28690v1
• Date: Sat, 27 Jun 2026 02:16:57 GMT
• Title: Formal Security Analysis of Agent Protocol Composition
• Abstract summary: Agent protocols define how agents use tools, delegate work, and coordinate across software systems.<n>We present AgentThread, a source-linked framework for security assurance analysis of agent protocols.
• Score: 11.199507689498736
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI agent protocols define how agents use tools, delegate work, and coordinate across software systems, but their security requirements remain incomplete and inconsistently enforced across deployments. We present AgentThread, a source-linked framework for security assurance analysis of agent protocols, from specification text to running SDKs. AgentThread contributes a layered security scope, protocol-derived checks formalized as TLA+ invariants, and a two-phase checker that compiles protocol specifications into model-checkable models and replays executable counterexamples against real SDKs through protocol adapters. For each finding, AgentThread records the source text behind the check and separates violated protocol requirements from missing recommendations, hardening gaps, and unassigned cross-protocol responsibilities. Across five emerging agent protocols, AgentThread identifies 35 specification-level findings, supports them with 80 implementation tests against production SDKs and reference servers, and finds 30 additional failures that emerge only under protocol composition. We further show that only one protocol enforces a security-relevant control in practice and no protocol assigns enforcement for cross-protocol behavior. Insecurity in agent protocols is therefore not only a specification or implementation problem, but also a responsibility gap across protocols, SDKs, and deployments.

Related papers

• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
  This study develops a technical taxonomy to classify and analyze large language models (LLMs) agent communication protocols.<n>The framework guides protocol selection and highlights open research gaps such as privacy and policy enforcement.
  arXiv  Detail & Related papers  (2026-06-17T14:45:20Z)
• LAP: An Agent-to-Instrument Protocol for Autonomous Science [6.00746946741668]
  Large language model agents now plan experiments, and self-driving laboratories execute them.<n>Every such system rebuilds the link between the reasoning agent and the physical instrument from scratch.<n>Recent agent-interoperability protocols clarify the agent-to-tool edge, and Google's Agent2Agent (A2A) the agent-to-agent edge.<n>We present the Lab Agent Protocol (LAP), a protocol that fills this gap.
  arXiv  Detail & Related papers  (2026-06-02T15:03:43Z)
• Agent Name Service (ANS): A Proof-of-Concept Trust Layer for Secure AI Agent Discovery, Identity, and Governance in Kubernetes [0.0]
  This paper presents an implementation-oriented proof of concept for the Agent Name Service (ANS)<n>ANS is a DNS-inspired trust layer for AI agent discovery and interoperability.<n>We observe sub-10ms response in demonstrated service paths and full success for scripted demo deployment scenarios.
  arXiv  Detail & Related papers  (2026-04-29T01:24:27Z)
• Autogenesis: A Self-Evolving Agent Protocol [60.15939127351914]
  We introduce Autogenesis Protocol (AGP), a self evolution protocol that decouples what evolves from how evolution occurs.<n>We present Autogenesis System (AGS), a self-evolving multi-agent system that dynamically instantiates, retrieves, and refines protocol-registered resources during execution.
  arXiv  Detail & Related papers  (2026-04-16T14:04:06Z)
• MPAC: A Multi-Principal Agent Coordination Protocol for Interoperable Multi-Agent Collaboration [2.643905034529239]
  MPAC is an application-layer protocol that fills this gap with explicit coordination semantics across five layers.<n> specification defines 21 message types, three state machines with normative transition tables, Lamport-clock causal watermarking, two execution models, three security profiles, and optimistic control on shared state.<n>A controlled three-agent code review benchmark shows a 95 percent reduction in coordination overhead and a 4.8 times wall-clock speedup.
  arXiv  Detail & Related papers  (2026-04-10T01:12:05Z)
• AgentRFC: Security Design Principles and Conformance Testing for Agent Protocols [2.1352949241716352]
  Agent protocols enable autonomous agents to discover capabilities, delegate tasks, and compose services across trust boundaries.<n>Despite massive deployment, no systematic security framework for these protocols exists.<n>We present three contributions: the Agent Protocol Stack, the Agent-Agnostic Security Model, and AgentConform.
  arXiv  Detail & Related papers  (2026-03-25T00:25:02Z)
• Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
  We study adaptive attacks by an untrusted model that knows the protocol and the monitor model.<n>We instantiate a simple adaptive attack vector by which the attacker embeds publicly known or zero-shot prompt injections in the model outputs.
  arXiv  Detail & Related papers  (2025-10-10T15:12:44Z)
• VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation [40.594947933580464]
  The deployment of autonomous AI agents in sensitive domains, such as healthcare, introduces critical risks to safety, security, and privacy.<n>We introduce VeriGuard, a novel framework that provides formal safety guarantees for LLM-based agents.
  arXiv  Detail & Related papers  (2025-10-03T04:11:43Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems.
  arXiv  Detail & Related papers  (2024-05-09T19:57:59Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.