摘要
使用归纳方法和串空间分别将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.
出处
《计算机研究与发展》
EI
CSCD
北大核心
2008年第z1期137-142,共6页
Journal of Computer Research and Development
基金
国家自然科学基金项目(60673050)
关键词
安全协议验证
归纳方法
串空间
类型论
cryptographic protocol
inductive method
strand space
type theory
