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

摘要：

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

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

作者: 乔海燕

作者单位: 中山大学计算机科学系,广州,510275

会议类型: 国内会议

会议名称: 2007全国理论计算机科学学术年会

会议地点: 南宁

会议语种:中文

页码: 137-142

在线出版日期: 2007-11-01（万方平台首次上网日期，不代表论文的发表时间）