WCDCAnalyzer: Scalable Security Analysis of Wi-Fi Certified Device Connectivity Protocols

WCDCAnalyzer: Scalable Security Analysis of Wi-Fi Certified Device Connectivity Protocols

Speakers: Zilin Shen

Conference: NDSS Symposium 2026

YouTube: https://www.youtube.com/watch?v=wESDCwLqw1A

Overview

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.

Background

▶ Watch: State explosion problem: 2TB RAM insufficient for Wi-Fi Direct verification (1:30)

Wi-Fi device connectivity protocols serve as the foundation for all subsequent Wi-Fi communication by handling initial device pairing and connection setup. Wi-Fi Direct enables peer-to-peer connections without a router, supported on billions of Android and Linux devices. Wi-Fi Easy Connect provides secure device onboarding using QR code scanning, commonly used in IoT deployments. Wi-Fi Easy Mesh supports multi-access-point home networks for extended Wi-Fi coverage.

Formal verification using tools like Tamarin can mathematically prove security properties (secrecy, authentication, privacy) or find counterexamples that reveal vulnerabilities. However, Tamarin faces a fundamental limitation with large protocols: the state explosion problem. Each new message sent to the public channel creates new states, and the state space grows exponentially with the number of messages and terms. Wi-Fi device connectivity protocols send more than 50 terms to the public channel, making direct verification infeasible. The researchers attempted to verify Wi-Fi Direct directly on a server with 2 terabytes of RAM, but Tamarin exhausted all available memory after hours of execution.

Key Findings

▶ Watch: Soundness preservation with disjoint cryptographic primitives (5:30)

The WCDCAnalyzer framework uncovered 10 new vulnerabilities across the three protocols:

Wi-Fi Direct (5 vulnerabilities): The most severe is D1, a downgrade authentication bypass. The root cause is that Wi-Fi Direct supports two configuration modes, with push-button being less secure, and the protocol design does not protect the configuration mode field. An attacker can sniff the device name from a legitimate device's probe request, then impersonate that device to trick the registrar into using the weaker push-button configuration, bypassing authentication entirely.

Wi-Fi Easy Connect (vulnerabilities including privacy leakage): The bootstrapping key is exposed in plaintext, allowing an attacker to detect device presence by sending probe messages and observing responses, enabling device tracking.

Wi-Fi Easy Mesh (vulnerabilities including privacy leakage): Similar privacy issues including unique device ID leakage transmitted in plaintext without rotation, persisting for over a day and enabling device tracking.

All 10 vulnerabilities were validated on commercial devices including OnePlus phones, various network cards, and IoT development boards, and reported to vendors and the Wi-Fi Alliance.

Technical Deep Dive

▶ Watch: 10 new vulnerabilities found across all three protocols (8:00)

WCDCAnalyzer operates in four stages: specification analysis, decomposition, compositional verification, and adversary testing.

Specification Analysis: The researchers analyzed over 1,000 pages of protocol documentation to build protocol state machines and define security properties (secrecy, authentication, privacy, executability).

Automatic Decomposition: The key observation is that wireless protocols typically run in sequential phases -- discovery, then negotiation, then provisioning -- where one phase completes before the next begins. The protocol is modeled as a directed graph (state machine), and the Strongly Connected Components (SCC) algorithm identifies sequential boundaries, automatically partitioning the protocol into sub-protocols. For Wi-Fi Direct, this produces two sub-protocols: P1 (discovery) and P2 (provisioning).

Soundness Preservation: The theoretical basis for compositional reasoning requires that sub-protocols use disjoint cryptographic primitives. If each sub-protocol uses different cryptographic functions, then security of the whole protocol follows from security of each sub-protocol. For shared terms between sub-protocols (e.g., device info, group ID), an interface mechanism transfers information while maintaining attacker knowledge consistency: if a term is secret in P1, it is treated as a fresh value in P2; if it is public in P1, it is sent to the public channel in P2's interface.

Security Property Decomposition: Global properties defined over the entire protocol must also be decomposed into local properties for each sub-protocol. The key guarantee is that a global property holds if and only if all corresponding local properties hold, ensuring no attacks are missed by the decomposition.

Scalability Results: Without decomposition, verification on a 256 GB machine is killed due to memory exhaustion. With decomposition, verification completes successfully on the same hardware.

Demo / Proof of Concept

▶ Watch: Privacy leakage: plaintext UIDs and bootstrapping key exposure (10:00)

The most severe vulnerability -- the Wi-Fi Direct downgrade authentication bypass -- was demonstrated on commercial devices. An attacker using a Linux laptop was able to impersonate a OnePlus phone during the connection setup, with the invitation appearing to come from the legitimate device. The attack flow is: (1) attacker passively sniffs probe requests to learn the target device name, (2) attacker sends a probe request using the stolen device name, (3) the registrar cannot distinguish the attacker from the legitimate device, (4) the attacker triggers push-button configuration (less secure), (5) the attacker bypasses authentication and connects. Privacy leakage vulnerabilities were validated through passive sniffing, demonstrating that unique device IDs and bootstrapping keys are transmitted in plaintext, enabling device tracking without any active attack.

Defensive Implications

▶ Watch: Real-world validation on commercial phones and IoT devices (11:30)

For Wi-Fi device manufacturers and the Wi-Fi Alliance, the authentication bypass in Wi-Fi Direct is a serious finding affecting billions of deployed devices. The fix requires specification-level changes -- protecting the configuration mode field from downgrade -- which the Wi-Fi Alliance has committed to addressing in the next specification version.

For enterprise security teams, Wi-Fi Direct is enabled by default on most Android devices and many Linux systems. The device tracking vulnerabilities (plaintext UIDs, non-rotating identifiers) are particularly relevant for organizations concerned about employee location tracking or device enumeration in their facilities.

For the formal verification community, WCDCAnalyzer demonstrates that automatic protocol decomposition using SCC-based partitioning can make formal analysis of large real-world protocols feasible. The framework and models are available on GitHub for others to apply to similar large protocol specifications.

For IoT deployments using Wi-Fi Easy Connect, the bootstrapping key exposure means that device presence detection is possible without any authentication, potentially enabling physical security reconnaissance.

Key Takeaways

• Wi-Fi device connectivity protocols (Direct, Easy Connect, Easy Mesh) had 10 previously unknown vulnerabilities
• The most severe is a downgrade authentication bypass in Wi-Fi Direct exploitable through device name impersonation
• Automatic protocol decomposition using SCC algorithms enables formal verification of protocols too large for standard tools
• Privacy leakage in all three protocols enables device tracking through plaintext UIDs and bootstrapping keys
• All vulnerabilities validated on commercial devices and reported to the Wi-Fi Alliance
• Framework and Tamarin models are open-source on GitHub
• The Wi-Fi Alliance will address findings in the next specification version

About the Speaker(s)

Zilin Shen is a researcher at Purdue University, mentored by Professor Mateus Karim and advised by Professor Elisa Bertino. The research combines formal methods expertise with practical wireless protocol security, and the team has produced both theoretical contributions in compositional verification and practical vulnerability findings validated on commercial hardware.