Formal Analysis of BLE Secure Connection Pairing and Revelation of the PE Confusion Attack

Formal Analysis of BLE Secure Connection Pairing and Revelation of the PE Confusion Attack

Speakers: Min Shi

Conference: NDSS Symposium

YouTube: https://www.youtube.com/watch?v=gkpd-UPXT78

Overview

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.

The vulnerability affects all susceptible pairing cases from Bluetooth 4.2 through the latest version 6.0 and was successfully validated on mainstream Android devices including the Pixel 4, Samsung Galaxy S10, Vivo iQOO, and Redmi K40. The Bluetooth SIG acknowledged the finding in February 2025. The researchers from the University of Washington verified 84 security properties across 84 distinct pairing scenarios using a distributed verification framework, providing the most comprehensive formal analysis of BLE pairing to date.

Background

▶ Watch: BLE Secure Connections overview and the three-phase pairing process (0:00)

BLE is projected to reach 7.37 billion device shipments annually by 2027, protecting sensitive data from keyboard inputs to health information. Bluetooth version 4.2 introduced Secure Connections (SC) mode, replacing the legacy short-term key mechanism with ECDH-based key exchange.

The BLE SC pairing protocol operates in three phases:

1. Pairing feature exchange: Devices negotiate IO capabilities, MITM protection requirements, out-of-band data availability, and encryption key size, which collectively determine the association model
2. IOTK generation: ECDH key exchange, followed by one of four association models (Just Works, Numeric Comparison, Passkey Entry, or Out-of-Band), then authorization verification using MAC key derivation and confirmation values
3. Specific key distribution: Additional keys distributed over the encrypted channel

Previous formal analyses have fallen short due to three challenges: the complex protocol stack (host/controller separation via HCI interface), the dynamic association model selection logic (table-driven based on both parties' IO capabilities), and unrealistic user behavior assumptions (assuming perfect randomness in pin selection).

Key Findings

▶ Watch: Why previous formal analyses fell short: three challenges (4:00)

Passkey Entry Confusion Attack discovered: A man-in-the-middle attack where the adversary tampers with the IO capability field during initial feature exchange, tricking the two devices into entering different pairing modes. The initiator believes it's in PE mode (responder displays, initiator inputs), while the responder believes it's in the opposite PE mode (initiator displays, responder inputs). The user, seeing two devices both prompting for input, mistakenly assumes both-input PE2 mode and enters the same PIN on both devices.

Two concrete attack variants:

1. Weak passkey exploitation: Users often choose simple numbers like 123456 or 000000, and research shows some Android UIs can mislead users toward simple codes. The adversary can brute-force at extremely low cost.
2. Pin reuse exploitation: If the user reuses the same PIN across sessions, the adversary can disrupt one pairing session, exploit a computational logic flaw to recover the PIN, then perform a full MITM hijack when the user retries with the same PIN.

Affects Bluetooth 4.2 through 6.0: Because the vulnerability is rooted in protocol logic, not implementation errors, it affects all BLE versions with Secure Connections.

Validated on mainstream devices: Pixel 4, Samsung Galaxy S10, Vivo iQOO, and Redmi K40 all confirmed vulnerable.

84 security properties verified across 84 scenarios: The most comprehensive formal analysis of BLE pairing, identifying the strongest attacker model each pairing scenario can tolerate. Notable finding: bidirectional OOB pairing retains security even when OOB channel confidentiality is compromised.

Security degrades rapidly with non-ideal user behavior: When users deviate from perfect assumptions (reusing PINs, choosing guessable numbers), security degrades significantly across most pairing scenarios.

Technical Deep Dive

▶ Watch: Security assumptions: user behavior and channel integrity (8:00)

The formal model introduced two key separations:

Host-Controller Decomposition: Each device is modeled as three distinct components: host, controller, and HCI interface. This enables modeling a stronger adversary capable of eavesdropping on or compromising the internal HCI channel -- a threat previous monolithic models could not represent.

State Machine Extraction: Separate state machines for the initiator host, responder host, and controller were extracted from the official Bluetooth Core Specification, serving as blueprints for the formal model. Every protocol step is faithfully represented.

Association Model Selection Formalization: Two functions formalize the table-driven selection logic:

• selectAM: Selects the association model
• mapIOcapsToAM: Maps IO capabilities to association model

23 equational rules capture the semantics of the two lookup tables, with proven termination and correctness.

Security assumptions are organized into user assumptions and channel assumptions:

• UNR (User Not Reuse): User does not reuse six-digit passkeys across sessions
• UNG (User Not Guessable): User does not enter easily guessable passkeys
• UNC (User Not Confused): User does not confuse PE and numeric comparison interaction modes
• IOS (IO Secure): Adversary cannot control the IO channel
• HCIS (HCI Secure): Adversary cannot compromise the HCI channel
• OBS (OB Secure): Adversary cannot break the out-of-band channel

Distributed Verification Framework: Docker containerization on a server cluster enables parallel verification. A core verification strategy: if a property holds under a stronger attacker model, it holds under weaker models; if verification fails, attacker capabilities are iteratively relaxed to identify the minimum security assumptions.

PE Confusion Attack Mechanics: The adversary with no IO capability (display:NoInputNoOutput) tampers with the IO capability field during feature exchange. Device A thinks Device B can display (so A inputs), while Device B thinks A can display (so B inputs). Both devices prompt for PIN input. The user, expecting both-input mode, enters the same PIN on both -- but the protocol computes different security parameters because each side believes it's in a different PE variant.

Demo / Proof of Concept

▶ Watch: 84 security properties verified across 84 pairing scenarios (9:30)

The attack was validated on four mainstream Android devices: Pixel 4, Samsung Galaxy S10, Vivo iQOO, and Redmi K40. Two concrete exploitation scenarios were demonstrated:

1. Weak passkey scenario: Users choosing simple PINs (123456, 000000) allow the adversary to brute-force the passkey at minimal computational cost during the MITM attack
2. PIN reuse scenario: The adversary disrupts one pairing attempt, recovers the PIN through a computational logic flaw, then performs a full MITM hijack when the user retries with the same PIN

The formal model and proof-of-concept code are publicly available on GitHub.

Defensive Implications

▶ Watch: Validated on Pixel 4, Galaxy S10, and more -- Bluetooth SIG acknowledged (11:30)

The researchers propose three countermeasures:

Bind IO capabilities to confirmation computation: Mandate that the confirmation computation (specifically the f4 function) includes a hash of the pairing feature exchange messages. This prevents midway tampering with IO capability fields because any modification would cause confirmation verification to fail.

Standardize UI prompts: The Bluetooth SIG should require clear, unambiguous user prompts such as "Please operate on the other device only" to prevent confusion between PE modes. Current ambiguous prompts enable the confusion attack.

Disable dual-input mode: When both devices request manual passkey input, the configuration should be rejected by default rather than allowing the user to proceed with the potentially confused pairing.

For security teams managing Bluetooth-enabled device fleets, this research means that PE-based pairing is vulnerable to MITM attacks when users choose weak or reused PINs, which is a common real-world behavior. Until the Bluetooth specification is updated with the proposed countermeasures, organizations should prefer numeric comparison or out-of-band pairing modes where possible and educate users about the risks of simple or reused PINs.

Key Takeaways

• The Passkey Entry Confusion Attack is a MITM vulnerability embedded in the BLE Secure Connection protocol logic, affecting Bluetooth 4.2 through 6.0
• The attack exploits user confusion between PE modes when the adversary tampers with IO capability fields during feature exchange
• Validated on Pixel 4, Samsung Galaxy S10, Vivo iQOO, and Redmi K40 -- the vulnerability is universal, not implementation-specific
• The Bluetooth SIG acknowledged the finding in February 2025
• The formal model is the first to capture host-controller separation, enabling analysis of HCI-level adversaries
• 84 security properties verified across 84 scenarios provide the most comprehensive BLE pairing security analysis to date

About the Speaker(s)

Min Shi is a PhD candidate at the University of Washington who presented this work on behalf of the original authors, who could not attend due to visa issues. The formal model and proof-of-concept code are publicly available on GitHub. Contact information for the authors is available in the presentation slides.