| Model Checking Electronic Commerce Security Protocols Based on CTL |
| |
| 作者姓名： | XIAODe-qin ZHANGHuan-guo |
| |
| 作者单位： | [1]Collegeoflnformation,SouthChinaAgricultureUniversity,Guangzhou5106,12,Guangdong,China／／StaleKeyLaboratoryofSoftwareEngeering,WuhanUniversity,Wuhan.130072,Hubei,China [2]StaleKeyLaboratoryofSoftwareEngeering,WuhanUniversity,Wuhan.130072,Hubei,China |
| |
| 基金项目： | Supported by the Natural Science Foundation of
the Department of Education of Guangdong Province (Z03001) |
| |
| 摘 要： | We present a model based on Computational Temporal Logic (CTL) methods for verifying security requirements of electronic commerce protocols. The model describes formally the authentication, confidentiality integrity, nowrepudiation, denial of service and access control of the electronic commerce protocols. We illustrate as case study a variant of the Lu-Smolka protocol proposed by Lu-Smolka. Moreover, we have discovered two attacks that allow a dis-honest user to purchase a good debiting the amount to another user. And also, we compared our work with relative research works and found that the formal way of this paper is more general to specify security protocols for E-Commerce.
|
| 关 键 词： | 电子商务 安全协议 计算时态逻辑 访问控制 密码协议 |
| 收稿时间： | 20 May 2004 |
Model checking electronic commerce security protocols based on CTL |
| |
| XIAODe-qin ZHANGHuan-guo.Model Checking Electronic Commerce Security Protocols Based on CTL[J].Wuhan University Journal of Natural Sciences,2005,10(1):333-337. |
| |
| Authors: | Xiao De-qin Zhang Huan-guo |
| |
| Institution: | (1) College of Information, South China Agriculture University, 510642 Guangzhou, Guangdong, China;(2) State Key Laboratory of Software Engeering, Wuhan University, 430072 Wuhan, Hubei, China |
| |
| Abstract: | We present a model based on Computational Temporal Logic (CTL) methods for verifying security requirements of electronic commerce protocols. The model describes formally the authentication, confidentiality integrity, non-repudiation, denial of service and access control of the electronic commerce protocols. We illustrate as case study a variant of the Lu-Smolka protocol proposed by Lu-Smolka. Moreover, we have discovered two attacks that allow a dishonest user to purchase a good debiting the amount to another user. And also, we compared our work with relative research works and found that the formal way of this paper is more general to specify security protocols for E-Commerce. |
| |
| Keywords: | E-commerce security protocols formal methods computational temporal logic |
| 本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录！ |
|
