Abstract
Consumers use various payment methods to purchase goods and services from retailers, such as cash, credit cards, debit cards, prepaid cards, and barcodes/two-dimensional codes. In the past, in the case of in-store payments using credit cards, the in-store terminal read the card number from the magnetic strip on the card and sent it with other purchase information to the credit card network. Recently, to prevent counterfeiting, the IC chip on the credit card and the in-store terminal communicates to authenticate each other and process the payment transaction. The medium of communication is not only contact but also contactless (“touch" payment), Moreover, the in-store terminal may process the payment either online or offline and optionally may require the customer to input their PIN. Various protocols and protocol flows are used depending on the medium and how the payment is processed. Credit cards are also used for remotely purchasing goods or services; in this case, other protocols and protocol flows are used. In some such protocols, researchers found serious security flaws that allow a malicious party to fraudulently purchase goods in such a way that is not allowed for legitimate customers. Such flaws must be fixed, but it is hard to fix and deploy protocols after they are widely used. Formal verification is a method to analyze and verify the security of such protocols and to detect flaws before they are widely deployed. In this paper, we will discuss the research trends in formal verification of the security of various cashless payment protocols, as well as future issues.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Casper: a compiler for the analysis of security protocols. https://www.cs.ox.ac.uk/gavin.lowe/Security/Casper/
The Coq proof assistant. https://coq.inria.fr/
Isabelle. https://isabelle.in.tum.de/
ProVerif: cryptographic protocol verifier in the formal model. https://bblanche.gitlabpages.inria.fr/proverif/
Tamarin prover. https://tamarin-prover.com/
Apple Inc.: Introducing apple pay merchant tokens. https://developer.apple.com/apple-pay/merchant-tokens/
Association, V.I.S.: 3-D Secure introduction, version 1.0.2 (2002)
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–194. USENIX Association (2021). https://www.usenix.org/conference/usenixsecurity21/presentation/basin
Basin, D., Sasse, R., Toro-Pozo, J.: The EMV standard: break, fix, verify. In: 2021 IEEE Symposium on Security and Privacy (SP), pp. 1766–1781. ieeexplore.ieee.org (2021). https://doi.org/10.1109/SP40001.2021.00037
Basin, D., Schaller, P., Toro-Pozo, J.: Inducing authentication failures to bypass credit card PINs. In: 32nd USENIX Security Symposium (USENIX Security 23), pp. 3065–3079. USENIX Association, Anaheim, CA (2023). https://www.usenix.org/conference/usenixsecurity23/presentation/basin
Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET purchase protocols. J. Autom. Reasoning 36(1), 5–37 (2006). https://doi.org/10.1007/s10817-005-9018-6
Bella, G., Massacci, F., Paulson, L.C., Tramontano, P.: Formal verification of cardholder registration in SET. In: Sixth European Symposium on Research in Computer Security: ESORICS 2000 (2000)
Bella, G., Paulson, L.C.: Verifying set purchase protocols. Report 524, Computer Laboratory, University of Cambridge (2001)
Bolignano, D.: Towards the formal verification of electronic commerce protocols. In: 10th IEEE Computer Security Foundations Workshop, pp. 133–146 (1997)
Do, Q.H., Hosseyni, P., Küsters, R., Schmitz, G., Wenzler, N., Würtele, T.: A formal security analysis of the W3C web payment APIs: attacks and verification. In: 2022 IEEE Symposium on Security and Privacy (SP), pp. 215–234 (2022). https://doi.org/10.1109/SP46214.2022.9833681
EMVCo, LLC: EMV payment tokenisation. https://www.emvco.com/emv-technologies/payment-tokenisation/
EMVCo, LLC: EMV specifications and associated bulletins. https://www.emvco.com/specifications/
EMVCo, LLC: EMV 3-D Secure protocol and core functions specification (ver. 2.3.1.1). https://www.emvco.com/specifications/?post_id=90911 (2023)
Formal Systems Ltd: Fdr2 user manual (1998)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978). https://doi.org/10.1145/359576.359585
Miyai, M.: Essence of Payment service and Cashless society (in Japanese). Kinzai Institute for Financial Affairs, Inc. (2020)
Murdoch, S.J., Drimer, S., Anderson, R., Bond, M.: Chip and pin is broken. In: 2010 IEEE Symposium on Security and Privacy, pp. 433–446 (2010). https://doi.org/10.1109/SP.2010.33
Pasupathinathan, V., Pieprzyk, J., Wang, H., Cho, J.Y.: Formal analysis of card-based payment systems in mobile devices. In: Proceedings of the 2006 Australasian workshops on Grid computing and e-research - Volume 54, ACSW Frontiers ’06, pp. 213–220. Australian Computer Society, Inc., AUS (2006). https://dl.acm.org/doi/10.5555/1151828.1151853
Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: 8th IEEE Computer Security Foundations Workshop, pp. 98–107 (1995)
de Ruiter, J., Poll, E.: Formal analysis of the EMV protocol suite. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 113–129. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27375-9_7
Sakurada, H.: Verification of secrecy of the set payment protocol (in Japanese). IPSJ J. 44(8), 2106–2116 (2003)
Sakurada, H., Sakurai, K.: Directions and issues in formal verification of payment protocols (in Japanese). In: 2024 Symposium on Cryptography and Information Security (SCIS2024) (2024)
Scoping SIG, Tokenization Taskforce, PCI Security Standards Council: information supplement: PCI DSS tokenization guidelines. https://listings.pcisecuritystandards.org/documents/Tokenization_Guidelines_Info_Supplement.pdf (2011)
Watanabe, K., Yoneyama, K.: Formal verification of challenge flow in EMV 3-D Secure (in Japanese). In: 2024 Symposium on Cryptography and Information Security (SCIS2024) (2024)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Sakurada, H., Sakurai, K. (2024). SoK: Directions and Issues in Formal Verification of Payment Protocols. In: Barolli, L. (eds) Advanced Information Networking and Applications. AINA 2024. Lecture Notes on Data Engineering and Communications Technologies, vol 202. Springer, Cham. https://doi.org/10.1007/978-3-031-57916-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-031-57916-5_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-57915-8
Online ISBN: 978-3-031-57916-5
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)