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

• 作者: 刘锋 周倜 李梦君 李舟军
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: FIoyd-Hoare逻辑 PCL 安全协议
• 年，卷（期）: 2008,（11）
• 所属期刊栏目: 计算机网络与安全
• 页码范围: 13-15
• 页数: 3页
• 分类号: TP309
• 字数: 3016字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2008.11.004

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘锋	国防科技大学计算机学院	16	38	3.0	5.0
2	周倜	国防科技大学计算机学院	8	33	3.0	5.0
3	李梦君	国防科技大学计算机学院	21	193	8.0	13.0
4	李舟军	国防科技大学计算机学院	31	594	10.0	24.0