{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:40:49Z","timestamp":1743136849013,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711619"},{"type":"electronic","value":"9783031711626"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"Abstract<\/jats:title>EMV is the international protocol standard for smart card payments and is used in billions of payment cards worldwide. Despite the standard\u2019s advertised security, various issues have\u00a0been previously uncovered, deriving from logical flaws that are hard\u00a0to spot in EMV\u2019s lengthy and complex specification. We have formalized various models of EMV in Tamarin, a symbolic model checker for cryptographic protocols. Tamarin was extremely effective in finding critical flaws, both\u00a0known and new, and in many cases exploitable on actual cards. We report on these past problems as well as followup work where\u00a0we verified the latest, improved version of the protocol, the EMV kernel C8. This work puts C8\u2019s correctness on a firm, formal basis,\u00a0and clarifies which guarantees hold for C8 and under which assumptions. Overall our work supports the thesis\u00a0that cryptographic protocol model checkers like Tamarin have an essential role to play in improving the security of real-world payment protocols and that they are up to this challenge.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_2","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"29-51","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Getting Chip Card Payments Right"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2952-939X","authenticated-orcid":false,"given":"David","family":"Basin","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0002-6909-8010","authenticated-orcid":false,"given":"Xenia","family":"Hofmeier","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5632-6099","authenticated-orcid":false,"given":"Ralf","family":"Sasse","sequence":"additional","affiliation":[]},{"given":"Jorge","family":"Toro-Pozo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"2_CR1","unstructured":"Tamarin Version 1.9.0, Git Revision: 57e619fef32033293e4a83c0be67cc6e296bf166, branch: develop"},{"key":"2_CR2","unstructured":"Apple Inc.: Tap to Pay on iPhone. https:\/\/developer.apple.com\/tap-to-pay\/"},{"key":"2_CR3","unstructured":"Basin, D., Cremers, C., Jannik, D., Sasse, R.: Modeling and analyzing security protocols with Tamarin: a comprehensive guide. In: Information Security and Cryptography. Springer (2024). To appear"},{"key":"2_CR4","unstructured":"Basin, D., Hofmeier, X., Sasse, R., Toro-Pozo, J.: Tamarin models of C8. https:\/\/github.com\/tamarin-prover\/tamarin-prover\/tree\/develop\/examples\/fm24-cardpayments"},{"key":"2_CR5","unstructured":"Basin, D., Sasse, R., Toro-Pozo, J.: Card brand mixup attack: bypassing the PIN in non-visa cards by using them for visa transactions. In: 30th USENIX Security Symposium (USENIX Security 21), pp. 179\u2013194. USENIX Association (2021)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Basin, D., Sasse, R., Toro-Pozo, J.: The EMV standard: break, fix, verify. In: 2021 IEEE Symposium on Security and Privacy (SP), pp. 1766\u20131781. IEEE, San Francisco (2021)","DOI":"10.1109\/SP40001.2021.00037"},{"key":"2_CR7","unstructured":"Basin, D., Schaller, P., Toro-Pozo, J.: Inducing authentication failures to bypass credit card PINs. In: 32nd USENIX Security Symposium, p.\u00a015. USENIX Association (2023)"},{"key":"2_CR8","unstructured":"Coppola, D., et al.: PURE: payments with UWB RElay-protection. In: 33rd USENIX Security Symposium (USENIX Security 2024) (2024)"},{"key":"2_CR9","unstructured":"EMVCo. EMV Contactless Specifications for Payment Systems, Book C-8, Kernel 8 Specification, Version 1.1 (2023). https:\/\/www.emvco.com\/specifications"},{"key":"2_CR10","unstructured":"EMVCo. EMV Contactless Specifications for Payment Systems, Book E, Security and Key Management, Version 1.0 (2023). https:\/\/www.emvco.com\/specifications\/"},{"key":"2_CR11","unstructured":"Ferro, C.: Annual Report 2023: Enhancing EMV Technologies to Supporting Emerging Payments. https:\/\/www.emvco.com\/knowledge-hub\/annual-report-2023-enhancing-emv-technologies-to-supporting-emerging-payments\/"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Proceedings 10th Computer Security Foundations Workshop, pp. 31\u201343 (1997)","DOI":"10.1109\/CSFW.1997.596782"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Mauw, S., Smith, Z., Toro-Pozo, J., Trujillo-Rasua, R.: Distance-bounding protocols: verification without time and location. In: 2018 IEEE Symposium on Security and Privacy (SP), pp. 549\u2013566 (2018)","DOI":"10.1109\/SP.2018.00001"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Murdoch, S.J., Drimer, S., Anderson, R., Bond, M.: Chip and PIN is broken. In: 2010 IEEE Symposium on Security and Privacy, pp. 433\u2013446. IEEE, Oakland (2010)","DOI":"10.1109\/SP.2010.33"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Radu, A.I., Chothia, T., Newton, C.J., Boureanu, I., Chen, L.: Practical EMV relay protection. In: 2022 IEEE Symposium on Security and Privacy (SP), pp. 1737\u20131756. IEEE, San Francisco (2022)","DOI":"10.1109\/SP46214.2022.9833642"},{"key":"2_CR17","unstructured":"Roland, M., Langer, J.: Cloning credit cards: a combined pre-play and downgrade attack on EMV contactless. In: 7th USENIX Workshop on Offensive Technologies (WOOT 13) (2013)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 2012 IEEE 25th Computer Security Foundations Symposium, pp. 78\u201394. IEEE, Cambridge (2012)","DOI":"10.1109\/CSF.2012.25"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T23:01:38Z","timestamp":1732748498000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}