形式化分析之BAN逻辑

手机

iphone11大小尺寸是多少？苹果iPhone11和iPhone13的区别是什么？

警方通报辅警执法直播中被撞飞：犯罪嫌疑人已投案

形式化分析之BAN逻辑

2023-06-16 11:12:17 来源：博客园

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.

未完待续……

关键词：