成果名称：网络安全协议技术及其系统

所属学科：网络与信息安全
成果概况：
 　　通过建立新的代数系统及其逻辑理论，创造性提出新的安全协议形式化模型，突破了安全协议安全性分析的算法复杂性、安全协议分析约简和安全协议一致性等难题，建立新的安全协议安全性分析技术和设计方法。研制成功了新的安全协议形式验证工具，设计了安全可靠的安全协议及其解决方案。为军用及民用安全协议的安全性评测提供了有效的形式化验证技术和工具，提高分析效率和可靠性，取得了良好的社会和经济效益。

水平及特色：
　　建立新的密码协议代数CPA及其理论，为安全协议形式化研究奠定了更为坚实的数学理论基础；通过对安全协议的攻击序列空间等价划分，为突破安全协议分析算法复杂性技术；提出泛多项式方程新概念及其求解算法，约束分析中冗余状态，设计了高效的安全协议自动分析算法，可高效地处理无限状态空间，并能构造出攻击过程，应用结果显示算法更可靠、高效；完成了高效的安全协议安全性分析系统ACT-SPA，并应用该系统分析了二十多个安全协议，发现了国际上未见发布的安全协议攻击和新的缺陷；提出了新的算法，设计了一系列高效实用的安全协议及其解决方案，解决了其中瓶颈性难点。

经济效益和社会效益：
　　应用于对网络系统进行高安全级别评测，发现系统的安全性隐患，提高系统的安全防护能力。安全协议的安全性评测是网络安全系统评测的核心，人工进行协议分析的难度和代价是非常高的，而且分析结果往往不可靠，特别是高级别安全性系统，必须经过形式化验证以保证其安全性，然而，看似简单的安全协议往往隐藏着难以察觉的缺陷，其理论研究和关键技术中尚有许多国际上未解难题，挑战性很强，研究和技术难度很大，导致国际上学术研究和有效的系统开发艰难，以至于目前国内外缺乏高效、实用的形式化验证工具，尤其国内此前尚未研制出可用的安全协议形式化验证系统。项目成果应用于检验、评估和测试安全协议的安全性，不仅可提高安全协议分析效率，而且更重要的是确保分析结果的可靠性，为安全协议的安全性评测提供了重要的科学依据，对发现网络未知的安全隐患，保障网络安全系统的高度安全性发挥了重要作用。

社会评价和获奖：
    该项成果2002年12月通过会议鉴定：“研究具有原创性，达到国际领先水平；系统具有较大创新性和应用前景，处于国际先进水平”。
    成果获得2004年度国家科技进步二等奖（2003年度国防科技一等奖）。