論文の概要: Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks

• arxiv url: http://arxiv.org/abs/2508.19430v1
• Date: Tue, 26 Aug 2025 20:59:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-28 19:07:41.425366
• Title: Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks
• Title（参考訳）: 次世代通信ネットワークのための物理層セキュリティプロトコルの形式検証
• Authors: Kangfeng Ye, Roberto Metere, Jim Woodcock, Poonam Yadav,
• Abstract要約: 音響アニメーションを生成するIsabelle形式を用いたNeedham-Schroederプロトコルをモデル化する。 以上の結果から,すべてのシナリオにおいて信頼性が保たれていることが示唆された。 我々は、透かしとジャミングを統合したPLSベースのDiffie-Hellmanプロトコルを提案している。
• 参考スコア（独自算出の注目度）: 1.5997757408973357
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification is crucial for ensuring the robustness of security protocols against adversarial attacks. The Needham-Schroeder protocol, a foundational authentication mechanism, has been extensively studied, including its integration with Physical Layer Security (PLS) techniques such as watermarking and jamming. Recent research has used ProVerif to verify these mechanisms in terms of secrecy. However, the ProVerif-based approach limits the ability to improve understanding of security beyond verification results. To overcome these limitations, we re-model the same protocol using an Isabelle formalism that generates sound animation, enabling interactive and automated formal verification of security protocols. Our modelling and verification framework is generic and highly configurable, supporting both cryptography and PLS. For the same protocol, we have conducted a comprehensive analysis (secrecy and authenticity in four different eavesdropper locations under both passive and active attacks) using our new web interface. Our findings not only successfully reproduce and reinforce previous results on secrecy but also reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios, even in cases where secrecy is compromised. We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming, and our analysis shows that it is secure for deriving a session key with required authentication. These highlight the advantages of our novel approach, demonstrating its robustness in formally verifying security properties beyond conventional methods.
• Abstract（参考訳）: 形式的検証は、敵の攻撃に対するセキュリティプロトコルの堅牢性を保証するために不可欠である。 基礎認証機構であるNeedham-Schroederプロトコルは、透かしやジャミングなどの物理層セキュリティ(PLS)技術との統合など、広く研究されている。 近年の研究では、これらのメカニズムを機密性の観点から検証するためにProVerifを使用している。 しかし、ProVerifベースのアプローチは、検証結果を超えてセキュリティの理解を改善する能力を制限する。 これらの制限を克服するために、Isabelle形式を用いて同じプロトコルを再構築し、音声アニメーションを生成し、対話的かつ自動でセキュリティプロトコルの形式検証を可能にする。 我々のモデリングおよび検証フレームワークは汎用的で高度に構成可能であり、暗号とPLSの両方をサポートしている。 同じプロトコルでは、新しいWebインターフェースを用いて、包括的な分析(受動的およびアクティブな攻撃の両方の下で、4つの異なる盗聴者の場所における秘密と認証)を行った。 本研究は, 秘密保持に関する過去の結果を再現し, 補強するだけでなく, 秘密保持が侵害された場合においても, 全ての検査シナリオにおいて, 信頼性が維持されるという, 稀だが期待される結果も明らかにする。 我々は,透かしとジャミングを統合したPLSベースのDiffie-Hellmanプロトコルを提案する。 これらは我々の新しいアプローチの利点を浮き彫りにして、従来の方法以上のセキュリティ特性を正式に検証する堅牢性を示している。

関連論文リスト

• Design and analysis of a set of discrete variable protocols for secure quantum communication [0.0]
  量子ID認証(QIA)プロトコルは過去30年間に提案されてきた。 この論文は、2つの新しいQKDプロトコルを示し、絡み合いや理想的な単一光子源の必要性を排除している。 これらのプロトコルは、インターセプトと特定の集団攻撃を含む様々な攻撃に対して安全であることが厳格に証明されている。
  論文  参考訳（メタデータ） (2025-08-08T15:12:29Z)
• Quantum-Safe Identity Verification using Relativistic Zero-Knowledge Proof Systems [3.8435472626703473]
  金融、医療、オンラインサービスなどの分野では、セキュリティの確保と不正防止のためにアイデンティティの検証が不可欠だ。 現在のパスワード/PINベースのIDソリューションはフィッシングやスキミング攻撃の影響を受けやすい。 グラフカラー化に基づく相対論的ゼロ知識証明によるアイデンティティ検証について検討する。
  論文  参考訳（メタデータ） (2025-07-18T18:59:19Z)
• Strands Rocq: Why is a Security Protocol Correct, Mechanically? [3.6840775431698893]
  StrandsRocq は Coq のストランド空間の機械化である。 新しい証明技法と、新しい最大貫入器の概念が組み込まれている。 これは2つの単純な認証プロトコルに対するセキュリティの合成証明を提供する。
  論文  参考訳（メタデータ） (2025-02-18T13:34:58Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• Formal Verification of Permission Voucher [1.4732811715354452]
  Permission Voucher Protocolは、分散環境におけるセキュアで認証されたアクセス制御のために設計されたシステムである。 この分析では、重要なセキュリティ特性を評価するために、象徴的検証のための最先端のツールであるTamarin Proverを使用している。 結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。
  論文  参考訳（メタデータ） (2024-12-18T14:11:50Z)
• ACRIC: Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  安全クリティカルな業界における最近のセキュリティインシデントは、適切なメッセージ認証の欠如により、攻撃者が悪意のあるコマンドを注入したり、システムの振る舞いを変更することができることを明らかにした。 これらの欠点は、サイバーセキュリティを強化するために圧力をかける必要性を強調する新しい規制を引き起こしている。 我々は,レガシ産業通信をセキュアにするためのメッセージ認証ソリューションであるACRICを紹介する。
  論文  参考訳（メタデータ） (2024-11-21T18:26:05Z)
• Excavating Vulnerabilities Lurking in Multi-Factor Authentication Protocols: A Systematic Security Analysis [2.729532849571912]
  単一要素認証(SFA)プロトコルは、しばしばサイドチャネルや他の攻撃技術によってバイパスされる。 この問題を軽減するため,近年,MFAプロトコルが広く採用されている。
  論文  参考訳（メタデータ） (2024-07-29T23:37:38Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive Privacy Analysis and Beyond [57.10914865054868]
  垂直ロジスティック回帰(VLR)をミニバッチ降下勾配で訓練した。 我々は、オープンソースのフェデレーション学習フレームワークのクラスにおいて、VLRの包括的で厳密なプライバシー分析を提供する。
  論文  参考訳（メタデータ） (2022-07-19T05:47:30Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)

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

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