随着因特网的普及,信息安全变得日益重要,如何在开放的互联网络上提供信息的保密性、完整性、可用性以及不可否认性服务成为研究的热点问题。在众多的解决方案中,安全协议是最有效的手段之一。但由于互联网的开放性和安全协议的并发性,安全协议的设计和分析极其困难。目前主要采用形式化方法来分析和验证协议的安全性。经过30多年的研究,安全协议形式化分析领域存在两种不同的方法:符号方法和计算方法。符号方法通过各种方法抽象描述协议中的消息、敌手以及密码学算法,结合各种工具验证协议的安全性。这些方法简洁易用,但存在可靠性问题:抽象过程过于理想化,一旦真实协议具有抽象协议未包含的实现细节,符号方法下证明安全的协议在实现时可能存在漏洞。计算方法则在计算模型下对协议忠实建模,其主要思想与密码算法的可证安全方法类似:将待证协议的安全性有效地归约到某个困难问题上。该方法也是目前大多数人认为最为可靠的安全性保障手段。但由于归约过程中涉及到很多概率和计算复杂度问题,计算方法的证明过程非常复杂,且易出错。目前,如何结合符号方法和计算方法的优点,得到一种既简洁易用、又具有计算可靠性的分析方法是安全协议形式化研究领域的研究焦点。沿着这个思路,本文从现有方法的分析和扩展、计算模型下安全协议的建模方法、计算可靠的定性验证和计算可靠的定量验证四个方面进行了深入研究,取得了一系列有价值的研究成果,主要体现在:1)自动验证工具CryptoVerif的扩展和分析研究。首先扩展了计算模型下著名的自动验证工具CryptoVerif对Zhou-Gollmann不可否认协议和Diffie-Hellman协议的证明能力,首次在计算模型下辅助(或自动)证明了Zhou-Gollmann和基于Diffie-Hellman密钥交换的Kerberos协议的安全性。其次发现了现有工作对上述两协议建模的缺陷,并提出了相应的修正方法。最后分析了CryptoVerif对安全协议和密码算法安全性的建模能力,提出了一种计算模型下使用逻辑方法对协议进行验证的研究思路。2)计算模型下的协议建模方法研究。首先提出了一种计算模型下的协议描述语言,可对安全协议主体的计算和通信行为进行准确建模,并在此基础上定义了协议逻辑,解释了计算模型下逻辑公式的语义。其次利用该方法建立了Needham-Scheoder-Lowe(NSL)和Challenge-Response(CR)的协议模型。最后将本方法与采用类似方法的计算协议组合逻辑(CPCL)进行了比较,分析结果表明本方法对协议的描述更为准确,能描述密钥查询、主体和密钥间的关联过程等行为。3)计算可靠的安全协议定性验证方法研究。首先建立了包含一阶公理、密码算法公理以及其他公理的证明系统,证明了公理系统的可靠性。与现有其他逻辑方法不同的是,本公理系统能对包括随机数生成、对称加密、公钥加密、公钥数字签名和消息认证码在内的密码算法的各种标准安全属性进行准确建模。其次比较了本方法与CPCL的证明能力,分析结果显示,CPCL对对称加密算法的安全属性建模存在错误,而本证明系统不存在。此外,本证明系统的密码算法公理包括时序属性,更适用于对协议安全性的证明。最后证明了NSL协议的双向认证性,验证了该方法的有效性。4)计算可靠的安全协议定量验证方法。首先对计算可靠的协议验证方法进行了概率扩展,建立了包含概率公理、随机数生成公理和密码算法公理的定量推理系统,并证明了其公理系统的可靠性。与CryptoVerif的定量方法以及经典的Adam概率逻辑相比,本定量验证逻辑建立在对概率事件明确定义的基础上,能有效兼容密码算法安全性中的概率因素,更适用于对安全协议的验证分析。其次,分析了CPCL的概率扩展能力,指出对其直接进行定量扩展的难点问题。最后,定量证明了CR协议的安全性,分析了证明结果。