The EMV Standard: Break, Fix, Verify

### Overview In this talk, security researcher Jorge Toro presents collaborative research conducted with David Basin and Ralph Sasse at ETH Zurich analyzing the EMV standard (commonly known as chip and PIN). With over 9 billion EMV smart cards in circulation worldwide, the standard is intended to safeguard high-value purchases through PIN verification known only to the legitimate cardholder. Using formal methods, the researchers developed the first comprehensive model of EMV to discover existing and new security issues, notably identifying and practically demonstrating a critical PIN bypass vulnerability in contactless Visa transactions, followed by proposing machine-checked fixes.

### Key Topics - **EMV Protocol Architecture:** The breakdown of EMV transactions into four core phases: initial application selection and data exchange, offline data authentication (via SDA, DDA, or CDA), cardholder verification methods (offline PIN, online PIN, or Consumer Device Cardholder Verification Method / CDCVM), and transaction authorization (offline terminal acceptance or online issuer authorization). - **Formal Verification with Tamarin:** Modeling protocol execution paths using multiset rewriting rules and verifying security properties expressed in first-order logic formulas, such as 'bank accepts', 'authentication to the terminal', and 'authentication to the bank' (formalized via injective agreement). - **Contact EMV Findings:** Confirmation that only transactions combining Combined Dynamic Data Authentication (CDA) with online PIN or no PIN are secure, whereas transactions relying on offline PIN remain susceptible to PIN bypass attacks previously reported in 2010. - **Contactless EMV & Visa PIN Bypass:** Uncovering that common MasterCard contactless transactions are secure, while common Visa transactions omit cryptographic signatures on Card Transaction Qualifiers (CTQ), allowing an attacker to tamper with the cardholder verification method.

### Technical Details In the Visa contactless protocol, the card specifies its preferred Cardholder Verification Method (CVM) inside a data object known as Card Transaction Qualifiers (CTQ). Although the specification supports signing the CTQ using Signed Dynamic Authentication Data (SDAD), standard Visa transactions do not mandate or verify this signature. As a result, the CTQ lacks integrity protection.

The researchers weaponized this flaw by constructing an Android application operating a man-in-the-middle attack over a relay architecture. During a high-value purchase where the terminal requests cardholder verification, a genuine card responds indicating that an online PIN is required. The attacker intercepts and modifies the CTQ to indicate that cardholder verification was performed on a consumer device (CDCVM, typical for smartphones or smartwatches). The payment terminal accepts the transaction under the assumption that the user authenticated on a mobile device, completing the purchase without PIN entry. The authors demonstrated this live using a 200 Swiss franc transaction.

To remediate the vulnerability, the authors proposed activating the card's SDAD signature by flipping a single bit in one of the terminal's commands. Because this change is implemented on the terminal side, it does not require replacing existing cards in circulation. Other findings, such as attacks against offline low-value transactions that lead terminals to accept charges later rejected by issuing banks, lack authentication and require card reissuance to resolve.

### Takeaways The findings highlight that human analysis alone cannot manage the branching complexity and state space of critical real-world protocols. Formal protocol verification using tools such as Tamarin should be integrated directly into development and standardization processes to identify and resolve vulnerabilities before mass deployment.