安全协议的形式化验证与分析已成为国际研究的热点。本文应用BAN 逻辑研究Needham-Schroeder 对称密钥认证协议，指出该协议存在的安全缺陷，利用消息新鲜性对其进行相应改进，并在BAN 逻辑下形式化证明改进的协议可以满足安全目标。关键词 安全性分析；形式化；BAN 逻辑；认证协议通信协议的安全是网络信息安全的基础，但仅根据以往的经验设计或分析验证一个安全协议是十分困难的，因此我们必须借助形式化方法。近20 年来涌现了很多形式化研究方法，其中基于知识和信仰的模态逻辑方法由于其简单、实用、抽象度高等特点在安全协议验证方面获得了广泛的应用。逻辑方法中BAN 逻辑是一项开创性的工作，GNY 逻辑、AT 逻辑、VO 逻辑和SVO 逻辑等都是对BAN 逻辑的扩展[1]。Needham-Schroeder 协议由Needham 和Schroeder 在1978 年提出，是最为著名的早期的认证协议[2]，该协议可分为对称密码体制和非对称密码体制下两个版本。在此只关注对称密钥体制下的Needham-Schroeder 协议（以下简称为NS 协议），它是一种具有可信第三方的对称密钥分发协议。Denning 和Sacco 在1981年指出该协议存在安全缺陷可以对其进行重放攻击[3]，但提出的改进方案仍存在问题。我们应用BAN 逻辑研究NS 协议的安全缺陷发现，该缺陷由缺乏消息新鲜性引起，容易被协议设计者忽视，其他协议如Yahalom 协议也存在类似安全缺陷。本文分析了如何改进，给出改进后的协议，并用BAN 逻辑证明了改进的协议可以满足安全目标。
京公网安备 11010802033920号
Copyright © 2005-2024 EEWORLD.com.cn, Inc. All rights reserved
评论