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

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

Abstract: 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.

Key words: modal logic, MBL logic, BAN-like logic, session key

中图分类号: 

• TP309