  EMV is the international protocol standard for smartcard payment and is used
in over 9 billion 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 formalize a comprehensive symbolic model of EMV in Tamarin, a
state-of-the-art protocol verifier. Our model is the first that supports a
fine-grained analysis of all relevant security guarantees that EMV is intended
to offer. We use our model to automatically identify flaws that lead to two
critical attacks: one that defrauds the cardholder and a second that defrauds
the merchant. First, criminals can use a victim's Visa contactless card to make
payments for amounts that require cardholder verification, without knowledge of
the card's PIN. We built a proof-of-concept Android application and
successfully demonstrated this attack on real-world payment terminals. Second,
criminals can trick the terminal into accepting an unauthentic offline
transaction, which the issuing bank should later decline, after the criminal
has walked away with the goods. This attack is possible for implementations
following the standard, although we did not test it on actual terminals for
ethical reasons. Finally, we propose and verify improvements to the standard
that prevent these attacks, as well as any other attacks that violate the
considered security properties. The proposed improvements can be easily
implemented in the terminals and do not affect the cards in circulation.
