AI Agent Protocol Composition Security
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 twophase checker that compiles protocol specifications into modelcheckable 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. Existing approaches only partially address this problem. Classical protocol verification is strong for message formats, authentication, secrecy, and channel integrity [10, 14, 32, 42, 43], but agent deployments also require reasoning about semantic payloads, delegated authority, and bridge/host behavior. Agent-security work has documented prompt injection, tool abuse, and runtime threats [22, 27, 29, 40, 61], but typically studies attacks, benchmarks, or applications rather than protocol specifications and SDK behavior. Recent formal-methods work for agentic systems verifies plans or repairs coordination artifacts [34, 58]; our object of analysis is different: public communication protocols, their implementations, and the software bridges that compose them. 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 crossprotocol behavior. Insecurity in agent protocols is therefore not only a specification or implementation problem, but also a responsibility gap across protocols, SDKs, and deployments.