For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 2018/09/01
Online ISSN: 1745-1361
Type of Manuscript: PAPER
Category: Information Network
electronic payment protocol, formal analysis, accountability, fairness, timeliness, logical reasoning,
Full Text: PDF(1MB)>>
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.