Distance-bounding protocols are cryptographic protocols that securely establish an upper bound on the physical distance between the participants.
Existing symbolic verification frameworks for distance-bounding protocols consider timestamps and the location of agents.
In this work we introduce a causality-based characterization of secure distance-bounding that discards the notions of time and location.
This allows us to verify the correctness of distance-bounding protocols with standard protocol verification tools. That is to say, we provide the first fully automated verification framework for distance-bounding protocols.
By using our framework, we confirmed known vulnerabilities in a number of protocols and discovered unreported attacks against two recently published protocols.
Dr. Rolando Trujillo is a Lecturer in Cyber Security at Deakin University.
He completed a Masters and PhD in Computer Engineering from Rovira i Virgili University, and shortly after joined the University of Luxembourg as a Postdoctoral researcher.
His research interests span the areas of formal methods, computer security and privacy protection.
His work has been published in highly competitive journals and conference proceedings in computer security, such as IEEE S&P, Euro S&P, and ESORICS.