Metadata only
Author
Date
2023-07Type
- Conference Paper
ETH Bibliography
yes
Altmetrics
Abstract
We report on experience using Tamarin, a security protocol model checker, to find numerous, serious exploitable vulnerabilities in EMV payment protocols. EMV is the international protocol standard for smartcard payment that is used in over 9 billion payment cards worldwide. Despite the standard’s advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV’s lengthy and complex specification, running over 2,000 pages. We have formalized a comprehensive model of EMV in Tamarin. We use our model to automatically discover new flaws that lead to critical attacks on EMV. In particular, an attacker can use a victim’s EMV card (e.g., Mastercard or Visa Card) for high-valued purchases without the victim’s PIN. We describe these attacks, their repair, and more generally why using formal methods is essential for critical protocols like payment protocols. Show more
Publication status
publishedExternal links
Book title
ASIA CCS '23: Proceedings of the 2023 ACM Asia Conference on Computer and Communications SecurityPages / Article No.
Publisher
Association for Computing MachineryEvent
Subject
verification; model checking; security protocols; EMVMore
Show all metadata
ETH Bibliography
yes
Altmetrics