Formal Methods for Payment Protocols
David Basin · 2023
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.