计算机网络的高速发展和网络新应用的不断涌现给网络安全带来了很大的冲击,网络安全成为新的信息安全的热点;安全协议作为计算机网络安全体系的重要组成部分,也就变得越来越重要。然而,由于安全协议的复杂性,设计一个完美的安全协议是十分困难的,许多公开发表的安全协议中后来被发现它们存在各种各样的安全漏洞。因此,以确保安全协议正确性为目的的安全协议分析成为一项重要的研究课题。安全协议分析可分为形式化分析和非形式化分析,其中,形式化分析方法是安全协议理论研究的热点之一。常见的形式化分析方法有BAN逻辑,Kailar逻辑,SPI演算,CSP方法,串空间模型等。串空间模型理论是安全协议分析领域最新的研究成果,它是在1998年由Thayer, Herzog和Guttman提出的,具有高效、直观、实用等特点,不仅可以用于证明安全协议的正确性,还可以用于构造攻击,揭示安全协议的内在缺陷。该方法已经成功地分析了Needham-Schroeder-Lowe协议,Otway-Rees协议,Yahalom协议等诸多协议,被公认为是一种先进的高效的协议分析方法。本文以串空间理论作为研究基础,主要进行了以下研究:(1)深入研究串空间模型的基础理论,应用串空间模型分析了Natalia Miloslavskaya等人提出的一个双向认证协议,发现该协议在认证方面存在缺陷,并对该协议进行了改进。(2)对运用串空间理论分析不可否认协议进行研究,发现了以往运用串空间理论分析协议公平性的两个问题,并给出了解决方法。随后对不可否认协议中弹性信道、同步消息等特定假设条件,采用串空间理论的方式进行形式化描述及推理,从而为串空间理论分析不可否认协议扫除了障碍。然后以一个实例来说明如何运用串空间理论证明不可否认协议的公平性,其中,关键之处是如何构造正确的命题。(3)分析TEENP不可否认协议,发现它的安全缺陷,在此基础上提出了一个新的不可否认协议。同时,对另外两个不可否认协议进行分析,发现以往文献中未提及的新的漏洞。(4)此外,还对不可否认协议中的公平性,异常数据处理等问题提出了自己的一些想法。