安全协议提供安全服务，是保证网络安全的基础。近年来，安全协议越来越多地用于保护因特网上传输的各种交易，保护针对计算机系统的访问。由于验证安全协议自身的安全性是十分困难的。因此，必须借助形式化方法，对安全协议进行分析。在众所多的形式化分析方法中，串空间模型是一种结合定理证明和协议迹的混合方法，将安全协议的形式化分析技术推向一个新的高度，由于其高效、严谨、直观的特点而受到广泛推崇。本文在对串空间模型研究的基础上，首次以串空间理论中的“理想”和“诚实”为工具，对改进的NSSK协议从机密性和认证性两个方面进行了严格的证明。结果表明，改进的NSSK认证协议实现了协议设计的目标，是正确有效的。安全协议的正确性主要体现在一致性和机密性两个方面。虽然串空间模型在协议分析过程中比其它形式化方法更为简洁和直观，但在分析协议为什么不正确及如何改进方面，同其他形式化分析方法一样，显得分析能力较弱。针对这一问题，本文在认证测试的基础上，提出了参数一致性矩阵的概念。利用参数一致性矩阵对安全协议的一致性进行分析，与原有的分析过程相比更为直观、简单，有效地揭示协议失败的原因，并针对这些原因给出相应的改进思路。