随着网络的飞速发展和信息交互量的不断增长,信息安全的问题受到了越来越多的关注。为了维护网络环境的安全,构建正确的安全协议是必要的。然而,如何保证安全协议的安全性,如何使协议的设计满足安全性,如何提高自动化验证的效率都是安全协议需要探索的问题。为了保证安全协议的安全性,研究人员提出了形式化分析方法,虽然该方法成功的发现了许多安全协议的漏洞和缺陷,但是这些方法一直存在着问题。一些形式化方法本身不完善,因此无法适用于某些安全协议的认证。现有的自动化工具资源占用量大,对系统要求高,鉴于此,本文以串空间模型和认证测试理论为基础,针对上述三个问题进行了深入的研究,并取得了有效的解决方案。本文首先介绍了安全协议研究背景及目前的发展现状,以及串空间模型的基本概念,原始的基于串空间模型仅仅考虑到了贫乏的密码原语,在安全协议中该模型不能描述和分析某些密码,例如哈希函数和签名。为了解决这个问题,本文提出了一种扩展的串空间模型,分别对消息项,消息子项,和入侵者模型进行了扩展。其次,在串空间模型的基础上引入了认证测试方法,介绍了认证测试理论的三种认证测试的方法以及相应的认证测试规则,以Needham-Schroeder公钥协议为例,应用了相关的理论。并且重新定义了一个转化边和出测试,证明了该理论的正确性,应用改进的协议Wide-Mouth Frog Protocol来验证重新定义的转化边和出测试的正确性。最后,实现了认证测试方法的自动化的安全验证算法。该算法从正面证明协议是否能够满足安全属性,利用串空间模型和认证测试方法中的节点间的偏序关系可以有效的减少了状态空间的生成数量,避免了协议验证过程中的状态空间爆炸问题,并通过实验验证。