論文の概要: Strands Rocq: Why is a Security Protocol Correct, Mechanically?

• arxiv url: http://arxiv.org/abs/2502.12848v1
• Date: Tue, 18 Feb 2025 13:34:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-19 14:05:11.422353
• Title: Strands Rocq: Why is a Security Protocol Correct, Mechanically?
• Title（参考訳）: Strands Rocq: なぜセキュリティプロトコルが機械的に正しいのか?
• Authors: Matteo Busi, Riccardo Focardi, Flaminia L. Luccio,
• Abstract要約: StrandsRocq は Coq のストランド空間の機械化である。 新しい証明技法と、新しい最大貫入器の概念が組み込まれている。 これは2つの単純な認証プロトコルに対するセキュリティの合成証明を提供する。
• 参考スコア（独自算出の注目度）: 3.6840775431698893
• License:
• Abstract: Strand spaces are a formal framework for symbolic protocol verification that allows for pen-and-paper proofs of security. While extremely insightful, pen-and-paper proofs are error-prone, and it is hard to gain confidence on their correctness. To overcome this problem, we developed StrandsRocq, a full mechanization of the strand spaces in Coq (soon to be renamed Rocq). The mechanization was designed to be faithful to the original pen-and-paper development, and it was engineered to be modular and extensible. StrandsRocq incorporates new original proof techniques, a novel notion of maximal penetrator that enables protocol compositionality, and a set of Coq tactics tailored to the domain, facilitating proof automation and reuse, and simplifying the work of protocol analysts. To demonstrate the versatility of our approach, we modelled and analyzed a family of authentication protocols, drawing inspiration from ISO/IEC 9798-2 two-pass authentication, the classical Needham-Schroeder-Lowe protocol, as well as a recently-proposed static analysis for a key management API. The analyses in StrandsRocq confirmed the high degree of proof reuse, and enabled us to distill the minimal requirements for protocol security. Through mechanization, we identified and addressed several issues in the original proofs and we were able to significantly improve the precision of the static analysis for the key management API. Moreover, we were able to leverage the novel notion of maximal penetrator to provide a compositional proof of security for two simple authentication protocols.
• Abstract（参考訳）: ストランドスペースは、セキュリティのペンとペーパーの証明を可能にするシンボルプロトコル検証のための正式なフレームワークである。 極めて洞察力に富むが、ペンと紙の証明はエラーを起こしやすいため、その正確性に自信を得るのは難しい。 この問題を解決するために、我々は Coq のストランド空間の完全な機械化である StrandsRocq を開発した(すぐに Rocq と改名される)。 機械化は、元々のペンと紙の開発に忠実に設計され、モジュラーで拡張可能なように設計された。 StrandsRocqには、プロトコルの構成性を可能にする新しい最大浸透器の概念と、証明の自動化と再利用を容易にし、プロトコルアナリストの作業を簡素化する一連のCoq戦術が組み込まれている。 提案手法の汎用性を実証するため,ISO/IEC 9798-2の2パス認証,古典的なNeedham-Schroeder-Loweプロトコル,および最近提案されたキー管理APIの静的解析からインスピレーションを得て,認証プロトコル群をモデル化,解析した。 StrandsRocqの分析により、高い証明再利用が確認され、プロトコルセキュリティの最小限の要件を抽出できるようになった。 メカニゼーションにより、元の証明でいくつかの問題を特定し、対処し、キー管理APIの静的解析の精度を大幅に向上することができた。 さらに,2つの単純な認証プロトコルのセキュリティを構成的に証明するために,最大浸透器という新しい概念を活用できた。

関連論文リスト

• PriRoAgg: Achieving Robust Model Aggregation with Minimum Privacy Leakage for Federated Learning [49.916365792036636]
  フェデレートラーニング(FL)は、大規模分散ユーザデータを活用する可能性から、最近大きな勢いを増している。 送信されたモデル更新は、センシティブなユーザ情報をリークする可能性があり、ローカルなトレーニングプロセスの集中的な制御の欠如は、モデル更新に対する悪意のある操作の影響を受けやすいグローバルモデルを残します。 我々は、Lagrange符号化計算と分散ゼロ知識証明を利用した汎用フレームワークPriRoAggを開発し、集約されたプライバシを満たすとともに、幅広いロバストな集約アルゴリズムを実行する。
  論文  参考訳（メタデータ） (2024-07-12T03:18:08Z)
• A consolidated and accessible security proof for finite-size decoy-state quantum key distribution [0.0]
  我々は,コヒーレント攻撃に対する有限サイズ1-デコイおよび2-デコイBB84プロトコルに対する厳密で包括的なセキュリティ証明を提供する。 我々は、多くの作品から概念を広く統合し、統一し、基礎となる前提を徹底的に議論し、技術的な矛盾を解消する。
  論文  参考訳（メタデータ） (2024-05-26T14:13:33Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。 プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。 本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
  論文  参考訳（メタデータ） (2024-05-09T19:57:59Z)
• Protocols for Quantum Weak Coin Flipping [0.1499944454332829]
  弱いコインフリップは重要な暗号プリミティブである。 我々は関連するユニタリ作用素の正確な構成を与える。 本稿では, 明快なコインフリッププロトコルの構築について述べる。
  論文  参考訳（メタデータ） (2024-02-24T16:52:54Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Performance-lossless Black-box Model Watermarking [69.22653003059031]
  本稿では,モデル知的財産権を保護するために,ブランチバックドアベースのモデル透かしプロトコルを提案する。 さらに,プロトコルに対する潜在的な脅威を分析し,言語モデルに対するセキュアで実現可能な透かしインスタンスを提供する。
  論文  参考訳（メタデータ） (2023-12-11T16:14:04Z)
• Practical quantum secure direct communication with squeezed states [55.41644538483948]
  CV-QSDCシステムの最初の実験実験を行い,その安全性について報告する。 この実現は、将来的な脅威のない量子大都市圏ネットワークへの道を歩み、既存の高度な波長分割多重化(WDM)システムと互換性がある。
  論文  参考訳（メタデータ） (2023-06-25T19:23:42Z)
• Finite-Size Security for Discrete-Modulated Continuous-Variable Quantum Key Distribution Protocols [4.58733012283457]
  本稿では,一般的なDM CV-QKDプロトコルに対して,独立かつ同一に分散された集団攻撃に対する構成可能な有限サイズセキュリティ証明を提案する。 我々は、セキュア鍵レートの厳密な下限を計算するために、数値的なセキュリティ証明手法を拡張し、適用する。 その結果,少なくとも72kmの伝送距離で実験可能な条件下では,セキュアな有限サイズ鍵レートが得られることがわかった。
  論文  参考訳（メタデータ） (2023-01-20T17:16:21Z)
• Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive Privacy Analysis and Beyond [57.10914865054868]
  垂直ロジスティック回帰(VLR)をミニバッチ降下勾配で訓練した。 我々は、オープンソースのフェデレーション学習フレームワークのクラスにおいて、VLRの包括的で厳密なプライバシー分析を提供する。
  論文  参考訳（メタデータ） (2022-07-19T05:47:30Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。 ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。 これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
  論文  参考訳（メタデータ） (2022-05-20T12:37:09Z)
• Twin-field quantum digital signatures [4.503555294002338]
  デジタルシグネチャ(Digital signature)は、情報セキュリティ、特にID認証において重要な技術である。 量子デジタルシグネチャ(QDS)は、情報理論のセキュリティなど、より高度なセキュリティを提供する。
  論文  参考訳（メタデータ） (2020-03-25T08:04:59Z)

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

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