【作者】 杨元原；

【导师】 马文平；

【作者基本信息】 西安电子科技大学 ， 密码学， 2011， 博士

【摘要】 随着网络技术的迅速普及与发展,网络中敏感信息的保护已变得越来越重要。密码协议正是为通信的双方或多方提供这样的安全保证。然而,由于网络本身的开放性,其中存在着严重的安全威胁,攻击者可以通过各种方式对密码协议进行攻击,破坏其安全特性。因此,对密码协议进行安全性分析至关重要。本文按照密码协议不同的应用环境将其分为两种,一种是应用于传统计算机网络的密码协议,这种协议在设计时不必考虑密码原语的复杂度,仅以保证协议的安全性为目标,称为传统密码协议;另外一种是应用于RFID系统的密码协议,这种密码协议由于受到标签成本限制,在设计时必须采用结构简单、计算复杂度低的密码原语,并利用他们的代数性质进行代数运算和等式推导来实现协议的安全目标,称为轻量级协议。当前,对这两种协议的分析方法也有所不同:针对传统的密码协议,一般采用形式化方法。形式化方法具有严格、明确、清晰和反直觉等特点,因此是分析密码协议的有效工具,但由于其抽象化程度太高,不能分析带有代数运算和等式推导的协议,因此对于应用于RFID系统的轻量级协议,只能采用手工验证方法。本文对这两种方法都进行了研究,对于传统的密码协议,研究了基于SAT模型检测的方法,并对该方法进行了功能扩展;对于轻量级协议,采用手工验证方法,分析了两个优秀的轻量级协议的安全性,找到了两个独特的攻击。本文的主要研究成果如下:(1)提出了一个新的可以检测类型缺陷攻击的模型SAT-1。该模型通过在匹配模式中引入无类型变量,并通过无类型消息的概念,解除了原SAT模型检测器对未知消息的类型限制。同时,通过增加消息匹配算法,使诚实主体能够接受带有类型缺陷的消息,从而实现了类型缺陷攻击的检测。在对Otway-Rees协议的检测中,不仅发现了已有的针对发起者A的类型缺陷攻击,而且发现了新的针对响应者B的类型缺陷攻击,证明了SAT-1模型的可靠性。(2)针对当前模型检测工具普遍不能检测带有异或运算密码协议的问题,提出了一个新的模型SAT-2。该模型通过引入抽象异或项的概念及其运算规则,大大降低了攻击者生成的异或消息数量,解决了由于引入异或运算所导致的状态空间爆炸问题。在此基础上,通过在SAT模型中增加基于抽象异或项的重写规则,扩展了攻击者的异或运算能力,实现了对带有异或运算密码协议的自动化检测。最后通过对BULL协议的检测,证明了抽象异或项的实用性,同时也证明了SAT-2模型检测器的可靠性。(3)设计了一个多协议攻击自动化检测系统ADMA。该系统由协议搜索子系统和攻击确认子系统两部分组成。协议搜索子系统根据多协议攻击中目标协议与辅助协议加密消息类型一致性的条件,自动化搜索可能对目标协议构成威胁的候选辅助协议。攻击确认子系统通过改进的SAT模型检测方法,自动化确认目标协议与候选辅助协议是否存在多协议攻击。试验结果表明,ADMA系统能够实现多协议攻击的自动化检测,并且检测中发现了新的多协议攻击。(4)提出了一个可变攻击者模型构造方案CIM。该方案利用异或运算,阿贝尔加法群运算以及阿贝尔乘法群运算的代数性质,定义了抽象项的概念及其运算规则,大大降低了攻击者进行代数运算的复杂度。在此基础上,将攻击者所有的攻击行为转化为重写规则,并定义了攻击者行为库和攻击规则选择算法,使检测者能够根据不同的协议选择并组合不同的攻击行为,构造可变的攻击者模型。与传统固定的攻击者模型方案相比,该方案能够根据不同的协议动态调整攻击者模型,并且能够降低攻击者执行代数运算的复杂度,因此保证了协议分析的效率和准确性。(5)针对Lee等人提出的应用于RFID系统的身份传输协议,提出了一个独特的三会话攻击。在该三会话攻击中,攻击者利用第一个会话监听目标标签和阅读器之间传递的消息,然后利用第二个会话收集目标标签的响应信息,最后通过第三个会话发动中间人攻击并对目标标签进行追踪,破坏了协议的不可追踪性。与传统的两会话攻击相比,三会话攻击更难于发现并且对攻击者要求更高,因此对三会话攻击进行了可行性分析,指出了其攻击成功的条件。(6)发现了三个针对Kulseng等人提出的应用于RFID系统的互认证协议的攻击。在这三个攻击中,第一个攻击通过修改两个会话中标签发送给阅读器的消息,成功的对标签进行了追踪,实现了追踪攻击。利用这个攻击,攻击者可以判断出了两条消息是否为同一个标签发送,然后利用线型移位寄存器的弱点,计算出标签和阅读器之间共享的秘密,从而成功的破坏了协议的机密性。在获得了标签和阅读器共享的秘密之后,攻击者能够在后续的会话中,模仿阅读器或标签与真正的标签或阅读器进行通信,最终破坏协议的互认证性。更多还原

【Abstract】 With the rapid popularization and development of computer networks, the protection of sensitive information in the network is becoming increasingly important. Cryptographic protocols are the critical methods to provide the security guarantees for two or more communicating parties. Due to the openness of the computer networks, however, there are many serious security threats in the network. The attacker has the chances to launch all kinds of attacks, and may destroy the security properties of cryptographic protocols. Therefore, analyzing cryptographic protocols and verifying their safety are of paramount importance.In this dissertation, cryptographic protocols are divided into two types according to their different application environments. One type is used in traditional computer networks. These protocols are designed to guarantee the safety of the protocols, and do not have to take the computational complexity of cryptographic primitives into account. They are called traditional cryptographic protocols. The other type is used in RFID systems. Due to the cost limitation of RFID tags, the protocols used in RFID systems have to adopt simple and low computational complexity cryptographic primitives, whose algebraic properties are utilized to perform algebraic operations and equation deduction to implement security targets. Therefore, these protocols are called lightweight protocols. Currently, different methods are used to analyze these two types of protocols. For the traditional cryptographic protocols, the formal analysis methods are used. Formal analysis methods are strict, definite, clear and non-intuitive, which are very effective to analyze traditional cryptographic protocols. But it has a high abstraction degree on cryptographic primitives, and can not analyze cryptographic protocols with algebraic operations and equation deduction. Therefore, for lightweight protocols used in RFID systems, artificial verification methods are used. In this dissertation, both of these analysis methods are researched. For the traditional cryptographic protocols, a formal analysis method named SAT-based model checking is studied, and then its function is enhanced. For the lightweight protocols, aritificial verification methods are used, and two unique attacks on two exellent lightweight protocols are found. The contributions of the dissertation are outlined as follows:(1) A new model named SAT-1 is proposed to detect type-flaw attack. Through introducing non-type variables to match pattern and defining the concept of non-type messages, the new model relaxes the type restriction to unknown messages in original SAT model checker. Meanwhile, through adding messages match algorithm, SAT-1 enables the honest agents to accept type flaw messages. Therefore, the type flaw attack can be detected. The detection results of Otway-Rees protocol demonstrate the correctness of SAT-1. Moreover, not only the well-known type flaw attack on initiator A but also a new type flaw attack on responder B is found.(2) Since most of the current model checking tools can not detect cryptographic protocols with XOR, a new model named SAT-2 is proposed. By defining the concept of abstract XOR term and its reduction rules, the new model greatly reduces the number of XOR messages produced by the intruder, and resolves the state space explosion problem resulting from the introduction of XOR operations. On these bases, through adding the rewrite rules of XOR based on abstract XOR term, the new model endows the intruder with the XOR operations, and thus is able to automaticly detect the cryptographic protocols with XOR. The detection results of BULL protocol show not only the practicality of abstract XOR term but also the reliability of the SAT-2.(3) An automatic detection system for multi-protocol attack named ADMA is designed. This system is composed of two parts named protocol search subsystem and attack verification subsystem. According to the consistency condition of the type of encrypted messages between the target protocol and its secondary protocol, the protocol search subsystem is able to automatically search for the candidate secondary protocols, which may be used to attack the target protocol. After that, by improving the SAT-based model checking, attack verification subsystem can automatically verify whether multi-protocol attack exists between the target protocol and its candidate secondary protocols. The experiment results show that ADMA system is able to implement automatic detection for multi-protocol attack. Moreover, some new multi-protocol attacks have been found in the detection.(4) A construction scheme of changeable intruder model named CIM is proposed. Utilizing algebraic properties of XOR, additive abelian group and multiplicative abelian group, CIM defines the concept of abstract terms and their operation rules, which greatly reduces the complexity of algebraic operations for the intruder. On these bases, all the actions of the intruder are transformed to rewrite rules. Then the intruder action library, as well as the attack rule selection algorithm is defined, which enable the analyst to choose and combine different intruder actions according to different protocols to construct a changeable intruder model. Compared with traditionally fixed intruder model, CIM is able to dynamically adjust the constructed intruder models according to different protocols. Moreover, it is able to decrease the complexity for the intruder to execute algebraic operations, which ensures both efficiency and correctness of the protocol analysis.(5) A unique three-session attack on the ID-transfer protocol proposed by Lee et al. is described. In this three-session attack, the attacker utilizes the first session to monitor messages transmited between the reader and the target tag, and then utilizes the second one to collect the reponse of the target tag. Finally, the attacker makes use of the third one to launch a man-in-the-middle attack to trace the target tag, and thus breaks the untraceability of the protocol. Compared with the traditional two-session attack, the three-session attack is more difficult to find, and requires stronger abilities to the attacker. Thus the feasibility of the three-session attack is analyzed and the conditions of success for the attack are presented.(6) Three attacks on the mutual authentication protocol proposed by Kulseng et al. are presented. In these three attacks, the first one successfully traces the tag by modifying the messages that the tag sends to the reader in two sessions, and implements the tracing attack. Based on this attack, the attacker is able to decide whether two messages are sent by the same tag, and then utilizes the weakness of LFSR to compute the secrets shared between the tag and the reader. Therefore, the attacker successfully breaks the confidentiality of the protocol. After obtaining the shared secrets between the reader and the tag, the attacker is able to successfully impersonate the reader or the tag to communicate with the real tag or the real reder in the future sessions, which breaks the mutual authentication property of the protocol in the end.更多还原