Analysis of Authentication Protocols Based on Strand Space and State Transition
基于串空间和状态转换的认证协议分析方法

Strand space is a new formal model for the analysis of security protocols.Precise though they are,theory testifies in the strand space model are difficult.Firstly,based on the strand space model,the state of system is de- fined.Secondly,analysis process of transitions between system states is explained by the example of Needham-Schroe- der-Lowe public key authentication protocol.Investigating nonces in transitions between system states,we draw some significant conclusions.Finally,the security of Needbam-Schroeder-Lowe protocol is validated.This new method for analyzing authentication protocols is simple and efficient,and it is prone to be automated.