安全协议也称密码协议，是建立在密码体制基础上的高互通的消息交换协议，它运行在计算机通信网或分布式系统中，其目的是在网络环境中提供各种安全服务。安全协议是构建安全网络环境的基石，它的正确性对于网络安全极其关键。然而由于安全协议的执行具有高度不确定性，以致有些安全协议往往不如它们的设计者所期望的那样安全，存在很多缺陷和漏洞。纵观国内外的研究成果，安全协议的安全性分析是揭示安全协议缺陷和漏洞的重要途径，分析方法从最初的非形式化的攻击检验，到多种形式化分析方法并存，已经出现了百家争鸣的景况。本课题以基于串空间模型安全协议的形式化验证方法为主要研究内容，从理论和实践两个层面上研究了安全协议形式化验证的相关技术。主要工作包括：●在深刻理解安全协议基本概念的基础上，从安全协议形式化验证方法所应用的技术手段、技术特点入手，对安全协议的形式化验证方法进行了总结和分类。并对安全协议形式化验证若干热点研究方向进行了归纳和展望。●在归纳现有串空间模型理论的基础上，深入分析了串空间模型内认证协议正确性的含义，并提出了基于串空间模型安全协议形式化验证的三种典型方法。最后，还指出串空间模型在对安全协议安全性目标的证明中仍然存在的问题及进一步的研究趋势。●应用第三节所提出的基于串空间模型安全协议形式化验证的三种典型方法对NSL协议、Yahalom改进协议和X.509改进协议进行了安全性分析，并从方法有效性和方法的内在特点两个方面对三种串空间形式化分析方法进行了对比分析。