基于事件逻辑的改进Needham-Schroeder协议安全性证明

安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论。利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的。此理论适用于类似复杂协议形式化分析与验证。     

一种基于问题求解理论的密码协议形式模型

提出了一种基于问题求解理论的密码协议模型，给出了模型的基本语法以及基于ρ演算的形式语义，明确了模型推理过程中涉及到的一些关键性的概念和命题。该模型具有以下特点：能够对密码协议进行精确的形式化描述；具有合理可靠的可证明语义；对密码协议安全性的定义精确合理；便于实现自动化推理。所有这些均确保了基于该模型的密码协议安全性分析的合理性和有效性，为正确的分析密码协议的安全性提供了可靠依据。     

用BAN逻辑方法分析TLS协议

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

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

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

一种基于规划理论的密码协议形式模型

将规划理论引入到密码协议形式化分析领域,结合密码协议在实际网络环境中的运行特点和规律,提出了密码协议攻击规划理论;建立了一种对密码协议进行安全性验证的形式化模型,即密码协议攻击规划问题模型;给出了模型的一阶语法、形式定义及相关运算语义.同时,分析了Dolev-Yao模型的不足之处,基于基本消息元素策略对其进行了改进;并通过增强应用语义来保证改进模型的可行性,从而避免了"状态空间爆炸"问题的发生,提高了密码协议攻击规划问题模型的完备性;并给出了基于该模型的NS公钥协议分析实例.提出的密码协议形式模型是证伪的,目的在于对密码协议进行验证,并查找协议中可能存在的漏洞,既可以方便地进行手工推导证明,也非常易于自动化实现.     

密码协议验证中的Petri网方法

如何验证密码协议的安全性是一个复杂的问题,只有形式化的验证方法才能证明密码协议的绝对正确.利用Petri网给出了一种用于密码协议验证的形式化方法.在合理假设的基础上,区分合法用户与攻击者在执行协议时的前提条件,列出执行协议后的结果,在此基础上建立了攻击者的Petri网模型.最后,用这种方法对NSPK协议进行了验证,证明了最初的NSPK协议中存在一个安全问题,而改进的NSPK协议则消除了这个问题.证明了这种方法的有效性.     

适应受限环境的认证协议及其SVO逻辑分析

针对认证协议在受限通信网络环境中的应用和安全问题,提出一种基于椭圆曲线密码技术的认证协议,使用对称密码为协议中的交互信息提供机密性,在协议最后生成参与者共享的会话密钥。采用扩展的SVO逻辑对推荐协议进行形式化分析,结果证明该协议的安全性符合要求。     

一种新的基于有色Petri网的安全协议建模方法

密码协议安全性的分析是网络安全的一个难题，运用形式化方法对密码协议进行分析一直是该领域的研究热点。本文提出了一种新的基于有色Petri网的安全协议建模方法，并以TMN密码协议为例，说明了这一方法的建模过程。     

模型检测技术和密码协议分析

1 引言密码协议是建立在密码体制基础上的一种交互通信的协议,它运行在计算机通信网或分布式系统中,借助于密码算法来达到密钥分配、身份认证等目的。目前密码协议已广泛应用于计算机通信网与分布式系统中,但密码协议安全性的论证仍是一个悬而未决的问题。九十年代以来,密码协议的形式化分析成为国际上的研究热点。这种方法的出发点是希望将密码协议形式化,而后借助于人工推导,甚至计算机的辅助分析,     

一种改进的Woo-Lam密码协议模型

提出了一种改进的Woo-Lam密码协议模型，即eWoo-Lam模型。与Woo-Lam模型相比，新模型具有以下特点：增强了模型中关于密码学原语操作的描述语法，使得对密码协议主体行为的描述更加精确，提高了模型在检测协议攻击方面的能力； 引入了匹配运算机制，保障了模型安全性证明的有效性； 提出了七条形式化准则，规范了模型的抽象过程； 扩充了模型基于状态迁移的形式语义，使其更加精确合理； 重新给出了模型安全性的形式定义，使其更具一般性。     

一种基于关联规则的安全协议验证方法

提出了一种基于关联规则的安全协议形式化分析方法。从主体认证关联、消息间关联和消息内部关联三个角度去刻画协议,提出了基于以上关联特点的协议验证方法。利用该方法对Woo and Lam认证协议进行了逆向验证分析，成功推导出现有的已知攻击路径，使这些已知攻击路径的推导能统一于该验证方法；同时还发现了一个未知的攻击路径，为协议的形式化分析提供了新思路。     

基于安全协议代码的形式化辅助建模研究

随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方案。首先,使用污点分析获取协议的通信流程,并且记录密码学原语操作;然后,根据通信流程之间的序列关系构建协议通信状态机;最终,根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明,此方案可以生成形式化模型中的关键部分,提高了形式化建模的自动化程度,为形式化分析技术的推广作出贡献。     

强安全三方认证密钥交换协议

针对现有的三方认证密钥交换协议缺乏严格安全证明的问题,研究三方密钥交换协议的安全模型。将两方认证密钥交换协议的强安全模型eCK模型推广至三方,同时考虑内部人攻击,定义强三方认证密钥交换协议安全模型,提出一个具体三方认证密钥交换协议并给出其在强安全模型中的安全性证明。     

基于GSPM的安全协议新鲜性分析*

安全协议形式化分析方法通过规范描述和数学推理来检验安全协议是否满足各种安全要求.GSPM是安全协议形式化分析的一般模型.在该模型中加入新鲜性的定义,形式化描述了新鲜性这一特殊的安全性质,扩展了GSPM的适用范围,并通过Andrew Secure RPC协议给出了形式化分析新鲜性的实例研究.     

Invariant-based reasoning about parameterized security protocols

We explore the applicability of the programming method of Feijen and van Gasteren to the domain of security protocols. This method addresses the derivation of concurrent programs from a formal specification, and it is based on common notions like invariants and pre- and post-conditions. We show that fundamental security concepts like secrecy and authentication can nicely be specified in this way. Using some small extensions, the style of formal reasoning from this method can be applied to the security domain. To demonstrate our approach, we discuss an authentication protocol and a public-key distribution protocol, and we deal with their composition. By focussing on a general setting where agents run the protocols multiple times, the nonce concept turns out to pop-up naturally. Although this work does not contain any new protocols, it does offer a new view on reasoning about security protocols.     

一种轻量级RFID安全协议

在分析了几种现有的典型RFID安全协议的特点和缺陷的基础上,提出了一种轻量级的RFID安全协议,该协议将一次性密码本与询问一应答机制相结合,实现了安全高效的读取访问控制,最后建立该协议的理想化模型,利用BAN逻辑对该协议进行了形式化分析,在理论上证明其安全性.     

安全属性形式化描述统一框架及其分析方法研究*

在安全协议的形式化分析研究当中,如何在统一的框架下对更多的安全属性进行分析和验证是一个亟待解决的重要问题。为了解决这个问题,本文提出了用匹配关系来形式化地描述各种安全属性的统一框架,建立了语法和语意系统,并证明了该框架的可靠性和完备性。在此基础上,将知识推理和进程演算结合起来,提出了一个安全协议形式化分析的一般模型。最后,给出了一些安全属性的研究实例,并指出了进一步完善此模型的研究方向。     

安全协议的形式化需求及验证

该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在AT模型的基础上加入信任和知识的非单调逻辑,建立了安全协议的计算模型。利用该计算模型对Denning_Sacco公钥协议进行了验证,发现了对此协议的重放攻击,并对协议进行了修改。     

On the security of an identity based multi-proxy signature scheme

In a multi-proxy signature scheme, an original signer could authorize a proxy group as his proxy agent. Then only the cooperation of all the signers in the proxy group can generate the proxy signatures on behalf of the original signer. Recently, Cao and Cao gave the first formal definition and security model of an identity-based multi-proxy signature scheme, then proposed an identity-based multi-proxy signature scheme from bilinear pairings and proved its security in their security model. Although they proved that their scheme is secure under this model, we disprove their claim and show that their scheme is not secure. We also present a simple fix to prevent this attack.