A systematic security analysis of EMV protocol

EMV is the leading and widely used international standard for payment with smart cards. The EMV specification defines a highly configurable toolkit for payment protocols, which allows different combinations of card authentication, cardholder authentication and transaction authorization. Due to its complexity and its flexibility, it is difficult to comprehensively analyze the security of EMV standard, yet it is critical to obtain practical security guarantees for EMV. In this paper, we present the first systematic and formal treatment of EMV protocol. We introduce a three-party security model, covering all known kinds of combinations and providing reasonably strong security notions. Furthermore, via a modular approach, we prove that the EMV protocol with reasonable improvement can achieve our desired security. We also identify various known attacks on EMV protocol in our security model.