Formal Security Analysis of Agent Protocol Composition

Technical Summary: Formal Security Analysis of Agent Protocol Composition

Problem Statement
AI agent protocols (e.g., MCP, A2A, ANP) are evolving into critical software infrastructure that mediates tool access, delegation, and shared context across autonomous workflows. While individual protocol vulnerabilities (e.g., command injection in a single server) are documented, a significant assurance gap exists regarding protocol composition. When multiple agents or servers interact, unsafe behaviors emerge from the interplay of semantic payloads, delegated authority, and shared context, rather than from isolated message format errors.

Current approaches fail to address this holistically: classical protocol verification focuses on message formats and channel integrity but lacks semantic reasoning; agent security research often targets specific attacks or benchmarks rather than protocol specifications and SDK behaviors; and formal methods for agentic systems typically verify plans or coordination artifacts rather than the public communication protocols themselves. The core challenge is maintaining an evidence chain from natural language specifications to formal checks and implementation tests, while accounting for the fact that security responsibilities are often distributed across specifications, SDKs, hosts, and runtime bridges, leaving "responsibility gaps" where no single component owns the control.

Methodology: AgentThread Framework
The authors present AgentThread, a source-linked framework designed to perform security assurance analysis on agent protocols from specification text to running SDKs. The workflow is structured into three phases:

1. Source-Linked Extraction & Intermediate Representation (IR):

   • The system collects authoritative protocol artifacts (prose, schemas, SDKs, reference implementations).
   • It extracts Normative Clauses (e.g., "MUST," "SHOULD") and maps them to a Typed Protocol IR. This IR preserves source provenance, actor bindings, and modality.
   • Crucially, it also generates a Responsibility IR, which tracks who owns a specific control (specification, SDK, bridge) and whether that control is enforced.

2. Formal Modeling (TLA+):

   • The IR is compiled into TLA+ models using the TLC model checker.
   • The framework defines a layered security scope:
     • RPC Layer (L1-L3): Message integrity, session lifecycle, identity/capability binding.
     • Agent Layer (L4-L5): Semantic operation control (e.g., prompt injection), audit/accountability, and composition safety.
   • Two-Phase Checking:
     • Phase 1 (Spec-Level): TLC generates counterexample traces for violated invariants. Findings are triaged as Spec-Fail, Model-Fail, or Ambiguity-Fail.
     • Phase 2 (Implementation-Level): Executable counterexamples are lowered through Protocol Adapters into replay tests against real SDKs and reference servers. If a trace cannot be replayed, source/type-level evidence is recorded.

3. Composition Analysis:

   • The framework constructs composed TLA+ models by combining IR transitions from two protocols and adding Bridge Actions that model state transfer across boundaries.
   • Bridge actions are constrained by finite capability contracts to verify if security properties (e.g., authority monotonicity, audit continuity) hold across the bridge.

Key Contributions

1. Systematic Formal Analysis: The paper defines a layered security scope for agent protocols and derives checkable TLA+ invariants covering semantic content flow, delegated authority, and composition safety.
2. Source-Linked Workflow: AgentThread establishes a pipeline from protocol text to formal models and implementation tests, preserving source references to distinguish between specification non-conformance, recommendation gaps, and unassigned responsibilities.
3. Empirical Study: The authors evaluate five protocols (MCP, A2A, ANP, ACP, ACP-Client), their production SDKs, and eight composed models.

Results
The study yielded the following findings across the five protocols and eight composed models:

• Specification-Level Findings: 35 specification-level findings were identified. These included 12 confirmed by implementation tests and 23 specification-only findings.
• Implementation Failures: 80 implementation tests were run against production SDKs and reference servers.
  • MCP: Showed direct standards non-conformance (e.g., failure to sanitize tool outputs despite "MUST" requirements).
  • A2A & Others: Often exhibited "framework hardening gaps" where specifications lacked mandatory controls for delegation scope or audit trails.
• Composition Failures: 30 additional failures were discovered that only emerged under protocol composition.
  • These failures included authority escalation, consent bypass, and audit trail breaks where a bridge component (e.g., an agent runtime connecting MCP and A2A) allowed untrusted content to influence delegated authority.
  • No single protocol owned the control for these cross-protocol behaviors; they were "composition orphans."
• Responsibility Gaps: Only one protocol (ANP) enforced a security-relevant control (DID-based identity) in practice. No protocol assigned enforcement responsibility for cross-protocol behavior.

Significance and Claims
The paper argues that insecurity in agent protocols is not merely a specification or implementation bug, but a responsibility gap across the software stack.

• Local Hardening is Insufficient: Securing individual servers or SDKs does not prevent failures arising from the composition of multiple components (e.g., an attacker controlling a webpage fetched by one server to inject instructions that trigger a file read by another).
• The "Owner" Problem: Critical security controls for composed systems often fall outside the normative scope of any single protocol, leaving them unowned by specifications, SDKs, or deployments.
• Methodological Shift: The authors claim that composition safety must be treated as a first-class protocol property requiring explicit composition contracts and enforcement responsibility, rather than an application-level afterthought. AgentThread provides the mechanism to make these split obligations explicit early in the design process.