Formal Analysis And Design Of Fair Exchange Protocols

With the surprisingly rapid development of the electronic commerce, the rising security problems of e-commerce are worrying both its suppliers and consumers, and becoming the increasing concerns of government and supervision departments. Fairness is the core attribute of e-commerce securities, and fair exchange protocols are the core protocols that guard e-commerce securities. Designing secure and efficient fair exchange protocols is an urgent task and an inherent requirement for the development of e-commerce. Security analysis of fair exchange protocols is the keystone and the most difficult part of analyzing e-commerce protocols. Therefore, both the theoretical research and its application of designing and analyzing fair exchange protocols are of great importance.Formal analysis is the generally acknowledged method of analyzing security protocols, and has been widely used in security analysis of all kinds of protocols. Many important results have been achieved since formal analysis was introduced. This paper first puts its focus on the analysis and research of the existing formal models and methods, and then makes intensive study, in the area of fair exchange protocols, on protocol features, formal specification of protocol attributes, formal description of protocol procedures, and formal proof of protocol securities. Finally, the paper addresses problems in designing efficient, secure and practical fair exchange protocols.The main contributions of this paper are as follows:1,Comprehensive research on the existing formal methods of security protocol analysis, especially the intensive research on BAN logic, game-based ATL logic and the strand space model, and their advantages and disadvantages in analyzing fair exchange protocols.2,Extensions of the strand space model for the purpose of enhancing its expressive and analysis capability. The extensions include improving the proving method of Authentication Tests, adding the formalism of the quality of different communication channels, introducing parallel-edges to describe concurrent message transmissions in the protocol procedures, and introducing a partial order into directed-graphs to compare how much fairness-data has been achieved. Intensive survey is also made on the concepts such as fairness, non-repudiation, optimistic fair exchange, and protocol parties versus attackers. Based on the extensions and the survey, formal definitions of the security properties of fairness, timeliness, viability are presented.3,Presentation of a formal pen-and-paper method, based on the strand space model, for analyzing fair exchange protocols. Using this two-stage method, the cooperation and confrontation relationship among participants of the fair exchange protocols can be easily expressed in the concept of conditional reachable states. When analyzing protocols using this formal method, it is found that the concurrency and mutual exclusion between the sub-protocols are crucial to the fairness of the protocols. 4,Formal analysis of some existing fair exchange protocols including the Asokan-Shoup-Waidner certified e-mail protocol, the Zhou-Gollmann offline non-repudiation protocol, and the Kremer-Markowitch multi-party fair exchange protocol. Two weaknesses were found with the ASW protocol, and an improvement to the protocol was made. With the ZG protocol, a weakness was found for the first time and improvement proposed. Improvement was also proposed to the KM protocol to deal with its problems of choosing the NRR user-set, the startup time of recovery protocols, and the way of getting the NRR user-set. All of improved protocols were formally analyzed on the properties of fairness, timeliness and effectiveness.5,Design of four typical fair exchange protocols. Among them, the certified e-mail protocol is very efficient with its main protocol only having three message transmissions. The Fair Electronic Purchase of Goods, the FEP protocol, does not depend on any extra trusted third party, and satisfies abuse-freeness, which is the first of this category. The two offline multi-party contract signing protocols have simple structure and great efficiency, the best performance as far as we know. In addition, all of the protocols newly designed in the paper were formally analyzed.The results of this paper are of importance and values for not only the research and construction of e-commerce, but also the study and establishment of electronic government and military information systems.