Research On Analysis Of Fair Exchange Protocols

With the development and popularization of Internet, electronic commerce has become one of main forms of modern economic activity based on Internet.Electronic commercial transactions involve multiple players who mutually distrust one another . One main problem of electronic commerce is how to exchange electronic data in a fair mode between two parties who are distrust. Fairness and viability become basic request of electronic commercial protocols . Fair exchange protocols can make participate to exchange information fairly .That is one party can get the information of the other party, only if the other party get his.It is well known that the design of authentication protocols is a difficult problem. There are often flaws because of some small problem. It needs strict fomal analysis to see whether a security protocol can realize the security that the deviser expect. There are a lot of formal methods to the analysis of authentication protocols. Fair exchange protocols are more complicated than authentication protocols. They need to satisfy security properties that not be involved in the authentication protocols besides properties that the authentication protocol must satisfy. For example fairness, timeliness, accountability etc. Methods which analyze authentication protocols is no longer applicable to directly analyze fair exchange protocols.Currently, there are several formal analysis methods of fair exchange protocols. Some methods are expansion of methods of analysis ofauthentication protocols. Such as the Paulson's inductive method, Schneider's CSP method, the MurO method that used by Vitaly Shmatikov and John Mitchell,etc. Some methods are the use of general checking tool.Boyd and Kearny proposed to use the specification animation tool Possum to analyze fair exchange protocols. Steve Kremer use ATS model checking tool Mocha check fair exchange protocols. Among the methods introduced above, some did not deal with branch of protocols, some can not analyze the accountability of protocols. At present, the study of analysis of fair exchange protocols is a new realm and the methods and technology need to be perfect.In this thesis , we try to study the analysis method of fair exchange protocols which include the analysis of the fairness, viability, timeliness, accountability.In the first part of this thesis(Chapter2-3), we introduce typical formal methods to the analysis of authentication protocols, where we point out the virtues and the shortcomings of each methods. We also introduce fair exchange protocols which include the evolution of fair exchange protocol the properties that fair exchange protocols must satisfy and the formal analysis methods of fair exchange protocols that have been proposed in other papers.In the second part of this thesis(Chapter4-7), we study the analysis method of fair exchange protocols which include the analysis of the fairness, viability, timeliness. The main results as follows:We first proposed a method which can describe protocol goals and messages formally. Through this method one can find terms that the originator can send without regarding to the protocol's specification.Based on a formal model of fair exchange protocols that is proposed by Qing Sihan, We propose a new method which can analyze fair exchange protocols. If we make assumption that communication channel isconfidential and authenticated, the new method can search after all possible bundles and inspect whether there are security flaws in protocol by analyzing if every bundle is fair. We propose a method which can search all possible bundles of protocols. We increase the search efficiency by reducing bundles of protocols in reason .Combining with the method to formal description of protocol goals and messages, we proposed a method that can analyze security properties of fair exchange protocol.Using our new method, we analyze two certified e-mail protocols and two contract signing protocols .Through comparing with the results of discussed in other papers, it can see the method that we propose can find flaws of protocols roundly. Our methods will accelerate the use of fair exchange protocols in practice.We design an arithmetic using the thinking of the new method. The arithmetic can analyze fairness as well as timeliness of protocols. Using the arithmetic one can design automatic analysis tool expediently.In the third part of this thesis, we study the analysis method to accountability of optimistic fair exchange protocols. Accountability is a basic requirement which safe e-commerce protocols must satisfy. Nonrepudiation is realized by originator non-repudiation evidence and recipient non-repudiation evidence. Originator non-repudiation evidence is the non-repudiation evidence offered to the recipient through protocol which is used to prove a message that the recipient received is sent by the origination. Recipient non-repudiation evidence is the non-repudiation evidence offered to the originator through protocol which is used to prove the recipient received the message. The non-repudiation evidence is different from the digital signature. The function of digital signatures can be used to prove that the signer is the origin of the message, and he is responsible for this information. For an information m signed by a person, many people are able to prove the information m is sent bythe signer , but the non-repudiation evidence must include the identity of the recipient which is to prove that the information is sent to the recipient. The non-repudiation evidence not only is able to prove the originator has sent the message, and is responsible for this message, but also is able to prove that the message is sent to the recipient. An originator non-repudiation evidence is able to offer the evidence that 0 can prove R has received m. A recipient non-repudiation evidence is able to offer the evidence that R can prove that 0 has sent m to R. Whether a protocol satisfying the accountability is related closely to the goal of the parities of the protocol. So, in the promise that the party can get his goal, analyzing whether a protocol satisfies accountability, only needs to analyze whether the goal of every party in the protocol is designed satisfying accountability .We extend the method that can analyze accountability of online electronic commerce protocols. Thus we can use the extended method to analyze accountability of optimistic fair exchange protocols. We analyze the accountability of two certified e-mail protocol and draw the conclusion that some goals can not satisfy accountability. Analysis of accountability of optimistic fair exchange protocols is a difficult problem. To our best known, there is no methods of analysis of accountability of optimistic fair exchange protocols. The method we propose will accelerate the design and application of optimistic fair exchange protocols.In the fourth part of this thesis, we introduce other results that we obtain. They are:We discuss the method of analysis fairness of optimistic fair exchange protocols using strand spaces. Strand space model is a new formal analysis tool to the analysis of cryptogram protocols. Based on strand spaces,we extend the authentication tests method .Using this method,optimistic fair exchange protocols can be described and analyzed. We apply it to the analysis of ASW protocol and find all attacks appeared in former literatures.Nenadic etc proposed a fair certified e-mail protocol.We indicate there are security flaws in the protocol and amend it. We also prove the fairness of amended protocol using the extended strand space method.To our best known.no one has pointed the flaws and our amending will accelerate the protocol' application.The study on analysis of fair exchange protocol especially optimistic fair exchange protocols just begin. Our research will accelerate design and analysis of fair exchange protocol and accelerate development of electronic commerce.