密码协议的安全性分析技术研究
|
摘要
随着网络技术的迅速普及与发展,网络中敏感信息的保护已变得越来越重要。密码协议正是为通信的双方或多方提供这样的安全保证。然而,由于网络本身的开放性,其中存在着严重的安全威胁,攻击者可以通过各种方式对密码协议进行攻击,破坏其安全特性。因此,对密码协议进行安全性分析至关重要。
本文按照密码协议不同的应用环境将其分为两种,一种是应用于传统计算机网络的密码协议,这种协议在设计时不必考虑密码原语的复杂度,仅以保证协议的安全性为目标,称为传统密码协议;另外一种是应用于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系统的互认证协议的攻击。在这三个攻击中,第一个攻击通过修改两个会话中标签发送给阅读器的消息,成功的对标签进行了追踪,实现了追踪攻击。利用这个攻击,攻击者可以判断出了两条消息是否为同一个标签发送,然后利用线型移位寄存器的弱点,计算出标签和阅读器之间共享的秘密,从而成功的破坏了协议的机密性。在获得了标签和阅读器共享的秘密之后,攻击者能够在后续的会话中,模仿阅读器或标签与真正的标签或阅读器进行通信,最终破坏协议的互认证性。
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.
本文按照密码协议不同的应用环境将其分为两种,一种是应用于传统计算机网络的密码协议,这种协议在设计时不必考虑密码原语的复杂度,仅以保证协议的安全性为目标,称为传统密码协议;另外一种是应用于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系统的互认证协议的攻击。在这三个攻击中,第一个攻击通过修改两个会话中标签发送给阅读器的消息,成功的对标签进行了追踪,实现了追踪攻击。利用这个攻击,攻击者可以判断出了两条消息是否为同一个标签发送,然后利用线型移位寄存器的弱点,计算出标签和阅读器之间共享的秘密,从而成功的破坏了协议的机密性。在获得了标签和阅读器共享的秘密之后,攻击者能够在后续的会话中,模仿阅读器或标签与真正的标签或阅读器进行通信,最终破坏协议的互认证性。
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.
引文
[1]杨波.现代密码学.北京:清华大学出版社, 2004.
[2] A. Menezes, P. Oorschot and S. Vanstone. Handbook of Applied Cryptography. Boca Raton: CRC. 1996.
[3]卢开澄.计算机密码学-计算机网络中的数据保密与安全(第3版).北京:清华大学出版社, 2003.
[4]王育民,刘建伟.通信网的安全理论与技术.西安:西安电子科技大学出版社, 2002.
[5]王亚弟,束妮娜,韩继红等.密码协议形式化分析.北京:机械工业出版社, 2006.
[6] Bruce Schneier著,吴世忠等译.应用密码学.北京:机械工业出版社, 2000.
[7]卿斯汉.安全协议.北京:清华大学出版社,2005.
[8] R. Want. An introduction to RFID technology. IEEE Pervasive Computing, 2006, 5(1): 25-33.
[9] C.M. Roberts. Radio frequency identification. Computer and Security, 2006, 25(1): 18-26.
[10]范红,冯登国.安全协议理论与方法.北京:科学出版社,2003.
[11] C. Boyd and A. Mathuria. Protocols for Authentication and Key Establishment. Berlin: Springer, 2003.
[12]钟诚.电子商务安全.重庆:重庆大学出版社, 2004.
[13] A. Juels, R. L. Rivest and M. Szydlo. The blocker tag: Selective blocking of RFID tags for consumer privacy. 8th ACM Conference on Computer and communications Security. Pennsylvania: ACM Press, 2003, pp. 103-111.
[14] A. Juels. RFID security and privacy: a research survey. IEEE Journal on Selected Areas in Communications. 2006, 24(2): 381-394.
[15] S. L. Garfinkel, A. Juels and R. Pappu. RFID privacy, an overview of problems and proposed solutions. IEEE Security and Privacy. 2005, 3(3): 34-43.
[16] I. Vajda and L. Buttyan. Lightweight authentication protocols for low-cost RFID tags. The Second Workshop on Security in Ubiquitous Computing. Washington: ACM Press, 2003, pp. 1-10.
[17] M. Feldhofer, S. Dominikus and J. Wolkerstorfer. Strong authentication for RFID systems using the AES algorithm. Cryptographic Hardware and Embedded Systems 2004. Boston: Springer, 2004, pp. 357-370.
[18] D. Henrici and P. Muller. Hash-based enhancement of location privacy for radio-frequency identification devices using varying identifiers. The Second IEEE Annual Conference on Pervasive Computing and Communications Workshops. Florida: IEEE Computer Society, 2004, pp. 149-153.
[19] G. P. Hancke and M. G. Kuhn. An RFID distance bounding protocol. The First International Conference on Security and Privacy for Emerging Areas in Communications networks. Athens: IEEE Computer Society, 2005, pp. 67-73.
[20] D. Molnar, A. Soppera and D. Wagner. A scalable delegatable pseudonym protocol enabling ownership transfer of RFID tags. Selected Areas in Cryptography 2005. New Mexico: Springer, 2005, pp. 276-290.
[21] E. Y. Choi, S. M. Lee, and D. H. Lee. Efficient RFID authentication protocol for ubiquitous computing environment. International Workshop on Security in Ubiquitous Computing Systems. Nagasaki: Springer, 2005, pp. 945-954.
[22] G. Avoine and P. Oechslin. A scalable and provably secure hash-based RFID protocol. The Third IEEE International Conference on Pervasive Computing and Communication Workshops. Hawaii: IEEE Computer Society, 2005, pp. 110-114.
[23] T. Dimitriou. A lightweight RFID protocol to protect against traceability and cloing attacks. The First International Conference on Security and Privacy for Emerging Areas in Communications Networks. Athens: IEEE Computer Society, 2005, pp. 59-66.
[24] H. Y. Chien and C. W. Huang. A lightweight RFID protocol using substring. Proceeding of the 2007 International Conference on Embedded and Ubiquitous Computing. Taipei: Springer, 2007, pp. 422-431.
[25] R. D. Pietro and R. Molva. Information confinement privacy and security in RFID systems. The 12th European Symposium on Research in Computer Security. Dresden: Springer, 2007, pp. 187-202.
[26] B. Song and C. J. Mitchell. RFID authentication protocol for low-cost tags. The First ACM Conference on Wireless Network Security. New York: ACM Press, 2008, pp. 140-147.
[27] H. Y. Chien. SASI: A new ultralightweight RFID authentication protocol providing strong authentication and strong integrity. IEEE Transactions on Dependable and Secure Computing. 2007, 4(4): 337-340.
[28] Y. K. Lee, L. Batina, and I. Verbauwhede. Untraceable RFID authentication protocols: Revision of EC-RAC. IEEE International Conference on RFID. Orlando: IEEE Computer Society, 2009, pp. 178-185.
[29] Y. K. Lee, L. Batina, D. Singele, and I. Verbauwhede. Low-cost Untraceable authentication protocols for RFID systems. Proceeding of 3rd ACM Conference on Wireless Network Security. New Jersey: ACM Press, 2010, pp. 55-64.
[30] L. Kulseng, Z. Yu, Y. Wei, and Y. Guan. Lightweight mutual authentication and ownership transfer for RFID systems. Proceeding of 29th Conference on Computer Communication. San Diego: IEEE Computer Society, 2010, pp. 1-5.
[31]薛锐,冯登国.安全协议的形式化分析方法.计算机学报. 2006, 29(1): 1-20.
[32] M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Transactions on Computer System. 1990, 8(1): 18-36.
[33] R. Needham and M. Schroeder. Using Encryption for authentication in large networks of computers. Communications of the ACM. 1978, 21(12): 393-399.
[34] MIT Kerberos Team. Kerberos: the network authentication protocol.
[35] L. Gong, R. Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. Proceeding of the 1990 IEEE Symposium on Research in Security and Privacy. California: IEEE Computer Society, 1990, pp. 234-148.
[36] M. Abadi, M. Tuttle. A semantics for a logic of authentication. Proceeding of the 10th Annual ACM Symposium on Principles of Distributed Computing. New York: ACM Press, 1991, pp. 201-216.
[37] P. C. van Oorschot. Extending cryptographic logics of belief to key agreement protocols. Proceeding of the First ACM Conference on Computer and Communications Security. Virginia: ACM Press, 1993, pp. 232-243.
[38] P. F. Syverson, P. C. van Oorschot. On unifying some cryptographic protocol logics. Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society, 1994, pp. 109-121.
[39] W. B. Mao and C. Boyd. Towards a formal analysis of security protocols. Proceedings of the Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society, 1991, pp. 147-158.
[40] V. Kessler and G. Wedel. AUTLOG-an advanced logic of authentication. Proceedings of Computer Security Foundations Workshop. Franconia: IEEE Computer Society, 1994, pp. 90-99.
[41] C. Boyd and W. B. Mao. On a limitation of BAN logic. Workshop on the Theory and Application of Cryptographic Techniques on Advances in Cryptology. Lofthus: Springer, 1993, pp. 240-247.
[42] R. Kailar. Accountability in electronic commerce protocols. IEEE Transactions onSoftware Engineering. 1996, 22(5): 18-36.
[43]周典萃,卿斯汉,周展飞. Kailar逻辑的缺陷.软件学报. 1999, 10(12): 1-11.
[44] C. Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming. 1996, 26(19): 113-131.
[45] G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Tools and Algorithms for the Construction and analysis of Systems. Passau: Springer, 1996, pp. 147-166.
[46] D. X. Song. Athena: a new efficient automatic checker for security protocol analysis. Proceedings of the 12th IEEE Computer Security Foundations Workshop. Mordano: IEEE Computer Society, 1999, pp. 28-30.
[47] A. Armando, D. Basin, and Y. Boichut et al. The AVISPA tool for the automated validation of internet seuciryt protocols and applications. 17th International Conference on Computer Aided Verification. Scotland: Springer, 2005, pp. 281-285.
[48] D. Basin, S. Modersheim, and L. vigano. OFMC: a symbolic model checker for security protocols. International Journal of Information Security. 2005, 4(3): 181-208.
[49] D. Basin, S. Modersheim, and L. Vigano. Constraint Differentiation: a new reduction technique for constraint-based analysis of security protocols. Proceedings of 10th ACM Conference on Computer and Communications Security. Washington: ACM Press, 2003, pp. 335-344.
[50] A. Armando and L. Compagna. SAT-based model-checking for security protocols analysis. International Journal of Information Security. 2008, 7(1): 3-32.
[51] D. Monniaux. Abstracting cryptographic protocols with tree automata. Science of Computer Programming. 2003, 47(2-3): 177-202.
[52] B. Blanchet. Proverif: Cryptographic protocol verifier in the formal model. http://www.proverif.ens.fr/
[53] E. M. Clarke, S. Jha, and W. Marrero. Verifying security protocols with Brutus. ACM Transctions on Software Engineering and Methodology. 2000, 9(4): 443-487.
[54] C. Cremer. The scyther tool: verification, falsification, and analysis of security protocols. 20th International Conference on Computer Aided Verification. Princeton: Springer, 2008, pp. 414-418.
[55] R. A. Kemmerer. Using formal verification technique to analyze encryption protocols. 1987 IEEE Symposium on Security and Privacy. Oakland: IEEEComputer Society, 1987, pp. 134-144.
[56] L. C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security. 1998, 6(1-2): 85-128.
[57] L. C. Paulson. Isabella. http://www.cl.cam.ac.uk/research/hvg/Isabelle/
[58] G. Bella. Modelling agent’s knowledge inductively. 7th International Workshop on Security Protocols. Cambridge: Springer, 1999, pp. 85-94.
[59] B. Blanchet. An efficient cryptographic protocol by prolog rules. 14th IEEE Computer Security Foundations Workshop. Nova: IEEE Computer Society, 2001, pp. 82-96.
[60] F. Thayer, J. C. Herzog, and J. D. Guttman. Strand space: proving security protocols correct. Journal of Computer Security, 1999, 7(2): 191-230.
[61]周宏斌,黄连生,桑田.基于串空间的安全协议形式化验证模型及算法.计算机研究与发展. 2003, 40(2): 252-257.
[62] M. O. Stehr. The open calculus of constructions: an equational type theory with dependent types for programming, specification, and interactive theorem proving. Fundamenta Informaticae. 2005, 68(1-2): 1-96.
[63] L. Cervesato and M. O. Stehr. Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types. Electronic Notes in Theoretical Computer Science. 2005, 11(20): 183-207.
[64] Dolev D, Yao A. On the security of public-key protocols[J]. IEEE Trans. on Information Theory, 1983, 29(2):198?208.
[65] T. van Deursen. Attacks on RFID protocols. Cryptology ePrint Archive 2008/310, 2008, pp. 1-56.
[66] P. Rizomiliotis, E. Rekleitis, and S. Gritzalis. Security analysis of the Song-Mitchell authentication protocol for low-cost RFID tags. IEEE Communications Letters. 2009, 13(4): 274-276.
[67] T. J. Cao, E. Bertino, and H. Lei. Security analysis of the SASI protocol. IEEE transactions on dependable and secure computing. 2009, 6(1): 73-77.
[68] P. Peris-Lopez, J. C. Hernadez-Castro, J. M. E. Tapiador et al. Vulnerability analysis of RFID protocols for tag ownership transfer. Computer Networks. 2010, 54(9): 1502-1508.
[69] G. Avoine. Adversary model for radio frequency identification. Technical Report LASEC-REPORT-2005-001, Swiss Federal Institute of Technology, Security and Cryptography Laboratory, Switzerland, 2009.
[70] J. C. Ha, S. J. Moon, J. M. G. Nieto, and C. Boyd. Security analysis andenhancement of one-way hash based low-cost authentication protocol. The 11th Pacific-Asia Conference on Knowledge Discovery and Data Mining. Nanjing: Springer, 2007, pp. 574-583.
[71] B. Defend, K. Fu,and A. Juels. Cryptanalysis of two lightweight RFID authentication schemes. Proceedings of the Fifth IEEE International Conference on Pervasive Computing and Communications Workshops. New York: IEEE Computer Society, 2007, pp. 211-126.
[72] Terese. Term rewrting systems. Cambridge: Cambridge University Press, 2003.
[73] L. Compagna. SAT-based model-checking of security protocols. PhD Thesis, University of Edinburgh, Sep. 2005.
[74] J. Hendler, A. Tate, and M. Drummond. AI planning: systems and techniques. AI Magazine. 1990, 11(2): 61-77.
[75] M. R. Garey and D. S. Johnson. Computers and intractability: a guide to the theory of NP-completeness. San Francisco: W. H. Freeman, 1990.
[76] D. Martin and P. Hillary. A computing procedure for quantification theory. Journal of the ACM. 1960, 7(3): 201-215.
[77] M. Davis, G. Logeman, and D. Loveland. A machine program for theorem proving. Communications of the ACM. 1962, 5(7): 394-397.
[78] H. Kautz, H. McAllester, and B. Selman. Encoding plans in propositional logic. Proceedings of the Fifth International Conference on the Principle of Knowledge Representation and Reasoning. Cambridge: Morgan Kaufmann, 1996, pp. 374-384.
[79] M. D. Ernst, T. D. Millstein, and D. S. Weld. Automatic SAT-compilation of planning problem. Proceedings of the 15th International Joint Conference on Artificial Intelligence. Aichi: Morgan Kaufmann, 1997, pp. 1169-1177.
[80] Marques-Silva, J. P. and Sakallah, K. A. GRASP-A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers.1999, 48 (5): 506-521.
[81] H. T. Zhang. SATO: an efficient prepositional prover. The 14th International Conference on Automated Deduction. North Queensland: Springer, 1997, 272-275.
[82] M. W. Moskewicz, C. F. Madigan, and Y. Zhao et al. Chaff: engineering an efficient SAT solver. The 38th Conference on Design Automation. Nevada: IEEE Computer Society, 2001, pp. 530-535.
[83] L. C. Paulson著,柯韦译. ML程序设计教程.北京:机械工业出版社, 2005.
[84] J. Heather, G. Lowe, and S. Schneider. How to prevent type flaw attacks on security protocols. Journal of Computer Security. 2003, 11(2): 217-244.
[85] J. Wang, J. W. Zhang, and H. G. Zhang. Type Flaw Attacks and Prevention in Security Protocols. The Ninth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing. Thailand: IEEE Computer Society, 2008, pp. 340-343.
[86] P. Ceelen, S. Mauw, and S. Radomirovi?. Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks. Electronic Notes in Theoretical Computer Science. 2008, 197(2): 31-43.
[87] C. Meadows, P. Syverson, and L. Cervesato. Formal specification and analysis of the group domain of interpretation protocol using NPATRL and the NRL protocol analyzer. Journal of Computer Security. 2004, 12(6): 893-931.
[88] H. Gao, C. Bodei, and P. Degano. A formal analysis of complex type flaw attacks on security protocols. Proceedings of the 12th international conference on Algebraic Methodology and Software Technology. Urbana: Springer, 2008, pp. 167-183.
[89] D.Otway and O.Rees. Efficient and timely mutual authentication. ACM SIGOPS Operating Systems Review, 1987, 21(1): 8-10.
[90] S. Delaune, P. Lafourcade, D. Lugiez, and R. Treinen. Symbolic protocol analysis for monoidal equational theories. Information and Computation. 2008, 206(2-4): 312-351.
[91] B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming. 2008, 75(1): 3-51.
[92] M. Baudet, V. Cortier, and S. Kremer. Computationally sound implementations of equational theories against passive adversaries. Information and Computation. 2009, 207(4): 496-520.
[93] Y. Chevalier, R. Küsters, and M. Rusinowitch et al. An NP decision procedure for protocol insecurity with XOR. Theoretical Computer Science. 2005, 338(1-3): 247-274.
[94] R. Küsters and T. Truderung. On the automatic analysis of recursive security protocols with XOR. The 24th Annual Symposium on Theoretical Aspects of Computer Science. Aachen: Springer, 2007. pp. 646-657.
[95] V. Cortier, G. Keighren, and G. Steel. Automatic analysis of the security of XOR-based key management schemes. The 13th International Conference onTools and Algorithms for the Construction and Analysis of Systems. Braga: Springer, 2007, pp. 538-552.
[96] R. Küsters and T. Truderung. Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. 15th ACM Conference on Computer and Communications Security. Alexandria: ACM, 2008, pp. 129-138.
[97] G. Bella. What is correctness of security protocols? Springer Journal of Universal Computer Science. 2008, 14(12): 2083-2107.
[98] P. Khoury, M. Hacid, and S. K. Sinha et al. A study on recent trends on integration of security mechanisms. Studies in Computational Intelligence. 2009, 223: 203-224.
[99] C. Cremers. Feasibility of multi-protocol attacks. The first International Conference on Availability, Reliability and Security. Vienna: IEEE Computer Society, 2006, pp. 287-294.
[100] A. Mathuria, A. R. Singh, and P. Sharavan et.al. Some new multi-protocol attacks. 15th International Conference on Advanced Computing and Communications. Guwahati: IEEE Computer Society, 2007, pp. 465-471.
[101] S. Andova, C. Cremers, and K. Gj?steen et al. A framework for compositional verification of security protocols. Information and Computation. 2008, 206 (2-4): 425-459.
[102] Security Protocols Open Repository. http://www.lsv.ens-cachan.fr/ Software /spore/table.html
[103] Y. Boichut, P. Héam, and O. Kouchnarenko. Tree automata for detecting attacks on protocols with algebraic cryptographic primitives. Electronic Notes in Theoretical Computer Science. 2009, (239): 57-72.
[104] B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming. 2008, 75(1): 3-51.
[105] V. Cortier, S. Delaune, and P. Lafourcade. A survey of algebraic properties used in cryptographic protocols. Journal of computer security. 2006.14(No.1):1-43.
[106] S. Bursuc and H. Comon-Lundh. Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions. The 20th International Conference on Rewriting Techniques and Applications. Brasília: Springer, 2009, pp. 133-147.
[107] M. Baudet, V. Cortier, and S. Kremer. Computationally sound implementations of equational theories against passive adversaries. Information and Computation.2009, 207(4): 496-520.
[108] D. Basin, S. M?dersheim, and L. Viganò. Algebraic Intruder Deductions. The 12th International Conference on Logic for programming, artificial intelligence, and reasoning. Montego Bay: Springer, 2005, pp. 549-564.
[109] T.Deursen and S.Radomirovic. Untraceable RFID protocols are not trivially composable: Attacks on the revision of EC-RAC. Cryptology ePrint Archive 2009/332, July 2009.
[110] G. E. Suh and S. Devadas. Physical unclonable functions for device authentication and secret key generation. Proceedings of the 44th annual Design Automation Conference. San Diego: IEEE Computer Society, 2007, pp. 9-14.
[111] A. J. Menezes, P. C. van Oorschot, and S. A. Vanstone. Handbook of Applied Cryptography. Boca Raton: CRC Press, 1996.
[112] S. Vaudenay. On privacy models for RFID. The 13th Annual International Conference on the Theory and Application Cryptology and Information Security. Sarawak: Springer, 2007, pp. 68-87.
[2] A. Menezes, P. Oorschot and S. Vanstone. Handbook of Applied Cryptography. Boca Raton: CRC. 1996.
[3]卢开澄.计算机密码学-计算机网络中的数据保密与安全(第3版).北京:清华大学出版社, 2003.
[4]王育民,刘建伟.通信网的安全理论与技术.西安:西安电子科技大学出版社, 2002.
[5]王亚弟,束妮娜,韩继红等.密码协议形式化分析.北京:机械工业出版社, 2006.
[6] Bruce Schneier著,吴世忠等译.应用密码学.北京:机械工业出版社, 2000.
[7]卿斯汉.安全协议.北京:清华大学出版社,2005.
[8] R. Want. An introduction to RFID technology. IEEE Pervasive Computing, 2006, 5(1): 25-33.
[9] C.M. Roberts. Radio frequency identification. Computer and Security, 2006, 25(1): 18-26.
[10]范红,冯登国.安全协议理论与方法.北京:科学出版社,2003.
[11] C. Boyd and A. Mathuria. Protocols for Authentication and Key Establishment. Berlin: Springer, 2003.
[12]钟诚.电子商务安全.重庆:重庆大学出版社, 2004.
[13] A. Juels, R. L. Rivest and M. Szydlo. The blocker tag: Selective blocking of RFID tags for consumer privacy. 8th ACM Conference on Computer and communications Security. Pennsylvania: ACM Press, 2003, pp. 103-111.
[14] A. Juels. RFID security and privacy: a research survey. IEEE Journal on Selected Areas in Communications. 2006, 24(2): 381-394.
[15] S. L. Garfinkel, A. Juels and R. Pappu. RFID privacy, an overview of problems and proposed solutions. IEEE Security and Privacy. 2005, 3(3): 34-43.
[16] I. Vajda and L. Buttyan. Lightweight authentication protocols for low-cost RFID tags. The Second Workshop on Security in Ubiquitous Computing. Washington: ACM Press, 2003, pp. 1-10.
[17] M. Feldhofer, S. Dominikus and J. Wolkerstorfer. Strong authentication for RFID systems using the AES algorithm. Cryptographic Hardware and Embedded Systems 2004. Boston: Springer, 2004, pp. 357-370.
[18] D. Henrici and P. Muller. Hash-based enhancement of location privacy for radio-frequency identification devices using varying identifiers. The Second IEEE Annual Conference on Pervasive Computing and Communications Workshops. Florida: IEEE Computer Society, 2004, pp. 149-153.
[19] G. P. Hancke and M. G. Kuhn. An RFID distance bounding protocol. The First International Conference on Security and Privacy for Emerging Areas in Communications networks. Athens: IEEE Computer Society, 2005, pp. 67-73.
[20] D. Molnar, A. Soppera and D. Wagner. A scalable delegatable pseudonym protocol enabling ownership transfer of RFID tags. Selected Areas in Cryptography 2005. New Mexico: Springer, 2005, pp. 276-290.
[21] E. Y. Choi, S. M. Lee, and D. H. Lee. Efficient RFID authentication protocol for ubiquitous computing environment. International Workshop on Security in Ubiquitous Computing Systems. Nagasaki: Springer, 2005, pp. 945-954.
[22] G. Avoine and P. Oechslin. A scalable and provably secure hash-based RFID protocol. The Third IEEE International Conference on Pervasive Computing and Communication Workshops. Hawaii: IEEE Computer Society, 2005, pp. 110-114.
[23] T. Dimitriou. A lightweight RFID protocol to protect against traceability and cloing attacks. The First International Conference on Security and Privacy for Emerging Areas in Communications Networks. Athens: IEEE Computer Society, 2005, pp. 59-66.
[24] H. Y. Chien and C. W. Huang. A lightweight RFID protocol using substring. Proceeding of the 2007 International Conference on Embedded and Ubiquitous Computing. Taipei: Springer, 2007, pp. 422-431.
[25] R. D. Pietro and R. Molva. Information confinement privacy and security in RFID systems. The 12th European Symposium on Research in Computer Security. Dresden: Springer, 2007, pp. 187-202.
[26] B. Song and C. J. Mitchell. RFID authentication protocol for low-cost tags. The First ACM Conference on Wireless Network Security. New York: ACM Press, 2008, pp. 140-147.
[27] H. Y. Chien. SASI: A new ultralightweight RFID authentication protocol providing strong authentication and strong integrity. IEEE Transactions on Dependable and Secure Computing. 2007, 4(4): 337-340.
[28] Y. K. Lee, L. Batina, and I. Verbauwhede. Untraceable RFID authentication protocols: Revision of EC-RAC. IEEE International Conference on RFID. Orlando: IEEE Computer Society, 2009, pp. 178-185.
[29] Y. K. Lee, L. Batina, D. Singele, and I. Verbauwhede. Low-cost Untraceable authentication protocols for RFID systems. Proceeding of 3rd ACM Conference on Wireless Network Security. New Jersey: ACM Press, 2010, pp. 55-64.
[30] L. Kulseng, Z. Yu, Y. Wei, and Y. Guan. Lightweight mutual authentication and ownership transfer for RFID systems. Proceeding of 29th Conference on Computer Communication. San Diego: IEEE Computer Society, 2010, pp. 1-5.
[31]薛锐,冯登国.安全协议的形式化分析方法.计算机学报. 2006, 29(1): 1-20.
[32] M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Transactions on Computer System. 1990, 8(1): 18-36.
[33] R. Needham and M. Schroeder. Using Encryption for authentication in large networks of computers. Communications of the ACM. 1978, 21(12): 393-399.
[34] MIT Kerberos Team. Kerberos: the network authentication protocol.
[35] L. Gong, R. Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. Proceeding of the 1990 IEEE Symposium on Research in Security and Privacy. California: IEEE Computer Society, 1990, pp. 234-148.
[36] M. Abadi, M. Tuttle. A semantics for a logic of authentication. Proceeding of the 10th Annual ACM Symposium on Principles of Distributed Computing. New York: ACM Press, 1991, pp. 201-216.
[37] P. C. van Oorschot. Extending cryptographic logics of belief to key agreement protocols. Proceeding of the First ACM Conference on Computer and Communications Security. Virginia: ACM Press, 1993, pp. 232-243.
[38] P. F. Syverson, P. C. van Oorschot. On unifying some cryptographic protocol logics. Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society, 1994, pp. 109-121.
[39] W. B. Mao and C. Boyd. Towards a formal analysis of security protocols. Proceedings of the Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society, 1991, pp. 147-158.
[40] V. Kessler and G. Wedel. AUTLOG-an advanced logic of authentication. Proceedings of Computer Security Foundations Workshop. Franconia: IEEE Computer Society, 1994, pp. 90-99.
[41] C. Boyd and W. B. Mao. On a limitation of BAN logic. Workshop on the Theory and Application of Cryptographic Techniques on Advances in Cryptology. Lofthus: Springer, 1993, pp. 240-247.
[42] R. Kailar. Accountability in electronic commerce protocols. IEEE Transactions onSoftware Engineering. 1996, 22(5): 18-36.
[43]周典萃,卿斯汉,周展飞. Kailar逻辑的缺陷.软件学报. 1999, 10(12): 1-11.
[44] C. Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming. 1996, 26(19): 113-131.
[45] G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Tools and Algorithms for the Construction and analysis of Systems. Passau: Springer, 1996, pp. 147-166.
[46] D. X. Song. Athena: a new efficient automatic checker for security protocol analysis. Proceedings of the 12th IEEE Computer Security Foundations Workshop. Mordano: IEEE Computer Society, 1999, pp. 28-30.
[47] A. Armando, D. Basin, and Y. Boichut et al. The AVISPA tool for the automated validation of internet seuciryt protocols and applications. 17th International Conference on Computer Aided Verification. Scotland: Springer, 2005, pp. 281-285.
[48] D. Basin, S. Modersheim, and L. vigano. OFMC: a symbolic model checker for security protocols. International Journal of Information Security. 2005, 4(3): 181-208.
[49] D. Basin, S. Modersheim, and L. Vigano. Constraint Differentiation: a new reduction technique for constraint-based analysis of security protocols. Proceedings of 10th ACM Conference on Computer and Communications Security. Washington: ACM Press, 2003, pp. 335-344.
[50] A. Armando and L. Compagna. SAT-based model-checking for security protocols analysis. International Journal of Information Security. 2008, 7(1): 3-32.
[51] D. Monniaux. Abstracting cryptographic protocols with tree automata. Science of Computer Programming. 2003, 47(2-3): 177-202.
[52] B. Blanchet. Proverif: Cryptographic protocol verifier in the formal model. http://www.proverif.ens.fr/
[53] E. M. Clarke, S. Jha, and W. Marrero. Verifying security protocols with Brutus. ACM Transctions on Software Engineering and Methodology. 2000, 9(4): 443-487.
[54] C. Cremer. The scyther tool: verification, falsification, and analysis of security protocols. 20th International Conference on Computer Aided Verification. Princeton: Springer, 2008, pp. 414-418.
[55] R. A. Kemmerer. Using formal verification technique to analyze encryption protocols. 1987 IEEE Symposium on Security and Privacy. Oakland: IEEEComputer Society, 1987, pp. 134-144.
[56] L. C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security. 1998, 6(1-2): 85-128.
[57] L. C. Paulson. Isabella. http://www.cl.cam.ac.uk/research/hvg/Isabelle/
[58] G. Bella. Modelling agent’s knowledge inductively. 7th International Workshop on Security Protocols. Cambridge: Springer, 1999, pp. 85-94.
[59] B. Blanchet. An efficient cryptographic protocol by prolog rules. 14th IEEE Computer Security Foundations Workshop. Nova: IEEE Computer Society, 2001, pp. 82-96.
[60] F. Thayer, J. C. Herzog, and J. D. Guttman. Strand space: proving security protocols correct. Journal of Computer Security, 1999, 7(2): 191-230.
[61]周宏斌,黄连生,桑田.基于串空间的安全协议形式化验证模型及算法.计算机研究与发展. 2003, 40(2): 252-257.
[62] M. O. Stehr. The open calculus of constructions: an equational type theory with dependent types for programming, specification, and interactive theorem proving. Fundamenta Informaticae. 2005, 68(1-2): 1-96.
[63] L. Cervesato and M. O. Stehr. Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types. Electronic Notes in Theoretical Computer Science. 2005, 11(20): 183-207.
[64] Dolev D, Yao A. On the security of public-key protocols[J]. IEEE Trans. on Information Theory, 1983, 29(2):198?208.
[65] T. van Deursen. Attacks on RFID protocols. Cryptology ePrint Archive 2008/310, 2008, pp. 1-56.
[66] P. Rizomiliotis, E. Rekleitis, and S. Gritzalis. Security analysis of the Song-Mitchell authentication protocol for low-cost RFID tags. IEEE Communications Letters. 2009, 13(4): 274-276.
[67] T. J. Cao, E. Bertino, and H. Lei. Security analysis of the SASI protocol. IEEE transactions on dependable and secure computing. 2009, 6(1): 73-77.
[68] P. Peris-Lopez, J. C. Hernadez-Castro, J. M. E. Tapiador et al. Vulnerability analysis of RFID protocols for tag ownership transfer. Computer Networks. 2010, 54(9): 1502-1508.
[69] G. Avoine. Adversary model for radio frequency identification. Technical Report LASEC-REPORT-2005-001, Swiss Federal Institute of Technology, Security and Cryptography Laboratory, Switzerland, 2009.
[70] J. C. Ha, S. J. Moon, J. M. G. Nieto, and C. Boyd. Security analysis andenhancement of one-way hash based low-cost authentication protocol. The 11th Pacific-Asia Conference on Knowledge Discovery and Data Mining. Nanjing: Springer, 2007, pp. 574-583.
[71] B. Defend, K. Fu,and A. Juels. Cryptanalysis of two lightweight RFID authentication schemes. Proceedings of the Fifth IEEE International Conference on Pervasive Computing and Communications Workshops. New York: IEEE Computer Society, 2007, pp. 211-126.
[72] Terese. Term rewrting systems. Cambridge: Cambridge University Press, 2003.
[73] L. Compagna. SAT-based model-checking of security protocols. PhD Thesis, University of Edinburgh, Sep. 2005.
[74] J. Hendler, A. Tate, and M. Drummond. AI planning: systems and techniques. AI Magazine. 1990, 11(2): 61-77.
[75] M. R. Garey and D. S. Johnson. Computers and intractability: a guide to the theory of NP-completeness. San Francisco: W. H. Freeman, 1990.
[76] D. Martin and P. Hillary. A computing procedure for quantification theory. Journal of the ACM. 1960, 7(3): 201-215.
[77] M. Davis, G. Logeman, and D. Loveland. A machine program for theorem proving. Communications of the ACM. 1962, 5(7): 394-397.
[78] H. Kautz, H. McAllester, and B. Selman. Encoding plans in propositional logic. Proceedings of the Fifth International Conference on the Principle of Knowledge Representation and Reasoning. Cambridge: Morgan Kaufmann, 1996, pp. 374-384.
[79] M. D. Ernst, T. D. Millstein, and D. S. Weld. Automatic SAT-compilation of planning problem. Proceedings of the 15th International Joint Conference on Artificial Intelligence. Aichi: Morgan Kaufmann, 1997, pp. 1169-1177.
[80] Marques-Silva, J. P. and Sakallah, K. A. GRASP-A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers.1999, 48 (5): 506-521.
[81] H. T. Zhang. SATO: an efficient prepositional prover. The 14th International Conference on Automated Deduction. North Queensland: Springer, 1997, 272-275.
[82] M. W. Moskewicz, C. F. Madigan, and Y. Zhao et al. Chaff: engineering an efficient SAT solver. The 38th Conference on Design Automation. Nevada: IEEE Computer Society, 2001, pp. 530-535.
[83] L. C. Paulson著,柯韦译. ML程序设计教程.北京:机械工业出版社, 2005.
[84] J. Heather, G. Lowe, and S. Schneider. How to prevent type flaw attacks on security protocols. Journal of Computer Security. 2003, 11(2): 217-244.
[85] J. Wang, J. W. Zhang, and H. G. Zhang. Type Flaw Attacks and Prevention in Security Protocols. The Ninth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing. Thailand: IEEE Computer Society, 2008, pp. 340-343.
[86] P. Ceelen, S. Mauw, and S. Radomirovi?. Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks. Electronic Notes in Theoretical Computer Science. 2008, 197(2): 31-43.
[87] C. Meadows, P. Syverson, and L. Cervesato. Formal specification and analysis of the group domain of interpretation protocol using NPATRL and the NRL protocol analyzer. Journal of Computer Security. 2004, 12(6): 893-931.
[88] H. Gao, C. Bodei, and P. Degano. A formal analysis of complex type flaw attacks on security protocols. Proceedings of the 12th international conference on Algebraic Methodology and Software Technology. Urbana: Springer, 2008, pp. 167-183.
[89] D.Otway and O.Rees. Efficient and timely mutual authentication. ACM SIGOPS Operating Systems Review, 1987, 21(1): 8-10.
[90] S. Delaune, P. Lafourcade, D. Lugiez, and R. Treinen. Symbolic protocol analysis for monoidal equational theories. Information and Computation. 2008, 206(2-4): 312-351.
[91] B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming. 2008, 75(1): 3-51.
[92] M. Baudet, V. Cortier, and S. Kremer. Computationally sound implementations of equational theories against passive adversaries. Information and Computation. 2009, 207(4): 496-520.
[93] Y. Chevalier, R. Küsters, and M. Rusinowitch et al. An NP decision procedure for protocol insecurity with XOR. Theoretical Computer Science. 2005, 338(1-3): 247-274.
[94] R. Küsters and T. Truderung. On the automatic analysis of recursive security protocols with XOR. The 24th Annual Symposium on Theoretical Aspects of Computer Science. Aachen: Springer, 2007. pp. 646-657.
[95] V. Cortier, G. Keighren, and G. Steel. Automatic analysis of the security of XOR-based key management schemes. The 13th International Conference onTools and Algorithms for the Construction and Analysis of Systems. Braga: Springer, 2007, pp. 538-552.
[96] R. Küsters and T. Truderung. Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. 15th ACM Conference on Computer and Communications Security. Alexandria: ACM, 2008, pp. 129-138.
[97] G. Bella. What is correctness of security protocols? Springer Journal of Universal Computer Science. 2008, 14(12): 2083-2107.
[98] P. Khoury, M. Hacid, and S. K. Sinha et al. A study on recent trends on integration of security mechanisms. Studies in Computational Intelligence. 2009, 223: 203-224.
[99] C. Cremers. Feasibility of multi-protocol attacks. The first International Conference on Availability, Reliability and Security. Vienna: IEEE Computer Society, 2006, pp. 287-294.
[100] A. Mathuria, A. R. Singh, and P. Sharavan et.al. Some new multi-protocol attacks. 15th International Conference on Advanced Computing and Communications. Guwahati: IEEE Computer Society, 2007, pp. 465-471.
[101] S. Andova, C. Cremers, and K. Gj?steen et al. A framework for compositional verification of security protocols. Information and Computation. 2008, 206 (2-4): 425-459.
[102] Security Protocols Open Repository. http://www.lsv.ens-cachan.fr/ Software /spore/table.html
[103] Y. Boichut, P. Héam, and O. Kouchnarenko. Tree automata for detecting attacks on protocols with algebraic cryptographic primitives. Electronic Notes in Theoretical Computer Science. 2009, (239): 57-72.
[104] B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming. 2008, 75(1): 3-51.
[105] V. Cortier, S. Delaune, and P. Lafourcade. A survey of algebraic properties used in cryptographic protocols. Journal of computer security. 2006.14(No.1):1-43.
[106] S. Bursuc and H. Comon-Lundh. Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions. The 20th International Conference on Rewriting Techniques and Applications. Brasília: Springer, 2009, pp. 133-147.
[107] M. Baudet, V. Cortier, and S. Kremer. Computationally sound implementations of equational theories against passive adversaries. Information and Computation.2009, 207(4): 496-520.
[108] D. Basin, S. M?dersheim, and L. Viganò. Algebraic Intruder Deductions. The 12th International Conference on Logic for programming, artificial intelligence, and reasoning. Montego Bay: Springer, 2005, pp. 549-564.
[109] T.Deursen and S.Radomirovic. Untraceable RFID protocols are not trivially composable: Attacks on the revision of EC-RAC. Cryptology ePrint Archive 2009/332, July 2009.
[110] G. E. Suh and S. Devadas. Physical unclonable functions for device authentication and secret key generation. Proceedings of the 44th annual Design Automation Conference. San Diego: IEEE Computer Society, 2007, pp. 9-14.
[111] A. J. Menezes, P. C. van Oorschot, and S. A. Vanstone. Handbook of Applied Cryptography. Boca Raton: CRC Press, 1996.
[112] S. Vaudenay. On privacy models for RFID. The 13th Annual International Conference on the Theory and Application Cryptology and Information Security. Sarawak: Springer, 2007, pp. 68-87.