AI agent protocols -- including MCP, A2A, ANP, and ACP -- enable autonomous agents to discover capabilities, delegate tasks, and compose services across trust boundaries. Despite massive deployment (MCP alone has 97M+ monthly SDK downloads), no systematic security framework for these protocols exists. We present three contributions. First, the Agent Protocol Stack, a 6-layer architectural model that defines what a complete agent protocol must specify at each layer -- analogous to ITU-T X.800 for the OSI stack. Second, the Agent-Agnostic Security Model, 11 security principles formalized as TLA+ invariants, each tagged with a property taxonomy (spec-mandated, spec-recommended, aasm-hardening, aps-completeness) that distinguishes protocol non-conformance from framework-imposed security requirements. Third, AgentConform, a two-phase conformance checker that (i)extracts normative clauses from protocol specifications into a typed Protocol~IR with explicit Protocol/Environment/Adversary action separation, (ii)compiles the IR into TLA+ models and model-checks them against AASM invariants, then (iii)replays counterexample traces against live SDK implementations to confirm findings. We introduce the Composition Safety (CS) principle: security properties that hold for individual protocols can break when protocols are composed through shared infrastructure. We demonstrate this with formal models of five protocol composition patterns, revealing cross-protocol design gaps that individual protocol analysis cannot detect. Preliminary application to representative agent protocols reveals recurrent gaps in credential lifecycle, consent enforcement, audit completeness, and composition safety. Some findings are under coordinated disclosure; full evaluation details will be released in the complete version.

翻译：AI智能体协议——包括MCP、A2A、ANP和ACP——使得自主智能体能够跨信任边界发现能力、委派任务并组合服务。尽管这些协议已被大规模部署（仅MCP的月SDK下载量就超过9700万次），但目前尚不存在针对这些协议的系统性安全框架。我们提出三项贡献。首先，智能体协议栈（Agent Protocol Stack），这是一个六层架构模型，定义了完整的智能体协议必须在各层规范的内容——类似于OSI协议栈的ITU-T X.800标准。其次，智能体无关安全模型（Agent-Agnostic Security Model），包含11条形式化为TLA+不变式的安全原则，每条原则均附有属性分类标签（协议规范强制、协议规范推荐、AASM加固、APS完备性），以区分协议不符合规范与框架强加的安全需求。第三，AgentConform，一个两阶段一致性检查器，它(i)从协议规范中提取规范性条款，形成带有显式协议/环境/攻击者行为区分的类型化协议中间表示（Protocol IR），(ii)将中间表示编译为TLA+模型并针对AASM不变式进行模型检验，然后(iii)在实时SDK实现上回放反例轨迹以确认发现。我们引入了组合安全性（CS）原则：当协议通过共享基础设施组合时，针对单个协议成立的安全属性可能被破坏。我们通过对五种协议组合模式的形式化模型展示了这一点，揭示了单个协议分析无法检测到的跨协议设计缺陷。对代表性智能体协议的初步应用揭示了凭证生命周期、同意执行、审计完备性和组合安全性方面的反复出现的缺陷。部分发现正在进行协调披露；完整评估细节将在完整版本中发布。