基于串空间模型安全协议形式化分析方法的研究  

Research on Formalisms Analysis Method Based on Strand Space Model Security Protocol

作　　者：董军[1] 杨秀娟[1] 赵艳芹[1] 

机构地区：[1]黑龙江科技学院计算机与信息工程学院,黑龙江哈尔滨150027

出　　处：《计算机技术与发展》2008年第4期151-154,157,共5页Computer Technology and Development

基　　金：黑龙江省自然科学基金(CF2005-05)

摘　　要：从串空间模型理论入手,提出了三种典型的串空间形式化方法(基于极小元理论的串空间方法、基于理想与诚实理论的串空间方法、基于认证测试理论的串空间方法),并对每一种方法的证明步骤及优缺点进行了分析。在此基础上,应用提出的串空间方法对Yahalom协议的秘密性和认证性进行了分析。分析结果表明利用不同方法的优点,能更好地保证安全协议形式化分析的准确性。Starting with the theory of strand space model,presents three typical formalisms based on strand space model ,including the strand space method based on the minimal theory, the strand space method based on the honest ideal theory and the strand space method based on the authentication test theory. Moreover,also analyses the process of verification,advantages and flaws of these methods. Finally, using the proposed methods, Yahalom protocol is analysed from the aspects of both secnecy and authentication. Experimental results show that utilizing the advantage of various formalisms can greatly ensure the accuracy of formal analysis.

关 键 词：串空间 安全协议 认证测试 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]