BAN逻辑在一类中间入侵攻击协议分析中的缺陷

BAN逻辑通过对密钥协商协议的运行进行形式化分析,研究密钥协商双方通过相互接收和发送消息从最初的信仰逐渐发展到协议最终要达到的目的,证明协议是否能够达到预期目标,以此发现协议中存在的一些缺陷。通过一个端到端协议例子的证明和分析,指出BAN逻辑对于一类密钥协商协议中存在的中间入侵攻击分析方面存在缺陷,还需要结合非形式化的分析方法来加以解决。