论文摘要
伴随着计算机网络的普及和电子商务新政务的发展，信息安全问题变得越来越关键。要保证信息的安全性，仅仅依赖良好的加密算法是不够的，在实际应用中，还需要有可信的机制为各个独立的通信实体分发密钥，并且在通信实体间进行身份认证，这就使人们研究出各种安全协议。安全协议，是使用了密码学方法的网络通信协议，其目的就是为了在复杂的、不安全的网络环境中提供各种安全服务。安全协议的目的是保证信息的安全，但是如果安全协议本身存在漏洞，攻击者就会利用这些漏洞，对合法通信者造成危害。因此需要对安全协议进行分析和验证，来验证安全协议是否能够达到其预期的安全目标。Strand Space模型是由Fábrega，Herzog和Guttman三人提出的一种形式化方法，该模型的提出为解决安全协议设计与分析的困难提供了一种可能，它是现有的安全协议形式化分析方法中最为直观、简洁、严格和有效的方法。本文在深入研究串空间理论的基础上，做了以下几个方面的工作：1)深入了解了安全协议的安全性质，尤其是机密性与认证性，熟悉串空间理论模型及其协议验证方法；2)运用串空间模型分析了MY-Helsinki协议，证明了其在机密性与认证性方面的正确性，并分析了该协议在改进前存在缺陷的原因；3)分析研究了理想和认证测试在安全协议分析中的应用，分别运用理想和认证测试方法对Weakened-Yahalom协议的认证性进行了分析，并对二者进行了比较；4)分析并修改了动态串空间模型算法，总结了已有的状态空间简化规则，在认证测试理论基础上提出一个新的剪枝定理，修改了其结点绑定算法并增加了丛扩展规则。将剪枝定理应用于协议认证性质分析中，减少了协议分析的工作量，提高了协议分析效率；丛扩展规则的增加使得算法能够适用于包括发起者、响应者和服务器的三方协议。最后通过两个实例分别说明算法修改的有效性。