摘要
串空间是一种新兴的安全协议形式化分析模型。串空间模型中的理论证明方法虽然严谨,但难度很大。本文基于串空间模型,首先定义系统状态,并以Needham-Schroeder-Lowe公钥认证协议为例说明系统状态转换的分析过程。通过对状态转换过程中现实的跟踪考察,得出了有意义的结论。结合串空间模型,验证了该认证协议的安全性。这种分析认证协议的新方法简洁和高效,并易于实现自动化。
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 defined. Secondly, analysis process of transitions between system states is explained by the example of Needham-Schroeder-Lowe public key authentication protocol. Investigating nonces in transitions between system states, we draw some significant conclusions. Finally, the security of Needham- Schroeder-Lowe protocol is validated. This new method for analyzing authentication protocols is simple and efficient, and it is prone to be automated.
出处
《计算机科学》
CSCD
北大核心
2007年第10期96-98,共3页
Computer Science
基金
本课题得到解放军信息工程大学重点研究方向基金资助。
关键词
串空间
认证协议
状态转换
现实
Strand space, Authentication protocol, State transition, Nonce
