随着网络的普及以及电子商务和电子政务蓬勃兴起,安全协议变得越来越重要,确保安全协议的安全性已经成为一项重要的研究课题.安全协议分析是一个很难解决的问题,20年来为了应对这一挑战,科学家们投入了大量的精力.在已有的理论和方法中,形式化分析方法的成果比较突出,其发展前景被专家们普遍看好,该文第二章对此进行了综述.串空间(STRAND SPACE)模型由F′abrega、Herzog和Guttman三人提出,它是分析安全协议的一种实用、直观和严格的形式化方法,它充分吸收了前人的研究成果,模型使用一种节点间存在因果关系的有向图来表示协议的运行.D.Song对串空间模型进行了扩展,并开发了安全协议自动验证工具ATHENA.在深入研究串空间理论的基础上,该文从理论和算法两个方面对串空间模型进行了扩展和完善.在理论上,该文引入了理想的语义,并首次使用了理想的概念对安全协议的秘密性进行严格的定义,同时使用理想的命题逻辑公式表示安全协议的秘密性;另外,该文修正了F′abrega、Herzog和Guttman三人文献中的一个引理的证明,原有的证明是不完善的.在算法上,该文增设了一条状态删减规则,并进行了严格的证明;另外,对模型检测算法进行了修改,使得算法可以找出协议在限定搜索深度下所有攻击反例.我们使用JAVA语言对该文的模型检测算法进行了具体实现,开发了一个拥有自主知识产权的安全协议自动验证工具AVSP.对已经进行的实验结果分析表明,该文对串空间模型的扩展是正确的和有效的;另外,利用AVSP我们发现了Woo-Lam<4>认证协议的一个新的在现有的文献中没有公布的攻击.