基于约束构造算法的密码协议安全性分析

摘要：

基于形式化方法开发自动分析工具是密码协议安全性分析的一种有效的方法, 然而, 由于密码协议参与主体的任意性、消息运算复杂性和运行的并发性, 密码协议的安全性分析是高度计算复杂性的难题. 基于最近提出的密码协议代数(CPA)模型, 采用代数方法描述密码协议活动, 精简密码协议描述, 提出一个高效的密码协议安全性自动分析算法. 该算法通过泛多项式方程求解技术, 减少密码协议安全性分析过程中产生的冗余状态数量, 并可提供在无限状态空间运行的协议安全性分析. 根据该算法, 实现了一个密码协议自动分析系统ACT-SPA, 应用该系统分析了二十多个密码协议, 结果显示系统显著提高了运行效率, 并发现了新的密码协议攻击.

关键词：密码协议、形式化分析、安全性验证

所属期刊栏目：35

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金90412011;国家自然科学基金;国家重点基础研究发展计划973计划2005CB321803;国家高技术研究发展计划863计划2003AA144150

在线出版日期：2005-11-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共22页

页码：1009-1030