Formal analysis of authentication in bluetooth device pairing

  • Chang R
  • Shmatikov V
  • 23


    Mendeley users who have this article in their library.
  • N/A


    Citations of this article.


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.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

There are no full text links


  • Richard Chang

  • Vitaly Shmatikov

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free