【作者】 高悦翔；

【导师】 彭代渊；

【作者基本信息】 西南交通大学 ， 信息安全， 2013， 博士

【摘要】 随着计算机网络的飞速发展,电子商务逐渐成为人们进行商务活动的新模式。电子商务安全协议是构建电子商务安全环境的基础,是保障电子商务顺利应用与发展的关键技术。电子商务安全协议是以密码学为基础的消息交换协议,参与者采取的一系列步骤去完成某一任务,其目的是在网络信道不可靠的情况下,确保通信安全以及传输数据的安全。电子商务安全协议除了需满足传统安全协议所需满足的认证性、保密性和完整性外,还需满足可追究性、公平性、时限性及匿名性等安全属性。因此电子商务安全协议的设计与分析面临着诸多困难和挑战,也成为了信息安全领域中的一个重要课题,具有重要的理论意义和现实应用价值。本文主要围绕电子商务安全协议的设计以及形式化分析技术展开研究,取得了些研究成果。对电子商务安全协议的基本概念、分类及其安全属性进行了综述和分析,对电子商务安全协议安全性设计及形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。指出了一个认证电子邮件协议在可追究性和公平性上存在的安全缺陷,在此基础上提出了一种基于在线第三方的认证电子邮件协议,以满足认证电子邮件的一般安全特性。利用扩展Kailar逻辑对该协议进行分析,说明该协议满足不可否认性及公平性,并具有抗篡改、重放等攻击、及第三方无法获得邮件内容等优点。采用组合协议分析方法及PCL逻辑分析了ECS2协议的弱公平性。指出了ZZW协议存在不满足保密性、可追究性和公平性的安全缺陷,并提出了改进方案。提出一种结合组合协议分析以及Kailar逻辑的分析思路,用于分析基于离线第三方的电子商务安全协议的可追究性及公平性,并分析了改进后的ZZW协议,证明了该协议能够弥补原协议的安全隐患。针对移动环境中网络及计算条件受限的情况,在考虑有效性和支付效率的基础上,设计了一个适应于移动环境的公平移动支付协议。该协议由认证、支付、恢复、结算四个子协议构成。在认证协议中通过基于Hash函数的动态ID机制满足了双向认证、有限的匿名性和不可追踪性,并获取不可伪造性的、可重用的支付证书。在支付过程中基于变色龙Hash函数和双Hash链,实现了交易的匿名性、可追究性和公平性。最后利用Kailar逻辑对协议的可追究性和公平性进行了形式化分析,结果表明,协议在保持较高执行效率的同时能满足可追究性和公平性,适用于在移动环境以及类似的通信、计算条件受限的环境中使用。针对一般信念逻辑难于分析乐观公平交换协议的公平性和时限性的现状,将乐观公平交换协议定义为类似于Kripke结构的状态转换系统,对扩展Kailar逻辑增加了时间限定条件及状态转换分析。在分析不可否认证据有效性的基础上,通过考察主体认知及信仰的转换过程,达到分析乐观公平交换协议的公平性和时限性的目的。同时,对一个典型的乐观公平交换协议进行了分析,发现了该协议存在的两个安全缺陷,并给出了改进方案。指出了一个典型的多方认证邮件协议存在不满足公平性、可追究性以及个别不诚实参与方行为会导致整个协议执行失败等安全隐患。基于签密方案,对该协议进行了改进,并利用Kailar逻辑对改进后的协议的安全属性进行了分析。研究结果表明,该协议能够满足保密性、不可否认性及公平性,并具有抗篡改、重放、合谋等攻击的特点。本文的研究工作对于电子商务安全协议的设计以及形式化分析技术有一定的理论和实用意义,同时对于提高电子商务活动的安全性也具有一定的价值。更多还原

【Abstract】 With the rapid development of network technology, Electronic commerce (E-commerce) has become a new model for ordinary business. E-commerce security protocol is cornerstones of building security e-commerce environment and works as a kind of the kernel technology for application and development of e-commerce successfully. E-commerce security protocol is a message exchange protocol based on cryptography. The participants adopted a series of steps to accomplish a task in these protocols which is ensured the security communication and data transmission security in unreliable network channel.E-commerce security protocols need to fulfill some special security attributes such as non-repudiation, fairness, timeliness and anonymity besides other attributes in traditional security protocols like authentication, confidentiality and integrity. Therefore, the design and formal analysis of E-commerce security protocols has been facing many difficulties and challenges and has been becoming an important research direction in the area of information security. Furthermore, the design and formal analysis of E-commerce security protocols has important theoretical and application value.This paper make further study on the design and formal analysis of E-commerce security protocols. The main works and results are as follows:Basic theories, classification and security attributes of E-commerce security protocols are reviewed and analyzed. Simultaneously, the main methods of formal analysis for e-commerce security protocols are reviewed, and the advantages, disadvantages and problems of each method are discussed.The security flaws of a certified E-mail protocol have been pointed out. In order to meet the general security attributes in certified E-mail protocol, an improved protocol was proposed based on Online TTP. The improved protocol analyzed by extended Kailar logic can achieve the non-repudiation, fairness as well as the other advantages that it can resist the attacks as distort, replay and the TTP can’t read the E-mail.The method of compositional analysis and PCL logic is introduced, and the weak fairness of ECS2is analyzed by this method. Aiming at to remedy the lack of fairness and non-repudiation of a typical certified mail protocol(ZZW protocol), an improved certified mail protocol with transparent semi-trusted third party is proposed. To improve the protocol analysis efficiency, a method applying Kailar logic in compositional analysis is proposed for analyzing the improved protocol. The analysis results indicate the improved protocol can meet fairness and non-repudiation.Considering the condition of network and the calculation capability of mobile terminal is limited in the mobile environment, the novel fair mobile payment protocol was proposed. The protocol is composed of four sub-protocols:authentication, payment, recovery and withdraw. In authentication sub-protocol, the dynamic ID mechanism based on the hash function is adopted to satisfy mutual authentication, the limited anonymity and intractability, and the unforgeable and reusable payment certificate is obtained. In the process of payment, the attribute of anonymity, non-repudiation and fairness, is achieved based on Chameleon Hash functions and double Hash chain. Finally, through formal analyzing the security attributes by Kailar logic, the result declares that of the protocol can fulfill the non-repudiation and fairness based on the higher efficiency in the implementation. The protocol can be applied to mobile environment and similar communication and calculate conditions constrained environments.Aiming at the circumstance that generic faith logic is difficult to analyze the fairness and timeliness of optimistic fair exchange protocol, we defined the optimistic fair exchange protocol as a state transition system with a structure similar to Kripke, and added time limit conditions and state transition analysis into extended Kailar Logic. By means of discussing the conversion process of cognition and faith of principals based on the investigation of validity of non-repudiation evidence, the fairness and timeliness of the protocol is analyzed. We analyzed a typical optimistic fair exchange protocol. Two flaws of the protocol are discovered and an improved protocol was proposed.The security flaws of a Multi-Party certified E-mail protocol have been pointed out. We declare the protocol can not meet fairness, non-repudiation and the security risks that the implementation of the protocol will be led to failure by individual acts of dishonesty. An improved protocol was proposed based on signcryption scheme. Through the analysis by Kailar logic, it is can be seen the improved protocol can achieve the non-repudiation, fairness. Furthermore, it has advantage of resisting the attacks as distort, replay and conspiracy.There are some theoretical and practical significance in design and formal analysis of e-commerce security protocols in this paper. Simultaneously, the studies of this paper also have some value for promoting the security of e-commerce.更多还原