Formal Logic And Automatic Proof For Optimistic Fair Exchange Protocols

With the increasing development of Internet, Internet-based electronic information exchange has become one of major forms of modern economic life. Electronic information exchange switches electronic data in a fair way between two un-trusted entities. A protocol achieving fair exchange of electronic information is known as a fair exchange protocol. Fairness is the basic security property of fair exchange protocols. The goal of a fair exchange protocol is to achieve the data exchange and not to leave any advantages over parties, and urges two un-trusted partners to complete a fair exchange.As is known to all, a secure security protocol designing is hard. A slight fault may even drive great flaws. Fair exchange protocol is of an important security protocol. So far, there are some formal methods for analyzing fair exchange protocols. The widely used method is the belief logic. Many researchers using the extended belief logic method successfully analyzed the non-repudiation of some online trusted third party fair exchange protocols. For the inherent defects in the belief logic method, it is difficult to analyze the fairness, timeliness and other properties of optimistic fair exchange protocol.Currently, the analyzing and designing of optimistic fair exchange protocol is one of the hottest research fields. The optimistic fair exchange protocol keeps a balance between fairness and efficiency. In the optimistic fair exchange protocol, the trusted third party only plays the arbiter instead of directly involving in the process of data exchange. So, during the transaction process, the number of requesting on the trusted third party is much lower than those of other types of fair exchange protocol, which avoids denial service attacks on the trusted third party. However, the optimistic fair exchange protocol leads to a branch structure, and there are several possible outcomes which make the protocols'formal analysis turns to be more complex and difficult.This dissertation studies the optimistic fair exchange protocol and its formal analysis techniques, including three following aspects: first, a literature review of fair exchange protocols and their formal techniques; second, a research of formal model, logic and automatic proof techniques of optimistic fair exchange protocols; third, a study of security and applications techniques of optimistic fair exchange protocols in e-commerce. The main study and innovative results of this dissertation are as follows:1. Basic theories and properties of fair exchange protocols are reviewed and analyzed, and some important properties are re-defined, such as fairness and the like. 2. The main methods of formal analysis of fair exchange protocols are reviewed, and the advantages, disadvantages and problems of each method are discussed as well.3. A new formal model of optimistic fair exchange protocols is proposed. The new formal model turns channel errors into channel attacks, divides the protocol participants into honesty ones and dishonesty ones, and attributes the conspiracy between intruders and dishonest participants as two types of Dolev-Yao intruders. Case analysis shows that the new model simplifies the problem space.4. A formal logic of optimistic fair exchange protocols is proposed. The new logic adopts the syntax structure of the belief logic, and defines optimistic fair exchange protocols as the evolution system with the Kripke semantic structure. Case analysis shows that the new logic has been successfully used to analyze the fairness and timeliness of optimistic fair exchange protocols.5. Based on Isabelle, an interactive theorem proving framework, the automatic theorem proving technology of logics and models in this dissertation are achieved. A more active attacker is achieved using Paulson induction, and the ability of the attacker to acquire knowledge initiatively is described as the inductive function to parsing and combining messages. The channel assuming is modeled as the behaviors of dishonest participants in order to reduce the complexity of the simulation protocol.6. The concept of dual authorizing in partially blind signature is put forward, which solves a problem, that is, bank manager in the abuse of power maliciously issues e-coins in electronic payments. A scheme of partially blind signature with dual authorizing is designed, and its security is proved under the random oracle model. Comparative analysis shows that the new mechanism has a high computational performance.7. A new optimistic electronic payment protocol is introduced. The scheme of partially blind signature with dual authorizing is employed, while off-line electronic cash payments (no need of online bank payment support) and optimistic fair exchange are achieved.The studies of formal technology in security protocols with the complex structure and e-commerce security are booming. There are some theoretical and practical significance in this dissertation for promoting those research fields.