A Formal Analysis of Syverson's Rational Exchange Protocol
Hubaux Srdjan · 2002
In this paper, we provide a formal analysis of a rational exchange protocol proposed by Syverson. A rational ex- change protocol guarantees that misbehavior cannot gen- erate benefits, and is therefore discouraged. The analysis is performed using our formal model, which is based on game theory. In this model, rational exchange is defined in terms of a Nash equilibrium. where fair exchange would be impossible or inefficient. In (3), we propose a formalmodelfor rationalexchange protocols, which is based on game theory. In this model, an exchange protocolis represented as a set of strategies (one strategy for each party) in a game that is constructed from the protocol description. Rational exchange is formally de- fined in terms of a Nash equilibrium in the protocol game. We also propose formal definitions for various other proper- ties of exchange protocols, including fairness, and we prove that fairness implies rationality, but not vice versa. This jus- tifies the intuition that rationalexchange provides weaker guarantees than fair exchange does. In this paper, we use our protocolgame modelfor the for- malanalysis of Syverson's rationalexchange protocolpro- posed in (9). For this reason, we first introduce the protocol game modeland the formaldefinition of rationalexchange within this modelin Sections 3 and 4, respectively. We keep the presentation brief, since this materialhas al ready been presented in (3). However, for completeness and for making this paper easier to follow, we preferred not to omit this part. Then, in Section 5, we construct the protocolgame of the Syverson protocoland prove that it satisfies the definition of rationalexchange assuming that the communication be- tween the protocol parties is reliable. Finally, in Section 6, we show that relaxing this assumption leads to the loss of the rationality property.