计算机网络的高速发展和网络新应用的不断涌现给网络安全带来了很大的冲击,网络安全成为新的信息安全的热点;安全协议作为计算机网络安全体系的重要组成部分,也就变得越来越重要。然而,由于安全协议的复杂性,设计一个完美的安全协议是十分困难的,许多公开发表的安全协议中后来被发现它们存在各种各样的安全漏洞。因此,以确保安全协议正确性为目的的安全协议分析成为一项重要的研究课题。安全协议分析方法可分为形式化分析方法和非形式化分析方法,其中,形式化分析方法是安全协议理论研究的热点之一。常见的形式化分析方法有BAN逻辑,Kailar逻辑,SPI演算,CSP方法,串空间模型等。串空间模型理论是安全协议分析领域最新的研究成果,它是在1998年由Thayer, Herzog和Guttman提出的,具有高效、直观、实用等特点,不仅可以用于证明安全协议的正确性,还可以用于构造攻击,揭示安全协议的内在缺陷。该方法已经成功地分析了Needham-Schroeder-Lowe协议,Otway-Rees协议,Yahalom协议等诸多协议,被公认为是一种先进的高效的协议分析方法。本文简要介绍了串空间模型的符号系统及其基本概念和理论,分析了基于串空间模型的极小元、理想与诚实、认证测试方法这三个分支的原理和应用场合,并体现了串空间模型的特点及优势。首先,本文以在无线局域网中广泛使用的IEEE 802.11i认证协议为例,用串空间模型中的相关符号和丛图对协议进行建模,并在此基础上用理想与诚实方法去证明协议的保密性和认证性。其次,对运用串空间模型理论分析重复认证协议进行研究,发现以往的运用串空间模型理论分析重复认证协议,都是把重复认证协议的不同子协议看成是独立的。为了解决这个问题,本文扩展串空间模型理论。在不同的子协议之间引入了一种新的因果关系,并重新定义了串空间与丛的定义,提出重复认证协议的两个属性,即重复认证一致性与重复认证保密性。最后,以Kao Chow重复认证协议为例。应用扩展后的串空间模型,对Kao Chow协议进行建模,并在此基础上用理想和诚实方法去证明协议的保密性和认证性。