使用组合协议逻辑PCL验证 |
| |
作者姓名: | 刘锋 李舟军 周倜 李梦君 |
| |
作者单位: | 国防科技大学计算机学院,湖南长沙410073 |
| |
摘 要: | 安全协议的形式化分析和验证一直是信息安全领域的一个重要问题。本文介绍了组合式验证方法以及面向安全协议验证的组合式验证工具PCL,并采用PCL对Amended Needham-Schroeder协议进行了验证,证明该协议满足保密性。在验证中将完整的协议划分为三个子协议,对子协议分别做性质描述和验证,最后将三个子协议组合成完整的协议,通过三个子协议之间前置断言和后置断言的一致性,证明了组合之后的协议满足保密性。
|
关 键 词: | Floyd-Hoare逻辑 PCL 安全协议 |
本文献已被 维普 等数据库收录! |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
|