首页 | 本学科首页   官方微博 | 高级检索  
     检索      

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 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号