Talk by Ross Horne (University of Strathclyde, Glasgow, Scotland)
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. Eavesdroppers can pick up that information 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 these privacy problems and released, in 2022, a new EMV protocol that addresses (without proof) the first but not the second of these threats to privacy.
I explain how we have designed 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. I touch on how compositional reasoning can help simplify some unlinkability proofs.