一类具有“开端”结构的安全协议分析方法研究

开端协议(Open-ended Protocol)的分析是安全协议领域中一个待解决的重要问题,而IKE则是一个有代表性的具有"开端"结构的安全协议.本文基于串空间的Athena方法,针对IKEv2协议中的"开端"结构涉及的DH(Diffie-Hellman)问题,增加了群、散列函数等原语,给出并证明了一个新的消减规则;针对"开端"结构,引入了集合的数学概念,建立了新的消息类型,重新定义了串空间中的消息项、替换、入侵者模型,以及Athena相应的内在项、目标和目标绑定,给出了一个新的替代关系.应用扩展后的方法,分析了协议,发现一个新的认证性缺陷,给出了解决该缺陷的方法.     

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

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

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

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

基于串空间的可信计算协议分析

可信计算技术能为终端、网络以及云计算平台等环境提供安全支撑,其本身的安全机制或者协议应该得到严格的形式化证明.该文基于串空间模型对其远程证明协议进行了分析.首先,扩展了串空间的消息代数和攻击者串,使其能表达可信计算相关的密码学操作,并对衍生的定理进行了证明;并且提出了4个新的认证测试准则,能对协议中的加密、签名、身份生成和哈希等组件进行推理.其次,基于扩展的串空间模型对远程证明协议的安全属性(隐私性、机密性和认证性)进行了抽象和分析.最后,给出了对发现攻击的消息流程,并基于ARM开发板对其中的布谷鸟攻击进行了实现,验证了串空间的分析结果.     

MANET虚假路由形式化验证

提出了Ad-hoc网络虚假路由攻击的形式化验证和分析方法,主要是在参数化Ad-hoc路由协议串空间模型的基础上采用改进的Athena状态表示法来描述问题域,并采用相应的证明搜索过程来完成目标验证。最后设计实现了虚假路由自动验证系统FRpoofor,用它验证和分析了Ariadne安全路由协议运行环境下某些虚假路由的建立过程,以此说明方法的有效性。     

基于串空间的安全协议自动化验证算法

以串空间模型为理论基础,提出安全协议自动化验证算法IVAP。对于有漏洞的协议,针对不安全属性逆向搜索主体串树,自动生成改进协议并对其进行验证,直至生成一个安全的改进协议。实验结果证明了该自动化验证算法的有效性,与AAAP算法相比,其协议验证效率更高。     

基于串空间模型的电子商务协议的形式化分析

采用形式化方法分析安全协议是协议分析的有效手段,近年来,出现了众多的研究方法。串空间模型是一种新兴的密码协议形式化分析工具。文章基于串空间模型,扩展了认证测试方法,使之能够描述和分析电子商务协议。并用该方法对一个具体的协议进行了形式化分析,得到了与以往文献相同的结论。     

基于串空间模型安全协议形式化分析方法的研究

从串空间模型理论人手,提出了三种典型的串空间形式化方法(基于极小元理论的串空间方法、基于理想与诚实理论的串空间方法、基于认证测试理论的串空间方法),并对每一种方法的证明步骤及优缺点进行了分析.在此基础上,应用提出的串空间方法对Yahalom协议的秘密性和认证性进行了分析.分析结果表明利用不同方法的优点,能更好地保证安全协议形式化分析的准确性.     

基于串空间模型安全协议形式化分析方法的研究

从串空间模型理论人手,提出了三种典型的串空间形式化方法（基于极小元理论的串空间方法、基于理想与诚实理论的串空间方法、基于认证测试理论的串空间方法）,并对每一种方法的证明步骤及优缺点进行了分析。在此基础上,应用提出的串空间方法对Yahalom协议的秘密性和认证性进行了分析。分析结果表明利用不同方法的优点,能更好地保证安全协议形式化分析的准确性。     

基于串空间和状态转换的认证协议分析方法

串空间是一种新兴的安全协议形式化分析模型。串空间模型中的理论证明方法虽然严谨,但难度很大。本文基于串空间模型,首先定义系统状态,并以Needham-Schroeder-Lowe公钥认证协议为例说明系统状态转换的分析过程。通过对状态转换过程中现实的跟踪考察,得出了有意义的结论。结合串空间模型,验证了该认证协议的安全性。这种分析认证协议的新方法简洁和高效,并易于实现自动化。     

改进Athena算法的多协议攻击自动化验证方法

多协议环境下协议安全性问题是安全协议形式化分析验证领域的一个公开问题。针对此问题,在分析Athena算法的基础上提出了一种多协议攻击自动化验证方法。该方法扩展了Athena状态表示方法和后继状态生成算法,使得攻击者具备截取其它协议交互消息和计算生成当前协议消息的能力,能够以自动化的方式验证协议是否存在多协议攻击。实验结果表明,提出的方法能够实现多协议攻击的自动化验证。     

安全协议自动验证工具的状态空间剪枝

串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构，提出一些剪枝规则对状态搜索空间进行剪枝。通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间，防止状态空间爆炸。     

安全协议验证模型的高效自动生成

为了能高效地利用模型检测技术对安全协议进行分析与验证,提高工作效率,提出了一种适用范围广,自动化程度及验证效率均较高的建模算法。开发了一个基于该建模算法“网络安全协议验证模型生成系统”,该系统可高效地对安全协议进行分析与验证,系统在对攻击者建模时采用偏序规约、语法重定序及类型检查等优化策略以提高验证效率,有效地缓解了模型检测过程中的状态爆炸问题。     

一种基于攻击序列求解的安全协议验证新算法

基于完美加密机制前提及D-Y攻击者模型,指出注入攻击是协议攻击者实现攻击目标的必要手段.分析了注入攻击及其形成的攻击序列的性质,并基于此提出了搜索攻击序列的算法,基于该算法实现了对安全协议的验证.提出和证明了该方法对于规则安全协议的搜索是可终止的,并通过实验实现了NS公钥协议的验证.实验结果表明,与OFMC等同类安全协议验证工具相比,该算法不仅能实现安全协议验证自动化,而且由于规则安全协议验证的可终止性,使得本算法更具实用性.     

注入攻击序列搜索算法对安全协议的验证研究

通过对D-Y攻击者模型研究,可知注入攻击是攻击者实现其攻击目标的必要手段。对注入攻击序列的性质进行分析,提出了一种在安全协议会话状态空间中搜索注入攻击序列的算法,基于该算法可实现一种新的安全协议验证方法。利用该方法实现了NS公钥协议的验证。实验表明该方法可以实现对安全协议的自动化验证,降低了验证的复杂度,并能给出安全协议漏洞的具体攻击方法。     

AVSP算法

AVSP(Automatic Verifier of Secrurity Protocols)是基于串空间模型(Strand Space Model),并结合使用定理证明和模型检测技术开发出来的密码安全协议自动验证工具。AVSP使用了理想的语义和逻辑来表达安全协议的保密性,同时采用了一些证明策略以控制和减少状态空间爆炸的规模,并加快发现协议中存在的漏洞。     

一种安全协议自动化分析方法*

提出了一种基于串空间的安全协议自动化分析模型,该模型运用一系列算法实现协议的自动化分析,克服了冗长的理论推导,使协议的分析更加简洁和直观。模型的主要功能已在MyEclipse环境下用Java编程实现,并首次运用实现后的自动化分析模型对改进前后的Helsinki协议进行分析验证,证明了该自动化分析方法的简洁性和有效性。