Ksenia Budykho (Surrey Centre for Cyber Security, University of Surrey, UK), Ioana Boureanu (Surrey Centre for Cyber Security, University of Surrey, UK), Steve Wesemeyer (Surrey Centre for Cyber Security, University of Surrey, UK), Daniel Romero (NCC Group), Matt Lewis (NCC Group), Yogaratnam Rahulan (5G/6G Innovation Centre - 5GIC/6GIC, University of Surrey, UK), Fortunat Rajaona (Surrey Centre for Cyber Security, University of Surrey, UK), Steve Schneider (Surrey Centre for Cyber Security, University of Surrey, UK)

We introduce a new framework, TrackDev, for encoding and analysing the tracing or "tracking" of an entity (e.g., a device) via its executions of a protocol or its usages of a system. TrackDev considers multiple dimensions combined: whether the attacker is active or passive, whether an entity is trackable in its every single appearances or just in a compound set thereof, and whether the entity can be explicitly or implicitly identified. TrackDev can be applied to most identification-based systems. TrackDev is to be applied in practice, over actual executions of systems; to this end, we test TrackDev on real-life traffic for two well-known protocols, the LoRaWAN Join and the 5G handovers, showing new trackability attacks therein and proposing countermeasures. We study the strength of TrackDev's various trackability properties and show that many of our notions are incomparable amongst each other, thus justifying the fine-grained nature of TrackDev. Finally, we detail how the main thrust of TrackDev can be mechanised in formal-verification tools, without any loss; we exemplify this fully on the LoRaWAN Join, in the Tamarin prover. In this process, we also uncover and discuss within two important aspects: (a) TrackDev’s separation between "explicit" and "implicit" trackability offers new formal-verification insights; (b) our analyses of the LoRaWAN Join protocol in Tamarin against TrackDev as well as against existing approximations of unlinkability by Baelde et al. concretely show that the latter approximations can be coarser than our notions.

View More Papers

InfoMasker: Preventing Eavesdropping Using Phoneme-Based Noise

Peng Huang (Zhejiang University), Yao Wei (Zhejiang University), Peng Cheng (Zhejiang University), Zhongjie Ba (Zhejiang University), Li Lu (Zhejiang University), Feng Lin (Zhejiang University), Fan Zhang (Zhejiang University), Kui Ren (Zhejiang University)

Read More

Faster Secure Comparisons with Offline Phase for Efficient Private...

Florian Kerschbaum (University of Waterloo), Erik-Oliver Blass (Airbus), Rasoul Akhavan Mahdavi (University of Waterloo)

Read More

Ghost Domain Reloaded: Vulnerable Links in Domain Name Delegation...

Xiang Li (Tsinghua University), Baojun Liu (Tsinghua University), Xuesong Bai (University of California, Irvine), Mingming Zhang (Tsinghua University), Qifan Zhang (University of California, Irvine), Zhou Li (University of California, Irvine), Haixin Duan (Tsinghua University; QI-ANXIN Technology Research Institute; Zhongguancun Laboratory), Qi Li (Tsinghua University; Zhongguancun Laboratory)

Read More

Evasion Attacks and Defenses on Smart Home Physical Event...

Muslum Ozgur Ozmen (Purdue University), Ruoyu Song (Purdue University), Habiba Farrukh (Purdue University), Z. Berkay Celik (Purdue University)

Read More