安全协议验证的归纳方法与串空间形式化比较  

Compairing the Inductive Method and Strand Spaces for Security Protocol Verification

作　　者：乔海燕[1] 

机构地区：[1]中山大学计算机科学系,广州510275

出　　处：《计算机研究与发展》2008年第z1期137-142,共6页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60673050)

摘　　要：使用归纳方法和串空间分别将NSL(Needham-Schroeder-Lowe)协议及其正确性在辅助证明系统Agda中形式化,并比较了这两种安全协议验证法,证明两种方法形式化的正确性和攻击者能力是相同的.Compared in this paper are the inductive method and strand spaces for security protocol verification. This is done by formalising the NSL (Needham-Schroeder-Lowe) protocol and its correctness in Agda, an interactive proof editor, using both the inductive method and strand spaces in Agda. The two formalisations in Agda are compared and it is shown that they formalise the same notion of the correctness of the protocol and the same penetrator's ability.

关 键 词：安全协议验证 归纳方法 串空间 类型论 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]