【安全性分析】BAN逻辑 (BAN Logic)之详细介绍

安全性分析-系列文章目录

第一章 【安全性分析】正式安全分析与非正式安全分析
第二章 【安全性分析】BAN逻辑 (BAN Logic)之详细介绍

---

---

一、BAN Logic是什么？

BAN逻辑（Burrows-Abadi-Needham逻辑）是一种针对身份验证和认证协议的形式化分析工具。该分析方法由Burrows，Abadi 和 Needham 提出，是一种基于知识和信任的形式逻辑分析方法，它主要用于分析参与者之间的信任、消息的真实性和知识的有效性。

二、使用步骤

2.1 定义及分析流程

BAN 逻辑遵循理想化、假设、安全目标和推导四个过程。首先，需要对协议进行理想化处理，将协议的消息转换成BAN逻辑中的公式，再根据具体情况进行合理假设，由逻辑的推理法则根据理想化协议和假设进行推理，推断协议能否完成预期的目标。如果在协议流程结束时能够建立关于共享通信密钥、对方身份等的信任，则表明协议是安全的。分析流程具体如图所示：

2.2 推理过程

2.3 表达式含义