Formal analysis of authentication in bluetooth device pairing

Abstract

Bluetooth is a popular standard for short-range wireless com- munications. Bluetooth device pairing enables two mobile devices to au- thenticate each other and establish a secure wireless connection. We present a formal analysis of authentication properties of Bluetooth device pairing. Using the ProVerif cryptographic protocol verifier, we first analyze the standard device pairing protocol specified in the Bluetooth Core Specification, which relies on short, low-entropy PINs for authenti- cation. Our analysis confirms a previously known attack guessing attack. We then analyze a recently proposed Simple Pairing protocol. Simple Pairing involves Diffie-Hellman-based key establishment, in which au- thentication relies on a human visual channel: owner(s) of the mobile devices confirm the established keys by manually comparing the respec- tive hash values of the parameters used to generate each key, as displayed on the devices’ screens. This form of authentication presents an interest- ing modeling challenge.We demonstrate how to formalize it in ProVerif. Our analysis shows that authentication can fail when the same device is involved in concurrent Simple Pairing sessions. We discuss the implica- tions of this authentication failure for typical Bluetooth usage scenarios. We then refine our model to incorporate session identifiers, and prove that the authentication properties of Simple Pairing hold in the new model. Out-of-band human verification based on image- or audio-matching is increasingly used for authentication of mobile devices. This study is the first step towards automated analysis of formal models of human- authenticated protocols.