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

摘要：

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

关键词：形式化验证、安全协议、认知逻辑、知识结构

所属期刊栏目：35

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金60496327,10410638,60473004;广东省自然科学基金04205407;教育部留学回国人员科研启动基金;上海市重点实验室基金

在线出版日期：2005-07-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共15页

页码：337-351