2018 IEEE Symposium on Security and Privacy (SP) (2018)
San Fransisco, CA, US
May 21, 2018 to May 23, 2018
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.
distance-bounding, security-protocols, causality, formal-verification, automatic-verification
S. Mauw, Z. Smith, J. Toro-Pozo and R. Trujillo-Rasua, "Distance-Bounding Protocols: Verification without Time and Location," 2018 IEEE Symposium on Security and Privacy (SP), San Fransisco, CA, US, , pp. 152-169.