Security analysis of Bluetooth Secure Simple Pairing protocols with extended threat model

Today, Bluetooth technology has become the primary means of short-distance. In the Bluetooth protocol stack, the Secure Simple Pairing (SSP) specifies three methods to provide authentication, Out-of-Band, Numeric Comparison, and Passkey Entry. All three schemes require extra or additional channel assistance in addition to the Bluetooth wireless channel during the authentication process. At the same time, attacks against the Bluetooth pairing protocol have gradually increased, and some attacks (e.g., Tap'n Ghost) targeting those extra channels have attracted the attention of the Bluetooth Association. Current attacks place new demands on Bluetooth SSP security and thus require new models to formalize these threats. Troncoso and Hale proposed the CYBORG model to address this challenge by modeling the channel between users and devices in detail and defining rich attacker capabilities and freshness rules. They also proposed an improved Passkey Entry protocol, Dual-Passkey Entry. However, the CYBORG model does not cover current attacks and threats as they claim, and it only focused on the Passkey Entry protocol. We formalized the threat models to clarify and bridge the gaps in the protocol design and practical requirements of the original CYBORG model. Attackers of Confidential -and Authenticated-extra channels are designed to deal with the settings in threats and protocol requirements. The analysis results show weaknesses and insecurities of SSP protocols.