电子商务安全协议的设计与形式化分析

发布时间：2018-05-01 13:02

本文选题：电子商务安全协议 + Kailar逻辑　；参考：《西南交通大学》2013年博士论文

【摘要】：随着计算机网络的飞速发展,电子商务逐渐成为人们进行商务活动的新模式。电子商务安全协议是构建电子商务安全环境的基础,是保障电子商务顺利应用与发展的关键技术。电子商务安全协议是以密码学为基础的消息交换协议,参与者采取的一系列步骤去完成某一任务,其目的是在网络信道不可靠的情况下,确保通信安全以及传输数据的安全。电子商务安全协议除了需满足传统安全协议所需满足的认证性、保密性和完整性外,还需满足可追究性、公平性、时限性及匿名性等安全属性。因此电子商务安全协议的设计与分析面临着诸多困难和挑战,也成为了信息安全领域中的一个重要课题,具有重要的理论意义和现实应用价值。本文主要围绕电子商务安全协议的设计以及形式化分析技术展开研究,取得了些研究成果。对电子商务安全协议的基本概念、分类及其安全属性进行了综述和分析,对电子商务安全协议安全性设计及形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。指出了一个认证电子邮件协议在可追究性和公平性上存在的安全缺陷,在此基础上提出了一种基于在线第三方的认证电子邮件协议,以满足认证电子邮件的一般安全特性。利用扩展Kailar逻辑对该协议进行分析,说明该协议满足不可否认性及公平性,并具有抗篡改、重放等攻击、及第三方无法获得邮件内容等优点。采用组合协议分析方法及PCL逻辑分析了ECS2协议的弱公平性。指出了ZZW协议存在不满足保密性、可追究性和公平性的安全缺陷,并提出了改进方案。提出一种结合组合协议分析以及Kailar逻辑的分析思路,用于分析基于离线第三方的电子商务安全协议的可追究性及公平性,并分析了改进后的ZZW协议,证明了该协议能够弥补原协议的安全隐患。针对移动环境中网络及计算条件受限的情况,在考虑有效性和支付效率的基础上,设计了一个适应于移动环境的公平移动支付协议。该协议由认证、支付、恢复、结算四个子协议构成。在认证协议中通过基于Hash函数的动态ID机制满足了双向认证、有限的匿名性和不可追踪性,并获取不可伪造性的、可重用的支付证书。在支付过程中基于变色龙Hash函数和双Hash链,实现了交易的匿名性、可追究性和公平性。最后利用Kailar逻辑对协议的可追究性和公平性进行了形式化分析,结果表明,协议在保持较高执行效率的同时能满足可追究性和公平性,适用于在移动环境以及类似的通信、计算条件受限的环境中使用。针对一般信念逻辑难于分析乐观公平交换协议的公平性和时限性的现状,将乐观公平交换协议定义为类似于Kripke结构的状态转换系统,对扩展Kailar逻辑增加了时间限定条件及状态转换分析。在分析不可否认证据有效性的基础上,通过考察主体认知及信仰的转换过程,达到分析乐观公平交换协议的公平性和时限性的目的。同时,对一个典型的乐观公平交换协议进行了分析,发现了该协议存在的两个安全缺陷,并给出了改进方案。指出了一个典型的多方认证邮件协议存在不满足公平性、可追究性以及个别不诚实参与方行为会导致整个协议执行失败等安全隐患。基于签密方案,对该协议进行了改进,并利用Kailar逻辑对改进后的协议的安全属性进行了分析。研究结果表明,该协议能够满足保密性、不可否认性及公平性,并具有抗篡改、重放、合谋等攻击的特点。本文的研究工作对于电子商务安全协议的设计以及形式化分析技术有一定的理论和实用意义,同时对于提高电子商务活动的安全性也具有一定的价值。
[Abstract]:With the rapid development of computer network, e-commerce has gradually become a new model for people to carry out business activities. E-commerce security protocol is the basis for the construction of electronic commerce security environment, and is the key technology to ensure the smooth application and development of e-commerce. The electronic commerce security protocol is a message exchange protocol based on cryptography, and participates in the information exchange protocol A series of steps taken by a person to accomplish a task are aimed at ensuring communication security and data transmission security when the network channel is unreliable.
In addition to satisfying the authentication, confidentiality and integrity of the traditional security protocol, the e-commerce security protocol needs to meet the security attributes such as accountability, fairness, time limit and anonymity. Therefore, the design and analysis of e-commerce security protocols are faced with many difficulties and challenges, and have also become one of the information security fields. An important topic has important theoretical significance and practical application value.
This paper focuses on the design of electronic commerce security protocols and formal analysis technology, and has made some research achievements.
The basic concepts, classification and security attributes of e-commerce security protocols are reviewed and analyzed. The security design and formal analysis methods of e-commerce security protocols are reviewed, and the advantages and disadvantages of various methods and their existing problems are discussed.
This paper points out the security defects of an authenticated e-mail protocol in accountability and fairness. On this basis, a authentication e-mail protocol based on online third party is proposed to meet the general security characteristics of authenticated e-mail. The protocol is analyzed with extended Kailar logic, which shows that the protocol satisfies non repudiation. Recognition and fairness, and has the advantages of anti tampering, replay attacks, and the three party can not get the content of the mail.
A combination protocol analysis method and PCL logic are used to analyze the weak fairness of the ECS2 protocol. It is pointed out that the ZZW protocol has a security defect that does not satisfy the security, can be prosecuted and fair, and proposes an improved scheme. A combination of combination protocol analysis and the analysis of Kailar logic is proposed to analyze the off-line third party based electronics. The feasibility and fairness of the business security protocol are analyzed, and the improved ZZW protocol is analyzed, which proves that the protocol can make up for the potential security risks of the original protocol.
In view of the constraints of network and computing conditions in mobile environment, a fair mobile payment protocol adapted to mobile environment is designed on the basis of effectiveness and payment efficiency. The protocol consists of four sub protocols, which are authentication, payment, recovery and settlement. In the authentication protocol, a dynamic ID mechanism based on Hash function is used to satisfy the double. To authenticated, limited anonymity and untraceability, and obtain unforgable, reusable payment certificates. In the process of payment, the anonymity, accountability and fairness of the transaction are realized based on the chameleon Hash function and double Hash chain. Finally, the formality and fairness of the protocol are analyzed with Kailar logic. The results show that the protocol can satisfy the accountability and fairness while maintaining high execution efficiency, and is suitable for use in a mobile environment and similar communications, with limited computing conditions.
In view of the fact that the general belief logic is difficult to analyze the fairness and the time limit of the optimistic fair exchange protocol, the optimistic fair exchange protocol is defined as a state conversion system similar to the Kripke structure. The time limit conditions and the state transformation analysis are added to the extended Kailar logic. In order to analyze the fairness and time limit of the optimistic and fair exchange protocol, a typical optimistic and fair exchange protocol is analyzed, and two security defects in the protocol are found, and an improved case is given.
It is pointed out that a typical multiparty authentication mail protocol is not satisfied with fairness, accountability and individual dishonest participant behavior will lead to the failure of the whole protocol execution. Based on the signcryption scheme, the protocol is improved, and the security properties of the improved protocol are analyzed with Kailar logic. The results show that the protocol can satisfy confidentiality, non repudiation and fairness, and has the characteristics of anti tampering, replay, collusion and other attacks.
The research work of this paper has some theoretical and practical significance for the design of e-commerce security protocol and the formalized analysis technology, and also has a certain value for improving the security of e-commerce activities.

【学位授予单位】：西南交通大学
【学位级别】：博士
【学位授予年份】：2013
【分类号】：TP309

【参考文献】