随着电子商务的蓬勃发展,电子商务协议的研究越来越深入。交换协议是电子商务协议中很重要的一类,可以通过对交换协议的建模和形式化分析研究的结果去指导交换协议的设计或弥补原协议中的潜在问题。本文首先对20多年来交换协议及其形式化的研究与发展做了系统的综述与分析。公平交换协议为了确保协议各方的公平性,不得不在协议执行过程中增加可信第三方来参与交换。而理性交换协议尽管不保证公平性,但可确保理性参与方没有理由不去遵守协议且不需要可信第三方参与交换。本文的主要工作是应用博弈论对理性交换协议进行建模和形式化分析。在这个模型中,理性交换协议被当作是协议参与方借助网络进行相互通信的博弈过程的战略集合,并且给出了包括理性交换和公平交换在内的交换协议的各种属性的形式化定义。最重要的是,利用协议博弈中纳什均衡的定义对理性交换做了形式化定义。根据这个模型以及这些形式化定义,本文对理性交换和公平交换的关系进行了详细的研究,并证明了公平交换蕴含理性交换而理性交换并不蕴含公平交换。最后,本文通过对Syverson协议的建模和形式化分析演示了如何运用协议博弈模型去严格证明已有的理性交换协议,并形式化证明了Syverson协议满足理性交换协议的定义。