Prof. Dr. David Basin
Professor ETH Zurich
29th November 2022, 1:00pm - 2:00pm (GST)
Using Formal Methods to Analyze Modern Payment Protocols
As a case study on the use of formal methods for security we show how to use Tamarin, a security protocol model checker, to find serious exploitable vulnerabilities in the 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.
David Basin is a full professor of Computer Science at ETH Zurich, since 2003. His research areas are Information Security and Software Engineering. He is the founding director of the ZISC, the Zurich Information Security Center, which he led from 2003-2011. He served as Editor-in-Chief of the ACM Transactions on Privacy and Security (2015-2020) and of Springer-Verlag's book series on Information Security and Cryptography (2008-present). He has co-founded three security companies, is on the board of directors of Anapaya Systems AG as well as various management and scientific advisory boards, and he has consulted extensively for IT companies and government organizations. He is an IEEE Fellow and an ACM Fellow