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

被引：1

作者：

乔海燕

机构：

[1] 中山大学计算机科学系

来源：

计算机研究与发展 | 2008年 / S1期

关键词：

安全协议验证; 归纳方法; 串空间; 类型论;

D O I：

暂无

中图分类号：

TP393.08 [];

学科分类号：

0839 ; 1402 ;

摘要：

使用归纳方法和串空间分别将NSL(Needham-Schroeder-Lowe)协议及其正确性在辅助证明系统Agda中形式化,并比较了这两种安全协议验证法,证明两种方法形式化的正确性和攻击者能力是相同的.

引用

收藏

页码：137 / 142

页数：6

相关论文

共 3 条

[1] 安全协议20年研究进展 [J].

卿斯汉 .

软件学报, 2003, (10) :1740-1752

[2]

Strand spaces: proving security protocols correct[J] . F. Javier Thayer Fábrega,Jonathan C. Herzog,Joshua D. Guttman.Journal of Computer Security . 1999 (2‐3)

[3]

The inductive approach to verifying cryptographic protocols[J] . Lawrence C. Paulson.Journal of Computer Security . 1998 (1,2)