What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908909847969792 |
|---|---|
| author | Metere, Roberto Lilli, Mario Arnaboldi, Luca Riccobene, Elvinia |
| author_facet | Metere, Roberto Lilli, Mario Arnaboldi, Luca Riccobene, Elvinia |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_23352 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication Metere, Roberto Lilli, Mario Arnaboldi, Luca Riccobene, Elvinia Cryptography and Security Networking and Internet Architecture C.2.2; C.2.1; D.2.4; F.3.1; K.6.5 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. |
| title | What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication |
| topic | Cryptography and Security Networking and Internet Architecture C.2.2; C.2.1; D.2.4; F.3.1; K.6.5 |
| url | https://arxiv.org/abs/2603.23352 |