网络安全协议的安全性是网络安全的重要基础,安全协议的安全性分析与验证是当今计算机安全领域中研究的热点和重大课题。形式化方法是安全协议分析的主要方法和可靠途径。目前常用的形式化分析方法有逻辑推证、模型检测及定理证明等,其中模型检测作为一种提高软硬件系统,特别是Safety-Critical系统的安全性与可靠性的自动分析与验证技术,以其简洁明了和自动化程度高而倍受注目。本文围绕安全协议形式化分析这一前沿领域,研究基于模型检测技术的安全协议的自动分析与验证技术,主要工作及成果有:1.为了能够便于计算机自动实现对安全协议的分析,本文作者通过对大量的安全协议实例进行分析与验证,归纳出协议的通用建模算法和协议存储的数据结构;2.扩展文献提出的协议描述语言PDL(Protocol Description Language)的语义描述能力,使其具有更强的语义描述能力,更具通用性:3.在对协议建模时采用了原子序列atomic和d step、偏序规约、语法重定序及类型检查等优化策略以提高验证效率,有效地缓解了模型检测过程中的状态爆炸问题;4.设计并实现了一个网络安全协议自动分析系统“安全协议自动分析系统”,该系统能够对认证协议及有可信第三方的电子商务协议进行自动分析,检测协议是否存在漏洞,如果存在漏洞,系统能够以图形化的方式显示攻击路径。该系统具有较强的实用性,可作为网络系统安全性评测以及安全协议设计的有效辅助工具。