SPA 安全协议分析系统(可参考用于数学模型化).pdfVIP

第 28 卷 　第 3 期 计 　　算 　　机 　　学 　　报 Vol . 28 No . 3 2005 年 3 月 C H IN ESE J OU RN AL O F COM PU T ER S Mar . 2005 　 SPA :新的高效安全协议分析系统 李建欣 　李先贤 　卓继亮 　怀进鹏 (北京航空航天大学计算机学院　北京 　100083) 摘 　要 　研制高效的自动分析系统是密码协议安全性分析的一项关键任务 ,然而由于密码协议的分析非常复杂 , 存在大量未解决的问题 ,使得很多现有分析系统在可靠性和效率方面仍存在许多局限性. 该文基于一种新提出的 ( 密码协议代数模型和安全性分析技术 ,设计并实现了一个高效的安全协议安全性 自动分析系统 Securit y Protocol Analyzer ,SPA) . 首先对协议安全 目标进行规范 ,然后从初始状态出发 ,采用有效的有哪些信誉好的足球投注网站算法进行分析证明 ,试图发 现针对协议的安全漏洞. 使用该系统分析了 10 多个密码协议的安全性 ,发现了一个未见公开的密码协议攻击实 例. 实验数据显示 ,该系统与现有分析工具相比,具有较高的分析可靠性和效率 ,可作为网络系统安全性评测以及 密码协议设计的有效辅助工具. 关键词 　信息安全 ;密码协议 ;形式化分析 ;有哪些信誉好的足球投注网站算法 ;攻击序列 中图法分类号 TP309 SPA : A Ne w Eff icient System f or Security Protocol Analysis L I J ianXin 　L I XianXian 　ZHU O J iLiang 　HU A I J inPeng ( ) S chool of Comp uter S cience , B ei hang Uni vers ity , B eij i ng 　100083 Abstract 　Cryp to grap hic p rotocol s are co mmunication p rotocol s of di st ribut ed sy st em s t hat u se cryp to grap hy to achieve variou s goal s such a s aut hentication an d key di st ribution in t he op en net wor k environment . Develop in g efficient auto matic sy st em i s a crucial t a sk in t he area of securit y analy si s for cryp to grap hic p rotocol s. However , t he securit y analy si s for cryp to grap hic p rotocol s