EMV is the international protocol standard for smart card 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.
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, and in many cases exploitable on actual cards.
We report on these past problems as well as followup work where we
verified the latest, improved version of the protocol, the EMV kernel
C8.  This work puts C8's correctness on a firm, formal basis, and
clarifies which guarantees hold for C8 and under which assumptions.
Overall our work supports the thesis that
cryptographic protocol model checkers like Tamarin have an essential
role to play in improving the security of real-world payment protocols
and that they are up to this challenge.