网络协议的安全性分析和验证是当今计算机安全领域中研究的重大课题。协议安全性分析包括非形式化和形式化两种方法，形式化方法是安全协议分析和验证的主要方法。我们以大量的协议形式化建模研究为基础，以网络安全认证协议为研究对象，采用模型检测技术，开发了网络安全认证协议自动分析系统。该系统功能主要是用来对认证协议进行自动建模与验证。本系统分为用户界面模块、自动分析建模模块以及自动验证模块。用户界面模块为用户提供了直观的GUI界面，以可见即可得的方式对网络认证协议进行录入，用这种方式形成系统所接收的原语言——PDL(Protocol Description Language)；自动建模分析子模块设计了认证协议的形式化分析算法，对认证协议进行建模与性质规约；自动验证子模块内嵌SPIN，对建模过程进行自动验证并返回验证结果。本系统完成了对双方公钥类型和三方对称密钥类型协议的自动建模与验证，并成功地发现了N-S、Helsinki、TMN等协议的攻击漏洞。针对状态爆炸问题，本系统采用了atomic和steps、顺序重定向、缩减随机数变量的取值范围以及偏序规约等多项优化策略，实验结果表明系统采用优化策略具有有效性。此外，系统的创新点还体现在它的抽象性、效率性、自动化程度高、可扩展性以及友好的用户界面等方面。本系统具有较高的应用价值，可作为以网络认证协议为核心的网络通信系统安全性的有效分析、评测工具。