Tom Chothia, "Formal Verification of EMV Payments", VeTSS Annual Conference 2026

Talk by Tom Chothia (University of Birmingham), at the VeTSS Annual Conference, 12th May 2026, Royal Academy of Engineering, London, UK. Formal Verification of EMV Payments The EMV contactless bank card payment system has many independent parties: payment providers, terminal companies, smart-phone companies, banks and regulators. Many of these stakeholders have unilaterally added undocumented features to the core protocol specifications, leading to a highly complex system. Our research has shown that formal verification is an effective method to understand, explain and test the security of EMV. This has led to the discovery of 12 different attacks against EMV cards; highlights of our work include taking $10,000 from the locked iPhone of YouTube influencer MKBHD and enabling an offline Square reader to accept transactions from fake cards for £20,000. In addition to finding vulnerabilities, we have designed a security protocol for smart cards and used formal verification to show that it stops most attacks against EMV. Our new protocol is currently being added to the ISO 14443 standard for all smart cards. This is joint work with many people, including Ioana Boureanu, Anna Clee, Andreea-Ina Radu and George Pavlides.