Computational and symbolic analysis of distance-bounding protocols

Contactless technologies are gaining more popularity everyday. Credit cards enabled with contactless payment, smart cards for transport ticketing, NFC-enabled mobile phones, and e-passports are just a few examples of contactless devices we are familiar with nowadays. Most secure systems meant for these devices presume physical proximity between the device and the reader terminal, due to their short communication range. In theory, a credit card should not be charged of an on-site purchase if the card is not up to a few centimeters away from the payment terminal. In practice, this is not always true. Indeed, some contactless payment protocols, such as Visa's payWave, have been shown vulnerable to relay attacks. In a relay attack, a man-in-the-middle uses one or more relay devices in order to make two distant devices believe they are close. Relay attacks have been implemented also to bypass keyless entry and start systems in various modern cars.

Relay attacks can be defended against with distance-bounding protocols, which are security protocols that measure the round-trip times of a series of challenge/response rounds in order to guarantee physical proximity. A large number of these protocols have been proposed and more sophisticated attacks against them have been discovered. Thus, frameworks for systematic security analysis of these protocols have become of high interest. As traditional security models, distance-bounding security models sit within the two classical approaches: the computational and the symbolic models. In this thesis we propose frameworks for security analysis of distance-bounding protocols, within the two aforementioned models.

First, we develop an automata-based computational framework that allows us to generically analyze a large class of distance-bounding protocols. Not only does the proposed framework allow us to straightforwardly deliver computational (in)security proofs but it also permits us to study problems such as optimal trade-offs between security and space complexity. Indeed, we solve this problem for a prominent class of protocols, and propose a protocol solution that is optimally secure amongst space-constrained protocols within the considered class.

Second, by building up on an existing symbolic framework, we develop a causality-based characterization of distance-bounding security. This constitutes the first symbolic property that guarantees physical proximity without modeling continuous time or physical location. We extend further our formalism in order to capture a non-standard attack known as terrorist fraud. By using our definitions and the verification tool Tamarin, we conduct a security survey of over 25 protocols, which include industrial protocols based on the ISO/IEC 14443 standard such as NXP's MIFARE Plus with proximity check and Mastercard's PayPass payment protocol. For the industrial protocols we find attacks, propose fixes and deliver security proofs of the repaired versions.