IKE2协议的形式化分析

现有的IPSec密钥交换标准存在着若干安全漏洞,为了解决相关的安全及应用问题,IETF提出了IKE2协议.应用SVO逻辑对IKE2协议进行了形式化分析,证明了IKE2协议的密钥交换和认证安全性.对IKE2协议的分析也证明了SVO逻辑可用于分析基于Diffie-Hellman交换的复杂安全协议.     

改进的可证安全的相互认证及密钥协商方法

提出一种新的用于移动通信的相互认证和密钥协商方法——NMAKAP。NMAKAP采用基于阿贝尔群的模幂运算和散列函数进行身份认证,取代了传统公钥密码算法和数字签名方案,降低了协议的计算开销和实现成本。在SVO逻辑系统证明下,NMAKAP协议是安全的。SVO逻辑是安全协议形式化分析的一种重要方法,文章扩展了SVO逻辑分析散列函数的逻辑语法。SVO逻辑方法的认证目标被发现存在中间人攻击,为此提出了新的认证目标,并分析了新目标的安全性。分析了一种可用于移动通信的认证协议——MAKEP。MAKEP协议通过预计算,大大降低了移动设备的计算量,但被认为存在Hijacking攻击。分析表明针对原MAKEP协议的Hijacking攻击并不成立,但该协议被发现存在未知共享密钥攻击,为此提出了改进意见。     

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

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

3G中安全增强的AKA协议设计与分析

提出了3G安全保密系统框架,设计了安全增强的认证与密钥协商协议,并对其进行了基于SVO逻辑的安全性分析。结果表明,SE-AKA协议在永久身份保密、双向认证、不可否认性等方面的安全性都优于3GPP-AKA协议,使UMTS接入网络能够抵抗改向攻击和主动攻击。而且协议中消除了重同步机制,避免了序列号操作困难带来的危害。这些安全功能满足了3G环境下特殊部门高级别的安全需求。     

协议组合逻辑安全的WMNs认证密钥协商方案*

IEEE P802.11 s?/D1.01中EMSA认证协议是无线网状网络(WMNs)安全的重要保证。论文基于协议组合逻辑形式化分析了EMSA协议的安全性,发现EMSA协议存在密钥泄露伪装攻击,针对该安全威胁,运用协议演绎系统提出了一种新的WMNs安全认证密钥协商方案,并使用协议组合逻辑对新方案进行了形式化的安全性证明分析,最终表明新协议相对于EMSA协议更加安全,具有前向安全性,可抵御密钥泄露伪装攻击,更适合WMNs应用环境。     

基于SVO逻辑的3G AKA协议形式化分析

AKA协议是3G通讯中的一个重要安全协议。利用SVO逻辑对该协议进行形式化分析,以期发现其是否存在安全缺陷。运用信息隐藏的方法对该协议的缺陷进行了修正。另外指出SVO逻辑不能分析协议运行中的关键性明文对协议安全性的影响,以及不能分析旁听攻击这两个新的缺陷,并对SVO逻辑进行了扩展。     

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

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

因特网密钥交换协议研究

密钥交换协议是密码协议中主要的一类协议，安全可靠的密钥交换是通信安全性的基础，因特网密钥交换协议IKE作为IPSEC协议族的关键组成部分，在因特网的安全通信和安全服务中发挥着非常重要的作用，成为密码协议分析和研究的一个热点。该文首先介绍IKE协议，然后对协议中一种具体的密钥交换模式的安全性使用逻辑方法进行证明，并得出关于协议正确性的结论。     

一种网络间可信连接协议

为了解决深化“互联网+先进制造业”进程中网络可信互连问题，引入了可信连接架构（trusted connect architecture，简称TCA）技术.基于TCA技术思想，针对网络间可信认证需求，设计了一种支持网络间互连的可信连接协议（TCA-SNI）.引入了网络间双向认证过程，给出了TCA-SNI协议的交互过程；使用扩展的SVO逻辑系统对协议进行逻辑推理，证明该协议是安全可靠的；使用Dolev-Yao攻击者模型对协议进行攻击测试，实验结果表明，协议的安全目标均已达成，证明该协议可以抵御真实网络中的攻击.     

一种通用可组合安全的快速密钥交换协议

针对快速密钥交换协议JFKi信息冗余及缺乏形式化证明的问题,提出一种轻量级快速密钥交互协议LJFKi。通过对比分析,发现所提协议的消息长度较原有协议减少1/3,具有较高的通信效率,更适用于对通信负载比较敏感的网络。利用通用可组合安全模型证明该协议能够实现安全会话理想函数,具有通用可组合安全性。     

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

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

类BAN逻辑基本模型及缺陷

类BAN逻辑是一种用于分析密码协议安全性的逻辑.在分析了BAN,AT,MB,GNY,SVO等类BAN逻辑之后,指出这些逻辑的缺陷,包括若干新发现的缺陷.首先把类BAN的模型抽象出来,形成一个五元组模型,然后分析该模型的各个要素,并依据该模型对类BAN逻辑的缺陷进行分类,最后指出进一步发展类BAN逻辑应解决的问题.     

Multi-Attacker Protocol Validation

Security protocols have been analysed focusing on a variety of properties to withstand the Dolev-Yao attacker. The Multi-Attacker treat model allows each protocol participant to behave maliciously intercepting and forging messages. Each principal may then behave as a Dolev-Yao attacker while neither colluding nor sharing knowledge with anyone else. This feature rules out the applicability of existing equivalence results in the Dolev-Yao model. The analysis of security protocols under the Multi-Attacker threat model brings forward yet more insights, such as retaliation attacks and anticipation attacks, which formalise currently realistic scenarios of principals competing each other for personal profit. They are variously demonstrated on a classical protocol, Needham-Schroeder??s, and on a modern deployed protocol, Google??s SAML-based single sign-on protocol. The general threat model for security protocols based on set-rewriting that was adopted in AVISPA (Armando et al. 2005) is extended to formalise the Multi-Attacker. The state-of-the-art model checker SATMC (Armando and Compagna, Int J Inf Secur 6(1):3?C32, 2007) is then used to automatically validate the protocols under the new threats, so that retaliation and anticipation attacks can automatically be found. The tool support scales up to the Multi-Attacker threat model at a reasonable price both in terms of human interaction effort and of computational time.     

电子商务支付协议认证性的SVO逻辑验证

与证伪法（如模型检测）相比,采用证真法（如定理证明和逻辑推理）能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。     

利用类型推理验证Ad Hoc安全路由协议

提出一种基于类型推理的移动Ad-Hoc网络安全路由协议的形式化验证方法.定义了一种邻域限制通信演算NCCC(neighborhood-constrained communication calculus),包括演算的语法和基于规约的操作语义,在类型系统中描述了移动Ad-Hoc网络路由协议的安全属性,定义了近似攻击消息集用以精简Dolev-Yao攻击模型.还给出了该方法的一个协议验证实例.基于类型推理,该方法不仅能够验证协议的安全性,也可以得出针对协议的攻击手段.因为攻击集的精简,有效地缩减了推理空间.     

Dolev-Yao攻击者模型的形式化描述

模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev-Yao攻击者模型建立了一套形式化描述方法。遵循这一方法,可以使用任何建模语言机械地建立Dolev-Yao攻击者模型,从而大大地减少了人工分析的成份。同时,本文还使用该方法验证了两个目的完全不同的协议,证明了它的通用性。     

一种可靠的多方不可否认协议的逻辑分析方法

多方不可否认协议需要满足不可否认性、公平性和时限性三大安全目标,但是现有的对多方不可否认协议的形式化分析方法大多是对两方协议分析方法的简单扩展,单一方法不能完整覆盖所有的安全目标分析;同时,对单一安全目标的分析能力有限,分析结果不可靠。首先,综合比较现有的分析技术,选定SVO逻辑进行扩展,显式引入时间因素,给出对应的语法定义和时间演算公理。然后,对改进逻辑的语义模型进行介绍,并证明了逻辑系统的可靠性,使得改进后的逻辑系统支持对多方不可否认协议三大安全目标的分析。最后,选取一个典型的多方不可否认协议,分别对其时限性和公平性进行分析,发现了其中存在的时限性和公平性缺陷,并给出了对应的攻击方法。其中,公平性缺陷是首次被发现。     

一种新型的非否认协议

在克服一种非否认协议草案的缺陷的基础上,提出一种新的非否认协议.新的协议可以在不安 全和不可靠的信道上工作,并能对付各种欺骗行为.此外,还对SVO逻辑进行扩充,引进一些新 的概念和方法,并用扩展后的SVO逻辑分析与证明新的非否认协议.