SoK: Directions and Issues in Formal Verification of Payment Protocols

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.