Formal Analysis of BLE Secure Connection Pairing and Revelation of the PE Confusion Attack
Min Shi
Network and Distributed System Security (NDSS) Symposium 2026 · Day 2 · Program Analysis
This talk presents the first fine-grained formal analysis of **Bluetooth Low Energy (BLE) Secure Connection pairing** that captures the host-controller separation architecture, and reveals the **Passkey Entry (PE) Confusion Attack** -- a man-in-the-middle vulnerability embedded in the protocol logic itself. The attack exploits the fact that users can be confused between passkey entry modes, tricking two devices into executing different pairing modes while the user assumes they are both in the same mode.
AI review
A rigorous formal analysis that discovers a real protocol-level MITM vulnerability in BLE Secure Connections affecting Bluetooth 4.2 through 6.0. The PE Confusion Attack exploits a fundamental design flaw in how IO capabilities are negotiated, not an implementation bug. Validated on mainstream Android devices, acknowledged by Bluetooth SIG. The host-controller decomposition in the formal model is the right approach, and 84 verified security properties provide comprehensive coverage.