形式化分析之BAN逻辑
BAN逻辑介绍
BAN逻辑是一种基于知识和信任的形式逻辑分析方法，由Burrows，Abadi 和 Needham 提出，通过对认证协议的运行进行形式分析，从协议执行者最初的一些基本信仰出发，根据协议执行的每个参与者发出和收到的消息，推理得到参与者的最终信仰。
BAN逻辑成功分析出NeedHam-Schroeder，Kerberos等协议的漏洞。
应用BAN逻辑对认证协议进行分析，首先需要进行理想化处理，将协议的消息转换成BAN逻辑中的公式，再根据具体情况进行合理假设，由逻辑的推理法则根据理想化协议和假设进行推理，推断协议能否完成预期的目标。如果在协议流程结束时能够建立关于共享通信密钥、对方身份等的信任，则表明协议是安全的。
BAN逻辑表达式和推理规则
- BAN逻辑处理的对象：主体、密钥和公式。
- BAN逻辑主要推理规则：消息含义规则、随机数验证规则、裁判规则和新鲜性规则等。
- BAN逻辑协议分析步骤：理想化步骤→确认初始假设→逻辑推理→得出结论。
表达式
推理规则
- 消息含义规则
1.1 对于共享密钥：
表示P相信K是P和Q之间的通信密钥，当P看到用K加密的信息X，则P相信Q曾经说过X。
1.2 对于公钥：
表示P相信K是Q的公钥，P看到用Q的私钥加密的消息，则P相信Q曾经说过X。
1.3 对于共享秘密：
- 随机数验证规则：
表示P相信X是新鲜的，且P相信Q曾经说过X，则P相信Q相信X是真实的。
- 裁判规则：
表示P相信Q对X由控制权，且P相信Q相信X，则P相信X。
- 新鲜性规则：
如果P相信X是新鲜的，则P相信X和Y级联的整体信息也是新鲜的。
- 解密规则：
如果P看到用自己有效公钥加密的信息，则P可以解密看到信息。
-
信仰规则：
-
发送规则：
如果P相信Q曾经发送过整个消息，那么P相信Q曾经发送过消息的子部分。
- 接收规则：
参考文献
[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.
未完待续……