The WPA3 Dragonfly handshake (SAE) protects Wi-Fi passwords against offline dictionary attacks, yet its implementations have repeatedly fallen to microarchitectural side channels. The Dragondoom/Dragonstar work (IEEE EuroS&P 2023) demonstrated cache-timing vulnerabilities reaching into the cryptographic libraries used by the hostap Wi-Fi daemon, and responded with Dragonstar, a provider built from the formally verified HACL* library whose cryptographic operations are proved secret-independent (free of secret-dependent branches and memory accesses). However, the verified guarantees stop at the branch- and memory-access leakage model on the low-level cryptographic primitives: fault-injection and transient-execution (Spectre-class) attacks fall outside the model, the integrated hostap+Dragonstar implementation has no mechanized proof that it conforms to the Dragonfly/SAE specification, and the underlying libraries (OpenSSL, wolfSSL) disclaim responsibility for secret-tainted inputs. This problem asks to close this verified-but-insecure gap: extend formal security guarantees for a deployed Dragonfly/SAE implementation to the unmodeled physical channels, to full protocol-level functional correctness, and across the library-API boundary, yielding an end-to-end verified, deployable SAE handshake.

Background

Wi-Fi security since 2018 is dominated by WPA3, whose personal mode replaces the pre-shared-key mechanism of WPA2 with the Dragonfly protocol, standardized as SAE (Simultaneous Authentication of Equals). Dragonfly is a password-authenticated key exchange (PAKE): two parties who share only a low-entropy password derive a strong session key, and the protocol is designed so that a network attacker cannot verify password guesses offline. This property is destroyed by any leakage of password-dependent behavior, which is why implementation quality is security-critical: a PAKE plus one leaked bit per handshake equals an offline dictionary attack.

The attack history is long. Dragonblood (Vanhoef and Ronen, IEEE S&P 2020) exhibited timing and cache side channels in the hunting-and-pecking password derivation — the loop that hashes the password and rejects curve points until a valid one is found, whose iteration count depends on the password — and De Almeida Braga, Fouque, and Sabt (ACSAC 2020) extended these cache attacks to more implementations. The Wi-Fi ecosystem responded with patches and with a deterministic alternative derivation based on SSWU (Simplified Shallue–Woestijne–Ulas), a hash-to-curve method that maps the password to an elliptic-curve point without data-dependent looping. Dragondoom (De Almeida Braga, Kulatova, Sabt, Fouque, Bhargavan, IEEE EuroS&P 2023) showed that the mitigations were insufficient: the leaks reach into the cryptographic libraries themselves (for example big-number conversion from byte strings, and elliptic-curve point decompression, called by hostap with secret-dependent values), the attacks defeat constant-time-minded code, and even the new SAE-PT mode is affected. Their attacks use Flush+Reload — a cache attack where the attacker flushes a cache line, lets the victim run, and reloads the line to learn whether the victim touched it — combined with performance-degradation tricks.

The constructive answer of that paper is Dragonstar: a cryptographic provider for hostap built on HACL*, a cryptographic library written and verified in the F* proof assistant, whose algorithms carry machine-checked proofs of functional correctness and of secret independence. Secret independence is the standard countermeasure model for timing and cache attacks: execution must not branch on, or index memory by, secret data. Dragonstar achieves performance comparable to the OpenSSL-based configuration, and the provider's operations are extracted from verified code. The open problem spans three limitations. First, secret independence says nothing about fault injection (active physical disturbance of computation, e.g., voltage or clock glitches that flip bits or skip instructions) or transient-execution attacks (Spectre-class attacks where speculative execution transiently computes with secrets before a misprediction is rolled back, leaving microarchitectural traces); verification and mitigation for these channels had not been incorporated into HACL*. Second, only the cryptographic provider is proved — there is no mechanized proof that the integrated hostap+Dragonstar implementation realizes the Dragonfly/SAE specification (covering both the hunting-and-pecking and SSWU derivations and the commit/confirm exchange), so integration bugs can remain. Third, the ecosystem dimension: OpenSSL and wolfSSL acknowledged that their big-number operations leak on secret inputs but declined to patch, arguing that avoiding secret-tainted calls is the caller's responsibility — leaving no systematic policy or tooling that guarantees secret independence of library APIs on secret-tainted inputs.

Adjacent research has advanced pieces of this landscape without closing any of the three gaps: the high-assurance cryptography program in the Spectre era (Barthe et al., IEEE S&P 2021) and the FaCT domain-specific language for timing-sensitive computation (Cauligi et al., PLDI 2019) develop verification against stronger leakage models; Jasmin-based enforcement of fine-grained constant-time policies (Shivakumar et al., 2022) and secure compilation of crypto code against transient-execution channels (the DOIT line, 2025) extend compiler-verified countermeasures; fault-injection formal verification is active chiefly for masked hardware-oriented implementations; and 2026 brought the first protocol-level formal models of SAE (Chen, Pan, Sanina; Metere et al.) in ProVerif/ASMETA — specifications, not verified implementations.

Problem Statement

Extend the formally verified security of the WPA3 Dragonfly/SAE handshake, as realized by the Dragonstar approach, from primitive-level secret independence to the full attacker-reachable surface, so that a deployed, performance-competitive Wi-Fi daemon implementation of Dragonfly carries end-to-end formal guarantees. Three linked directions organize this goal:

  1. Advanced physical channels: incorporate verification and mitigations against fault-injection and transient-execution (speculative-execution) attacks into the verified-crypto toolchain on which Dragonstar is built (HACL* or a successor provider), so that the implementation's leakage guarantees are no longer limited to the branch- and memory-access (secret-independence) model. This requires leakage models for these channels that are simultaneously sound with respect to real hardware behavior and amenable to machine-checked verification of the generated or hand-written code, together with countermeasures whose overhead preserves deployability.

  2. Protocol-level conformance: provide a full mechanized proof that the integrated implementation (hostap with the verified provider) implements the Dragonfly/SAE handshake exactly as specified — covering both the probabilistic hunting-and-pecking and the deterministic SSWU password derivations, the commit/confirm exchange, and the SAE-PT mode — against a formal model of the specification pinned to the relevant IEEE 802.11 clauses, so that higher-level protocol and integration bugs cannot remain outside the verified perimeter. Existing 2026 ProVerif/ASMETA models of the specification do not by themselves satisfy this, since the claim concerns the deployed implementation, not the specification.

  3. The library-API boundary: establish a systematic policy or verification tooling that guarantees secret independence of cryptographic library APIs (of the kind exposed by OpenSSL and wolfSSL) when called on secret-tainted values, resolving the current division of responsibility under which the libraries disclaim the leak and every caller must re-derive its own guarantees.

The three components share one scientific objective — closing the verified-but-insecure gap between what is proved (secret independence of isolated primitives) and what an attacker can reach (physical channels, the unverified protocol integration, and the unverified library boundary). A result on any one direction advances this objective but closes only one facet of the gap, and the objective is met only when all three are closed: direction 1, a verified-crypto toolchain whose machine-checked leakage guarantees for the provider extend beyond secret independence to fault-injection and transient-execution channels while its overhead preserves deployability; direction 2, a mechanized proof that the deployed hostap+provider implementation conforms to the pinned Dragonfly/SAE specification; direction 3, an enforceable policy or verification tooling that guarantees secret independence of cryptographic library APIs when called on secret-tainted values.

References

  1. Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan. 'From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake.' IEEE European Symposium on Security and Privacy (EuroS&P) 2023. DOI: 10.1109/EuroSP57164.2023.00048; arXiv:2307.09243. https://arxiv.org/abs/2307.09243
  2. Mathy Vanhoef, Eyal Ronen. 'Dragonblood: Analyzing the Dragonfly Handshake of WPA3 and EAP-pwd.' IEEE Symposium on Security and Privacy 2020. IACR ePrint 2019/383. https://eprint.iacr.org/2019/383
  3. Daniel De Almeida Braga, Pierre-Alain Fouque, Mohamed Sabt. 'Dragonblood is Still Leaking: Practical Cache-based Side-Channel in the Wild.' ACSAC 2020. DOI: 10.1145/3427228.3427295. https://doi.org/10.1145/3427228.3427295
  4. Shan Chen, Kaige Pan, Olga Sanina. 'Provable Security and Privacy Analysis of WPA3's SAE and SAE-PK Protocols.' IACR ePrint 2026/348. https://eprint.iacr.org/2026/348
  5. Roberto Metere, Mario Lilli, Luca Arnaboldi, Elvinia Riccobene. 'What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication.' arXiv:2603.23352. https://arxiv.org/abs/2603.23352
  6. Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya. 'Enforcing fine-grained constant-time policies.' IACR ePrint 2022/630. https://eprint.iacr.org/2022/630
  7. Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe. 'High-Assurance Cryptography in the Spectre Era.' IEEE Symposium on Security and Privacy 2021. DOI: 10.1109/SP40001.2021.00046. https://doi.org/10.1109/SP40001.2021.00046
  8. Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, Peter Schwabe. 'Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code.' IACR ePrint 2025/759. https://eprint.iacr.org/2025/759
  9. Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan. 'FaCT: a DSL for timing-sensitive computation.' PLDI 2019. DOI: 10.1145/3314221.3314605. https://doi.org/10.1145/3314221.3314605
  10. Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom. 'Spectre Declassified: Reading from the Right Place at the Wrong Time.' IACR ePrint 2022/426. https://eprint.iacr.org/2022/426
  11. Billy Bob Brumley. 'SoK: The Constant Time Model.' IACR ePrint 2026/1242. https://eprint.iacr.org/2026/1242
  12. Marcel Fourné, Daniel De Almeida Braga, Jan Jancar, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar. '"These results must be false": A usability evaluation of constant-time analysis tools.' USENIX Security Symposium 2024. https://www.usenix.org/conference/usenixsecurity24/presentation/fourne (HAL: hal-04712302, https://inria.hal.science/hal-04712302)
  13. Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar. 'They're not that hard to mitigate: What Cryptographic Library Developers Think About Timing Attacks.' GI Sicherheit 2024. DOI: 10.18420/sw2024_47. https://doi.org/10.18420/sw2024_47 (resolving record: https://dl.gi.de/items/c42b10ba-2380-400c-8457-7c56bdd9962b; HAL: https://hal.science/hal-04832863)
  14. Jukka Ruohonen. 'SoK: The Design Paradigm of Safe and Secure Defaults.' Journal of Information Security and Applications, 2025. arXiv:2412.17329; DOI: 10.1016/j.jisa.2025.103989. https://arxiv.org/abs/2412.17329