|
|||||
|
|
| 基于知识结构的认证协议验证 | |
| 作者姓名： | 苏开乐 吕关锋 陈清亮 |
| 作者单位： | 中山大学计算机科学系,广州,510275 |
| 基金项目： | 国家自然科学基金，广东省自然科学基金，教育部留学回国人员科研启动基金，上海市重点实验室基金 |
| 摘 要： | 认知逻辑的Kripke语义,已被成功地运用到分析无黑客存在的安全网络下的通信协议.提出认知逻辑的Kripke语义的一种简单而自然的形式,称之为知识结构,并把这种语义用到分析黑客存在的非安全网络环境中的通信协议,特别是认证协议.与类BAN的那一类逻辑相比,文中的方法可以直接转化成算法实现,对协议本身进行操作,而不需对协议进行一些难以把握的抽象判断.而且,在这套理论的基础上开发了安全协议分析器SPV.文中的方法是基于证明的而不是证伪的,即证明协议的正确性而不是找协议漏洞. |
| 关 键 词： | 形式化验证 安全协议 认知逻辑 知识结构 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |