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

1

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

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

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

在线阅读 下载PDF 职称材料

一种新的类BAN逻辑模态语义模型——兼论类BAN逻辑的语法缺陷

2

作者 谢鸿波 周明天 《计算机科学》 CSCD 北大核心 2006年第1期198-201,共4页

由于类 BAN 逻辑缺乏明确而清晰的语义,其语法规则和推理的正确性就受到了质疑。本文定义了安全协议的计算模型,在此基础上定义了符合模态逻辑的类 BAN 逻辑“可能世界”语义模型,并从语义的角度证明了在该模型下的类 BAN 逻辑语法存在... 由于类 BAN 逻辑缺乏明确而清晰的语义,其语法规则和推理的正确性就受到了质疑。本文定义了安全协议的计算模型,在此基础上定义了符合模态逻辑的类 BAN 逻辑“可能世界”语义模型,并从语义的角度证明了在该模型下的类 BAN 逻辑语法存在的缺陷,同时,指出了建立或改进类 BAN 逻辑的方向。 展开更多

关键词 类ban逻辑 模态逻辑 形式语义 ban逻辑 语义模型 语法规则 缺陷 计算模型 安全协议 定义

在线阅读 下载PDF 职称材料

关于BAN逻辑扩展的注记

3

作者 郑东 田建波 王育民 《电子科学学刊》 CSCD 2000年第1期73-77,共5页

本文指出了W.Mao(1995)对其协议(1)的证明中存在的错误,并对其在协议理想化过程中提出的N-u规则作了探讨,指出其扩展N-u的三条规则的缺陷,并作了改进,最后,给出一个例子说明N-u规则的应用。

关键词 认证协议 ban逻辑 密码学

在线阅读 下载PDF 职称材料

BAN类逻辑的两个缺陷分析

4

作者 王倩 王龙葛 《电脑知识与技术（过刊）》 2011年第3X期1761-1763,共3页

BAN类逻辑是安全协议形式化分析的一种重要方法。BAN类逻辑都是以BAN逻辑为基础发展起来的。通过对BAN逻辑的研究得出了BAN类的两个重要缺陷,缺少环境模型和缺少完整性分析,并指出了下一步研究的方向。

关键词 安全协议 形式化分析 ban类逻辑 环境模型 完整性

在线阅读 下载PDF 职称材料

基于BAN类逻辑的协议自动化分析工具设计

5

作者 邓媛劼 王倩 《科技信息》 2010年第09X期10-11,7,共3页

BAN类逻辑广泛应用于安全协议分析,具有简洁性和易用性。使用Prolog人工智能语言设计开发了基于BAN类逻辑协议的自动化分析工具,实验表明工具能够严谨、高效地分析安全协议的正确性及认证性等安全属性。

关键词 ban类逻辑 自动化分析工具 PROLOG语言

在线阅读 下载PDF 职称材料

基于数理逻辑的安全协议本征逻辑分析方法

6

作者 李益发 孔雪曼 +1 位作者 耿宇 沈昌祥 《密码学报（中英文）》 CSCD 北大核心 2024年第3期588-601,共14页

本文提出了一种基于数理逻辑的安全协议本征逻辑分析方法—SPALL方法.该方法在一阶谓词逻辑的基础上,增加了基于密码学的若干新语义,包括新的密码函数项、与密码学和安全协议分析相关的一阶谓词和二阶谓词等,并给出了十三类二十九条公理... 本文提出了一种基于数理逻辑的安全协议本征逻辑分析方法—SPALL方法.该方法在一阶谓词逻辑的基础上,增加了基于密码学的若干新语义,包括新的密码函数项、与密码学和安全协议分析相关的一阶谓词和二阶谓词等,并给出了十三类二十九条公理,仍使用谓词逻辑的分离规则和概括规则,形成新的安全协议分析系统,称为本征(latent)逻辑系统(也称本征逻辑或L逻辑).该系统是一阶谓词系统的扩充,以密码学和安全协议为“特定解释”,并定义了“概率真”的概念,力求每条公理在“特定解释”下是概率真的,而分离和概括规则又能保证从概率真演绎出概率真,从而使每条定理都概率真,以保证公理系统的可靠性.清晰的语义可以精确描述安全协议的前提与目标,基于公理和定理的协议分析,可简洁有效地推导出协议自身具有的安全特性.本文给出了详细的语义和公理,以及若干实用定理,然后对著名的密钥建立协议进行了详细分析,并对比了可证安全方法的分析结果,展示了本文方法的优势.此外还分析了电子选举协议和非否认协议,展示了本文方法有着广泛的适用范围. 展开更多

关键词 安全协议 协议分析 ban类逻辑 SPALL方法(SPALL逻辑) 本征逻辑

在线阅读 下载PDF 职称材料

WAPI认证机制的性能和安全性分析 被引量：29

7

作者 张帆 马建峰 《西安电子科技大学学报》 EI CAS CSCD 北大核心 2005年第2期210-215,共6页

利用BAN类逻辑(WK逻辑),对中国无线局域网安全标准WAPI的认证基础设施WAI进行了形式化分析,指出其无法实现全部的认证及密钥协商目标.进一步分析表明,WAI中存在诸多安全问题,如无法提供身份保护、无法抵抗密钥一致性等攻击、缺乏私钥验... 利用BAN类逻辑(WK逻辑),对中国无线局域网安全标准WAPI的认证基础设施WAI进行了形式化分析,指出其无法实现全部的认证及密钥协商目标.进一步分析表明,WAI中存在诸多安全问题,如无法提供身份保护、无法抵抗密钥一致性等攻击、缺乏私钥验证、不能提供如PFS、密钥控制等相应的安全属性等.因此,WAPI无法提供足够级别的安全保护.最后对WAPI与IEEE802 11i在安全性和性能上进行了比较. 展开更多

关键词 ban类逻辑WK 无线局域网 WAPI IEEE 802.11i 认证 密钥协商

在线阅读 下载PDF 职称材料

公钥密码体制下认证协议的形式化分析方法研究 被引量：4

8

作者 钱勇 谷大武 +1 位作者 陈克非 白英彩 《小型微型计算机系统》 CSCD 北大核心 2002年第2期145-147,共3页

本文通过对形式化方法中最广泛使用的类 BAN逻辑进行研究发现 ,此方法更侧重于对称密码体制下认证协议的分析 ,而在分析基于公钥体制的认证协议时 ,该方法有很大的局限性 .因此 ,文中针对公钥密码的特点对类 BAN逻辑进行了扩展 .

关键词 公钥密码体制 认证协议 形式化方法 类ban逻辑 身份认证 网络安全 计算机网络

在线阅读 下载PDF 职称材料

面向远程证明的安全协议设计方法 被引量：3

9

作者 余荣威 王丽娜 匡波 《通信学报》 EI CSCD 北大核心 2008年第10期19-24,共6页

通过引入优胜劣汰的自然规律,提出了改进的基于演化计算的密码协议自动化设计方法。该方法采用模态逻辑作为描述协议的基本工具,重点改进了衡量安全协议个体性能的评估函数,以求获得全局最优解。实验结果显示,该方法能保证所设计协议的... 通过引入优胜劣汰的自然规律,提出了改进的基于演化计算的密码协议自动化设计方法。该方法采用模态逻辑作为描述协议的基本工具,重点改进了衡量安全协议个体性能的评估函数,以求获得全局最优解。实验结果显示,该方法能保证所设计协议的正确性和安全性,具有较强的可行性和适用性。 展开更多

关键词 远程证明 认证协议 演化计算 ban逻辑

在线阅读 下载PDF 职称材料

基于消息唯一起源的动态逻辑方法

10

作者 谢鸿波 吴远成 周明天 《电子学报》 EI CAS CSCD 北大核心 2007年第8期1516-1520,共5页

本文提出了一种新的逻辑方法分析安全协议的安全性.该方法给出了一种安全协议的动态分析模型,从而克服了类BAN逻辑"理想化协议"步骤的缺陷,提出了消息唯一起源的概念和判定规则,严格区分"可靠信任"和"不可靠信... 本文提出了一种新的逻辑方法分析安全协议的安全性.该方法给出了一种安全协议的动态分析模型,从而克服了类BAN逻辑"理想化协议"步骤的缺陷,提出了消息唯一起源的概念和判定规则,严格区分"可靠信任"和"不可靠信任",解决了"相信事情的发生"和"相信事情的真实性"两种不同信任的区别,并在此基础上建立了动态逻辑方法.通过实例分析,该方法可以发现类BAN逻辑不能发现的协议漏洞,从而证明了方法的有效性. 展开更多

关键词 协议分析 动态逻辑 类ban逻辑

在线阅读 下载PDF 职称材料

一种可分析保密性与认证性的模态逻辑

11

作者 赵华伟 秦静 《计算机工程》 CAS CSCD 北大核心 2007年第20期30-33,共4页

提出了一种新的基于信念的模态逻辑——MBL逻辑,来分析由单向函数构造的对称钥认证交换协议的安全性。该逻辑有严格的证明体系,可证明推理规则在其语义模型下的正确性,说明该逻辑具有合理性。其推理规则不仅能对单向函数保护的消息进行... 提出了一种新的基于信念的模态逻辑——MBL逻辑,来分析由单向函数构造的对称钥认证交换协议的安全性。该逻辑有严格的证明体系,可证明推理规则在其语义模型下的正确性,说明该逻辑具有合理性。其推理规则不仅能对单向函数保护的消息进行有关认证性的推理,克服了以往逻辑系统使用不当的安全服务来分析协议认证性的缺陷,而且可分析消息的保密性,避免了其他逻辑分析协议时对可信中心的过分依赖,可发现敌手通过欺骗可信中心而造成的攻击。 展开更多

关键词 模态逻辑 MBL逻辑 ban类逻辑 会话密钥

在线阅读 下载PDF 职称材料

3G认证与密钥分发协议逻辑化分析 被引量：5

12

作者 袁亚飞 廉玉忠 《信息工程大学学报》 2004年第4期15-17,88,共4页

逻辑化方法是当前分析密码协议安全性的重要方法。文章通过运用一种新的认证逻辑系统,分析3G认证与密钥分发协议的安全性,并针对协议的安全漏洞,提出了改进的认证与密钥分发协议方案,解决用户的身份泄露和MS对VLR的认证问题,增强了网络... 逻辑化方法是当前分析密码协议安全性的重要方法。文章通过运用一种新的认证逻辑系统,分析3G认证与密钥分发协议的安全性,并针对协议的安全漏洞,提出了改进的认证与密钥分发协议方案,解决用户的身份泄露和MS对VLR的认证问题,增强了网络安全性。最后,对改进的协议安全性进行了分析。 展开更多

关键词 密钥分发协议 认证 安全漏洞 密码协议 网络安全性 协议安全 逻辑系统 用户 方案 增强

在线阅读 下载PDF 职称材料

一种新的安全协议形式化验证方法 被引量：1

13

作者 侯峻峰 张磊 黄连生 《计算机研究与发展》 EI CSCD 北大核心 2004年第8期1415-1420,共6页

形式化方法能有效检验安全协议的安全性 ,BAN类逻辑的发展极大地促进了这一领域的研究 ,但是现有的BAN类逻辑仍然存在许多问题 在分析现有BAN类逻辑的基础上 ,提出一种新的安全协议形式化验证方法 ,实现现有BAN类逻辑的验证功能 ,并使... 形式化方法能有效检验安全协议的安全性 ,BAN类逻辑的发展极大地促进了这一领域的研究 ,但是现有的BAN类逻辑仍然存在许多问题 在分析现有BAN类逻辑的基础上 ,提出一种新的安全协议形式化验证方法 ,实现现有BAN类逻辑的验证功能 ,并使安全协议验证工作简单可行 ,便于实现机器自动验证 展开更多

关键词 安全协议 形式化验证 ban类逻辑 自动验证

在线阅读 下载PDF 职称材料

一种安全协议的形式化验证方法

14

作者 石曙东 《湖北师范学院学报（自然科学版）》 2004年第1期15-18,共4页

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

关键词 安全协议 协议分析 ban类逻辑 验证方法 网络数据安全

在线阅读 下载PDF 职称材料

Otway-Rees协议改进及安全分析 被引量：1

15

作者 王君 昝亚洲 +1 位作者 刘爱森 屈萌 《信息工程大学学报》 2014年第5期525-530,共6页

选取Otway-Rees协议作为研究对象,用一种改进的BAN类逻辑――安全协议分析本征逻辑(SPALL)作为协议分析工具展开研究。首先对SPALL系统进行扩展,针对Otway-Rees协议存在的缺陷,提出了改进方案。为了更好地描述改进协议,用SPALL系统对其... 选取Otway-Rees协议作为研究对象,用一种改进的BAN类逻辑――安全协议分析本征逻辑(SPALL)作为协议分析工具展开研究。首先对SPALL系统进行扩展,针对Otway-Rees协议存在的缺陷,提出了改进方案。为了更好地描述改进协议,用SPALL系统对其安全属性进行了形式化描述,并做出安全分析。分析结果表明,改进协议能够确保密钥分发的正确性,并具有密钥机密性和强认证性,还能满足通信双方验证会话密钥一致性的要求。 展开更多

关键词 安全协议 ban类逻辑 形式化方法 OTWAY-REES协议

在线阅读 下载PDF 职称材料

GNY逻辑系统可靠性分析

16

作者 荣昆 李益发 付吉 《信息工程大学学报》 2006年第2期132-136,共5页

网络安全在信息时代非常重要,而网络安全的关键问题之一是安全协议的安全性。人们提出了多种安全协议的分析方法,BAN类逻辑是其中重要的一种,GNY逻辑就是一种BAN类逻辑。而认证逻辑本身的可靠性关系到分析结果的正确性。文章通过对GNY... 网络安全在信息时代非常重要,而网络安全的关键问题之一是安全协议的安全性。人们提出了多种安全协议的分析方法,BAN类逻辑是其中重要的一种,GNY逻辑就是一种BAN类逻辑。而认证逻辑本身的可靠性关系到分析结果的正确性。文章通过对GNY逻辑的可靠性分析,指出GNY逻辑是一个不可靠的认证逻辑系统。 展开更多

关键词 安全协议 可靠性 GNY逻辑 ban类逻辑

在线阅读 下载PDF 职称材料

NSL协议逻辑化分析

17

作者 袁亚飞 廉玉忠 《宜春学院学报》 2004年第4期70-71,共2页

逻辑化方法是当前分析密码协议安全性的重要方法.本文通过运用一种新的认证逻辑系统,给出NSL 认证协议的形式化分析证明,并提出协议改进方案.

关键词 逻辑化方法 认证逻辑系统 NSL协议

在线阅读 下载PDF 职称材料

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

18

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

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

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

在线阅读 下载PDF 职称材料

多播水印协议MAMWP的BAN逻辑分析 被引量：4

19

作者 陆正福 叶锐 王国栋 《云南大学学报（自然科学版）》 CAS CSCD 北大核心 2005年第1期18-21,共4页

用形式化的方法分析密码协议可以检测出协议中的漏洞和证明协议的安全性,BAN类逻辑是目前使用最广泛的一种形式化分析密码协议的方法.文章介绍了基于移动代理的多播水印协议MAMWP和BAN逻辑,并给出了用BAN逻辑分析MAMWP协议的详细过程.

关键词 ban逻辑 多播 水印 密码协议 形式化分析 移动代理 漏洞 ban类逻辑 安全性

原文传递

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

20

作者 张玉清 吴建平 李星 《清华大学学报（自然科学版）》 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类逻辑 形式化分析方法 协议理想化 推理规则

原文传递