Security Analysis and Implementation of Relay-Resistant Contacless Payments
Ioana Boureanu,
Tom Chothia,
Alexandre Debant,
and Stéphanie Delaune
Abstract
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
We provide three files:
- payBCR.pv: models the PayBCR protocol as described in Figure 1 in the submitted paper;
- payBCR-.pv: models the PayBCR protocol with indistinguishable certificates for cards and TPMs;
- payCCR++.pv: models the PayCCR++ protocol which is a slightly modified version of the PayCCR protocol in which the TPM identity and the two timestamps are added in the AC message (as described in Section 4.3).
| Protocols |
Role authentication |
Time-bound authentication |
Causality-based security |
| PayCCR++ |
✗ |
✓ |
✓ |
| PayBCR- |
✗ |
✓ |
✓ |
| PayBCR |
✓ |
✓ |
✓ |
Results of the analyses
(✗: attack found, ✓: proved secure)
Implementations
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:
RelayBox-apks.zip
Here is the source code of our relay box implementation:
RelayBox-Src.zip
Then we provide several log files illustrating the following scenarios:
- a full execution of the PayPass protocol with an honest PayPass reader:
paypass.log
- a full execution the PayPass-RRP protocol with an honest PayPass-RRP reader:
honest-rrp.log
- a full execution PayBCR protocol with an honest PayBCR reader:
honest-paybcr.log
- a full execution the PayPass-RRP protocol with a timing-rogue PayPass-RRP reader:
timing-rogue-rrp.log
- a full execution PayBCR protocol with an timing-rogue PayBCR reader:
timing-rogue-paybcr.log
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
Homepage