网络安全协议从功能上主要可分为数字签名协议、密钥交换协议、密钥分配协议、身份认证协议等。随着计算机网络的普及以及电子商务和电子政务的蓬勃兴起，网络安全协议的应用越来越广泛，确保网络安全协议的安全性已经成为一项重要的研究课题。20年来，业界投入大量精力对网络安全协议的分析进行了深入的研究，取得了较多成果。在现有的理论和方法中，形式化分析方法研究最为突出。本文对网络安全协议的形式化分析作了较为全面的综述。在前人研究基础上，F’abrega，Herzog和Gunman三人提出了串空间(STRANDSPACE)模型，使用一种节点间存在因果关系的有向图来表示协议的运行，是分析网络安全协议的一种实用、直观和严格的形式化方法。在深入研究串空间理论的基础上，本文对攻击者模型进行了扩展，增加了攻击者签名、签名验证和HMAC功能以及相应的初始化假设，并基于扩展模型进行了实例协议分析，找到了协议的漏洞。最后，本文分析了目前串空间分析工具的研究现状，并深入研究了基于软约束的串空间工具，借助分析工具Csoiver实现了对NSPK和NSPK-L等协议的实例分析，找到了NSPK和NSPK-L协议所受的中间人攻击和消息重放攻击。