形式化分析之BAN逻辑

BAN逻辑介绍

BAN逻辑是一种基于知识和信任的形式逻辑分析方法,由Burrows,Abadi 和 Needham 提出,通过对认证协议的运行进行形式分析,从协议执行者最初的一些基本信仰出发,根据协议执行的每个参与者发出和收到的消息,推理得到参与者的最终信仰。
BAN逻辑成功分析出NeedHam-Schroeder,Kerberos等协议的漏洞。
应用BAN逻辑对认证协议进行分析,首先需要进行理想化处理,将协议的消息转换成BAN逻辑中的公式,再根据具体情况进行合理假设,由逻辑的推理法则根据理想化协议和假设进行推理,推断协议能否完成预期的目标。如果在协议流程结束时能够建立关于共享通信密钥、对方身份等的信任,则表明协议是安全的。

BAN逻辑表达式和推理规则

  1. BAN逻辑处理的对象:主体、密钥和公式。
  2. BAN逻辑主要推理规则:消息含义规则、随机数验证规则、裁判规则和新鲜性规则等。
  3. BAN逻辑协议分析步骤:理想化步骤→确认初始假设→逻辑推理→得出结论。

表达式

推理规则

  1. 消息含义规则

1.1 对于共享密钥:

表示P相信K是P和Q之间的通信密钥,当P看到用K加密的信息X,则P相信Q曾经说过X。
1.2 对于公钥:

表示P相信K是Q的公钥,P看到用Q的私钥加密的消息,则P相信Q曾经说过X。
1.3 对于共享秘密:

  1. 随机数验证规则

表示P相信X是新鲜的,且P相信Q曾经说过X,则P相信Q相信X是真实的。

  1. 裁判规则

表示P相信Q对X由控制权,且P相信Q相信X,则P相信X。

  1. 新鲜性规则

如果P相信X是新鲜的,则P相信X和Y级联的整体信息也是新鲜的。

  1. 解密规则

如果P看到用自己有效公钥加密的信息,则P可以解密看到信息。

  1. 信仰规则

  2. 发送规则

如果P相信Q曾经发送过整个消息,那么P相信Q曾经发送过消息的子部分。

  1. 接收规则

参考文献

[1]于代荣,杨扬,马炳先,刘明军,王世贤.基于身份的TLS协议及其BAN逻辑分析[J].计算机工程,2011,37(01):142-144+148.
[2]张玉清,李继红,肖国镇.密码协议分析工具——BAN逻辑及其缺陷[J].西安电子科技大学学报,1999(03):116-118.
[3]王惠芳,郭金庚.用BAN逻辑方法分析SSL 3.0协议[J].计算机工程,2001(11):147-149.

未完待续……

热门相关:总裁别再玩了   豪门重生盛世闲女   梦回大明春   重生当学神,又又又考第一了!   朕是红颜祸水