一种新的密码协议分析方法及其应用  

New approach for formal analyzing encryption protocols

作　　者：文静华[1] 张梅[1] 李祥[2] 

机构地区：[1]贵州财经学院信息学院,贵州贵阳550004 [2]贵州大学计算机软件与理论研究所,贵州贵阳550025

出　　处：《计算机应用》2006年第5期1087-1089,共3页journal of Computer Applications

基　　金：贵州省自然科学基金资助项目(20042111);贵州省教育厅自然科学基金资助项目(2004219)

摘　　要：针对传统时序逻辑把协议看成封闭系统进行分析的缺点,提出一种新的基于策略的ATL(AlternatingtimeTemporalLogic)逻辑方法分析密码协议。最后用新方法对NeedhamSchroeder协议进行了严格的形式化分析,结果验证了该协议存在重放攻击。工作表明基于博弈的ATL逻辑比传统的CTL更适合于描述和分析密码协议。Aiming at the shortcoming that traditional temporal logic regards protocols as close system to analyse, this paper proposes a ATL（ Ahemating-time Temporal Logic） logical method based on game to analyse cryptographic protocols. In the end, we make strict formal analysis for needham-schroeder protocol with this new method, as a result we validate there exists reply attacks. These works indicate that the ATL logic based on game is more suitable to describe and analyze cryptographic protocols than traditional CTL.

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

分 类 号：TP309.7[自动化与计算机技术—计算机系统结构]