Formal Analysis and Patching of BLE-SC Pairing

Bluetooth Low Energy (BLE) is the mainstream Bluetooth standard and BLE Secure Connections (BLC-SC) pairing is a protocol that authenticates two Bluetooth devices and derives a shared secret key between them. Although BLE-SC pairing employs well-studied cryptographic primitives to guarantee its security, a recent study revealed a logic flaw in the protocol.

In this paper, we develop the first comprehensive formal model of the BLE-SC pairing protocol. Our model is compliant with the latest Bluetooth specification version 5.3 and covers all association models in the specification to discover attacks caused by the interplay between different association models. We also partly loosen the perfect cryptography assumption in traditional symbolic analysis approaches by designing a low-entropy key oracle to detect attacks caused by the poorly derived keys. Our analysis confirms two existing attacks and discloses a new attack. We propose a countermeasure to fix the flaws found in the BLE-SC pairing protocol and discuss the backward compatibility. Moreover, we extend our model to verify the countermeasure, and the results demonstrate its effectiveness in our extended model.

Keyboard Input z KeyboardDisplay KeyboardOnly Yes-No Input

DisplayOnly NoInputNoOutput

x: Device has the ability to display a 6-digit number. y: Device does not have the ability to display a 6-digit number. z: Device has a numeric keyboard that can input the digits '0' to '9' and a confirmation. : Device has the ability to indicate "yes" and "no". |: Device does not have the ability to indicate "yes" or "no".

This phase aims to determine the parameters used in the subsequent phases. It can be invoked by the initiating device sending a pairing request or the responding device sending a security request. The following four fields are important to our model. They are sent by the initiating/responding device in the pairing request/response.

• IOCap: This field indicates the specification-defined IO capability used in the LTK generation phase. The Bluetooth specification defines five IO capabilities of the device, as shown in Table 1.

• OOB: This field indicates whether the device has received authentication data using Out-Of-Band (OOB) capabilities, i.e., IO capabilities that are not defined in the specification.

• MITM: This field indicates whether the device requires preventing Man-In-The-Middle (MITM) attacks.