摘要
针对传统时序逻辑把协议看成封闭系统进行分析的缺点,提出一种新的基于策略的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.
出处
《计算机应用》
CSCD
北大核心
2006年第5期1087-1089,共3页
journal of Computer Applications
基金
贵州省自然科学基金资助项目(20042111)
贵州省教育厅自然科学基金资助项目(2004219)
关键词
密码协议
安全性
形式化分析
ATL
cryptographic protocols
security
formal analysis
ATL
