A New Approach for Formal Analyzing Encryption Protocols
一种新的密码协议分析方法及其应用

Aiming at the shortcoming that traditional temporal logic regards protocols as close system to analyse, this paper proposes a ATL(Alternating-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.