基于约束构造算法的密码协议安全性分析 |
| |
作者姓名: | 李先贤 怀进鹏 |
| |
作者单位: | 北京航空航天大学计算机学院,北京,100083 |
| |
基金项目: | 国家自然科学基金重大资助项目(批准号:90412011)、国家杰出青年科学基金,国家973重大基础研究计划(2005CB321803),国家“863”高技术研究发展计划(2003AA144150)资助项目 |
| |
摘 要: | 基于形式化方法开发自动分析工具是密码协议安全性分析的一种有效的方法,然而,由于密码协议参与主体的任意性、消息运算复杂性和运行的并发性,密码协议的安全性分析是高度计算复杂性的难题。基于最近提出的密码协议代数(CPA)模型,采用代数方法描述密码协议活动,精简密码协议描述,提出一个高效的密码协议安全性自动分析算法。该算法通过泛多项式方程求解技术,减少密码协议安全性分析过程中产生的冗余状态数量,并可提供在无限状态空间运行的协议安全性分析。根据该算法,实现了一个密码协议自动分析系统ACT-SPA,应用该系统分析了二十多个密码协议,结果显示系统显著提高了运行效率,并发现了新的密码协议攻击。
|
关 键 词: | 密码协议 形式化分析 安全性验证 约束构造算法 CPA模型 |
收稿时间: | 2003-01-27 |
修稿时间: | 2003-01-272003-07-22 |
本文献已被 CNKI 维普 万方数据 等数据库收录! |
|