Design And Formal Analysis Of Electronic Commerce Security Protocols

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.