随着计算机网络与信息安全技术的迅速发展,电子商务活动出现了更为复杂的交易过程,一次交易可能涉及多个买方或卖方。为了实现多个参与方的安全交互,出现了各种各样的多方安全协议(Multi-party Security Protocol),如多方不可否认协议、多方公平交换协议、多方认证邮件协议、多方合同签约协议等。与一般的安全协议相比,多方安全协议的复杂度大大增加,同时它对带宽等涉及效率的特性要求越来越高,需要更加复杂的密码学基础。因此,多方安全协议的设计和形式化分析过程更为复杂,目前已成为信息安全领域的一个重要研究方向。多方安全协议是建构在底层的安全技术基础之上的,选择具有不同特性的安全技术将会影响到最终多方安全协议的效率、安全性等。除了使用传统的数据加密和数字签名技术外,多方安全协议更多地采用了组加密技术、可验证秘密分享、签密及门限签密技术。组加密是一种基于CRT和公钥密码机制的加密技术,它产生一个只有组成员才能获得的密钥。秘密共享是信息安全和数据保密中的重要手段,可验证秘密分享(VSS)是设计多方安全协议的一个基本工具。签密(Signcryption)是在一个逻辑步内同时实现签名和加密,它可以消除因使用可信第三方TTP产生的通信瓶颈,从而大大提高安全协议(包括两方和多方协议,特别是多方安全协议)的运行效率。本文首先对多方安全协议涉及的相关技术进行研究,并给出一些典型的多方安全协议实例。多方安全协议由于涉及多种密码学与信息安全技术,在进行多方安全协议设计时不可避免地会出现一些缺陷。目前已经有很多种研究安全协议的理论和方法,其中形式化方法是多方安全协议分析的主要方式。安全协议形式化分析方法主要分为三类:基于知识和信念的形式逻辑方法、模型检测方法和定理证明方法。本文主要对基于逻辑的形式化方法与模型检测技术及其在多方安全协议形式化分析中的应用进行了系统研究,重点对SVO逻辑的扩展及其在多方安全协议分析中的应用进行了研究。另外,我们还对基于博弈的ATL逻辑及其在多方安全协议的形式化分析中的应用进行了研究。总的来说,我们从理论和应用两个方面研究了多方安全协议的形式化分析相关技术。主要工作有以下几个方面:1.对多方安全协议涉及的组加密、可验证秘密分享方案、签密技术进行了研究,这些技术在多方安全协议的设计和改进中非常重要。在此基础上对门限签密技术进行研究,提出了一个基于椭圆曲线密码体制的(t,n)门限共享解签密方案。该方案除了计算量与通信量少外,还具有保密性、认证性、不可伪造性、不可否认性、抵抗接收组成员欺骗等特点,可以满足群体通信的要求。2.对基于逻辑的安全协议形式化分析方法进行研究,重点对SVO逻辑的基本符号、推理规则、推理过程、SVO逻辑的语义及SVO逻辑的特点进行阐述,指出用SVO逻辑进行安全协议(包括两方和多方安全协议)形式化分析时存在一些亟待改进的缺陷。3.为了使SVO逻辑能用于分析两方或多方安全协议的不可否认性、时限性、公平性及哈希函数的描述,我们对SVO逻辑形式化方法的各种扩展方法进行了系统地研究,并用扩展SVO逻辑的推理规则对新ZG不可否认协议进行了形式化分析。4.对一种基于SVO逻辑的新形式化方法进行分析研究,用标准的SVO逻辑基本符号对其推理规则进行重新描述,对其中出现的错误进行了改正,使其能够更好地用于两方或多方安全协议的形式化分析。另外,我们提出了一种新的SVO逻辑扩展方法,并用它对改进的电子支付协议进行了形式化分析。5.SVO逻辑及其扩展公理不仅可以用于简单的安全协议安全性分析,也可以用于复杂的多方安全协议的不可否认性、公平性、时限性、基于哈希函数的身份认证等安全属性的有效分析。我们对此进行了研究,并利用SVO逻辑的公理和推理规则分别对一个不含TTP的多方不可否认协议的不可否认性和一个基于双重组加密的多方不可否认协议的公平性进行了形式化证明。6.对基于博弈的ATL逻辑及其在多方安全协议的形式化分析中的应用进行了研究。使用ATL逻辑和模型检测工具MOCHA对著名的Markowitch-Kremer多方不可否认协议进行建模分析,发现该协议存在的不公平性问题,通过增加时间限制方法对该协议进行改进,使其同时具有时限性和公平性。