DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SP.2018.00001
Sjouke Mauw , CSC/SnT, University of Luxembourg
Zach Smith , CSC, University of Luxembourg
Jorge Toro-Pozo , CSC, University of Luxembourg
Rolando Trujillo-Rasua , SnT, University of Luxembourg
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.