IEICE TRANSACTIONS on Information
Formal Method for Security Analysis of Electronic Payment Protocols
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information 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
Authors
Yi LIU
National University of Defense Technology
Qingkun MENG
National University of Defense Technology
Xingtong LIU
National University of Defense Technology
Jian WANG
National University of Defense Technology
Lei ZHANG
National University of Defense Technology
Chaojing TANG
National University of Defense Technology
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Yi LIU, Qingkun MENG, Xingtong LIU, Jian WANG, Lei ZHANG, Chaojing TANG, "Formal Method for Security Analysis of Electronic Payment Protocols" in IEICE TRANSACTIONS on Information,
vol. E101-D, no. 9, pp. 2291-2297, September 2018, doi: 10.1587/transinf.2018EDP7108.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2018EDP7108/_p
Copy
@ARTICLE{e101-d_9_2291,
author={Yi LIU, Qingkun MENG, Xingtong LIU, Jian WANG, Lei ZHANG, Chaojing TANG, },
journal={IEICE TRANSACTIONS on Information},
title={Formal Method for Security Analysis of Electronic Payment Protocols},
year={2018},
volume={E101-D},
number={9},
pages={2291-2297},
abstract={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.},
keywords={},
doi={10.1587/transinf.2018EDP7108},
ISSN={1745-1361},
month={September},}
Copy
TY - JOUR
TI - Formal Method for Security Analysis of Electronic Payment Protocols
T2 - IEICE TRANSACTIONS on Information
SP - 2291
EP - 2297
AU - Yi LIU
AU - Qingkun MENG
AU - Xingtong LIU
AU - Jian WANG
AU - Lei ZHANG
AU - Chaojing TANG
PY - 2018
DO - 10.1587/transinf.2018EDP7108
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E101-D
IS - 9
JA - IEICE TRANSACTIONS on Information
Y1 - September 2018
AB - 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.
ER -
English
