基于串空间和状态转换的认证协议分析方法

串空间是一种新兴的安全协议形式化分析模型。串空间模型中的理论证明方法虽然严谨，但难度很大。本文基于串空间模型，首先定义系统状态，并以Needham-Schroeder-Lowe公钥认证协议为例说明系统状态转换的分析过程。通过对状态转换过程中现实的跟踪考察，得出了有意义的结论。结合串空间模型，验证了该认证协议的安全性。这种分析认证协议的新方法简洁和高效，并易于实现自动化。

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.