論文の概要: LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean
- arxiv url: http://arxiv.org/abs/2607.03406v2
- Date: Tue, 07 Jul 2026 08:03:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-08 21:24:51.252346
- Title: LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean
- Title（参考訳）: LeanDY: リーンにおける型ベースおよびトレースベースのシンボリックプロトコル検証
- Abstract要約: 本稿では,タイプベースの推論とトレースベースの推論を組み合わせることで,ステートフルプロトコルとアンバウンドプロトコルのモジュール検証を実現する手法を提案する。
私たちはこのフレームワークをリーン実証アシスタント用のLeanDYライブラリとして実装し、DY*の設計を構築し拡張します。
我々は、LeanDYでSegWitスタイルのブロックチェーンプリミティブを形式化し、支払いチャネルの詳細な形式化を行うことで、その表現性を実証する。
- 参考スコア（独自算出の注目度）: 9.293322518056357
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Computer-aided formal verification is a widely used approach for the symbolic analysis of cryptographic protocols. However, many modern protocols rely on features that remain challenging for existing techniques. In particular, reasoning about state, time-dependent behavior, inductively defined data structures, unbounded executions, and conditional secrecy requires a level of expressiveness that is difficult to reconcile with effective automation. As a result, protocol verification has largely followed two disjoint paths: fully automated methods with limited expressiveness, or interactive proofs in general-purpose theorem provers that offer flexibility but only limited, non-specialized automation. We present an orthogonal approach that bridges this gap by combining compositional type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols. Guided by the language-and-automation co-design (LAC) principle, our approach delivers protocol-specific automation while retaining high expressiveness. We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*, and combining protocol-specific automation with interactive proofs. Our framework supports, in a unified setting, a broad class of functional and security requirements, including secrecy and authentication for stateful protocols, as well as recursive conditional secrecy for protocols using XOR. We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels on top of this blockchain model, verifying punishment mechanisms and properties that depend on chain liveness.
- Abstract（参考訳）: コンピュータ支援形式検証は暗号プロトコルの記号解析に広く用いられている手法である。
しかし、多くの現代的なプロトコルは既存の技術に挑戦し続ける機能に依存している。
特に、状態の推論、時間依存の振る舞い、帰納的定義されたデータ構造、無制限の実行、条件付き機密は、効果的な自動化と整合しがたい表現力のレベルを必要とします。
その結果、プロトコル検証は、表現力に制限のある完全自動手法と、柔軟性を提供するが限定的な非特殊化自動化のみを提供する汎用定理証明器の対話的証明の2つの相反する経路に大きく従ってきた。
このギャップを埋める直交的アプローチとして,コンポジション型推論とトレース型推論を組み合わせることで,ステートフルプロトコルとアンバウンドプロトコルのモジュール検証を可能にする。
言語と自動の協調設計(LAC)の原則に導かれ,高い表現性を保ちながらプロトコル固有の自動化を実現する。
我々は、このフレームワークをリーン実証アシスタント用のLeanDYライブラリとして実装し、DY*の設計を構築し拡張し、プロトコル固有の自動化と対話的な証明を組み合わせる。
我々のフレームワークは、統一された設定で、ステートフルプロトコルの機密と認証を含む幅広い機能およびセキュリティ要件をサポートし、また、XORを使用したプロトコルの再帰的条件秘密をサポートしている。
我々はLeanDYでSegWitスタイルのブロックチェーンプリミティブを形式化し、このブロックチェーンモデル上で支払いチャネルの詳細な形式化を実行し、チェーンの生き方に依存する罰則と特性を検証することによって、その表現性を実証する。
関連論文リスト
- Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。
既存のアプローチはそのようなシステムレベルの保証を提供していません。
本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
論文 参考訳（メタデータ） (2026-08-04T13:01:30Z) - A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
本研究では,大規模言語モデル(LLM)エージェント通信プロトコルの分類と解析を行う技術的分類法を開発する。
このフレームワークはプロトコルの選択をガイドし、プライバシーやポリシー執行といったオープンな研究ギャップを強調する。
論文 参考訳（メタデータ） (2026-06-17T14:45:20Z) - Provably Secure Agent Guardrail [89.79561918065122]
既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。
本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
論文 参考訳（メタデータ） (2026-05-28T02:12:41Z) - Beyond Message Passing: A Semantic View of Agent Communication Protocols [19.409127393922216]
エージェント通信プロトコルは,大規模言語モデル(LLM)システムにとって重要な基盤になりつつある。
この研究は、エージェントコミュニケーションをコミュニケーション、構文、セマンティックという3つの層にまとめることで、この新興の風景を人間にインスパイアされた視点で表現する。
論文 参考訳（メタデータ） (2026-03-30T00:40:30Z) - The Gatekeeper Knows Enough [0.0]
Gatekeeper Protocolは、エージェント・システム間のインタラクションを管理するドメインに依存しないフレームワークである。
提案手法は,エージェントの信頼性を著しく向上し,トークン消費を最小化することで計算効率を向上し,複雑なシステムとのスケーラブルな相互作用を可能にする。
論文 参考訳（メタデータ） (2025-10-16T17:00:42Z) - Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
音響アニメーションを生成するIsabelle形式を用いたNeedham-Schroederプロトコルをモデル化する。
以上の結果から,すべてのシナリオにおいて信頼性が保たれていることが示唆された。
我々は、透かしとジャミングを統合したPLSベースのDiffie-Hellmanプロトコルを提案している。
論文 参考訳（メタデータ） (2025-08-26T20:59:16Z) - LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
プロトコル動作の障害は脆弱性やシステム障害につながる可能性がある。
プロトコルテストに対する一般的なアプローチは、プロトコルの状態遷移と期待される振る舞いをキャプチャするマルコフモデルを構築することである。
本稿では,大規模言語モデル(LLM)を利用して,ネットワークプロトコルの実装をテストするためのシーケンスを自動的に生成する手法を提案する。
論文 参考訳（メタデータ） (2025-08-03T13:16:18Z) - ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
本稿では,広く使用されているSystemVerilogプロトコルを対象とした最初のベンチマークスイートであるProtocolLLMを紹介する。
我々は,ほとんどのモデルがタイミング制約に従う通信プロトコルのSystemVerilogコードを生成するのに失敗したことを観察する。
論文 参考訳（メタデータ） (2025-06-09T17:10:47Z) - CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。
私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文 参考訳（メタデータ） (2024-11-20T14:16:55Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。