論文の概要: What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication
- arxiv url: http://arxiv.org/abs/2603.23352v1
- Date: Tue, 24 Mar 2026 15:54:05 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-25 19:53:37.56872
- Title: What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication
- Title（参考訳）: メッシュとは何か: WPA3 SAE無線認証の形式的セキュリティ分析
- Authors: Roberto Metere, Mario Lilli, Luca Arnaboldi, Elvinia Riccobene,
- Abstract要約: IEEE 802.11にはSAEと呼ばれるセキュアな認証プロトコルが含まれており、このプロトコルはWPA3-Personalネットワークに必須である。
プロトコルは、ネットワークデバイス間の通信ロジックの従来の暗号記述と、各デバイスで前者を実現するステートマシン記述である。
両レベルでプロトコルの詳細な形式モデルを示し、そのセキュリティ特性の正確な仕様を提供し、ProVerifとTAでマシンチェックされた証明を解析する。
- 参考スコア（独自算出の注目度）: 1.1536806813645057
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The latest Wi-Fi security standard, IEEE 802.11, includes a secure authentication protocol called SAE, whose use is mandatory for WPA3-Personal networks. The protocol is specified at two separate but linked levels: a traditional cryptographic description of the communication logic between network devices, and a state machine description that realises the former in each single device. Current formal verification efforts focus mainly on communication logic. We present detailed formal models of the protocol at both levels, provide precise specifications of its security properties, and analyse machine-checked proofs in ProVerif and ASMETA. The integrated analysis of the above two models is particularly novel, enabling us to identify and address several issues in the current IEEE 802.11 specification more thoroughly than would have been possible otherwise, leading to several official revisions of the standard.
- Abstract（参考訳）: 最新のWi-Fiセキュリティ標準であるIEEE 802.11にはSAEと呼ばれるセキュアな認証プロトコルが含まれており、WPA3-Personalネットワークでは必須である。
プロトコルは、ネットワークデバイス間の通信ロジックの従来の暗号記述と、各デバイスで前者を実現するステートマシン記述の2つの異なるリンクレベルで定義されている。
現在の正式な検証は、主に通信ロジックに焦点を当てている。
両レベルでプロトコルの詳細な形式モデルを示し、そのセキュリティ特性の正確な仕様を提供し、ProVerifとASMETAでマシンチェックされた証明を解析する。
上記の2つのモデルの統合分析は特に新しいもので、現在のIEEE 802.11仕様のいくつかの問題を特定し、対処することができる。
関連論文リスト
- Secure Wi-Fi Ranging Today: Security and Adoption of IEEE 802.11az/bk [5.178641558831555]
IEEE 802.11azとIEEE 802.11bkで定義されたセキュアWi-Fiのコアメカニズムを分析する。
一般的なデプロイメント選択が、不正な範囲、ダウングレードアタック、シンプルなサービス拒否アタックをもたらすことを示しています。
その結果、セキュアなWi-Fiレンジは構成選択に非常に敏感であり、既存のハードウェアで実装するのは簡単ではないことがわかった。
論文 参考訳（メタデータ） (2026-03-19T09:46:43Z) - 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) - ACRIC: Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
安全クリティカルな業界における最近のセキュリティインシデントは、適切なメッセージ認証の欠如により、攻撃者が悪意のあるコマンドを注入したり、システムの振る舞いを変更することができることを明らかにした。
これらの欠点は、サイバーセキュリティを強化するために圧力をかける必要性を強調する新しい規制を引き起こしている。
我々は,レガシ産業通信をセキュアにするためのメッセージ認証ソリューションであるACRICを紹介する。
論文 参考訳（メタデータ） (2024-11-21T18:26:05Z) - 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) - Tamper-Evident Pairing [55.2480439325792]
Tamper-Evident Pairing (TEP)はPush-ButtonConfiguration (PBC)標準の改良である。
TEP は Tamper-Evident Announcement (TEA) に依存しており、相手が送信されたメッセージを検出せずに改ざんしたり、メッセージが送信された事実を隠蔽したりすることを保証している。
本稿では,その動作を理解するために必要なすべての情報を含む,TEPプロトコルの概要について概説する。
論文 参考訳（メタデータ） (2023-11-24T18:54:00Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - Twin-field quantum digital signatures [4.503555294002338]
デジタルシグネチャ(Digital signature)は、情報セキュリティ、特にID認証において重要な技術である。
量子デジタルシグネチャ(QDS)は、情報理論のセキュリティなど、より高度なセキュリティを提供する。
論文 参考訳（メタデータ） (2020-03-25T08:04:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。