論文の概要: Formal Security Analysis of Agent Protocol Composition
- arxiv url: http://arxiv.org/abs/2606.28690v1
- Date: Sat, 27 Jun 2026 02:16:57 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-30 18:07:15.645353
- Title: Formal Security Analysis of Agent Protocol Composition
- Title(参考訳): エージェントプロトコル構成の形式的セキュリティ解析
- Authors: Shenghan Zheng, Qifan Zhang, Zheng Zhang, Haonan Li, Christophe Hauser,
- Abstract要約: エージェントプロトコルは、エージェントがツールの使用方法を定義し、作業を委譲し、ソフトウェアシステム間で調整する。
本稿では,エージェントプロトコルのセキュリティ保証分析のためのソースリンクフレームワークであるAgentThreadを提案する。
- 参考スコア(独自算出の注目度): 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.
- Abstract(参考訳): AIエージェントプロトコルは、エージェントがツールの使用方法、作業の委譲、ソフトウェアシステム間のコーディネートを定義するが、そのセキュリティ要件は不完全であり、デプロイメント全体にわたって一貫性がないままである。
我々は、仕様テキストからSDKの実行まで、エージェントプロトコルのセキュリティ保証分析のためのソースリンクフレームワークであるAgentThreadを提案する。
AgentThreadはレイヤ化されたセキュリティスコープ、TLA+不変として形式化されたプロトコル由来のチェック、およびプロトコル仕様をモデルチェック可能なモデルにコンパイルし、プロトコルアダプタを通じて実際のSDKに対して実行可能な反例を再生する2フェーズチェッカーを提供する。
それぞれの発見について、AgentThreadはチェックの背後にあるソーステキストを記録し、違反したプロトコル要件を、欠落したレコメンデーション、ハードニングギャップ、未割り当てのクロスプロトコール責任から分離する。
5つの新しいエージェントプロトコルの中で、AgentThreadは35の仕様レベルの発見を特定し、本番SDKとリファレンスサーバに対する80の実装テストでそれらをサポートし、プロトコル構成下でのみ発生する30の障害を見つける。
さらに、1つのプロトコルのみが実際にセキュリティ関連制御を強制し、プロトコルがクロスプロトコルの動作に強制を割り当てることも示している。
したがって、エージェントプロトコルの不セキュリティは、仕様や実装の問題だけでなく、プロトコル、SDK、デプロイメント間の責任ギャップでもある。
関連論文リスト
- A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
本研究では,大規模言語モデル(LLM)エージェント通信プロトコルの分類と解析を行う技術的分類法を開発する。
このフレームワークはプロトコルの選択をガイドし、プライバシーやポリシー執行といったオープンな研究ギャップを強調する。
論文 参考訳(メタデータ) (2026-06-17T14:45:20Z) - LAP: An Agent-to-Instrument Protocol for Autonomous Science [6.00746946741668]
大規模な言語モデルエージェントが実験を計画し、自動運転研究所がそれらを実行している。
このようなシステムはすべて、推論エージェントと物理機器のリンクをゼロから再構築する。
最近のエージェント・インターオペラビリティ・プロトコルはエージェント・ツー・ツールエッジを明確にし、Googleのエージェント・ツー・エージェントエッジ(A2A)はエージェント・ツー・エージェントエッジである。
このギャップを埋めるプロトコルであるLab Agent Protocol (LAP) を提示する。
論文 参考訳(メタデータ) (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]
本稿では,エージェント名サービス(ANS)における実装指向の概念実証について述べる。
ANSは、AIエージェントの発見と相互運用性のためのDNSにインスパイアされた信頼層である。
実演されたサービスパスにおけるサブ10ms応答と、スクリプト化されたデモデプロイメントシナリオの完全な成功を観察します。
論文 参考訳(メタデータ) (2026-04-29T01:24:27Z) - Autogenesis: A Self-Evolving Agent Protocol [60.15939127351914]
本稿では,自己進化プロトコルであるAutogenesis Protocol(AGP)を紹介する。
本稿では,実行中のプロトコル登録リソースを動的にインスタンス化し,検索し,精錬する自己進化型マルチエージェントシステムAGSを提案する。
論文 参考訳(メタデータ) (2026-04-16T14:04:06Z) - MPAC: A Multi-Principal Agent Coordination Protocol for Interoperable Multi-Agent Collaboration [2.643905034529239]
MPACはアプリケーション層プロトコルで、このギャップを5つの層にまたがる明示的なコーディネーションセマンティクスで埋める。
仕様では21のメッセージタイプ、標準トランジションテーブルを備えた3つのステートマシン、Lamport-clock因果電子透かし、2つの実行モデル、3つのセキュリティプロファイル、共有状態の楽観的な制御を定義している。
制御された3エージェントのコードレビューベンチマークでは、調整オーバーヘッドが95%削減され、壁時計の4.8倍のスピードアップを示した。
論文 参考訳(メタデータ) (2026-04-10T01:12:05Z) - AgentRFC: Security Design Principles and Conformance Testing for Agent Protocols [2.1352949241716352]
エージェントプロトコルにより、自律的なエージェントが機能を発見し、タスクを委譲し、信頼境界を越えてサービスを構成することができる。
大規模なデプロイメントにもかかわらず、これらのプロトコルの体系的なセキュリティフレームワークは存在しない。
Agent Protocol Stack、Agent-Agnostic Security Model、AgentConformの3つのコントリビューションを提示します。
論文 参考訳(メタデータ) (2026-03-25T00:25:02Z) - Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
プロトコルとモニタモデルを知っている信頼できないモデルによるアダプティブアタックについて検討する。
我々は、攻撃者がモデル出力に公知またはゼロショットプロンプトインジェクションを埋め込む単純な適応攻撃ベクトルをインスタンス化する。
論文 参考訳(メタデータ) (2025-10-10T15:12:44Z) - VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation [40.594947933580464]
医療などのセンシティブなドメインに自律的なAIエージェントを配置することは、安全性、セキュリティ、プライバシに重大なリスクをもたらす。
LLMをベースとしたエージェントに対して、正式な安全保証を提供する新しいフレームワークであるVeriGuardを紹介する。
論文 参考訳(メタデータ) (2025-10-03T04:11:43Z) - CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。
私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文 参考訳(メタデータ) (2024-11-20T14:16:55Z) - Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。
プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。
本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
論文 参考訳(メタデータ) (2024-05-09T19:57:59Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳(メタデータ) (2024-01-19T14:52:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。