論文の概要: Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin

• arxiv url: http://arxiv.org/abs/2605.29465v1
• Date: Thu, 28 May 2026 06:57:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-30 02:45:55.876359
• Title: Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin
• Title（参考訳）: ブリッジ理論と実践:ProVerifとTamarinのセキュリティ特性の実行可能な分類法
• Authors: Leonard Tudorache, Ivan Kurtev, Mark van den Brand,
• Abstract要約: セキュリティは、現代のデジタルシステムに依存するものすべてにとって重要だ。 ProVerifやTamarinといったツールは、自動検証を行うために広く利用されている。 この研究は、理論的セキュリティプロパティ定義と実用的で実行可能な検証モデルの間のギャップを埋めることによって、技術の現状を前進させる。
• 参考スコア（独自算出の注目度）: 0.9339654135645749
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Security is critical for everything relying on modern digital systems. Because almost all digital interactions are governed by the Internet and cryptographic protocols, these protocols must serve as reliable mechanisms that guarantee core security properties, such as confidentiality and integrity. Formal verification of these protocols is a critical step in securing interconnected systems. Tools such as ProVerif and Tamarin are widely employed to perform automated verification. However, their effective use demands specialized domain knowledge, creating a significant learning curve for security protocol designers who often have a security, rather than a formal verification background. We therefore need structured, accessible resources to help protocol designers to express their design and requirements in the language of the formal verification tools. To address this, we introduce a systematic and evidence-based taxonomy of security properties. This taxonomy is derived from a literature review of 53 recent studies (2022-2025) that used ProVerif and Tamarin, providing an up-to-date view of verified properties. We systematically categorize and define these properties, providing both informal definitions for intuitive comprehension and rigorous formal definitions expressed in first-order logic for clarity and consistency. We further detail modeling patterns and implement executable examples in both ProVerif and Tamarin, collected in an open repository. This work advances the state of the art by bridging the gap between theoretical security property definitions and their practical, executable verification models.
• Abstract（参考訳）: セキュリティは、現代のデジタルシステムに依存するものすべてにとって重要だ。 ほとんど全てのデジタルインタラクションはインターネットと暗号化プロトコルによって管理されているため、これらのプロトコルは機密性や整合性といった中核的なセキュリティ特性を保証する信頼性の高いメカニズムとして機能する必要がある。 これらのプロトコルの形式的検証は相互接続システムを確保するための重要なステップである。 ProVerifやTamarinといったツールは、自動検証を行うために広く利用されている。 しかし、それらの効果的な利用には専門的なドメイン知識が必要であり、正式な検証の背景ではなく、しばしばセキュリティを持つセキュリティプロトコルデザイナのための重要な学習曲線を作成する。 したがって、プロトコル設計者が形式的な検証ツールの言語で設計と要求を表現するのを助けるために、構造化されたアクセス可能なリソースが必要です。 この問題に対処するために,セキュリティ特性の体系的およびエビデンスに基づく分類を導入する。 この分類法は、ProVerifとTamarinを用いた53の最近の研究(2022-2025)の文献レビューから派生し、検証された資産の最新の見方を提供する。 我々はこれらの特性を体系的に分類し定義し、直観的理解のための非公式な定義と、明瞭さと一貫性のための一階述語論理で表される厳密な形式的定義を提供する。 オープンリポジトリで収集されたProVerifとTamarinの両方で、モデリングパターンの詳細と実行可能な例を実装します。 この研究は、理論上のセキュリティ特性の定義と、実用的で実行可能な検証モデルとのギャップを埋めることによって、最先端の技術を推し進める。

関連論文リスト

• 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)
• Deep Learning Models for Robust Facial Liveness Detection [56.08694048252482]
  本研究では,現代のアンチスプーフィング手法の欠陥に対処する新しい深層学習モデルを用いて,ロバストな解を提案する。 テクスチャ解析と実際の人間の特性に関連する反射特性を革新的に統合することにより、我々のモデルは、顕著な精度でレプリカと真の存在を区別する。
  論文  参考訳（メタデータ） (2025-08-12T17:19:20Z)
• Formal Verification of Permission Voucher [1.4732811715354452]
  Permission Voucher Protocolは、分散環境におけるセキュアで認証されたアクセス制御のために設計されたシステムである。 この分析では、重要なセキュリティ特性を評価するために、象徴的検証のための最先端のツールであるTamarin Proverを使用している。 結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。
  論文  参考訳（メタデータ） (2024-12-18T14:11:50Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• On Cryptographic Mechanisms for the Selective Disclosure of Verifiable Credentials [39.4080639822574]
  認証資格は、物理的資格のデジタルアナログである。 検証者に提示して属性を明らかにしたり、クレデンシャルに含まれる属性を述語することも可能だ。 プレゼンテーション中にプライバシを保存する1つの方法は、クレデンシャル内の属性を選択的に開示することである。
  論文  参考訳（メタデータ） (2024-01-16T08:22:28Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Value Functions are Control Barrier Functions: Verification of Safe Policies using Control Theory [46.85103495283037]
  本稿では,制御理論から学習値関数への検証手法の適用方法を提案する。 我々は値関数と制御障壁関数の間の関係を確立する原定理を定式化する。 我々の研究は、RLベースの制御システムの汎用的でスケーラブルで検証可能な設計のための公式なフレームワークに向けた重要な一歩である。
  論文  参考訳（メタデータ） (2023-06-06T21:41:31Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。 ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。 提案手法を実用的な暗号プロトコルの検証に適用して評価する。
  論文  参考訳（メタデータ） (2023-04-26T02:37:43Z)

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

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