一种可分析保密性与认证性的模态逻辑

摘要：

提出了一种新的基于信念的模态逻辑--MBL逻辑,来分析由单向函数构造的对称钥认证交换协议的安全性.该逻辑有严格的证明体系,可证明推理规则在其语义模型下的正确性,说明该逻辑具有合理性.其推理规则不仅能对单向函数保护的消息进行有关认证性的推理,克服了以往逻辑系统使用不当的安全服务来分析协议认证性的缺陷,而且可分析消息的保密性,避免了其他逻辑分析协议时对可信中心的过分依赖,可发现敌手通过欺骗可信中心而造成的攻击.

关键词：模态逻辑、MBL逻辑、BAN类逻辑、会话密钥

所属期刊栏目：33

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

资助基金：国家高技术研究发展计划863计划2003AA141120;2004AA001260;山东省自然科学基金Y2003A03

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

页数：共4页

页码：30-33