Mohit Kumar Jangid (The Ohio State University), Yue Zhang (Computer Science & Engineering, Ohio State University), Zhiqiang Lin (The Ohio State University)

Bluetooth is a leading wireless communication technology used by billions of Internet of Things (IoT) devices today. Its ubiquity demands systematic security scrutiny. A key ingredient in Bluetooth security is secure pairing, which includes Numeric comparison (NC) and Passkey Entry (PE). However, most prior formal efforts have considered only NC, and PE has not yet been formally studied in depth. In this paper, we propose a detailed formal analysis of the PE protocol. In particular, we present a generic formal model, built using Tamarin, to verify the security of PE by precisely capturing the protocol behaviors and attacker capabilities. Encouragingly, it rediscovers three known attacks (confusion attacks, static passcode attacks, and reflection attacks), and more importantly, also uncovers two new attacks (group guessing attacks and ghost attacks) spanning across diverse attack vectors (e.g., static variable reuse, multi-threading, reflection, human error, and compromise device). Finally, after applying fixes to each vulnerability, our model further proves the confidentiality and authentication properties of the PE protocol using an inductive base model.

View More Papers

Hope of Delivery: Extracting User Locations From Mobile Instant...

Theodor Schnitzler (Research Center Trustworthy Data Science and Security, TU Dortmund, and Ruhr-Universität Bochum), Katharina Kohls (Radboud University), Evangelos Bitsikas (Northeastern University and New York University Abu Dhabi), Christina Pöpper (New York University Abu Dhabi)

Read More

Cyber Threat Intelligence for SOC Analysts

Nidhi Rastogi, Md Tanvirul Alam (Rochester Institute of Technology)

Read More

Reminding Drivers of the Stalking Vehicles on the Road

Wei Sun, Kannan Srinivsan (The Ohio State University)

Read More

Cryptographic Oracle-based Conditional Payments

Varun Madathil (North Carolina State University), Sri Aravinda Krishnan Thyagarajan (NTT Research), Dimitrios Vasilopoulos (IMDEA Software Institute), Lloyd Fournier (None), Giulio Malavolta (Max Planck Institute for Security and Privacy), Pedro Moreno-Sanchez (IMDEA Software Institute)

Read More