一种时间相关的分析安全协议的扩展逻辑

Coffey和Saidha提出的CS逻辑可以分析与时间相关的的公钥协议。〖BP）〗在对CS逻辑进行研究的基础上,提出了CS逻辑的扩展逻辑。该扩展逻辑对CS逻辑中存在的一些缺陷进行了修改和扩展,使其不仅可以分析公钥协议,还可以分析对称密钥协议。最后对一个协议实例进行了有效的形式化分析。     

一种证书管理协议的改进方案

公钥认证体制中认证机构和其它实体使用证书管理协议进行交互，完成证书管理功能．本文对IETF制定的证书管理协议草案进行了分析，针对其缺点提出了改进方案，并使用BAN逻辑进行了形式化分析，以达到互操作性、安全性的目的．     

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

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

单向函数在公钥认证协议中的作用

对认证协议进行了研究,指出采用保密服务是设计认证协议是一种安全服务的误用,存在两种潜在的安全隐患。针对带密钥的单向函数提出了一种扩展的BAN逻辑。利用该逻辑对两种改进的公钥认证协议进行形式化分析,说明带密钥的单向函数所提供的两种安全服务能够保证公钥认证协议的安全。     

基于WPKI的移动通信端到端认证协议

提出了一个在不同移动运营商中移动终端的相互认证协议.该协议利用WPKI机制,实现对双方公钥证书的认证.最后采用BAN逻辑,对协议的形式化分析表明协议达到了认证目标.     

基于身份的TLS协议及其BAN逻辑分析

基于身份的密码体制(IBC)轻量、高效,密钥管理方式简单,但缺乏有效安全协议的支持限制了其应用。通过增加支持IBC的加密套件,引入IBC公钥代替RSA证书公钥,减少消息交换数量,提出支持IBC的、高效的基于身份的IB_TLS协议。使用BAN逻辑对其进行形式化分析,证明IB_TLS协议是安全的。     

一种类BAN逻辑的分析和改进

ＢＡＮ作为对认证协议形式化分析的逻辑,在获得巨大的声望的同时也受到诸多抨击。如对秘密性要求的形式化表示,以及将协议格式改写为ＢＡＮ可分为格式时的困难。其中一个例子就是对Ｎｅｓｓｅｔｔ协议的分析。为解决这些问题,ＷｅｎＢｏ Ｍａｏ,ＣｏｌｉｎＢＯｙｄ于１９９３年提出了一个新的逻辑（ＭＢ９３）。该文将介绍这两个逻辑,并构造一个简单协议来指出ＭＢ９３逻辑在分析Ｎｅｓｓｅｔｔ协议及类似公钥体制的认证协议时     

认证协议攻击与非形式化分析

协议的分析验证方法有形式化与非形式化之分．很多代表性的协议虽然存在着缺陷，但对这些协议的非形式化分析，却可以提出一些值得借鉴的规则，参考这些规则可以避免和减少协议逻辑的漏洞，本文针对Woo-Lam两个改进协议以及SSL协议给出了攻击方法，分析协议存在的漏洞并提出如何使协议更为安全的建议。     

一种快速安全认证协议及其形式化分析

介绍了现有的常用身份认证方法,分析了其安全性和不足之处,针对安全性和效率问题,提出了一种可实现快速安全认证的一种新协议,差使用协议组合逻辑形式化分析了新协议的安全性和新协议的效率,结果证明该协议既具有基于证书的公钥密码体制的安全性,又保持了对称密码体制的高效性.     

用BAN逻辑方法分析TLS协议

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

TMN密码协议的SMV分析

密码协议安全性的分析是网络安全的一个难题，运用形式方法对密码协议进行分析一直是该领域的研究热点。运用模型检测工具SMV对TMN密码协议进行了形式分析。在建立一个有限状态系统模型和刻画TMN密码协议安全性质的基础上，使用SMV对TMN密码协议进行了安全分析。分析结果表明TMN密码协议存在一些未被发现的新攻击。     

一种新的密码协议分析方法及其应用

针对传统时序逻辑把协议看成封闭系统进行分析的缺点, 提出一种新的基于策略的ATL逻辑方法分析密码协议。最后用新方法对Needham-Schroeder协议进行了严格的形式化分析,结果验证了该协议存在重放攻击。工作表明基于博弈的ATL逻辑比传统的CTL更适合于描述和分析密码协议。     

基于CCS的加密协议分析

加密协议的分析需要形式化的方法和工具.该文定义了加密协议描述语言PEP (principals+environment=protocol),并说明对于一类加密协议,其PEP描述可以转化为有穷的基本CCS进程,由此可以在基于CCS的CWB(concurrency workbench)工具中分析加密协议的性质.此方法的优点在于隐式地刻画攻击者的行为,试图通过模型检查(model checking)发现协议潜在的安全漏洞,找到攻击协议的途径.     

基于

Formal methods and tools are key aspects for the analysis of cryptographic protocols. In this paper, a formal language PEP (principals+environment=protocol) for the specification of cryptographic protocols is proposed. For some cryptographic protocols, their PEP specifications can be translated into finite basic CCS processes, so it is possible to analyze the security properties using CCS-based tools such as CWB (concurrency workbench). The advantage of the mothod proposed in this paper is that the actions of the attacker can be implicitly specified, and if the potential back door of the protocol analyzed exists, the attacking action trace can be explicitly found out by model checker.     

Neuman-Stubblebine协议的串空间模型及分析

串空间模型是一种新兴的密码协议形式化分析工具,其理论中理想和诚实概念的提出大大减少了协议的证明步骤.首次利用串空间理论从机密性和认证性两个方面对Neuman-Stubblebine协议进行了分析.分析结果证明该协议是安全的,而且理想对公开密钥算法和对称密钥算法产生的协议的分析都是有效的.     

用BAN逻辑方法分析SSL3．0协议

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

分析安全协议猜测攻击的模态逻辑方法

以CKT5逻辑为基础,对其进行了多方面重要的扩展;在原有对称密钥机制的基础上,增加了公开密钥机制和vernam加密机制以增强其描述协议的能力;打破完善加密假设,给出了一组定义和规则使主体具备猜测和验证口令的能力;给出了与在线猜测攻击相关的定理以反映在线猜测攻击的特点;通过相关引理和定理的证明,简化了猜测攻击的分析过程,使该文方法比现有方法更加简洁高效.扩展后的逻辑能够用于分析安全协议的猜测攻击,包括在线猜测攻击.     

基于形式方法的Andrew RPC认证协议的分析与改进

密码协议安全性分析是网络安全的一个难题，运用形式方法对密码协议进行分析一直是该领域的研究热点。运用BAN逻辑对Andrew RPC（Remote Procedure Call）认证协议进行了形式分析，发现了协议中存在的安全缺陷。对协议进行改进，并给出改进后的安全协议。     

一种新的安全协议形式化分析方法——证据逻辑

形式化分析技术对于安全协议的正确设计至关重要,考虑到现有信仰逻辑分析方法的不足,该文提出一种新的安全协议形式化分析方法——证据逻辑,即通过对协议主体证据的推理来实现安全协议的形式化分析。与现有的方法相比,该方法不仅能够用于认证协议、密钥协商(交换)协议的分析,也能用于电子商务协议的不可否认性和公平性的分析,因此具有更好的通用性和更强的协议分析能力。