随着网络及电子商务的迅猛发展，信息安全问题变得越来越重要，作为基础的安全协议的安全性成为了关键问题，事实证明，协议的安全性分析是很有挑战的工作。形式化分析方法的出现不但使分析过程更有章可循，还能实现自动化分析以防止人工错误。在众多形式化分析方法中，串空间模型以其高效、严谨和直观的特点受到广泛推崇，将形式化分析技术推向了更高的高度。　　本文首先介绍了安全协议的基本概念和安全性质，及现有的形式化分析方法，重点研究了串空间模型理论，在此基础上对现有的自动化分析系统进行研究，提出了一种基于串空间模型理论的安全协议自动化分析方法，并实现了自动化分析系统。本文的主要工作如下：　　1.在深入研究了串空间模型理论的基础上，针对现有自动化分析工具存在的状态空间爆炸的问题，结合串空间模型理论中的认证测试理论和参数一致性验证算法，提出了一种基于串空间模型理论的安全协议自动化分析方法，实现了对安全协议机密性和认证性的验证，并找出其中的安全缺陷。　　2.基于提出的自动化分析方法，使用C++语言开发了基于串空间模型理论的安全协议自动化分析方法的原型系统。该系统应用串空间模型理论，将输入的安全协议转化为形式化描述，并对消息项进行预处理，然后使用提出的自动化分析方法对协议的机密性和认证性进行验证，从而达到对协议整体安全性进行分析的目的。　　3.应用本文实现的自动化分析系统分析了Otway-Rees协议和Yahalom-Paulson协议的安全性，发现了通信主体双方在认证过程中对其中某些参数无法达成一致的缺陷，该结论与使用理论分析所得到的结论一致。　　4.应用本文实现的自动化分析系统分析了3GPP AKA协议的安全性，指出了协议的认证性无法满足的缺陷，并针对该缺陷构造出相应的攻击方法，可导致用户的密钥泄露，身份被伪冒。　　通过测试可知，根据本文实现的原型系统，在用于实际的安全协议分析时，不仅能够发现安全协议的已知缺陷，还能分析出协议中存在的未知问题，且与同类自动化分析系统相比适用性更广。