Studies On Security Analysis Of Cryptographic Protocols

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.