乐观公平交换协议是一类典型的安全协议,用于在两个或多个主体之间安全、高效地进行电子交易。与其它安全协议相比,乐观公平交换协议在结构上较为复杂,从而更容易存在安全缺陷,同时也为其形式化分析带来了挑战。　　本文主要研究了乐观公平交换协议的形式化分析技术,所取得的主要研究结果有:　　(1)深入剖析了IETF(Internet Engineering Task Force)的IPSEC工作组提交的IKEv2协议草案;在对协议进行形式建模,以及应用CTL对相应的安全性质进行形式描述的基础上,借助SMV分析了协议的认证性、秘密性、和完整性,发现了两个攻击;对这两个攻击所产生的影响进行了讨论。　　(2)针对乐观公平交换协议,提出了一种基于有限状态机的分析模型;应用该模型,借助SMV分析了GJM电子合同签订协议,检测出由V.Shmatikov首先发现的缺陷;分析了ASW电子合同签订协议,指出在协议实现过程中应该注意的问题;分析了FPH挂号电子邮件协议,发现该协议存在安全缺陷。　　(3)针对所发现的安全缺陷,对FPH挂号电子邮件协议进行了改进;应用上述模型,对改进后的协议进行模型检测分析,分析结果表明协议达到了安全要求。　　(4)对C.W.Hao给出的协议运行模型及协议规格和分析框架进行扩充和改进,给出了一个较为完整的安全协议规格及验证系统;应用该系统,对ASW电子合同签订协议进行了规格,对其公平性进行了逻辑推证。