关于BAN逻辑的语义模型的分析与改进1.PDF

关于 BAN 逻辑的语义模型的分析与改进1 费定舟 邓达强 （中山大学逻辑与认知研究所，广州510275） 摘要：本文针对 BAN 逻辑及其语义模型的不足之处，提供了我们的改进后的定义，它比 BAN 原作者们所提供 的信念定义显得更合理些。 关键词：Authentication logic； BAN 逻辑；语义模型 中图分类号：B81 文献标识码：A 1、引言 Internet 以及 e－Commerce 的发展要求不断提高通信过程和信息的安全性。密码学的重 要任务之一是研究设计并开发高安全性的认证方法和系统。其中，安全协议是一个关键领 域．从逻辑形式结构方面研究安全协议，开拓性工作是 BAN 逻辑系统［Burrows, M., Abadi, M., Needham, R., 1990］，以较为严密和应用的普遍性见长，因为并不需要过多的细节。它 可以对两个重要的工业安全协议应用 GSM(Global System for Mobil Communication) [Gunnar , H., 1999]和 SET (Secure Electronic Transactions)提供直觉和足够的解释力［Agray, N., vonder Hoek, E., de vink, 2002］。目前，BAN 逻辑成为研究密码和安全协议的广泛采用的 形式化工具。就 BAN 逻辑本身而言，近十年来重点放在它的模态变种及其理论模型方面。其 语义模型正处于不断的改进和修改之中，这方面的工作见［Abadi, M., Tuttle, M., 1991; Gong, L., Needham, R., Yahalom, R., 1991; Wedel, G., Kessler, V., 1996］。 本文讨论 BAN 逻辑的语义模型。与以 GNY[Gong, L., Neddham, R., Yahalom, R., 1990] 为代表的工作不同，他们讨论 Beliefs 与 Know 之间的逻辑联系，我们考察 Belief 的模型定义 并分析其不足之处，相应地给出我们关于 Belief 的新定义，它能提供直觉上和推理上的更合理 的说明。 2 、BAN 逻辑 2.1 Authentication 是确定参加通信的实体的身份的计算行为，在安全协议中起非常 重要的作用。一个认证协议（Authentication protocol ）告诉我们 secret 如何分配给这些实体， 以及如何确定其身份的。认证逻辑则抽掉认证过程的诸多细节如算法和数学的细节，保留反 映安全问题的逻辑上的特征和结构 ［白硕等，2000 ］，考察中参与认证协议中各实体信念问题， 建立起相应的形式化系统。BAN 逻辑则是这些形式化系统中研究较多的一种。下面介绍改进 后的 BAN 逻辑形式系统。 2.2 先从直观上引进几个认证协议中常用的几个概念。 实体：P，Q，R，S 加密密钥：K 公式：X，Y 消息： m，M，X，Y 1 P believes X：P 相信 X 是真的，而 X 本身既真既假，但 P 把 X 当做真的。 P see X：P 已经接收到消息X 。假如 P 有相应的解密密钥，那么他能够读出它的内容， 同时 P 亦把 X 发送给其它实体。 P said X：P 已经发送消息X，P 相信他发送的 X 是真的。 P controls X：P 对 X 有判定权，即 P 是对 X 的真的可信任的当局。 fresh(X)：X 是新鲜的。时间分为两个时段：过去与现在。而现在则以当前协议执 行的起点为起点。当 X 不包含在过去发送的消息中，X 是新鲜的。 K P ↔ Q：K 是 P 和 Q 的公钥。K 是 P、Q 之间通信的安全密钥，除 P、Q 之外，其它 实体包括 P、Q 信任的实体都不能破译。 P # x Q：X 是 P