随着网络技术的发展，网络应用己经日益渗透到我们生活的方方面面，但网络给人们带来巨大便利的同时也带来了一些潜伏的不安全因素。作为通信基础的协议，承载着网络中通信的所有数据和信息，担当着通信方之间的通信桥梁，如何从协议的角度实现安全是一个重要而基本的研究课题。使用密码算法的安全协议为开放网络中的安全通信提供了基本保证，但实践证明，即便是一个简单的协议，其分析也是不容易的。协议的分析需要一套严格的形式化方法。形式化的分析方法是采用各种形式化的语言或者模型，为安全协议建立模型，并按照规定的假设和分析、验证方法证明协议的安全性。形式化的分析方法是当前分析安全协议领域研究的热点。近几年来，密码学家提出了许多关于安全协议的形式化分析方法，以检验协议中是否存在安全缺陷。串空间模型是一种著名的安全协议形式化模型，它的提出本身体现了协议形式化分析领域的发展方向，它结合了多种形式化方法的思想和技术，而且串空间理论是定理证明方法，可以手动的完成证明，得到可信的结果。该理论简洁易用，而且基于图论对协议进行描述，可以使用图形表示在协议证明中提供辅助说明。从串空间模型提出到现在，已经有研究者利用它发现了一些协议的漏洞，也有不少研究者利用它设计出了新型的安全协议自动分析工具。可见，这是一种很有研究前景的形式化模型。但是基本的串空间理论只能分析简单的使用连接、加密操作的安全协议，且对攻击者的能力描述有限，大大限制了其可分析的协议的范围。随着二十世纪七十年代以来，各种密码算法已经大量应用于安全协议中，如签名、散列函数等。为了能够分析更多类型的数据类型和操作，我们对串空间理论进行了扩展和完善。本文的主要工作有以下几个方面：●原理性阐述了几个具有代表性的安全协议形式化分析技术，其中详细阐述了串空间理论的定义、分析协议的方法和原理。●从语义上研究串空间模型，针对BAN逻辑语义不明确的问题，给出了基于串空间模型的逻辑的语义表示，并对BAN逻辑进行扩展，重新定义了BAN逻辑的协议分析过程。●介绍了串空间理论两个重要的发展：理想和认证测试。●对基本串空间理论和认证测试进行了扩展，包括项代数的扩展和攻击者模型的扩展，加入了对散列操作、签名操作的描述和分析能力。本文的主要创新之处为：●给出了基于串空间模型的BAN逻辑的语义表示，并对BAN逻辑进行扩展。●扩展串空间模型，使其能够分析含有签名、散列函数的协议。