Rational Model Of Fair Exchange Protocol And Its Formal Analysis

In e-commerce or online application environment, participants have the rational characteristics(these participants have been called rational participants). Rational exchange protocol gradually cause the attention of scholars both in the domestic and international by introducing the rational participants in the traditional exchange protocol, becoming the hot topic which comes from the crossing subject of cryptography and game theory. It has important research significance that considering the participants' self-interest, establishing a rational exchange protocol based on game theory and constraint participants choice behavior.Formal analysis is an kind of effective method to analysis the cryptographic protocols through that it is necessary to analyze rational fair exchange protocol. In this paper, the main research work is as follows:(1) Exchange protocol has modeled by extensive mixed strategy game and the entropy function has introduced to discuss the fairness in the process of exchange. In addition, the rational fairness has formally defined by using the concept of mixed strategy Nash equilibrium under the principle of the fairness in the process, and on the basis of this model to construct a new rational exchange protocol.(2) The reputation of the participants as its long-term interests, and constructs the appropriate utility function to describe the participants' benefits. On the other hand, the rational exchange protocol model under the reputation mechanism has established that based on repeated game, and the rational fairness has formally defined by using the concept of repeated game theory of Nash equilibrium.(3) ATL can analyze and verify the fairness of the traditional security protocol. But considering the participants' self-interest, ATL can't formally analyze cryptographic protocols.So by adding mixed strategy, utility and the preference in CEGS, we put forward mATEL and give the formal definition of mixed strategy rational exchange protocol. Finally, a formal analysis of the protocol is given with the mATEL.