使用组合协议逻辑PCL验证Amended Needham-Schroeder协议

摘要：

安全协议的形式化分析和验证一直是信息安全领域的一个重要问题。本文介绍了组合式验证方法以及面向安全协议验证的组合式验证工具PCL,并采用PCL对Amended Needham-Sehroeder协议进行了验证,证明该协议满足保密性。在验证中将完整的协议划分为三个子协议,对子协议分别做性质描述和验证,最后将三个子协议组合成完整的协议,通过三个子协议之间前置断言和后置断言的一致性,证明了组合之后的协议满足保密性。

关键词： 安全协议 信息安全 组合式验证 性质描述 后置断言 前置断言

作者: 刘锋 李舟军 周倜 李梦君

作者单位: 国防科技大学计算机学院,湖南,长沙,410073

会议类型: 国内会议

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

会议地点: 西安

会议语种:中文

页码: 13-15

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