BAN逻辑的可靠性分析与改进 被引量：17

1

作者 王正才 许道云 +2 位作者 王晓峰 唐郑熠 韦立 《计算机工程》 CAS CSCD 2012年第17期110-115,共6页

BAN逻辑的推理过程中可能引入错误的推理条件,导致不安全的协议被验证为安全的。为解决该问题,对消息的形式化描述方式进行改进,在消息含义推理规则中加上一个隐含但不能被忽略的条件,以增强验证的可靠性,通过对发送和推理的消息单元进... BAN逻辑的推理过程中可能引入错误的推理条件,导致不安全的协议被验证为安全的。为解决该问题,对消息的形式化描述方式进行改进,在消息含义推理规则中加上一个隐含但不能被忽略的条件,以增强验证的可靠性,通过对发送和推理的消息单元进行限定,使消息新鲜性判定规则适用于更多类型的协议安全性验证。 展开更多

关键词 ban逻辑 安全协议 形式化 非形式化 消息新鲜性 推理

在线阅读 下载PDF 职称材料

密码协议分析工具——BAN逻辑及其缺陷 被引量：13

2

作者 张玉清 李继红 肖国镇 《西安电子科技大学学报》 EI CAS CSCD 北大核心 1999年第3期376-378,共3页

在介绍密码协议分析工具——ＢＡＮ逻辑的基础上，研究和分析了ＢＡＮ逻辑在初始假设、理想化步骤、语义和探测协议违规运行等方面所存在的缺陷，并用实际例子具体说明了这些缺陷，最后指出了ＢＡＮ逻辑改进的方向．

关键词 密码协议 协议分析 ban逻辑

在线阅读 下载PDF 职称材料

类BAN逻辑基本模型及缺陷 被引量：5

3

作者 许剑卓 戴英侠 左英男 《软件学报》 EI CSCD 北大核心 2000年第12期1660-1665,共6页

类 BA N逻辑是一种用于分析密码协议安全性的逻辑 .在分析了 BA N,A T,M B,G NY,SV O等类 BAN逻辑之后 ,指出这些逻辑的缺陷 ,包括若干新发现的缺陷 .首先把类 BA N的模型抽象出来 ,形成一个五元组模型 ,然后分析该模型的各个要素 ,并... 类 BA N逻辑是一种用于分析密码协议安全性的逻辑 .在分析了 BA N,A T,M B,G NY,SV O等类 BAN逻辑之后 ,指出这些逻辑的缺陷 ,包括若干新发现的缺陷 .首先把类 BA N的模型抽象出来 ,形成一个五元组模型 ,然后分析该模型的各个要素 ,并依据该模型对类 BA N逻辑的缺陷进行分类 ,最后指出进一步发展类 展开更多

关键词 密码协议 ban逻辑 缺陷

在线阅读 下载PDF 职称材料

用BAN逻辑方法分析SSL 3.0协议 被引量：6

4

作者 王惠芳 郭金庚 《计算机工程》 CAS CSCD 北大核心 2001年第11期147-149,共3页

形式化分析密码协议渐渐成为密码学中一个发展的新方向，因为形式化方法的确能检测出密码协议中的漏洞。ＢＡＮ逻辑是目前使用最广泛的。文章介绍了ＢＡＮ逻辑和ＳＳＬ３．０协议，并给出了用ＢＡＮ逻辑分析ＳＳＬ３．０协议的详细过程。

关键词 形式化分析 密码协议 ban逻辑 SSL3.0协议

在线阅读 下载PDF 职称材料

“对BAN逻辑中新鲜子的研究”的注记 被引量：1

5

作者 袁丁 范平志 何明星 《电子与信息学报》 EI CSCD 北大核心 2002年第8期1131-1133,共3页

该文通过一个反例说明,宋荣功等“对BAN逻辑中新鲜子的研究”中关于BAN逻辑新鲜子规则条件过于严格,可能把一个安全的协议分析成不安全的协议。

关键词 密码协议 ban逻辑 新鲜子 形式化分析

在线阅读 下载PDF 职称材料

用BAN逻辑方法分析TLS协议 被引量：2

6

作者 马英杰 肖丽萍 +1 位作者 何文才 李彦兵 《微处理机》 2006年第1期20-23,共4页

密码协议的形式化正在成为国际上研究的热点,通过形式化分析密码协议来判断密码协议是否安全可靠。BAN逻辑是最早提出、最为重要的一种安全协议分析方法,被广泛地用于密码协议的安全性证明。文章介绍了BAN逻辑和TLS协议,用BAN逻辑分析TL... 密码协议的形式化正在成为国际上研究的热点,通过形式化分析密码协议来判断密码协议是否安全可靠。BAN逻辑是最早提出、最为重要的一种安全协议分析方法,被广泛地用于密码协议的安全性证明。文章介绍了BAN逻辑和TLS协议,用BAN逻辑分析TLS协议,从而证明TLS协议的双方认证协议是完整的、没有漏洞的。 展开更多

关键词 ban逻辑 TLS协议 形式化分析密码协议

在线阅读 下载PDF 职称材料

BAN类逻辑的进一步研究 被引量：3

7

作者 陈更力 张青 《微计算机信息》 北大核心 2006年第06X期84-86,共3页

BAN类逻辑是近年来主要的密码协议分析工具之一,在分析了BAN逻辑存在的各类缺陷并用实例详细说明的基础上,研究和归纳了各种扩展的BAN类逻辑的特点和他们共同的缺陷,指出了BAN类逻辑应该改进的方面以及今后进一步的研究方向。

关键词 密码协议 形式化分析 ban类逻辑

在线阅读 下载PDF 职称材料

基于BAN逻辑分析Otway-Rees协议安全性 被引量：1

8

作者 李新中 周小燕 《微计算机信息》 北大核心 2007年第18期71-72,68,共3页

本文通采用BAN逻辑对Otway-Rees协议建立理想化协议模型,利用协议的初始假设和BAN逻辑的公设分析了Ot-way-Rees协议的安全性。

关键词 安全协议 ban逻辑 OtwayRees协议

在线阅读 下载PDF 职称材料

类BAN逻辑的两个重要缺陷 被引量：1

9

作者 张萌 许剑卓 左英男 《计算机工程》 EI CAS CSCD 北大核心 2000年第7期133-135,共3页

类ＢＡＮ逻辑通常都分析了ＢＡＮ逻辑的缺陷并相应地发展了自己的推理法则，在 ＢＡＮ逻辑的缺陷中最受关注的是消息可识别性问题和密钥保密性问题。该文重新对这两个问题进行分析并指出以前类ＢＡＮ逻辑中对这两个缺陷的理解是错误的... 类ＢＡＮ逻辑通常都分析了ＢＡＮ逻辑的缺陷并相应地发展了自己的推理法则，在 ＢＡＮ逻辑的缺陷中最受关注的是消息可识别性问题和密钥保密性问题。该文重新对这两个问题进行分析并指出以前类ＢＡＮ逻辑中对这两个缺陷的理解是错误的，并把这两个缺陷归结为消息不可伪造问题和信任模型问题。同时指出进一步法则类ＢＡＮ逻辑应解决的问题。 展开更多

关键词 密码协议 ban逻辑 缺陷 密码学 网络通信安全

在线阅读 下载PDF 职称材料

Otway Rees协议的安全分析 被引量：1

10

作者 曾子维 李鹏 孙学波 《计算机应用与软件》 CSCD 北大核心 2006年第2期122-124,共3页

互联网的迅速发展引起人们对协议安全性的关注,现在国际上流行安全协议的分析方法集中在形式化验证方面,其中BAN逻辑是一种方法。本文通过使用BAN逻辑证明O tway Rees协议的安全性,同时也得出BAN逻辑在证明协议安全性方面的一些缺陷。

关键词 安全协议 ban逻辑 Otway Rees协议 安全分析 逻辑证明 形式化验证 安全性 互联网

在线阅读 下载PDF 职称材料

密钥分发协议及其形式化分析 被引量：2

11

作者 解建军 李俊红 《河北师范大学学报（自然科学版）》 CAS 2003年第6期570-573,共4页

探讨了形式化分析在设计密码认证协议中的作用;基于Needham Schroeder共享密钥协议和Ot way Rees协议,提出了新的认证协议,并用BAN逻辑对它进行形式分析,发现了潜在的攻击方法,指出形式分析可以辅助发现协议的设计缺陷;并讨论了这种分... 探讨了形式化分析在设计密码认证协议中的作用;基于Needham Schroeder共享密钥协议和Ot way Rees协议,提出了新的认证协议,并用BAN逻辑对它进行形式分析,发现了潜在的攻击方法,指出形式分析可以辅助发现协议的设计缺陷;并讨论了这种分析的局限性以及可能的改进方向. 展开更多

关键词 密钥分发协议 形式化分析 密码认证协议 ban逻辑 Needham-Schroeder共享密钥协议 OTWAY-REES协议 网络安全

在线阅读 下载PDF 职称材料

一种安全协议的逻辑分析与改进 被引量：2

12

作者 石曙东 李芝棠 《华中科技大学学报（自然科学版）》 EI CAS CSCD 北大核心 2004年第7期4-6,共3页

采用BAN逻辑对著名的Needham Schroeder(NS)协议建立理想化协议模型 ,利用协议的初始假设和BAN逻辑的公设分析NS协议的安全性 .分析结果表明 ,该协议只有增加初试假设 ,即用户B获得的会话密钥是新的会话密钥的前提下才能达到认证的目标 。

关键词 安全协议 ban逻辑 Needham-Schroeder协议

在线阅读 下载PDF 职称材料

NS协议的形式化分析与改进 被引量：1

13

作者 李之棠 石曙东 解云峰 《计算机工程与科学》 CSCD 2004年第2期1-3,共3页

随着网络的发展,协议的安全性越来越受到关注,现在国际上的热点集中在对安全协议的形式化验证和分析方面。本文通过使用BAN逻辑证明Needham-Schroeder协议的安全性,得出其存在的缺陷并提出改进方案。

关键词 网络安全 Needham-Schmeder协议 数据加密 数字签名 数据传输

在线阅读 下载PDF 职称材料

一种基于双向Hash认证的RFID安全协议 被引量：13

14

作者 陈瑞鑫 邹传云 黄景武 《微计算机信息》 2010年第11期149-151,共3页

射频识别(RFID)系统是使用无线射频技术在开放系统环境中进行对象识别,但由于RFID系统及其设备的特殊性和局限性带来了很多安全问题,针对这些问题,在分析了几种现有的典型RFID安全协议的特点和缺陷的基础上,提出了一种新的方法——基于... 射频识别(RFID)系统是使用无线射频技术在开放系统环境中进行对象识别,但由于RFID系统及其设备的特殊性和局限性带来了很多安全问题,针对这些问题,在分析了几种现有的典型RFID安全协议的特点和缺陷的基础上,提出了一种新的方法——基于双向Hash认证的RFID安全协议,最后建立该协议的理想化模型,利用BAN逻辑对该协议进行了形式化分析,在理论上证明其安全性。 展开更多

关键词 Hash认证 安全协议 ban逻辑

在线阅读 下载PDF 职称材料

Needham Schroeder协议的安全缺陷与改进

15

作者 石曙东 李之棠 《计算机工程与应用》 CSCD 北大核心 2004年第1期136-137,189,共3页

随着网络的发展协议的安全性越来越受到人们的关注,现在国际上的热点集中在对安全协议的形式化验证方面。通过使用BAN逻辑证明Needham-Schroeder协议的安全性,得出其存在的缺陷的结论并提出改进方案。

关键词 安全协议 ban逻辑 Needham—Schroeder协议

在线阅读 下载PDF 职称材料

密码协议的形式化分析与设计原则 被引量：3

16

作者 徐晓东 岳殿武 《南京邮电学院学报》 2001年第3期28-32,共5页

介绍了密码协议的形式化分析方法和设计原则 ,着重介绍了BAN逻辑及其发展以及一些重要的协议设计原则 ,并提出了作者的一些观点。

关键词 密码协议 形式化分析 保密通信

在线阅读 下载PDF 职称材料

密码协议分析的逻辑方法及其哲学意蕴

17

作者 程华清 《贵州工程应用技术学院学报》 2017年第6期63-68,共6页

逻辑方法是密码协议分析中具有代表性的形式化方法。从已有文献的技术成果出发,以经典的类BAN逻辑作为主要对象,把逻辑方法在密码协议分析上与经验方法和计算方法分别进行比较。通过这种比较,分析了类BAN逻辑方法在分析结论的全面性、... 逻辑方法是密码协议分析中具有代表性的形式化方法。从已有文献的技术成果出发,以经典的类BAN逻辑作为主要对象,把逻辑方法在密码协议分析上与经验方法和计算方法分别进行比较。通过这种比较,分析了类BAN逻辑方法在分析结论的全面性、可操作性方面所具有的优势以及在有效攻击的构造和分析结论可信度上的局限性,以及从参与分析的主体角度分析了类BAN逻辑方法在协议分析上的主体特征。除了这种比较分析,也试图在计算主义框架下提供类BAN逻辑方法应用于密码协议分析的哲学基础,并给出了方法论上的启示。 展开更多

关键词 类ban逻辑 密码协议分析 计算主义

在线阅读 下载PDF 职称材料

BAN类逻辑的由来与发展 被引量：5

18

作者 张玉清 吴建平 李星 《清华大学学报（自然科学版）》 EI CAS CSCD 北大核心 2002年第1期96-99,共4页

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的密码协议。该文介绍了 BAN逻辑的产生、成分和分析步骤 ,进而全面指出了 BAN逻辑的缺陷 ,由此而产生的改进的 BAN逻辑和现状 ,从而对 BAN类逻辑作了... BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的密码协议。该文介绍了 BAN逻辑的产生、成分和分析步骤 ,进而全面指出了 BAN逻辑的缺陷 ,由此而产生的改进的 BAN逻辑和现状 ,从而对 BAN类逻辑作了全面的回顾与展望 ,并得出结论 :BAN类逻辑仍然是密码协议分析和设计的主要工具 ,但理想化步骤是 BAN类逻辑的致命缺陷。指出了 BAN类逻辑研究工作的展望。 展开更多

关键词 密码协议 协议分析 ban类逻辑 形式化分析方法 协议理想化 推理规则

原文传递

密码协议的健全性分析 被引量：1

19

作者 李军 何大可 《通信技术》 2002年第2X期67-69,79,共4页

“健全”的密码协议，可以抵抗多种类型的攻击，建议作为密码协议设计的一个准则，这将有助于协议的早期分析，部分地弥补ＢＡＮ逻辑的不足。

关键词 密码协议 安全性分析 ban逻辑 健全性

原文传递