Formal Methods for Modern Payment Protocols

EMV is the international protocol standard for smartcard payments and is used in billions of 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 various models of EMV in Tamarin, a symbolic model checker for cryptographic protocols. Tamarin was extremely effective in finding critical flaws, both known and new. For example, we discovered multiple ways that an attacker can use a victim’s EMV card (e.g., Mastercard or Visa Card) for high-valued purchases without the victim’s supposedly required PIN. Said more simply, the PIN on your EMV card is useless! We report on this, as well as follow-up work with an EMV consortium member on verifying the latest, improved version of the protocol, the EMV Kernel C-8. Overall our work provides evidence that security protocol model checkers like Tamarin have an essential role to play in developing real-world payment protocols and that they
are up to this challenge.