资料下载
×
Needham-Schroeder对称密钥认证协议安全性分析
消耗积分:5 |
格式:rar |
大小:116 |
2009-08-25
王静
分享资料个
安全协议的形式化验证与分析已成为国际研究的热点。本文应用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 逻辑证明了改进的协议可以满足安全目标。
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 逻辑证明了改进的协议可以满足安全目标。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
