随着网络的普及、信息技术和电子商务的蓬勃发展,电子商务协议的研究越来越深入。交换协议是电子商务协议中很重要的一部分,通过对交换协议的建模和形式化分析来研究交换协议的设计和检测协议中的潜在问题。公平交换协议为了确保协议参与方的公平性,在协议执行过程中增加可信第三方来参与交换或者很复杂的通信计算来保证其实现。而理性交换协议尽管不保证公平性,但可确保理性参与者没有理由不去遵守协议且不需要可信第三方参与交换或以更少的通信计算。本文首先对交换协议及其形式化的研究与发展做了综述,并着重介绍了博弈论。本文的主要工作是应用博弈论对理性交换协议和公平交换协议进行建模和形式化分析。　　 在这个模型中,理性交换协议和公平交换协议被当作是协议参与方进行相互通信的博弈过程的策略集合,并且给出了理性交换和公平交换在内交换协议的各种性质的形式化定义。最重要的是,利用协议博弈中子博弈精炼纳什均衡的定义对理性交换做了形式化定义,并与Buttyan模型做了比较。公平性则定义在不完全信息的协议博弈及相应的博弈树上。根据这个模型以及这些形式化定义,通过对Syverson协议和ASW协议的建模和形式化分析演示了如何运用协议博弈模型去证明已有的理性交换协议和对公平交换协议的潜在问题的发现。