认证协议的形式逻辑分析方法——BAN类逻辑综述

介绍了最早的认证协议形式化分析方法———BAN逻辑及扩展的BAN逻辑 ,统称为BAN类逻辑。并通过分析比较 ,指出了各种扩展的BAN逻辑对原BAN逻辑的扩展和改进之处。

BAN类逻辑的进一步研究

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

BAN类逻辑的两个缺陷分析

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

BAN逻辑及BAN类逻辑研究

一、引言 当用户通过网络进行信息交互时，网络通信的安全性成为人们首要关心的问题。密码协议是建立在密码体制基础上的交互通信协议，利用密码协议可实现密钥的分配和交换、身份认证等。它与普通通信协议的主要区别在于使用了密码技术。

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

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

BAN类逻辑的由来与发展

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

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

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

类BAN逻辑缺陷的进一步分析

类BAN逻辑是一种用于分析密码协议安全性的逻辑。文章分析了各种类BAN逻辑的缺陷,并对其进行了详细的分类描述,最后指出进一步发展类BAN逻辑需要解决的问题。

安全协议的设计与逻辑分析

随着网络应用的迅速发展,网络安全的问题日益重要.研究下述课题:安全协议的设计原则;安全协议设计中形式化方法的应用;各种形式化分析方法,特别是逻辑分析方法的特点.另外,还探讨了串空间模型在逻辑分析中的应用以及串空间模型指导安全协议形式化设计的可能性.

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

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

GNY逻辑系统可靠性分析

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

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

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

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

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

WAPI认证机制的性能和安全性分析

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

多播水印协议MAMWP的BAN逻辑分析

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

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

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

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

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

基于CPK的IKE协议的改进

本文在简要介绍和分析评述IPsec协议的基础上,基于CPK系统提出了对IPsec协议的改进,并对改进的协议利用逻辑化方法作了详细地安全性分析,指出了改进的协议在安全性和效率等方面所具有的优势,同时对应用环境作了说明。

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

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

Otway-Rees协议改进及安全分析

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