論文の概要: A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis
- arxiv url: http://arxiv.org/abs/2608.06315v2
- Date: Sat, 08 Aug 2026 15:04:34 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-11 13:55:18.739771
- Title: A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis
- Title（参考訳）: タマリンから ProVerif への音訳:比較分析の実践
- Authors: Kevin Morio, Yavor Ivanov, Robert Künnemann,
- Abstract要約: TamarinとProVerifは、セキュリティプロトコルの正式な検証のための2つのツールである。
本稿では,2つのツールの厳密な比較を可能にする,タマリンからProVerifへの音声翻訳について述べる。
- 参考スコア（独自算出の注目度）: 7.354864369233212
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Tamarin and ProVerif are two prominent tools for the formal verification of security protocols. They share the same high-level goal but differ significantly in their underlying formalisms and verification techniques, making a systematic comparison challenging: Tamarin uses multiset rewrite rules with sound and complete verification, whereas ProVerif employs an extension of the applied-pi calculus that provides fast but potentially incomplete results. We present a sound translation from Tamarin to ProVerif that enables a rigorous comparison of the two tools. It introduces techniques for formula rewriting, encoding multiset rewrite semantics, and handling simultaneous events, supporting a large subset of Tamarin's features, including multiset rewrite rules, lemmas, and restrictions, while precisely characterizing the cases where faithful translation is not possible. We provide formal proofs: within the faithful fragment, soundness ensures that any property verified in ProVerif also holds in the original Tamarin model, and completeness ensures that exists-trace properties not involving attacker knowledge are preserved. Best-effort encodings, in particular XOR, are reported separately and are outside these guarantees. Finally, we evaluate our translation on 121 Tamarin models. The ProVerif front end accepts executable translations for 523 of 566 lemma tasks. Among non-XOR tasks with definitive results from both tools, 237 of 238 agree, with the remaining verdict explicitly flagged as using an incomplete model. Among the 344 tasks for which Tamarin returns a Boolean result and ProVerif completes with a logical result, ProVerif is faster in 316 cases (91.9%), with median per-task runtime and peak-memory ratios of 6.74x and 6.13x, respectively.
- Abstract（参考訳）: TamarinとProVerifは、セキュリティプロトコルの正式な検証のための2つの重要なツールである。
彼らは同じハイレベルな目標を共有しているが、基礎となる形式主義や検証技術では著しく異なるため、体系的な比較は困難である。
本稿では,2つのツールの厳密な比較を可能にする,タマリンからProVerifへの音声翻訳について述べる。
複数セットの書き直しセマンティクスを符号化し、同時イベントを処理し、多セットの書き直し規則、補題、制限を含む玉林の特徴の大規模なサブセットをサポートしながら、忠実な翻訳ができない場合を正確に特徴づける技術を導入している。
忠実な断片の中では、音性は、ProVerifで検証されたプロパティが元の玉林モデルにも保持されることを保証し、完全性は、攻撃者の知識を含まない既存のトレース特性が保存されることを保証する。
ベスト・エフォート・エンコーディング、特にXORは別々に報告され、これらの保証の外部にある。
最後に,121タマリンモデルを用いた翻訳について検討した。
ProVerifフロントエンドは566のレムマタスクのうち523の実行可能な翻訳を受け付けている。
どちらのツールからも決定的な結果が得られた非XORタスクのうち、238の237は一致しており、残りの判定は不完全なモデルとして明示的にフラグ付けされている。
TamarinがBoolean結果を返す344タスクとProVerifが論理的な結果で完了する344タスクのうち、ProVerifは316ケース(91.9%)で高速で、各タスク毎の中央値とピークメモリ比は6.74xと6.13xである。
関連論文リスト
- PULSE: An Executable Contract Language for Spatiotemporal Knowledge Graph Engineering [2.2262915480980063]
PULSEはObject-Process-Methodologyにインスパイアされた言語で、4つの運用ロールをローカライズし、その書き込み効果を1つの型付きランタイムで表現する。
実装されたコントラクトは、非オーバーライト、ブランチアイソレーション、接地されたマルチオブジェクトタイマー、ガードされた状態変更、時間と空間に関する宣言付きイベント順序のエビデンスを修正する。
Lean 4は、位置、エビデンス、クロック、モニター、アトミック性、ブランチソース保持のカーネルアナログをチェックする。
論文 参考訳（メタデータ） (2026-07-26T17:44:05Z) - Beyond Pass Rate: A Multilingual, Execution-Grounded Evaluation of Open Code LLMs [0.0]
ベストモデルの平均正しさは23.64%に達し、人間受け入れベースラインは57.2%である。
Qwen2.5-Coder-14B-Instructは、難しい問題と明確なプロブレムカバレッジで最強である。
Gemma-2-27B-ITは全言語でのリント通過率が最も高い。
論文 参考訳（メタデータ） (2026-06-07T21:10:30Z) - Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
コーディングエージェントは、しばしば自身のローカル検証ルーチンを過度に信頼し、表面チェックを満たすアーティファクトの成功を宣言する。
この問題は、事前評価が結果駆動である変換において特に深刻である。
ブラインド・コンバージョンは26.7-28.9%に達し、スペック・パスレートは91.1%まで上昇した。
このことは、失敗は限られた予算やバックボーンの強さよりも、契約ミスによる自己検証に起因していることを示唆している。
論文 参考訳（メタデータ） (2026-05-27T19:57:15Z) - The Path Matters: Learning a Token-Commitment Policy for Diffusion Language Models [52.93186090124315]
トークンのコミットメントは、再利用可能なトレースステートポリシとして学ぶことができる、と私たちは主張する。
凍結拡散言語モデルのためにこのポリシーをインスタンス化する軽量プラグインコントローラであるTraceLockを紹介する。
論文 参考訳（メタデータ） (2026-05-23T18:23:46Z) - A Systematic Benchmark of Machine Transliteration Models for the Tajik-Farsi Language Pair: A Comparative Study from Rule-Based to Transformer Architectures [0.0]
本稿では,タジク文字(キリル文字)とペルシア文字(アラビア文字)の文字化のための現代機械学習アーキテクチャの包括的比較分析について述べる。
最初のデータセットは328,253対の文対で構成され、成層ランダムサンプリングを用いて4万対の代表的サブセットが形成された。
結果は、他のモデルよりもByT5(TajikからFarsiへのchrF++ 87.4、逆の80.1)の圧倒的な優位性を示している。
論文 参考訳（メタデータ） (2026-05-04T06:24:51Z) - AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。
このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文 参考訳（メタデータ） (2026-02-10T06:58:26Z) - CLOVER: A Test Case Generation Benchmark with Coverage, Long-Context, and Verification [71.34070740261072]
本稿では,テストケースの生成と完成におけるモデルの能力を評価するためのベンチマークCLOVERを提案する。
ベンチマークはタスク間でのコード実行のためにコンテナ化されています。
論文 参考訳（メタデータ） (2025-02-12T21:42:56Z) - Tamgram: A Frontend for Large-scale Protocol Modeling in Tamarin [3.7541073979828723]
この研究は、Tamgramと呼ばれる高レベルなプロトコルモデリング言語を導入し、Tamrinのマルチセット書き換えセマンティクスに変換できる形式的セマンティクスを導入している。
TamgramはネイティブなTamarinコードを直接記述できるだけでなく、さまざまな高レベルな構成で大きな仕様を簡単に構築できる。
本研究では,タマリンのトレースセマンティクスに関するタマグラムの健全性と完全性を証明し,異なる翻訳戦略について議論し,手作業によるタマリン仕様に匹敵する性能をもたらす最適戦略を特定する。
論文 参考訳（メタデータ） (2024-08-23T15:00:44Z) - REPOFUSE: Repository-Level Code Completion with Fused Dual Context [11.531678717514724]
本稿では,遅延トレードオフを伴わずにリポジトリレベルのコード補完を向上するための先駆的ソリューションであるREPOFUSEを紹介する。
本稿では、2種類の文脈を制限された大きさのプロンプトに効率的に凝縮する新しいランク・トランケート・ジェネレーション(RTG)手法を提案する。
REPOFUSEは既存のモデルよりも大幅に飛躍し、コード補完の正確な一致(EM)精度が40.90%から59.75%向上し、推論速度が26.8%向上した。
論文 参考訳（メタデータ） (2024-02-22T06:34:50Z) - A Template-based Method for Constrained Neural Machine Translation [100.02590022551718]
本稿では,デコード速度を維持しつつ,高い翻訳品質と精度で結果が得られるテンプレートベースの手法を提案する。
テンプレートの生成と導出は、1つのシーケンスからシーケンスまでのトレーニングフレームワークを通じて学習することができる。
実験結果から,提案手法は語彙的,構造的に制約された翻訳タスクにおいて,いくつかの代表的ベースラインを上回り得ることが示された。
論文 参考訳（メタデータ） (2022-05-23T12:24:34Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。