网络安全协议(或称密码协议)是网络安全体系中的关键环节,然而安全协议的设计却极易出错,攻击者常常可以绕开密码系统而通过安全协议来对系统发起攻击.随着网络应用的普及,对安全协议进行安全性评测已成为保障网络安全的一项重要任务.安全协议的安全性评测是指对协议的安全性进行分析、测试和评估,试图找出其中的安全缺陷,并做出相应的安全性评价结论.由于安全协议的缺陷往往非常隐蔽,一般分析方法通常难以发现;现在普遍认为,形式化方法是分析安全协议的最为可靠和有效的方法.以形式化方法为基础建立安全协议的自动分析工具(评测系统)成为当前的一个研究热点.该文以最近提出的一种原创性安全协议形式化分析理论——CPA理论为基础,成功研制了一个安全协议分析工具,并应用于安全协议的安全性评测中.该文主要贡献包括:1.设计并实现了一个安全协议评测系统——安全协议分析器SPA(Security Protocol Analyzer),一方面验证了CPA理论,另一方面为实际安全协议评测提供了一个有效的辅助工具.2.将SPA系统应用于具体安全协议的安全性评测中,分析了一些常见安全协议的安全性,并发现一个未见公开的对BAN-Yahalom协议的攻击方法.这项工作加深了我们对安全协议缺陷和攻击的认识,并为设计新协议提供了许多借鉴.3.针对实用网络安全协议的特点和形式化分析方法(工具)的局限性,从安全协议攻击分类的角度对安全协议评测方法进行研究,给出一种基于攻击者能力和攻击后果的二维攻击分类方法,并在此基础上提出一种面向实用网络安全协议的分级评测思想.