The Community for Technology Leaders
(2018)
to
ISSN:
ISBN:
pp: 152-169
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
ABSTRACT
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.
INDEX TERMS
CITATION
REFERENCES
(Ver 3.3 (11022016))