基于知识结构的认证协议验证

• 作者: 吕关锋 苏开乐 陈清亮
• 来源期刊: 中国科学E辑
• 学科: 工学
• 关键词: 形式化验证 安全协议 认知逻辑 知识结构
• 年，卷（期）: 2005,（4）
• 页码范围: 337-351
• 页数: 15页
• 分类号: TP3
• 字数: 9677字
• 语种: 中文
• DOI: 10.3321/j.issn:1006-9275.2005.04.001

摘要

认知逻辑的Kripke语义,已被成功地运用到分析无黑客存在的安全网络下的通信协议.提出认知逻辑的Kripke语义的一种简单而自然的形式,称之为知识结构,并把这种语义用到分析黑客存在的非安全网络环境中的通信协议,特别是认证协议.与类BAN的那一类逻辑相比,文中的方法可以直接转化成算法实现,对协议本身进行操作,而不需对协议进行一些难以把握的抽象判断.而且,在这套理论的基础上开发了安全协议分析器SPV.文中的方法是基于证明的而不是证伪的,即证明协议的正确性而不是找协议漏洞.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏开乐	中山大学计算机科学系	22	309	11.0	17.0
2	陈清亮	中山大学计算机科学系	4	53	3.0	4.0
3	吕关锋	中山大学计算机科学系	2	25	2.0	2.0