Fugu-MT 論文翻訳(概要): Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin

論文の概要: Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin

arxiv url: http://arxiv.org/abs/2605.23643v1
Date: Fri, 22 May 2026 13:55:11 GMT
ステータス: 翻訳完了
システム内更新日: 2026-05-25 17:29:20.376734
Title: Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
Title（参考訳）: 少ない努力と短い証明:玉林におけるセキュリティプロトコル分析のための強化学習
Authors: Matthias Cosler, Cas Cremers, Bernd Finkbeiner, Mohamed Ghanem, Niklas Medinger,
Abstract要約: TamarinとProVerifは、複雑な現実世界のプロトコルの分析と検証において顕著な成功を収めた。本稿では,AlphaZeroとAlphaProofにヒントを得た強化学習(RL)フレームワークを提案する。
参考スコア（独自算出の注目度）: 15.896847410252263
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Tools like Tamarin and ProVerif have achieved notable success in analyzing and verifying complex real-world protocols such as EMV, 5G, and WPA2, even detecting zero-day exploits. Despite these successes, verifying such protocols remains a time-consuming, challenging task, often requiring significant human effort and expertise. In this paper, we present a reinforcement learning (RL) framework inspired by AlphaZero and AlphaProof that implements a new style of proof search for Tamarin. We have developed a stateless API for Tamarin that acts as a classical RL environment. We guide a Monte Carlo Tree Search (MCTS) by a neural heuristic that learns from completed subproofs. We evaluate our framework on 16 case studies, ranging from classical protocol models to challenging state-of-the-art protocol models from recent publications. Our method finds more proofs automatically than Tamarin's standard search and produces shorter proofs than both the standard and human-engineered heuristics. Our pipeline is applicable out of the box to assist Tamarin users in active research, reducing the human effort required. Moreover, our standardized interface provides a programmatic way for users to interact with Tamarin. Finally, our work demonstrates the promising potential of adapting RL-based methods to the Tamarin domain.
Abstract（参考訳）: TamarinやProVerifのようなツールは、EMVや5G、WPA2といった複雑な現実世界のプロトコルを分析し検証し、ゼロデイエクスプロイトを検知することに成功した。これらの成功にもかかわらず、このようなプロトコルの検証は依然として時間がかかり、困難な作業であり、しばしば人的努力と専門知識を必要としている。本稿では,AlphaZeroとAlphaProofにヒントを得た強化学習(RL)フレームワークを提案する。我々は,古典的なRL環境として機能するタマリンのためのステートレスAPIを開発した。我々は,モンテカルロ木探索 (MCTS) を神経ヒューリスティックでガイドし,完全サブプロテクションから学習する。我々は,古典的プロトコルモデルから最近の出版物から最先端のプロトコルモデルまで,16のケーススタディの枠組みを評価した。本手法は, タマリンの標準探索よりも多くの証明を自動生成し, 標準的なヒューリスティックと人為的ヒューリスティックの両方よりも短い証明を生成する。当社のパイプラインは,タマリン利用者の積極的な研究を支援するために,最初から適用されており,人的労力の削減が図られている。さらに、標準化されたインターフェースは、ユーザがタマリンと対話するためのプログラム的な方法を提供する。最後に,本研究は,RL法を玉林領域に適用する有望な可能性を示すものである。

関連論文リスト

Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
大言語モデル(LLM)は、単純なテキストジェネレータから、検索強化、ツール呼び出し、マルチターンインタラクションを統合する複雑なソフトウェアシステムへと進化してきた。その固有の非決定主義、ダイナミズム、文脈依存は品質保証に根本的な課題をもたらす。本稿では,LLMアプリケーションを3層アーキテクチャに分解する: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, textbftextitLLM Inference Core。
論文参考訳（メタデータ） (2025-08-28T13:00:28Z)
LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
プロトコル動作の障害は脆弱性やシステム障害につながる可能性がある。プロトコルテストに対する一般的なアプローチは、プロトコルの状態遷移と期待される振る舞いをキャプチャするマルコフモデルを構築することである。本稿では,大規模言語モデル(LLM)を利用して,ネットワークプロトコルの実装をテストするためのシーケンスを自動的に生成する手法を提案する。
論文参考訳（メタデータ） (2025-08-03T13:16:18Z)
Tamgram: A Frontend for Large-scale Protocol Modeling in Tamarin [3.7541073979828723]
この研究は、Tamgramと呼ばれる高レベルなプロトコルモデリング言語を導入し、Tamrinのマルチセット書き換えセマンティクスに変換できる形式的セマンティクスを導入している。 TamgramはネイティブなTamarinコードを直接記述できるだけでなく、さまざまな高レベルな構成で大きな仕様を簡単に構築できる。本研究では,タマリンのトレースセマンティクスに関するタマグラムの健全性と完全性を証明し,異なる翻訳戦略について議論し,手作業によるタマリン仕様に匹敵する性能をもたらす最適戦略を特定する。
論文参考訳（メタデータ） (2024-08-23T15:00:44Z)
LEAD: Liberal Feature-based Distillation for Dense Retrieval [67.48820723639601]
知識蒸留は、強い教師モデルから比較的弱い学生モデルに知識を伝達するためにしばしば用いられる。従来のメソッドにはレスポンスベースのメソッドとフィーチャーベースのメソッドが含まれる。本稿では,リベラルな特徴量に基づく蒸留法(LEAD)を提案する。
論文参考訳（メタデータ） (2022-12-10T06:30:54Z)
Mastering the Unsupervised Reinforcement Learning Benchmark from Pixels [112.63440666617494]
強化学習アルゴリズムは成功するが、エージェントと環境の間の大量の相互作用を必要とする。本稿では,教師なしモデルベースRLを用いてエージェントを事前学習する手法を提案する。我々はReal-Word RLベンチマークにおいて、適応中の環境摂動に対する抵抗性を示唆し、堅牢な性能を示す。
論文参考訳（メタデータ） (2022-09-24T14:22:29Z)
Verifying Learning-Based Robotic Navigation Systems [61.01217374879221]
有効モデル選択に現代検証エンジンをどのように利用できるかを示す。具体的には、検証を使用して、最適下行動を示す可能性のあるポリシーを検出し、除外する。我々の研究は、現実世界のロボットにおける準最適DRLポリシーを認識するための検証バックエンドの使用を初めて実証したものである。
論文参考訳（メタデータ） (2022-05-26T17:56:43Z)
Search-Based Testing of Reinforcement Learning [0.0]
ディープRLエージェントの安全性と性能を評価するための検索ベーステストフレームワークを提案する。安全試験には,RLタスクを解く参照トレースを探索する検索アルゴリズムを用いる。堅牢なパフォーマンステストのために、ファズテストを通じてさまざまなトレースセットを作成します。任天堂のスーパーマリオブラザーズのRLに検索ベースのテストアプローチを適用した。
論文参考訳（メタデータ） (2022-05-07T12:40:45Z)
Jump-Start Reinforcement Learning [68.82380421479675]
本稿では、オフラインデータやデモ、あるいは既存のポリシーを使ってRLポリシーを初期化するメタアルゴリズムを提案する。特に,タスク解決に2つのポリシーを利用するアルゴリズムであるJump-Start Reinforcement Learning (JSRL)を提案する。実験により、JSRLは既存の模倣と強化学習アルゴリズムを大幅に上回っていることを示す。
論文参考訳（メタデータ） (2022-04-05T17:25:22Z)
GalilAI: Out-of-Task Distribution Detection using Causal Active Experimentation for Safe Transfer RL [11.058960131490903]
アウト・オブ・ディストリビューション(OOD)検出は教師あり学習においてよく研究されているトピックである。本稿では,OOTD(Out-of-Task Distribution)検出という新しいタスクを提案する。ガリレオ・ガリレイ(Galileo Galilei)に敬意を表して、我々の手法をガリライ(GalilAI)と名付けた。
論文参考訳（メタデータ） (2021-10-29T01:45:56Z)
Continuous Coordination As a Realistic Scenario for Lifelong Learning [6.044372319762058]
ゼロショット設定と少数ショット設定の両方をサポートするマルチエージェント生涯学習テストベッドを導入する。最近のMARL法、および制限メモリおよび計算における最新のLLLアルゴリズムのベンチマークを評価します。我々は経験的に、我々の設定で訓練されたエージェントは、以前の作業による追加の仮定なしに、未発見のエージェントとうまく協調できることを示します。
論文参考訳（メタデータ） (2021-03-04T18:44:03Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。