New approach for formal analyzing encryption protocols
Jinghua Wen · Journal of Computer Applications · 2006
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.