随着电子商务迅速进入人们的工作和日常生活,伴随而来的安全性问题也困扰着电子商务的服务供应方与消费方,并且成为政府及监管部门日益关注的对象。公平性是电子商务安全的核心属性,公平交换协议是保证电子商务安全的核心协议。设计出高效安全的公平交换协议是电子商务发展的内在迫切要求。公平交换协议的安全性分析,是电子商务协议分析的重点和难点。因此,公平交换协议的设计和分析具有十分重要的意义。安全协议的形式化分析是目前普遍认可的协议安全性分析手段,已经被广泛应用于各种安全协议的安全性分析,并取得了大量的成果。本文在分析和研究现有形式化分析方法的基础上,针对公平交换协议的特点,就公平交换协议安全属性的形式化描述、协议过程的形式化描述、协议安全属性的形式化分析,以及高效、安全、实用的公平交换协议的设计等问题展开深入研究。本文的主要工作归纳如下:一、综合研究了现有的安全协议形式化分析方法,重点研究了BAN逻辑、ATL博弈逻辑、串空间模型等三种形式化方法及其在分析公平交换协议方面的优缺点。二、对串空间模型进行了扩展以增强其对公平交换协议形式化表示和分析的能力。这方面的工作包括:提出一种改进的认证测试方法提高了串空间模型分析认证消息的能力,通过对串空间模型中协议的有向边引入权值扩展了串空间模型对通信信道质量的描述能力,通过引入“平行边”扩展了串空间模型对协议步骤的描述能力,通过在协议有向图中引入关于公平数据的偏序关系扩展了串空间模型描述和分析协议目标的能力。对公平交换协议相关的重要概念如公平性、非否认性、乐观公平交换协议、协议合法主体与攻击者等进行了深入讨论,并且给出了公平交换协议公平性、时限性、有效性等在串空间模型中的形式化定义。三、提出了一种对公平交换协议安全属性进行形式化分析的两阶段分析法。该方法基于串空间模型,将公平交换协议的主体之间以及主体与信道之间的合作与对抗关系用主体在协议有向图中的可达状态表达出来,对协议公平性等安全属性的分析转化为对协议有向图中可达状态的分析,分析过程包括递进的两个阶段。给出了公平交换协议的公平性、时限性、有效性等安全属性在两阶段分析法中的分析步骤。利用该方法分析有关协议时,发现子协议之间的并发和互斥关系是影响离线公平交换协议公平性的关键。四、用两阶段分析法对ASW挂号电子邮件协议、ZG离线非否认协议、KM多方离线公平交换协议等进行了形式化分析。发现了影响ASW协议公平性的两个漏洞并给出了改进的协议;发现了ZG协议的一个新漏洞并给出了改进的协议;发现了KM协议在认定非否认接收主体集合、决定恢复子协议的发起时间、选取TTP获取非否认接收主体集合的途径等问题上存在的不足,并给出了改进的协议。对所有改进后的协议的公平性等安全属性进行了形式化分析。五、设计了三种(四个)有代表性的公平交换协议,并对它们的安全属性进行了形式化分析。设计的离线挂号电子邮件协议只需一个包含三次消息交换的主协议及一个包含三次消息交换的恢复子协议,具有较高的效率。设计的公平电子购物协议不依赖于额外的可信第三方,并使用一种特殊的签名算法在电子购物协议中实现了非滥用性,协议保证了交易主体在协议中的公平性。设计的两个离线多方合同签署协议具有良好的结构,协议描述不因协议参与者数量的变化而变化;协议只需两轮,具有较高的效率;使用一种合同签署专用的签名算法使其中的一个协议满足非滥用性。并且给出了所设计的多方合同签署协议的形式化分析,在多方合同签署协议的设计和形式化分析方面都取得了较好的结果。本文的研究成果不仅对电子商务的研究和建设有着重要的理论意义和实用参考,而且对电子政务和军事信息系统安全问题的研究也有重要的参考价值。