论文部分内容阅读
针对传统时序逻辑把协议看成封闭系统进行分析的缺点，提出一种新的基于策略的ATL（Ahemating-time Temporal Logic）逻辑方法分析密码协议。最后用新方法对Needham-Schroeder协议进行了严格的形式化分析，结果验证了该协议存在重放攻击。工作表明基于博弈的ATL逻辑比传统的CTL更适合于描述和分析密码协议。