随着网络技术和信息技术的迅速发展,计算机网络在诸多领域内的应用日益普及,然而由于其运行环境具有开放性,使得计算机网络在给人们带来巨大便利的同时,也产生一系列的安全问题,因此如何确保网络中信息的安全性成为亟待解决的问题。安全协议又称密码协议,是以密码学技术为基础,在不安全的公共网络和分布式系统中提供各种安全服务的一种通信协议。由于安全协议的安全性是评价网络好坏的一个重要指标,所以在安全协议投入使用之前,对其安全性分析就显得尤为重要。至今,安全协议的形式化分析和自动化检测己成为分析和研究安全协议领域的两个重要方向,而研制可靠实用的安全协议自动化分析工具也逐渐成为主流趋势。本文以串空间理论为基础,通过对当前存在的一些安全协议形式化方法和自动化技术进行比较分析,深入地研究了安全协议的自动化分析方法。主要内容包括：1)深入研究了安全协议的安全性质,针对当前运用比较广泛的形式化分析方法——串空间模型,通过研究构造方法,重点介绍了NSL协议的分析过程；同时,以SSM协议为例,探讨了如何使用认证测试验证协议的过程及设计原理。2)给出了一种基于串空间模型的安全协议自动化验证方法。在该方法中,针对参与方不检测某些消息的来源,只是将其作为消息的子项参与协议的运行的问题,通过构造和合法串结构相同的攻击者串的方式,给出了一种自动化验证方法；它不仅能够分析具有加密类型的攻击缺陷的协议,还将可信方引入到协议的参与方,使之能够分析具有重放类型攻击缺陷的协议,整个过程无需人工干预,直观和高效。在文章的最后借助两个实例,详细说明了该系统的验证过程,结果表明系统具有良好的性能。