A New Method for Formalizing Optimistic Fair Exchange Protocols

It is difficult to analyze the timeliness of optimistic fair exchange protocols by using belief logic. For the problem, a new formal model and reasoning logic were proposed. In the new model, channel errors were attackers' behaviors, the participants were divided into honest and dishonest ones, and the attackers were attributed to two types of intruders. Based on the ideas of the model checking, the protocol was defined as an evolved logic system that has the Kripke structure. The new logic defined the time operators that describe the temporal relations among the participants' behaviors. By a typical optimistic fair exchange protocol, the article demonstrates the protocol analysis process in the new model. Two flaws were discovered and improved, which shows that the new method can be used to analyze the fairness and timeliness of optimistic fair exchange protocols.