保护通信系统信息安全的核心技术包括密码系统和密码协议(也称安全协议)。系统的安全性不仅依赖于所采用的密码算法强度，而且与算法所使用的环境(安全协议)密切相关。密码系统相对比较成熟，攻击的代价是相当大的。相对密码系统而言，密码协议是比较脆弱的，很容易受到攻击。安全协议是通讯和网络安全体系、分布式系统和电子商务的关键组成部分，是安全系统的主要保障手段和工具。由于安全协议运行在复杂的分布式网络环境中，设计出的安全协议难免会存在安全漏洞，许多安全协议在使用多年后都被发现存在很严重的安全漏洞，例如著名的Needham-Schroeder公开密钥协议在公开17年后，它存在的入侵者攻击漏洞才被Lowe发现。如果使用存在漏洞的安全协议，势必会形成严重的安全威胁。因此，网络安全协议的研究具有很强的理论价值和现实应用背景。　　 形式化方法是提高软件系统，特别是safety-critical系统的安全性与可靠性的重要手段。多年来人们采用的安全协议分析与验证方法主要是形式化方法，形式化方法主要有模型检测和定理证明。模型检测是一种重要的形式化自动验证技术，以其简洁明了和自动化程度高而倍受注目，模型检测使用状态空间搜索的办法自动地验证系统是否满足其设计规约，此技术的成功应用归功于有效验证工具的开发和支持。SPIN是一种著名的分析验证并发系统逻辑一致性的模型检测工具，2002年被ACM授予最具声望的“系统软件奖”(System Software Award)。　　 本文使用模型检测方法，基于算法知识逻辑形式化分析安全协议，在分析和比较常用安全协议形式化分析方法及对应支撑工具优劣的基础上，设计网络安全协议验证模型生成系统，目的是发现安全协议中隐藏的漏洞并对协议加以改进。研究成果表现为：　　 1.形式化描述了安全协议的组成要素，包括消息、动作(迹)、消息状态及修改、协议运行及消息构造规则等，设计了协议描述语言PDL(ProtocolDescription Language)，PDL中初步体现了协议安全构建块(SecurityBuilding Blocks)抽象建模机制。　　 2.提出了基于算法知识逻辑的网络安全协议模型检测分析方法，用于显式地刻画入侵者模型能力，从理论上分析了其知识完备性。　　 3.开发了网络安全协议验证模型生成系统，能将安全协议的PDL描述自动转换为对应协议的Promela语言描述，调用SPIN模型检测器，自动找出攻击漏洞，当协议不满足安全性质时，可以用消息序列图MSC直观地列出攻击序列。　　 4.在网络安全协议验证模型生成系统中采用了多项优化策略(包括偏序归约、语法重定序以及静态分析等)解决安全协议模型检测过程中状态爆炸问题( State Explosion)，实验结果证实了系统采用这些优化策略的有效性及效率。　　 5.认证协议的实例分析(Needham-Schroeder协议、TMN协议、BAN-Yahalom协议、Helsinki协议、密钥交换协议IKEv2等)，发现了这些协议已公布的安全漏洞。