Distance-Bounding Protocols: Verification without Time and Location

Distance-bounding protocols are cryptographic protocols

that securely establish an upper bound on the physi-
cal 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 correct-
ness of distance-bounding protocols with standard pro-
tocol verification tools. That is to say, we provide the

first fully automated verification framework for distance-
bounding protocols. By using our framework, we con-
firmed known vulnerabilities in a number of protocols

and discovered unreported attacks against two recently
published protocols.