该文对安全协议的特点作了深入的探讨.通过对目前安全协议的检验方法的研究,对安全协议分析有了深入的认识.模型检验方法是一种形式化的安全协议检验技术,该技术建立有限状态系统,验证有限状态系统的性质,便于实现自动化.而设计安全协议自动检验工具是提高协议检验效率的必然选择之一.Strand空间模型把协议的描述和安全属性都转化为图的结构,有利于借助图的理论和算法来分析协议.该文将Strand空间模型和模型检验技术结合起来,设计了基于Strand空间的安全协议模型检验方法.但是模型检验技术都面临着较突出的状态空间爆炸问题.因此,如何解决好这个问题,是模型检验方法的重要部分.该文对安全协议模型检验方法的研究,从安全协议的安全性质入手,将其归结为同一形式的逻辑公式,把对安全性质的验证转化为对逻辑公式的求解,使得检验系统可以在统一的模式下进行.针对使用Strand空间模型的攻击者角色和合法参与者Strand实现对目标的绑定的方法,提出以攻击者知识来代替攻击者角色的作用,用攻击者知识和Strand集合来表示状态.对于目标的绑定,在状态内部进行判断,将状态处理表示为使用攻击者知识对Strand集合进行处理,只以增加协议合法参与者Strand作为产生后续状态的条件.在对后续状态的求解过程中,充分考虑加解密方法和身份认证的关系,通过加入一些限制条件,尽量避免产生不可达状态.将终止状态划分为不可达状态,安全状态和不安全状态,通过对终止状态的判断来实现验证.通过这些步骤,大大地减少了状态数目,避免了状态空间的急剧增长,有效的解决了状态空间爆炸问题.当然这种方法是以增加每个状态的处理的复杂性为代价.在对方法进行研究的基础上,实现了安全协议自动检测工具.在保证功能实现的基础上,也充分考虑了计算的效率问题.为了方便用户使用,在人机交互方面也做了大量的工作.该工具应用在一些安全协议的分析尝试上,取得不错的效果.