计算机网络安全问题日益引起人们的重视。安全协议是用来保证网络通信安全的重要工具。但研究证明安全协议大多数都有安全漏洞。作为信息安全的一项重要研究内容，安全协议的分析具有极为重要的理论意义和实际价值。论文以形式化分析方法为核心，对BAN逻辑与串空间理论以及模型自动校验工具SPIN进行了深入研究，并在此基础上提出了一种逻辑性更加严密，实用性更强的形式化分析方法。　　 本文了BAN逻辑与串空间理论的基本概念、主要推理规则以及分析方法，并用两种方法分别对Helsinki协议进行了分析，验证了Helsinki协议存在的安全漏洞。并藉此对BAN逻辑与串空间理论进行了对比分析，对二者的不足进行了归纳总结。理论方法对于安全协议的分析固然有效，但模型自动校验工具能够模拟协议执行的实际环境，从而使得对协议安全性的分析变得相当直观。对Promela语言的关键技术作了全面论述，介绍了利用SPIN构造及验证Promela语言描述的系统模型的基本步骤，并以Helsinki协议作为分析实例，重点讲述了如何用Promela语言实现对安全协议进行建模的思想和方法。在理论分析与模型校验工具分析相结合的基础上，提出了一种串行的安全协议分析方法，既用BAN逻辑分析随机数的新鲜性，用串空间模型来对协议的认证性进行分析，再借助SPIN工具用Promela语言对协议进行建模分析。通过对Helsinki协议及其改进协议的分析，发现此方法的逻辑性比BAN逻辑和串空间理论更加严密，而且实用性更强。