Formal Verification of Challenge Flow in EMV 3-D Secure and Its Improvement

EMV 3-D Secure is an authentication service mainly to identify and verify cardholders for card-not-present (CNP) transactions over the Internet. EMV 3-D Secure services are provided by international credit card brands such as Visa, Mastercard and American Express, and its protocol is specified by EMVCo. There are known existing works on evaluating security of several versions of 3-D Secure, such as a formal verification using Casper/FDR2 for the old specification (3-D Secure 1.0) and a spoofing attack using reverse engineering on risk assessment indicators for the current specification, EMV 3-D Secure (3-D Secure 2.0). However, there is no security verification of EMV 3-D Secure based on its protocol specification. Formal methods are known as methods that can verify security with high fidelity to the protocol specification and have been actively researched in recent years. In this paper, we verify the security of EMV 3-D Secure using ProVerif, an automated security verification tool for cryptographic protocols. First, one of the difficulties we faced is to correctly extract the detailed protocol structure from the entire specification that is written by natural language over 400 pages. Based on the extracted protocol structure, we formalize Challenge Flow for authentication by secret information under three environments (App-based (default-sdk), App-based (split-sdk), and Browser-based) in the latest version 2.3.1.1, which are specified for the purpose of identity verification in CNP transactions. We then verify the confidentiality and resistance to off-line dictionary attacks of secret information, the authenticity and the resistance to replay attacks against both man-in-the-middle attacks and colluding attacks with relay servers. As verification results, we show that Challenge Flow satisfies all of the above security requirements. Furthermore, we discuss the necessity of the unilateral authenticated channel between the cardholder and the card issuer assumed in the EMV 3-D Secure specification, and show that if we use a public channel instead of a unilateral authenticated channel, Challenge Flow still satisfies security requirements. It indicates that the protocol can be more efficient than the specification without reducing security.