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

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

基于状态转移系统的安全协议形式模型

提出一种基于状态转移系统的安全协议模型,以Dolev-Yao攻击者模型为前提假设,以状态转移系统为框架,用语义编码的方式定义消息和事件,用重写关系定义协议规则,用事件的集合来描述协议的安全属性,并给出安全属性的检验策略。该模型能够对安全协议进行精确的形式化描述,且便于实现自动化分析。     

运用SPIN对开放授权协议OAuth 2.0的分析与验证

OAuth 2.0协议是一种开放授权协议,主要用于解决用户账号关联与资源共享问题。但是,其弱安全性导致各网络公司海量用户信息泄露,且OAuth 2.0传输数据采用的https通道效率低下,成为黑客攻击对象。提出采用http通道传输OAuth 2.0协议数据,基于Promale语言及Dolev-Yao攻击者模型对OAuth 2.0协议建模,运用SPIN进行模型检测。形式化分析结果表明,采用公钥加密体系对OAuth 2.0协议进行加密不安全。上述建模方法对类似的授权协议形式化分析有重要借鉴意义。     

运用SPIN对云环境双向认证协议Nayak的安全性验证

随着云计算的发展,由欺诈行为驱动的窃取云资源和云服务的行为日趋严重,导致云资源提供商与用户间出现信任危机。Nayak协议是一种改进的云环境双向认证协议,用于保障用户安全登录云服务器,防止第三方恶意窃取用户信息。采用对称密钥密码体系对Nayak协议进行加密,基于Dolev-Yao攻击者模型,提出四通道并行建模法描述攻击者能力。该建模方法解决了Nayak协议并行运行过程中的模型检测问题以及安全隐患,优化了模型复杂度与存储状态数。运用SPIN模型验证工具分析表明采用对称密钥密码体系对Nayak协议加密不安全。此方法可运用于类似复杂协议形式化分析与验证。     

基于Strand模型的Needham-Schroeder协议分析

Strand空间模型是一种安全协议分析模型.使用图的形式来描述协议,证明协议的正确性.通过分析研究,本文建立了攻击者模型.并在此基础上运用安全协议的形式化分析方法-Stmnd空间模型,对公开密钥协议NSPK进行了分析,说明了该方法进行协议分析的过程,证明了该协议在保密性和认证性方面的正确性,并分析了该协议存在的安全缺陷.     

基于OAuth2.0协议的安全授权模型研究

本文在OAuth2.0授权码模型的基础上做出改进,采用HLPSL语言对授权码模型进行形式化建模,建立OAuth2.0协议授权码模型形式化模型,找到授权码模型出现安全漏洞的根本原因是客户端凭证可以被攻击者窃取。结合惰性无限状态方法和惰性攻击者优化方法对形式化模型分析和验证。提出OAuth2.0安全授权码模型,并分析和验证其在理论上无安全漏洞。通过的研究,本文可以提供一套安全的OAuth2.0授权协议模型,对目前安全要求高的开放平台的授权是有指导意义的。     

基于 Spin/Promela 的 Woo-Lam 协议安全性质高效验证磁

形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于 Promela 语言,将 P ．Maggi 和 R ．Sisto 提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型,枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中,提高了协议建模效率,保证了建模准确性。以Woo-Lam 协议为例,运用 Spin 工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。     

基于连续ARQ协议的隐蔽洪水攻击

通信协议设计时的疏漏很容易造成严重的后果,因此有必要采用形式化的方法来保证协议的安全性和可靠性.模型检测是一种具有工业应用前景的形式化分析方法,并具有很高的自动化程度,适合于协议的分析与验证.文中采用模型检测工具SPIN对连续ARQ协议建模,通过验证该协议的基本属性证明所建模型的正确性.然后依据Dolev和Yao的思想加入攻击者模型再进行分析,发现了连续ARQ协议的一个新漏洞,攻击者能够利用这个漏洞造成大量冗余数据的传输和存储.这种攻击建立在互信的数据传输基础上,且攻击者并不直接发送冗余数据,因此具有很高的隐蔽性.     

NS公钥协议新的分析方法

密码协议安全性的分析是当前网络安全研究领域的一个世界性难题。在函数式程序设计语言haskell中给出一种NS公钥协议的分析方法。在形式化建模时,以Dolev-Yao攻击者模型为前提假设,状态转移系统为框架,用语义编码的方式定义消息和事件,用事件的集合来描述协议的安全属性,并给出安全属性的检验策略。Haskell的惰性计算特性解决了对协议形式化分析的语义描述等关键问题,发现了NS协议的中间人攻击。     

802.11i双向认证协议的模型检查

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。     

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

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

On the decidability of cryptographic protocols with open-ended data structures

Formal analysis of cryptographic protocols has concentrated mainly on protocols with closed-ended data structures, i.e., protocols where the messages exchanged between principals have fixed and finite format. In many protocols, however, the data structures used are open-ended, i.e., messages have an unbounded number of data fields. In this paper, decidability issues for such protocols are studied. We propose a protocol model in which principals are described by transducers, i.e., finite automata with output, and show that in this model security is decidable and PSPACE-hard in presence of the standard Dolev-Yao intruder.     

Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks

In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability.Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.     

Towards a Quantitative Analysis of Security Protocols

This paper contributes to further closing the gap between formal analysis and concrete implementations of security protocols by introducing a quantitative extension of the usual Dolev-Yao intruder model. This extended model provides a basis for considering protocol attacks that are possible when the intruder has a reasonable amount of computational power, in particular when he is able, with a certain probability, to guess encryption keys or other particular kind of data such as the body of a hashed message. We also show that these extensions do not augment the computational complexity of the protocol insecurity problem in the case of a finite number of interleaved protocol sessions.     

基于树语言逼近的安全协议形式化分析

利用形式化方法或工具自动化分析实用安全协议十分必要,定理证明技术因其可解决无限状态系统的验证备受关注,但扩展其验证规模和自动化实现时仍然存在一些局限性。以定理证明和重写逼近理论为基础,以项重写形式化定义协议模型,以树自动机模拟协议攻击者知识集,给出攻击者知识集可达项逼近求解的算法,并根据上述模型讨论秘密性和认证性的验证方法,最后以Needham-Schroeder公钥认证协议为例验证模型的有效性,并指出下一步研究方向。     

基于攻击者行为能力的SVO协议分析

SVO原逻辑不适用于证明基于证书的认证与密钥交换协议安全性问题。为此,提出2个SVO逻辑相关公理,对证书真实性与会话密钥安全性进行判断及验证,并结合Dolev-Yao安全模型,从攻击者行为能力的角度评估密码协议的安全性。经分析证明Mangipudi协议未能提供前向安全且存在假冒攻击的安全缺陷,因此给出一个在Dolev-Yao安全模型下可证明安全的解决方案。     

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.     

基于Tamarin的MQTT协议安全性分析方法

MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一种基于Tamarin的MQTT协议安全性分析方法。该方法首先面向MQTT协议3.1.1标准,构建了协议状态机,并依据Tamarin语法规则,完成了形式化描述;然后针对保密属性和认证属性,给出了MQTT协议需要满足的安全属性引理描述;最后,基于Dolev-Yao威胁模型在Tamarin中完成了对47种协议安全属性的验证。结果显示有9种保密属性违反和29种认证属性违反,对结果进行攻击测试,验证了该方法对MQTT协议安全性分析的有效性,并提出了一种基于身份重认证的优化改进方案。