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

Modal Logic for Analyzing Privacy and Authentication

作　　者：赵华伟[1] 秦静[2] 

机构地区：[1]山东财政学院计算机信息工程学院,济南250014 [2]山东大学数学与系统科学学院,济南250100

出　　处：《计算机工程》2007年第20期30-33,共4页Computer Engineering

基　　金：国家"863"计划基金资助项目(2003AA141120;2004AA001260);山东省自然科学基金资助项目(Y2003A03)

摘　　要：提出了一种新的基于信念的模态逻辑——MBL逻辑,来分析由单向函数构造的对称钥认证交换协议的安全性。该逻辑有严格的证明体系,可证明推理规则在其语义模型下的正确性,说明该逻辑具有合理性。其推理规则不仅能对单向函数保护的消息进行有关认证性的推理,克服了以往逻辑系统使用不当的安全服务来分析协议认证性的缺陷,而且可分析消息的保密性,避免了其他逻辑分析协议时对可信中心的过分依赖,可发现敌手通过欺骗可信中心而造成的攻击。A modal logic based on belief, MBL logic, is introduced to analyze security of authentication key-exchange protocols with one-way functions. The logic has following characteristics： it has a rational proof system and its inference rules can be proved right under its own semantic model. It can analyze authentication of messages protected by one-way functions, and analyze whether messages are kept secret. Through these rules, analyzer could reduce the dependency on trusted third part about the security of temporary session key, and be able to find whether adversaries could make effective attacks on protocols through cheating trusted third part.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]