What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication

• URL: http://arxiv.org/abs/2603.23352v1
• Date: Tue, 24 Mar 2026 15:54:05 GMT
• Title: What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication
• Abstract summary: IEEE 802.11 includes a secure authentication protocol called SAE, whose use is mandatory for WPA3-Personal networks.<n> 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.<n>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 andTA.
• Score: 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.

Related papers

• A2ABreak: Systematic Security Analysis of the A2A Protocol [9.340181893879683]
  This paper presents A2ABreak, the first rigorous systematic security analysis of the A2A protocol.<n>We introduce a novel framework that utilizes an LLM-assisted extraction of a verified finite-state machine directly from the natural-language specification.<n>Our analysis uncovers 11 new vulnerabilities, each exploitable by a specification-compliant adversary without requiring any implementation flaw.
  arXiv  Detail & Related papers  (2026-09-09T22:18:36Z)
• FIDEM: A Standard-Compliant Framework for Secure Binding of MUD Profiles to IoT Devices [90.91375734523943]
  FIDEM is a standard-compliant framework for securing DHCP-based MUD URL issuance.<n>It provides cryptographic binding between IoT devices and their MUD profiles by leveraging Zero-Knowledge-Proof authentication.
  arXiv  Detail & Related papers  (2026-05-28T09:16:50Z)
• Secure Wi-Fi Ranging Today: Security and Adoption of IEEE 802.11az/bk [5.178641558831555]
  We analyse the core mechanisms of secure Wi-Fi ranging as defined in IEEE 802.11az and IEEE 802.11bk.<n>We show how common deployment choices can result in unauthenticated ranging, downgrade attacks, and simple denial-of-service attacks.<n>Our results show that secure Wi-Fi ranging is highly sensitive to configuration choices and is non-trivial to implement on existing hardware.
  arXiv  Detail & Related papers  (2026-03-19T09:46:43Z)
• Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
  We re-model the Needham-Schroeder protocol using an Isabelle formalism that generates sound animation.<n>Our findings reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios.<n>We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming.
  arXiv  Detail & Related papers  (2025-08-26T20:59:16Z)
• EAP-FIDO: A Novel EAP Method for Using FIDO2 Credentials for Network Authentication [43.91777308855348]
  EAP-FIDO allows organisations with WPA2/3-Enterprise wireless networks or MACSec-enabled wired networks to leverage FIDO2's passwordless authentication.<n>We provide a comprehensive security and performance analysis to support the feasibility of this approach.
  arXiv  Detail & Related papers  (2024-12-04T12:35:30Z)
• ACRIC: Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  Recent security incidents in safety-critical industries exposed how the lack of proper message authentication enables attackers to inject malicious commands or alter system behavior.<n>These shortcomings have prompted new regulations that emphasize the pressing need to strengthen cybersecurity.<n>We introduce ACRIC, a message authentication solution to secure legacy industrial communications.
  arXiv  Detail & Related papers  (2024-11-21T18:26:05Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems.
  arXiv  Detail & Related papers  (2024-05-09T19:57:59Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP) is an improvement of the Push-Button configuration (PBC) standard. TEP relies on the Tamper-Evident Announcement (TEA), which guarantees that an adversary can neither tamper a transmitted message without being detected, nor hide the fact that the message has been sent. This paper provides a comprehensive overview of the TEP protocol, including all information needed to understand how it works.
  arXiv  Detail & Related papers  (2023-11-24T18:54:00Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Twin-field quantum digital signatures [4.503555294002338]
  Digital signature is a key technique in information security, especially for identity authentications. Quantum digital signatures (QDSs) provide a considerably higher level of security, i.e., information-theoretic security.
  arXiv  Detail & Related papers  (2020-03-25T08:04:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.