8 July 2022 - David Basin (ETH Zurich) Speaker David Basin (ETH Zurich) Title Robbing the Bank with a Model Checker Abstract 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. 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 victims PIN. Said more simply, the PIN on your EMV card is useless! We describe these attacks, their repair, and more generally why using formal methods is essential for critical protocols like payment protocols. 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 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. Jul 08 2022 12.00 - 13.00 8 July 2022 - David Basin (ETH Zurich) Security, Privacy & Trust, and LFCS joint Seminar by David Basin The Bayes Centre (G.03) 47 Potterrow Edinburgh EH8 9BT & online... Join Zoom Meeting https://ed-ac-uk.zoom.us/j/85211333263 Meeting ID: 852 1133 3263 Passcode: b9a8asVq Google Map Eventbrite
8 July 2022 - David Basin (ETH Zurich) Speaker David Basin (ETH Zurich) Title Robbing the Bank with a Model Checker Abstract 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. 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 victims PIN. Said more simply, the PIN on your EMV card is useless! We describe these attacks, their repair, and more generally why using formal methods is essential for critical protocols like payment protocols. 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 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. Jul 08 2022 12.00 - 13.00 8 July 2022 - David Basin (ETH Zurich) Security, Privacy & Trust, and LFCS joint Seminar by David Basin The Bayes Centre (G.03) 47 Potterrow Edinburgh EH8 9BT & online... Join Zoom Meeting https://ed-ac-uk.zoom.us/j/85211333263 Meeting ID: 852 1133 3263 Passcode: b9a8asVq Google Map Eventbrite
Jul 08 2022 12.00 - 13.00 8 July 2022 - David Basin (ETH Zurich) Security, Privacy & Trust, and LFCS joint Seminar by David Basin
