BAN逻辑是一种基于知识和信任的形式逻辑分析方法,由Burrows,Abadi 和 Needham 提出,通过对认证协议的运行进行形式分析,从协议执行者最初的一些基本信仰出发,根据协议执行的每个参与者发出和收到的消息,推理得到参与者的最终信仰。BAN逻辑成功分析出NeedHam-Schroeder,Kerberos等协议的漏洞。应用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.
未完待续……
Copyright @ 2015-2022 现在家电网版权所有 备案号: 粤ICP备18023326号-5 联系邮箱:855 729 8@qq.com