論文の概要: AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation
- arxiv url: http://arxiv.org/abs/2606.19937v1
- Date: Thu, 18 Jun 2026 08:34:17 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-19 18:23:39.73443
- Title: AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation
- Title（参考訳）: AutoTam:玉林モデル生成によるセキュアプロトコル実装の仕様化
- Authors: Johannes Wilson, Mikael Asplund, Niklas Johansson,
- Abstract要約: 本稿では,プロトコル実装のためのドメイン固有言語を用いて,トレース特性の検証を行う新しい言語ファースト手法を提案する。
検証のためのタマリン証明器を目標とし、検証された普遍的トレース特性が実装に戻すことを証明する。
我々は、署名されたDiffie-HellmanプロトコルとWireGuard VPNプロトコルの正確なモデルの実装と生成にツールを使用します。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification is a challenging but important task for ensuring the security of cryptographic protocols. While modern protocol verification tools significantly reduce verification effort, modelling remains challenging to practitioners without a background in formal verification. In addition, transferring verification results to a concrete protocol implementation requires expert knowledge. In this paper, we present a novel language-first method for verification of trace properties using a domain-specific language for protocol implementations. We target the Tamarin prover for verification, and we prove that verified universal trace properties translate back to the implementation. We additionally integrate symbolic execution in order to analyse the memory safety of protocol implementations. We use our tool to implement and generate accurate models for a signed Diffie-Hellman protocol, and for the WireGuard VPN protocol. Our WireGuard implementation is interoperable with existing implementations when using our interpreter, and achieves acceptable performance. We formally prove our implementations secure using a combination of symbolic execution and verification of the generated Tamarin models.
- Abstract（参考訳）: 形式検証は、暗号プロトコルのセキュリティを確保する上で、難しいが重要なタスクである。
現代のプロトコル検証ツールは検証の労力を大幅に削減するが、形式的検証のバックグラウンドを持たない実践者にとってはモデリングは依然として困難である。
さらに、検証結果を具体的なプロトコル実装に転送するには、専門家の知識が必要である。
本稿では,プロトコル実装のためのドメイン固有言語を用いて,トレース特性を検証するための新しい言語優先手法を提案する。
検証のためのタマリン証明器を目標とし、検証された普遍的トレース特性が実装に戻すことを証明する。
また,プロトコル実装のメモリ安全性を解析するために,シンボル実行を統合する。
我々は、署名されたDiffie-HellmanプロトコルとWireGuard VPNプロトコルの正確なモデルの実装と生成にツールを使用します。
WireGuardの実装は、インタプリタを使用する場合、既存の実装と相互運用可能で、許容可能なパフォーマンスを実現しています。
シンボル実行と生成したタマリンモデルの検証を組み合わせることで,実装の安全性を正式に証明する。
関連論文リスト
- 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) - Voting-Based Semi-Parallel Proof-of-Work Protocol [45.776687601070705]
まず、既存の並列PoWプロトコルを検討し、ハードコード型インセンティブアタック構造を開発する。
我々は,中本コンセンサスと既存のパラレルPoWプロトコルよりも優れた投票ベースの半並列PoWプロトコルを提案する。
論文 参考訳（メタデータ） (2025-08-08T17:57:35Z) - 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) - ModelForge: Using GenAI to Improve the Development of Security Protocols [1.9241821314180376]
プロトコル仕様の翻訳を自動化する新しいツールであるModelForgeを紹介する。
自然言語処理(NLP)と生成AI(GenAI)の進歩を活用することで、ModelForgeはプロトコル仕様を処理し、CPSAプロトコル定義を生成する。
論文 参考訳（メタデータ） (2025-06-08T06:27:09Z) - CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。
私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文 参考訳（メタデータ） (2024-11-20T14:16:55Z) - Games for AI Control: Models of Safety Evaluations of AI Deployment Protocols [52.40622903199512]
本稿では,多目的かつ部分的に観察可能なゲームとして,AI-Control Gamesを紹介した。
我々は、信頼できない言語モデルをプログラミングアシスタントとしてデプロイするためのプロトコルをモデル化、評価、合成するために、フォーマリズムを適用した。
論文 参考訳（メタデータ） (2024-09-12T12:30:07Z) - 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) - A Security Verification Framework of Cryptographic Protocols Using
Machine Learning [0.0]
機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。
ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。
提案手法を実用的な暗号プロトコルの検証に適用して評価する。
論文 参考訳（メタデータ） (2023-04-26T02:37:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。