随着网络的不断发展,网络信息安全变得日益重要,安全协议作为网络信息安全的基础,它的安全性变成了一个关键的问题。然而安全协议分析是一个很困难的问题,安全领域的科学家为此开发了许多不同种类的形式化分析方法和理论,本文在第二章中对安全协议及其形式化研究方法二十多年来的发展进行了综述和总结。串空间(STRAND SPACE)模型由Fabrega, Herzog和Guttman三人提出,是分析安全协议的一种实用、直观和严格的形式化方法。串空间方法包括了一个描述因果结构的偏序和一个类递归证明方法,提出了与所分析的具体协议无关的攻击者能力边界,是一种新型有效的形式化方法。本文首先从理论上对串空间模型进行了扩展,针对密钥协商协议中的单向HASH函数,利用诚实函数的概念,扩充了攻击者能力,同时也扩展了串空间中的相关定理;在对WTLS协议进行安全分析时,首先给出了协议的一个简化形式,得到了WTLS串空间,并结合理想和诚实函数的概念,分析了WTLS协议的秘密性和认证性,指出了Paulson关于TLS主秘密的弱理论改进的缺陷。本文给出了基于对称密码算法产生和发布共享秘密的Yahalom协议的串空间模型,并运用基于串空间理论的一种简便认证方法对其安全性进行了验证,证明了该协议的正确性;并且针对这一认证方法,给出了安全协议设计的几点建议。