Contactless Payments made Private via Bisimilarity
Ross Horne ( University of Strathclyde, Glasgow (Scotland) )
- 14:00 22nd January 2024 ( week 2, Hilary Term 2024 )Tony Hoare room
The EMV (Europay, Mastercard & Visa) protocol standardises how cards talk to payment terminals. The protocol that your card currently uses almost certainly broadcasts transaction details including personally identifying information during transactions. That information can be picked up on the air within a range of 20 meters. Furthermore, a device closer to your card can power it up and enter a session that also reveals personally identifying information even if the card is not involved in a transaction with a merchant. EMVco have been aware of this problem and released, in 2022, a new EMV protocol that addresses (without proof) the first but not the second of these threats to privacy.
We explain how to design a still tighter protocol than the latest incarnation of EMV. Our protocol satisfies the strong privacy property unlinkability that counters both threats described above, as well as improving data minimisation (and hence data protection) within payment systems. Unlinkability is formulated as a behavioural equivalence problem and is proven by providing, by hand, a rather large bisimulation relation. We explain that, by exploiting some compositional reasoning, part of the protocol can be proven using automated equivalence checkers such as recent extensions to ProVerif.
Share this:
