The Mechanism Design On Fairness And Its Formal Analysis Of Rational Exchange Protocol

Secure protocol is one of the important methods to guarantee electronic commerce transactions,and its fairness is the key problem for secure protocols.The fairness of secure protocols is achieved by the trusted third party,however,for some scenarios,the cost of using the trusted third party leads to practical weakened.Therefore,it is great academic and applied value to study the rational fair exchange protocol without the third party from the view of game.Taking into consideration participants' self-interest behavior,this paper designs a two-party rational exchange protocol that satisfies the correctness and rational fairness based on the mechanism design,extensive form game and dominant strategy equilibrium method,and proves the completeness and soundness of the rational alternating-time temporal epistemic logic inference system,which is applied to formal analysis the fairness of the two-party rational exchange protocol.The main study works of this paper are as follows:(1)The formal definition of exchange protocols' rational fairness is proposed based on dominant strategy equilibrium,and the paper designs a rational exchange fairness mechanism that satisfy incentive compatibility based on mechanism design theory;Under the bounded rational assumption,the two-party rational exchange protocol is designed on the basis of rational fairness and exchange mechanism.(2)A formal description of rational fairness and game tree is given based on extensive form game,and the formalized analysis of rational exchange protocol is provided by using the inverse induction method.The results show that the proposed rational exchange protocol satisfies the correctness and rational fairness.(3)After improving the rational alternating-time temporal epistemic logic inference system,and its completeness and soundness are proved;a formalized description of the rational fairness is given based on the rational concurrent epistemic game structure of the rational exchange protocol;and on the basis of rational alternating-time temporal epistemic logic inference system,the fairness of the rational exchange protocol is analyzed by using inference system.This way expands and improves the theoretical systems of formal analysis for rational protocols.(4)On the basis of analyzing the traditional secure protocols of the electronic contract signing,a rational electronic contract signing scheme is put forward based on the proposed rational exchange protocol.This scheme provides a new way for realizing the fairness of the electronic contract signing by removing the trusted third party.