Title:

Breaking and Fixing Modern Payment Protocols with Tamarin

 

Abstract:

The security of payment systems is critical, as their exploitation canlead to widespread, large-scale financial loss. We show how to useTamarin, a security protocol model checker, to find seriousexploitable vulnerabilities in the EMV payment protocols. EMV is theinternational protocol standard for smartcard payment that is used inover 9 billion payment cards worldwide. Despite the standard’sadvertised 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 ourmodel to automatically discover new flaws that lead to critical attacks onEMV. In particular, an attacker can use a victim's EMV card (e.g.,Mastercard or Visa Card) for high-valued purchases without the victimsPIN. Said more simply, the PIN on your EMV card is useless! Wedescribe these attacks, their repair, and more generally whyusing formal methods is essential for critical protocols like paymentprotocols.

 

Speaker:

Prof. Dr. David Basin

Head of Information Security Group
Department of Computer Science
ETH Zurich

 

Bio:

David Basin is a full professor of Computer Science at ETH Zurich. He received his Ph.D. in Computer Science from Cornell University in 1989 and his Habilitation in Computer Science from the University of Saarbrucken in 1996. From 1997–2002 he held the chair of Software Engineering at the University of Freiburg in Germany.
His research areas are Information Security and Software Engineering. He is the founding director of the ZISC, the Zurich Information SecurityCenter, which he led from 2003-2011. He served as Editor-in-Chief of the ACM Transactions on Privacy and Security (2015-2020) and ofSpringer-Verlag's book series on Information Security and Cryptography (2008-present). He is an IEEE Fellow and an ACMFellow.