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

作　　者：李先贤[1] 怀进鹏[1] 

机构地区：[1]北京航空航天大学计算机学院,北京100083

出　　处：《中国科学（E辑）》2005年第10期1009-1030,共22页Science in China(Series E)

基　　金：国家自然科学基金重大资助项目(批准号:90412011);国家杰出青年科学基金;国家973重大基础研究计划(2005CB321803);国家"863"高技术研究发展计划(2003AA144150)资助项目

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

关 键 词：密码协议 形式化分析 安全性验证 约束构造算法 CPA模型 

分 类 号：TN918[电子电信—通信与信息系统]