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

BARS: Local Robustness Certification for Deep Learning based Traffic...

Kai Wang (Tsinghua University), Zhiliang Wang (Tsinghua University), Dongqi Han (Tsinghua University), Wenqi Chen (Tsinghua University), Jiahai Yang (Tsinghua University), Xingang Shi (Tsinghua University), Xia Yin (Tsinghua University)

Read More

PISE: Protocol Inference using Symbolic Execution and Automata Learning

Ron Marcovich, Orna Grumberg, Gabi Nakibly (Technion, Israel Institute of Technology)

Read More

HeteroScore: Evaluating and Mitigating Cloud Security Threats Brought by...

Chongzhou Fang (University of California, Davis), Najmeh Nazari (University of California, Davis), Behnam Omidi (George Mason University), Han Wang (Temple University), Aditya Puri (Foothill High School, Pleasanton, CA), Manish Arora (LearnDesk, Inc.), Setareh Rafatirad (University of California, Davis), Houman Homayoun (University of California, Davis), Khaled N. Khasawneh (George Mason University)

Read More

On the Feasibility of Profiling Electric Vehicles through Charging...

Ankit Gangwal (IIIT Hyderabad), Aakash Jain (IIIT Hyderabad) and Mauro Conti (University of Padua)

Read More