Formal Study Of Rational Exchange Protocols Based On Game Theory

With the rapid development of e-commerce,the study of the e-commerce protocols is in more depth.The exchange protocols is a very important class of the e-commerce protocols.We can use the research results of the model and formal analysis of the exchange protocols to guide the design of the exchange protocols,or make up for potential problems in the original protocols.This paper firstly make a systematic overview and analysis of the research and development of the formal analysis of the twenty years's exchange protocols.The fair exchange protocols ensure fairness to participants but at the exense of entities such as TTPs having to be involved in the exchange.By contrast,rational exchange protocols,although not ensuring fairness,assure that rational entities would have no reason to deviate from the protocol and,have the advantage of not needing the services of a TTP.The main goal of this paper is to apply concepts from Game Theory to both the modeling and formal analysis of rational exchange protocols.In this model, an rational exchange protocol is represented as a set of strategies in a game played by the protocol parties and the network that they use to communicate with each other.This paper give formal definitions for various properties of exchange protocols in this model,including rational exchang and fair exchange.Most importantly,rational exchange is defined in terms of a Nash equilibrium in the protocol game.The model and the formal definitions allow us to rigorously study the relationship between rational exchange and fair exchange,and to prove that fair exchange implies rational exchange,but the reverse is not true in general. Finally, this paper illustrate how the protocol game can be used for rigorous verification of existing rational exchange protocols by modeling and analyzing the Syverson's protocol,and formally proving that this protocol satisfy the definition of rational exchange protocol.