Security Analysis and Implementation of Relay-Resistant Contacless Payments

Ioana Boureanu, Tom Chothia, Alexandre Debant, and Stéphanie Delaune

Download: [pdf]


Contactless systems, such as the EMV (Europay, Mastercard and Visa) payment protocol, are vulnerable to relay attacks. The typical countermeasure to this relies ondistance bounding protocols, in which a reader estimates an upper bound on its physical distance from a card by doing round-trip time (RTT) measurements. However, these protocols are trivially broken in the presence of rogue readers. At Financial Crypto 2019, we proposed two novel EMV- based relay-resistant protocols: they integrate distance-bounding with the use of hardware roots of trust (HWRoT) in such a way that correct RTT-measurements can no longer be bypassed.
Our contributions are threefold: first, we design a calculus to model this advanced type of distance-bounding protocols integrated with HWRoT; as an additional novelty, our calculus is also the first to allow for mobility of cards and readers during a proximity-checking phase. Second, to make it possible to analyse these protocols via more standard mechanisms and tools, we consider a 2018 characterisation of distance-bounding security that does away with physical aspects and relies only on the causality of events; we cast it in our richer calculus and extend its theoretical guarantees to our more expressive models (with mobility, potentially rogue readers, and HWRoT). Due to this extension, we can carry out the security analysis in the standard protocol verification tool ProVerif. Third, we provide the first implementation of Mastercard's relay-resistant EMV protocol PayPass-RRP as well as one of its 2019 extension with HWRoT called PayBCR. We evaluate their efficiency and their robustness to relay attacks, in presence of both honest and rogue readers. Our experiments are the first to show that Mastercard's PayPass-RRP and its HWRoT-based extension PayBCR are both practical in preventing relay attacks of the magnitude shown thus-far in EMV.

Symbolic verification using the ProVerif tool

The verifications have been performed using ProVerif 2.00. All the information about this tool are abailable at:

We provide three files:
Protocols Role authentication Time-bound authentication Causality-based security
Results of the analyses
(✗: attack found, ✓: proved secure)


The following links gather all the material and logs used to obtain the results presented in Section 5 of the paper.

We provide an archive that contains the Android APKs and server-side code of our relay "box" + setup/run instructions here:

Here is the source code of our relay box implementation:

Then we provide several log files illustrating the following scenarios: Finally, more EMV-C2-specific details w.r.t. the time measurements, gathered with our CardCracker-based implementation and added to Table 1 can be found at: timings.pdf