Distance bounding protocols constitute a special class of authentication protocol, in which participants must verify not only the identity of their partner, but also their physical location. They are important for systems such as contactless card payments or electronic doors, to avoid scenarios in which an attacker might relay messages over a longer distance than intended. This is typically achieved by using a time-sensitive challenge-response phase, where the verifying agent estimates distance by calculating the round trip time of their challenge messages. There are some difficulties in applying traditional security verification approaches to this family of protocols. Symbolic approaches, which aim to abstract away details (such as the nature of the cryptographic primitives used), must deal with the fact that many attack scenarios are intrinsically linked with the location and timing of messages.
In this talk, we present a model for analysing distance bounding protocols. The model of Basin et al., which uses a bespoke implementation in Isabelle/HOL, is adapted to remove speed-of-light calculations for message timings. Instead, a (provably) equivalent security claim is developed that instead focuses on the precise ordering of actions during a protocol execution. This approach enables an embedding into the Tamarin prover tool, allowing for rapid automated verification. Further, we discuss extensions to the model to analyse so-called "dishonest" agents -- who generally follow their specification but are willing to temporarily deviate in order to collaborate with the network adversary. Such agents are particularly relevant for modelling "Terrorist fraud" attacks, where an adversary can be (illegally) granted a one-time key. Finally, the results of an extensive literature survey is presented, discussing common pitfalls in protocol design.
Zach is a PhD candidate at the University of Luxembourg in the field of computer security. His focus is on the development of formal models for security protocols, in order to define precise security requirements. Research interests include security for RFID and IoT devices, as well as multiparty protocols. His other interests include game development, swing dance, and locking himself inside to write his PhD thesis.