电子发烧友网>电子资料下载>电子论文>网络协议论文>Needham-Schroeder对称密钥认证协议安全性分析

Needham-Schroeder对称密钥认证协议安全性分析

2512841 2009-08-25 | rar | 116 | 次下载 | 免费

资料介绍

安全协议的形式化验证与分析已成为国际研究的热点。本文应用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 逻辑证明了改进的协议可以满足安全目标。