Abstract
This paper presents a formal model of the EMV (Europay-MasterCard-Visa) protocol suite in F# and its analysis using the protocol verification tool ProVerif [5] in combination with FS2PV [4].
The formalisation covers all the major options of the EMV protocol suite, including all card authentication mechanisms and both on- and offline transactions. Some configuration parameters have to be fixed to allow any security analysis; here we follow the configuration of Dutch EMV banking cards, but the model could easily be adapted to other configurations.
As far as we know this is the first comprehensive formal description of EMV. The convenience and expressivity of F# proved to be a crucial advantage to make the formalisation of something as complex as EMV feasible. Even though the EMV specs amount to over 700 pages, our formal model is only 370 lines of code.
Formal analysis of our model with ProVerif is still possible, though this requires some care. Our formal analysis does not reveal any new weaknesses of the EMV protocol suite, but it does reveal all the known weaknesses, as a formal analysis of course should.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adida, B., Bond, M., Clulow, J., Lin, A., Murdoch, S., Anderson, R., Rivest, R.: Phish and chips: Traditional and new recipes for attacking EMV. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols. LNCS, vol. 5087, pp. 40–48. Springer, Heidelberg (2009)
Barisani, A., Bianco, D., Laurie, A., Franken, Z.: Chip & PIN is definitely broken. Presentation at CanSecWest Applied Security Conference, Vancouver (2011), slides http://dev.inversepath.com/download/emv/emv_2011.pdf
Bhargavan, K., Fournet, C., Gordon, A.: Modular verification of security protocol code by typing. ACM SIGPLAN Notices 45(1), 445–456 (2010)
Bhargavan, K., Fournet, C., Tse, S.: Verified interoperable implementations of security protocols. In: Computer Security Foundations Workshop (CSFW), pp. 139–152. IEEE, Los Alamitos (2006)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW), pp. 82–96. IEEE, Los Alamitos (2001)
de Soete, M., Ward, M.: EMV. In: van Tilborg, H. (ed.) Encyclopedia of Cryptography and Security, pp. 197–202. Springer, Heidelberg (2005)
Drimer, S., Murdoch, S., Anderson, R.: Optimised to fail: Card readers for online banking. In: Dingledine, R., Golle, P. (eds.) FC 2009. LNCS, vol. 5628, pp. 184–200. Springer, Heidelberg (2009)
EMVCo. EMV– Integrated Circuit Card Specifications for Payment Systems, Book 1: Application Independent ICC to Terminal Interface Requirements (2008)
EMVCo. EMV– Integrated Circuit Card Specifications for Payment Systems, Book 2: Security and Key Management (2008)
EMVCo. EMV– Integrated Circuit Card Specifications for Payment Systems, Book 3: Application Specification (2008)
EMVCo. EMV– Integrated Circuit Card Specifications for Payment Systems, Book 4: Cardholder, Attendant, and Acquirer Interface Requirements (2008)
Murdoch, S., Drimer, S., Anderson, R., Bond, M.: Chip and PIN is Broken. In: Symposium on Security and Privacy, pp. 433–446. IEEE, Los Alamitos (2010)
Van Herreweghen, E., Wille, U.: Risks and potentials of using EMV for internet payments. In: Proceedings of the 1st USENIX Workshop on Smartcard Technology, USENIX Association (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Ruiter, J., Poll, E. (2012). Formal Analysis of the EMV Protocol Suite. In: Mödersheim, S., Palamidessi, C. (eds) Theory of Security and Applications. TOSCA 2011. Lecture Notes in Computer Science, vol 6993. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27375-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-27375-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27374-2
Online ISBN: 978-3-642-27375-9
eBook Packages: Computer ScienceComputer Science (R0)