摘要
Strand空间模型是一种安全协议分析模型,使用图的形式来描述协议,证明协议的正确性。通过分析研究,本文建立了攻击者模型,并在此基础上运用安全协议的形式化分析方法—Strand空间模型,对公开密钥协议NSPK进行了分析,说明了该方法进行协议分析的过程,证明了该协议在保密性和认证性方面的正确性,并分析了该协议存在的安全缺陷。
Strand Space is a model of analysising security protocol which specificate the protocol using the form of Graph and demonstrate the correctness of the protocol.Throughing a lot of research,the paper builds the model of attacter.Based on the model of attacter,we analysis Needham-Schroder public key protocol using the Strand Space model which is a formal method for analysis of security protocols and indicate the process of analysis of protocols and demonstrate the correctness of Needham-Schroeder on secrecy and authentication using the mothod.Finally,we indicate the reason of the Needham-Schroeder drawbacks.
出处
《微计算机信息》
北大核心
2008年第27期37-39,共3页
Control & Automation
基金
河南省教育厅基金
基于时间自动机的模型验证理论及应用研究(2006520015)
河南省自然科学基金
模型验证技术研究(0411012169)
关键词
串空间
丛
攻击者模型
形式化分析
安全协议
Strand Space
Bundle
attacker model
formal analysis
security protocol
