作为网络通信的安全保障,安全协议是整个信息系统架构的安全基础。为了保证安全协议的正确性,研究人员提出了一系列基于形式化方法的自动化验证算法来对安全协议进行分析验证,并已经成功地发现很多安全协议中存在的漏洞和攻击,但这些算法只能指出协议中的漏洞和攻击,不能自动生成改进协议,而且这些算法还存在验证效率低、使用难度大的问题。鉴于此,本文以串空间模型和认证测试方法为理论基础,对以上问题进行深入研究,研究内容主要包括以下几个方面：首先,在深入研究形式化方法的基础上,详细分析了几种应用较为广泛的自动化验证算法,并针对现有算法的不足,提出了IVAP算法(Intelligent Validator for Authentication Protocols)。IVAP算法不仅能自动地完成协议的验证,而且还能根据不安全属性逆向搜索主体串树,自动生成改进协议并继续完成改进协议的验证。然后,详细设计并开发了基于IVAP算法的安全协议自动化验证原型系统,原型系统采用B/S架构,由安全协议图形转换接口模块、安全协议形式化描述接口模块、安全协议验证模块和改进协议生成模块四个功能模块组成。最后,用原型系统对一系列经典认证协议进行了实验验证,分析了在协议验证过程中所需的时间复杂度和空间复杂度,并把实验数据与其它同类算法作了详尽的比较分析。通过实验结果表明了IVAP算法的有效性和高效性。本文的创新工作有以下两点：1.提出了基于串空间的IVAP算法,在协议验证过程中,若发现协议有安全漏洞,则自动生成改进协议,在理论的应用上具有创新性；2.开发了基于IVAP算法的安全协议自动化验证原型系统,通过实验分析结果表明,跟其它同类系统相比效率更高,在理论的应用上具有创新性。