安全协议的扩展Horn逻辑模型及其验证方法

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法，针对它们构造不满足安全性质的安全协议反例的不足，提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法，使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例．在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中，实现了上述算法，验证了算法的正确性．     

基于Horn逻辑扩展模型的安全协议反例的自动构造

根据安全协议的Horn逻辑扩展模型和相应的安全协议验证方法,提出了自动构造不满足安全性质的安全协议反例的求解策略,并给出了重要定理的证明,设计了一系列自动构造协议攻击的构造算法,并在基于函数式编程语言Objective Caml开发的安全协议验证工具SPVT中实现了这些算法,给出了主要算法的优化方法,详细分析了主要算法的时间复杂度,从理论上证明了算法是线性时间算法.最后,用SPVT对一些典型的安全协议进行了验证,得到了不安全协议的反例,并对反例进行了分析.得到的反例非常方便于阅读,与Alice-Bob标记非常接近,从而使任何领域的专家都可以用这种形式化的方法检查安全协议是否存在真实的反例.     

基于同态的安全协议攻击及其形式化验证

介绍2种利用加密算法同态特性的安全协议攻击,定义安全协议项代数表示和基于角色行为序列的协议模型,提出一种基于角色行为实例交互的安全协议约束序列生成方法,应用等式理论将Dolev D等人提出的Dolev-Yao模型（IEEE Transactions on Information Theory,1983,第12期）进行扩展,设计攻击者一阶逻辑演绎系统,采用约束求解方法对NSL协议进行建模和形式化验证,发现基于“完美密码系统假设”无法验证的同态攻击。     

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

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

SPVT:一个有效的安全协议验证工具

描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性.     

有穷机和逻辑结合的电子商务协议分析方法

提出一种扩展的有穷自动机模型,并结合卿-周逻辑给出一种新的电子商务协议形式化分析方法,用于分析电子商务协议的可追究性、公平性和时限性.该方法结合了模型检测和逻辑分析两种形式化分析方法的优点,可以准确形象地描述协议的具体运行过程,并且在发生重放攻击时能够正确分析各方的责任.利用该方法对Kim等人提出的改进版ZG协议进行了实例分析,给出了描述该协议运行过程的状态转换图,结合状态转换图对该协议分析得出其满足可追究性、公平性、时限性,并且不存在被重放攻击的可能.最后用时间自动机UPPAAL验证了新方法中有穷自动机模型的准确性和时限性分析的有效性.     

一种基于ECB模式的NSL协议改进方案

安全协议形式化方法大都在一个很高的抽象层次建立协议模型。但是协议的许多安全问题是在很低的抽象层次产生。本文分析了ECB工作模式下的NSL协议的安全问题,并通过破坏同态性的方法给出一种改进方案。通过扩展规则的BAN逻辑对NSL协议建模和分析,验证结果表明协议中存在着安全漏洞,新的改进方案可以避免这种攻击。     

针对猜测攻击的Athena方法的扩展

猜测攻击是安全协议中一类特殊问题，对其进行研究具有现实意义。本文针对猜测攻击，引入了基于串空间模型的Athena分析方法，并考虑了攻击者对弱口令的猜测能力。为此，在串空间模型的消息项中引入了可验证项的概念，以描述猜测攻击条件中的验证项，同时扩展了串空间中攻击者的能力，赋予了攻击者对弱口令的猜测能力；为在Athena后继函数搜索算法中实现对验证项的关联，以判断猜测攻击，在Athena方法的状态表示法中引入猜测验证目标及猜测验证目标绑定的概念，对状态、推理规则进行相应的修改，同时扩展后继状态函数，使扩展后的函数具备分析猜测攻击的能力；最后运用扩展后的Athena方法对会话密钥建立协议（key-establishment protocol）进行分析。分析发现，当pk为对称密钥时，协议存在猜测攻击，并给出了攻击路径。     

Needham-Schroeder公钥协议的模型检测分析

密码协议安全性的分析是当前网络安全研究领域的一个世界性难题.提出了运用模型检测工 具SMV(symbolic model verifier)分析密码协议的方法,并对著名的Needham-Schroeder(NS )公钥协议进行了分析.分析结果表明,入侵者可以轻松地对NS公钥协议进行有效攻击,而这个 攻击是BAN逻辑分析所没有发现过的.同时,给出了经SMV分析过的一个安全的NS公钥协议 的改进版本.     

基于扩展CS逻辑的非否认协议形式化分析方法

将基于知识逻辑的CS逻辑系统用于分析具有时限性的非否认协议,针对非否认协议的性质对CS逻辑进行了扩展,给出了描述和分析非否认性以及公平性的方法,并使用扩展后的逻辑对改进的ZG协议进行了分析。在分析过程中,发现了该协议存在对签名的重放攻击漏洞,不满足强非否认性。验证过程也表明,扩展后的CS逻辑能够有效地描述和分析具有时限性的非否认协议的安全性质。