論文の概要: A Formal Analysis of Agent Payment Protocols
- arxiv url: http://arxiv.org/abs/2609.00060v1
- Date: Sun, 30 Aug 2026 14:04:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-02 16:31:35.805271
- Title: A Formal Analysis of Agent Payment Protocols
- Title（参考訳）: エージェント支払いプロトコルの形式解析
- Abstract要約: 自動商取引における重要なトランザクション層としてエージェント支払いプロトコルが登場している。
我々はタマリンでx402,MPP,ACP,AP2の4つの代表エージェント支払いプロトコルを定式化した。
ソースバックの検証質問と反例トレースを使用して、欠落したバインディング、状態制約、およびステージ横断の対応を公開します。
- 参考スコア（独自算出の注目度）: 21.91506763477032
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Agent payment protocols are emerging as a key transaction layer for autonomous commerce, enabling AI agents to purchase goods and services and execute payments on users' behalf. Unlike conventional payment flows, they distribute user intent, delegated authority, credential use, settlement, and fulfillment across multiple actors and stages, creating security dependencies that no single message or participant can enforce. Yet these guarantees remain largely implicit across evolving specifications, schemas, and reference implementations, with little systematic formal analysis. We formalize four representative agent payment protocols: x402, MPP, ACP, and AP2 in Tamarin. Using a common abstraction of the agent payment lifecycle, we construct source-grounded models that capture each protocol's roles, state, trust assumptions, and lifecycle transitions. Rather than assuming a complete property taxonomy, we use source-backed verification questions and counterexample traces to expose missing bindings, state constraints, and cross-stage correspondences, consolidating them into 18 shared security principles. Across 86 verification cases, our analysis reproduces 46 known or calibration cases and identifies 40 previously undocumented formal-consistency findings. For each retained violation, we isolate the missing protocol relation, construct a minimally strengthened reference model, and reverify the intended property. We further evaluate the new x402 findings across three implementations and validate ten representative findings through implementation PoCs, SDK/schema-level witnesses, and source-aligned executable traces spanning five security principles. Our results show that delegated authorization must remain consistent with its resulting economic and service effects across actors, states, and protocol stages.
- Abstract（参考訳）: AIエージェントは商品やサービスを購入し、ユーザの代理として支払いを実行することができる。
従来の支払いフローとは異なり、ユーザ意図、委任された権限、クレデンシャル使用、決済、および充足を複数のアクターとステージに分散し、単一のメッセージや参加者が強制できないセキュリティ依存関係を作成する。
しかし、これらの保証は、進化している仕様、スキーマ、参照実装に対してほとんど暗黙的なままであり、体系的な形式分析はほとんどない。
我々はタマリンでx402,MPP,ACP,AP2の4つの代表エージェント支払いプロトコルを定式化した。
エージェント支払いライフサイクルの共通の抽象化を用いて、各プロトコルの役割、状態、信頼前提、ライフサイクル遷移をキャプチャするソース基底モデルを構築します。
完全な資産分類を仮定するのではなく、ソースバックの検証質問と反例のトレースを使用して、欠落したバインディング、状態制約、およびクロスステージ対応を公開し、それらを18の共有セキュリティ原則に統合します。
86例中46例の検診を再現し,既往の形式整合性所見を40例同定した。
保持された各違反に対して、欠落したプロトコル関係を分離し、最小限に強化された参照モデルを構築し、意図したプロパティを再検証する。
さらに、3つの実装にまたがる新しいx402結果を評価し、PoCの実装、SDK/スキーマレベルの証人、および5つのセキュリティ原則にまたがるソース整合可能なトレースを通じて10の代表的な結果を検証する。
我々の結果は、委譲された認可は、アクター、状態、プロトコルステージ間で生じる経済的およびサービス的効果と一致し続けなければならないことを示している。
関連論文リスト
- Zero-Knowledge Predicate Proofs Between AI Agents: A Measured, Cross-Protocol Gateway and the Source-Integrity Gap [0.0]
マルチエージェントAIプラットフォームは、ステージングからプロダクションへ素早く移行するが、エージェントが信頼を確立する方法はまだ初歩的だ。
提案から実行システムまで,エージェント間での検証可能なデータ最小化を行う。
32ビットのしきい値述語は6.2msで証明され、608バイトのBulletproofs証明で1.0msで検証される。
論文 参考訳（メタデータ） (2026-08-30T23:16:17Z) - AgentProv: Auditing Agentic LLM API Providers via Tool-use Policy Probes [38.37599802008238]
商用LLM APIは特定の基盤モデルを宣伝するが、提供されたバックボーンは静かに代用され、定量化され、あるいはラップされることがある。
既存の監査はすべて、テキスト出力チャネルからバックボーンアイデンティティを決定する。
本稿では,AgentProv(AgentProv)について紹介する。
論文 参考訳（メタデータ） (2026-08-30T08:22:12Z) - Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。
Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。
ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
論文 参考訳（メタデータ） (2026-08-13T17:41:27Z) - Preventing Premature Commitment in Coding Agents with an Evidence-Conditioned Execution Layer [38.62073085926841]
LLMベースのコーディングエージェントはソースコードを編集したり、変更を正当化するための十分なリポジトリ証拠を調べる前にパッチを提出する。
我々は、エビデンス条件付き実行を実行するために、エージェントとレポジトリの間を介在する実行層であるECLoopを提案する。
論文 参考訳（メタデータ） (2026-07-30T20:16:35Z) - A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
本研究では,大規模言語モデル(LLM)エージェント通信プロトコルの分類と解析を行う技術的分類法を開発する。
このフレームワークはプロトコルの選択をガイドし、プライバシーやポリシー執行といったオープンな研究ギャップを強調する。
論文 参考訳（メタデータ） (2026-06-17T14:45:20Z) - 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) - Anumati: Proof of Adherence as a Formal Consent Model for Autonomous Agent Protocols [0.0]
本稿では,エージェント対エージェント通信のためのバージョン付き,追加のみの同意モデルを提案する。
このモデルは、2つの広く使用されるエージェントプロトコルに対する非破壊的拡張としてインスタンス化される。
論文 参考訳（メタデータ） (2026-04-16T10:48:21Z) - SoK: Security of Autonomous LLM Agents in Agentic Commerce [17.16390433047924]
本稿では、商業・金融における自律型LLMエージェントの統一セキュリティフレームワークを開発する。
エージェントの完全性、トランザクション承認、エージェント間信頼、市場操作、規制コンプライアンスの5つの側面に沿って脅威を編成します。
本稿では,現行のエージェント支払いプロトコルが残している認証ギャップに対処する階層型防衛アーキテクチャを提案する。
論文 参考訳（メタデータ） (2026-04-15T01:55:40Z) - 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) - CreditAudit: 2$^\ ext{nd}$ Dimension for LLM Evaluation and Selection [44.251742023911135]
CreditAuditはデプロイ指向の信用監査フレームワークで、セマンティックアライメントと非敵対的なシステムプロンプトテンプレートのファミリ下でモデルを評価する。
同様の平均能力を持つモデルは、かなり異なる変動を示し、安定リスクは、エージェントまたは高失敗コストの制度における優先順位決定を覆す可能性があることを示す。
論文 参考訳（メタデータ） (2026-01-23T07:53:25Z) - SmartSnap: Proactive Evidence Seeking for Self-Verifying Agents [45.71333459905404]
SmartSnapは、受動的でポストホックな検証から、エージェント自身による積極的な自己検証へのパラダイムシフトである。
両ミッションで設計された新しいタイプのエージェントである「自己検証エージェント」を導入し、タスクを完了し、検証された証拠でその達成を証明した。
モデルファミリとスケールにわたるモバイルタスクの実験は、SmartSnapパラダイムによって、スケーラブルなLLM駆動エージェントのトレーニングが可能になることを実証しています。
論文 参考訳（メタデータ） (2025-12-26T14:51:39Z) - Binding Agent ID: Unleashing the Power of AI Agents with accountability and credibility [46.323590135279126]
BAID(Binding Agent ID)は、検証可能なユーザコードバインディングを確立するための総合的なアイデンティティ基盤である。
ブロックチェーンベースのID管理とzkVMベースの認証プロトコルの実現可能性を実証し、完全なプロトタイプシステムの実装と評価を行った。
論文 参考訳（メタデータ） (2025-12-19T13:01:54Z) - A Taxonomy and Methodology for Proof-of-Location Systems [42.222053626544366]
本稿では,PoL(Proof-of-Location)システムの4つの中核領域を同定する分類法を提案する。
次に、アプリケーション固有の要件を適切なPoLアーキテクチャにマッピングする方法論を紹介します。
全体として、この作業はセキュアでスケーラブルで相互運用可能なPoLシステムを構築するための構造化されたアプローチを提供する。
論文 参考訳（メタデータ） (2025-08-19T19:39:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。