Formal Method for Security Analysis of Electronic Payment Protocols

Yi LIU  Qingkun MENG  Xingtong LIU  Jian WANG  Lei ZHANG  Chaojing TANG  

IEICE TRANSACTIONS on Information and Systems   Vol.E101-D   No.9   pp.2291-2297
Publication Date: 2018/09/01
Publicized: 2018/06/19
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2018EDP7108
Type of Manuscript: PAPER
Category: Information Network
electronic payment protocol,  formal analysis,  accountability,  fairness,  timeliness,  logical reasoning,  

Full Text: PDF(1MB)>>
Buy this Article

Electronic payment protocols provide secure service for electronic commerce transactions and protect private information from malicious entities in a network. Formal methods have been introduced to verify the security of electronic payment protocols; however, these methods concentrate on the accountability and fairness of the protocols, without considering the impact caused by timeliness. To make up for this deficiency, we present a formal method to analyze the security properties of electronic payment protocols, namely, accountability, fairness and timeliness. We add a concise time expression to an existing logical reasoning method to represent the event time and extend the time characteristics of the logical inference rules. Then, the Netbill protocol is analyzed with our formal method, and we find that the fairness of the protocol is not satisfied due to the timeliness problem. The results illustrate that our formal method can analyze the key properties of electronic payment protocols. Furthermore, it can be used to verify the time properties of other security protocols.