WCDCAnalyzer: Scalable Security Analysis of Wi-Fi Certified Device Connectivity Protocols
Zilin Shen
Network and Distributed System Security (NDSS) Symposium 2026 · Day 3 · Connectivity & Privacy
The **Wi-Fi Alliance's device connectivity protocols** -- **Wi-Fi Direct**, **Wi-Fi Easy Connect**, and **Wi-Fi Easy Mesh** -- handle the critical initial pairing and connection setup for billions of devices across Android, Linux, and IoT systems. Yet while Wi-Fi security research has extensively studied **WPA2** and **WPA3** access protection, these device connectivity protocols have remained largely unstudied from a formal security perspective. This talk presents **WCDCAnalyzer**, a formal verification framework that overcomes the **state explosion problem** that prevents standard tools like **Tamarin** from handling these complex protocols. Using automatic protocol decomposition with compositional verification, the framework identified **10 new vulnerabilities** across all three protocols, including a severe **downgrade authentication bypass** in Wi-Fi Direct that allows an attacker to impersonate a legitimate device. All vulnerabilities were validated on commercial devices and reported to vendors and the Wi-Fi Alliance, which will address them in the next specification version.
AI review
A formal verification framework that scales to analyze large Wi-Fi device connectivity protocols, uncovering 10 vulnerabilities including a downgrade authentication bypass in Wi-Fi Direct affecting billions of devices. The automatic decomposition technique is a genuine contribution, and the vulnerabilities are validated on commercial hardware.