安全协议是构建网络安全环境的基石,是网络安全通信系统的核心技术,它的正确性对整个网络环境的安全起着至关重要的作用。然而如何保证安全协议的安全性,如何使协议的设计能够满足安全性的要求,如何提高安全协议自动化验证的效率等,都是安全协议研究领域不断探索的问题。为了保证安全协议的安全性,研究人员提出了形式化的方法。虽然形式化方法已经成功地发现了许多安全协议的漏洞和攻击,但是这些方法仍然存在很多问题。一些形式化的方法本身并不完善,因此无法适用于某些安全协议的验证;一些理论完善的形式化方法由于过于复杂而缺乏自动化工具的支持;现有的自动化协议验证工具资源占用量大,对系统要求高。鉴于此,本文以串空间模型理论和认证测试方法为基础,针对上述三个方面的问题进行了深入的研究,并且提出了有效的解决方案,取得了一定的科研成果。论文的研究内容主要包括以下三个方面:首先,对于串空间模型和认证测试方法理论在典型安全协议验证中的应用进行了深入的研究,通过形式化的验证指出协议中存在的安全漏洞,构造可能的攻击方式,并以理论分析结果为指导提出对这些协议的改进方案,最后使用理论方法验证改进协议的安全性。本文还以认证测试方法为理论基础,对通用安全协议的设计方法进行了研究。以Needham-Schroeder协议为例,使用基于认证测试的通用安全协议设计方法指导该协议的重新设计,并对重新设计后的协议应用形式化的理论方法证明其安全性。其次,在对认证测试方法深入研究的基础上,指出该方法在对称密钥协议验证中存在无法确定消息项初始产生主体的问题,以及由此可能引起的消息重放攻击和类型攻击。通过引入消息类型对认证测试方法进行了改进,提出了基于消息类型检测的改进认证测试方法,并通过对认证协议的验证表明了改进的认证测试方法能够有效地发现原有认证测试方法没有发现的类型攻击。与此同时,还将改进的认证测试方法应用于无线认证协议的验证,证明了改进的认证测试方法对无线认证协议安全性验证的有效性。