几类安全协议的研究与设计
|
摘要
随着网络应用的迅速发展,网络安全问题日益重要。安全协议是构建网络安全环境的基石,是网络安全通信系统的核心技术,它的正确性和安全性对整个网络环境的安全起着至关重要的作用。安全协议的设计和分析已经成为近年来国际上在网络安全和信息安全领域最活跃的研究方向之一。
由于时间和篇幅有限,本文主要对基于口令的安全协议、电子支付协议和射频识别(RFID)系统安全协议这三类有代表性的新型安全协议进行了研究,主要包括下列内容:
1.基于串空间模型,对攻击者串进行了扩展,以便分析安全协议中的口令猜测攻击。为了抵御口令猜测攻击,在一个两方基于口令的安全协议中引人一类散列函数,对修改后的协议进行了形式化分析,证明能够有效抵御猜测攻击。
2.在通用可组合模型下,定义了一个三方口令认证密钥交换理想函数,然后在两方口令认证密钥交换理想函数辅助的混合模型下,构造了一个实现该理想函数的三方口令认证密钥交换协议。设计的协议不仅是通用可组合安全的,并且结构简单。
3.公平性是电子支付协议的一个基本属性。基于通用可组合模型,定义了公平电子支付理想函数。在可转化签名理想函数、注册理想函数和安全会话理想函数辅助的混合模型下,构造了一个实现公平电子支付理想函数的公平电子支付协议。新的协议结构简单,通信量较低。
4.针对RFID系统的特殊需求,在通用可组合模型下,设计了一个低成本的RFID匿名认证协议,该协议的实现对于一般的RFID结构是切实可行的。通过对近年来提出的符合EPCGen2标准的RFID协议的安全性分析,提出了符合EPCGen2标准的RFID认证协议的设计原则,并设计了一个新的符合EPCGen2标准的RFID认证协议。对RFID搜索协议的安全需求进行了分析,设计了一个不需要后端数据库参与的低成本RFID搜索协议。分析了供应链环境下RFID通信协议应该满足的安全需求,提出了一个基于伪随机函数原语实现的供应链环境下安全的RFID通信协议,该协议具有较高的效率,标签端的计算负荷和存储成本较低。
5.对串空间模型进行扩展,使其能够用来分析标签的不可追踪性。基于扩展的串空间模型,对Feldhofer协议和O′-FRAP协议进行了分析。
With the rapid growth of network applications, network security has become an important issue. Security protocols works as a kind of the kernel technology for the secure network communication,thus their correctness and security are very crucial to network security. In recent years, the design and analysis of security protocols has become one of the most active research topics in the field of network and information security.
For lack of time and space, the password-based security protocols, electronic payment protocols and security protocols for radio frequency identification (RFID) are studied in this thesis.
Firstly, based on the strand space model, these standard strands of the attacker were extended for the purpose of analyzing the guessing attack. A kind hash function was used for resisting guessing attacks in a two-party password-based security protocol. A formal analysis of the modified protocol shows that it can prevent guessing attacks.
Secondly, an ideal functionality of three-party password-authenticated key exchange was defined in the universal composability model,and a three-party password-authenticated key exchange protocol was constructed to realize this ideal functionality in the hybrid model which aided by two-party password-authenticated key exchange ideal functionality. The proposed protocol is universally composable, and has simpler structure.
Thirdly, fairness is an essential property in electronic payment protocol. An ideal functionality of fair electronic payment was defined in the universal composability model. In the hybrid model which aided by ideal convertible signature functionality, ideal registration functionality and ideal secure session functionality, a fair electronic payment protocol was constructed to realize this ideal functionality. The new protocol has simpler structure and lower communication overhead.
Fourthly, safety requirements for RFID protocols were analyzed and a low cost anonymous authentication protocol for RFID was proposed based on the universal composability mode. The implementation of this protocol is feasible for a wide range of RFID architectures. Recently proposed EPCGen2 compliant security protocols were analyzed, and the design principles of EPCGen2 compliant authentication protocols were given. A new RFID authentication protocol based on the EPCGen2 standards was also proposed. Safety requirements for RFID search protocols were analyzed, and a low cost RFID search protocol was proposed without the need for a bake-end database. Security requirements for RFID communication protocols in supply chain environments were analyzed, and a new secure RFID communication protocol in supply chains was proposed. The new protocol imposes lower computation load and storage cost on RFID tags and has higher efficiency.
Fifthly, the strand space model was extended so that it can be applied to analyze untraceability of tags in RFID protocols. Based on the extended strand space model, Feldhofer protocol and O′-FRAP protocol were analyzed.
由于时间和篇幅有限,本文主要对基于口令的安全协议、电子支付协议和射频识别(RFID)系统安全协议这三类有代表性的新型安全协议进行了研究,主要包括下列内容:
1.基于串空间模型,对攻击者串进行了扩展,以便分析安全协议中的口令猜测攻击。为了抵御口令猜测攻击,在一个两方基于口令的安全协议中引人一类散列函数,对修改后的协议进行了形式化分析,证明能够有效抵御猜测攻击。
2.在通用可组合模型下,定义了一个三方口令认证密钥交换理想函数,然后在两方口令认证密钥交换理想函数辅助的混合模型下,构造了一个实现该理想函数的三方口令认证密钥交换协议。设计的协议不仅是通用可组合安全的,并且结构简单。
3.公平性是电子支付协议的一个基本属性。基于通用可组合模型,定义了公平电子支付理想函数。在可转化签名理想函数、注册理想函数和安全会话理想函数辅助的混合模型下,构造了一个实现公平电子支付理想函数的公平电子支付协议。新的协议结构简单,通信量较低。
4.针对RFID系统的特殊需求,在通用可组合模型下,设计了一个低成本的RFID匿名认证协议,该协议的实现对于一般的RFID结构是切实可行的。通过对近年来提出的符合EPCGen2标准的RFID协议的安全性分析,提出了符合EPCGen2标准的RFID认证协议的设计原则,并设计了一个新的符合EPCGen2标准的RFID认证协议。对RFID搜索协议的安全需求进行了分析,设计了一个不需要后端数据库参与的低成本RFID搜索协议。分析了供应链环境下RFID通信协议应该满足的安全需求,提出了一个基于伪随机函数原语实现的供应链环境下安全的RFID通信协议,该协议具有较高的效率,标签端的计算负荷和存储成本较低。
5.对串空间模型进行扩展,使其能够用来分析标签的不可追踪性。基于扩展的串空间模型,对Feldhofer协议和O′-FRAP协议进行了分析。
With the rapid growth of network applications, network security has become an important issue. Security protocols works as a kind of the kernel technology for the secure network communication,thus their correctness and security are very crucial to network security. In recent years, the design and analysis of security protocols has become one of the most active research topics in the field of network and information security.
For lack of time and space, the password-based security protocols, electronic payment protocols and security protocols for radio frequency identification (RFID) are studied in this thesis.
Firstly, based on the strand space model, these standard strands of the attacker were extended for the purpose of analyzing the guessing attack. A kind hash function was used for resisting guessing attacks in a two-party password-based security protocol. A formal analysis of the modified protocol shows that it can prevent guessing attacks.
Secondly, an ideal functionality of three-party password-authenticated key exchange was defined in the universal composability model,and a three-party password-authenticated key exchange protocol was constructed to realize this ideal functionality in the hybrid model which aided by two-party password-authenticated key exchange ideal functionality. The proposed protocol is universally composable, and has simpler structure.
Thirdly, fairness is an essential property in electronic payment protocol. An ideal functionality of fair electronic payment was defined in the universal composability model. In the hybrid model which aided by ideal convertible signature functionality, ideal registration functionality and ideal secure session functionality, a fair electronic payment protocol was constructed to realize this ideal functionality. The new protocol has simpler structure and lower communication overhead.
Fourthly, safety requirements for RFID protocols were analyzed and a low cost anonymous authentication protocol for RFID was proposed based on the universal composability mode. The implementation of this protocol is feasible for a wide range of RFID architectures. Recently proposed EPCGen2 compliant security protocols were analyzed, and the design principles of EPCGen2 compliant authentication protocols were given. A new RFID authentication protocol based on the EPCGen2 standards was also proposed. Safety requirements for RFID search protocols were analyzed, and a low cost RFID search protocol was proposed without the need for a bake-end database. Security requirements for RFID communication protocols in supply chain environments were analyzed, and a new secure RFID communication protocol in supply chains was proposed. The new protocol imposes lower computation load and storage cost on RFID tags and has higher efficiency.
Fifthly, the strand space model was extended so that it can be applied to analyze untraceability of tags in RFID protocols. Based on the extended strand space model, Feldhofer protocol and O′-FRAP protocol were analyzed.
引文
[1] Needham R M,Schroeder M D. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978, 21(12): 993-999.
[2] Denning D E, Sacco G M. Timestamps in key distribution protocols. Communications of the ACM, 1981, 24(8): 533-536.
[3] Choi K Y, Hwang J Y, Lee D H. Efficient ID-based group key agreement with bilinear maps. Proc. of Public Key Cryptography (PKC’04), Singapore: Springer-Verlag, 2004: 130-144.
[4] Zhang F G, Chen X F. Attack on an ID-based authenticated group key agreement scheme from PKC 2004. Information Processing Letters, 2004. 91(4): 191-193.
[5] Lu R, Cao Z. Simple three-party key exchange protocol. Computer & Security, 2007, 26(1): 94-97.
[6] Guo H, Li Z, Mu Y, et al. Cryptanalysis of simple three-party key exchange protocol. Computers & Security, 2008, 27(1): 16-21.
[7] Phan R C, Yau W, Goi B. Cryptanalysis of simple three-party key exchange protocol. Information Sciences, 2008, 178(13): 2849-2856.
[8] Nam J, Paik J, and Kang H, et al. An off-line dictionary attack on a simple three-party key exchange protocol. IEEE Communications Letters, 2009, 13(3): 205-208.
[9] Micali S. Simple and fast optimistic protocols for fair electronic exchange. Proc. of Symposium on Principles of Distributed Computing, Boston: ACM Press, 2003: 12-19.
[10] Bao Feng, Wang Guilin, Zhou Jianying, et al. Analysis and improvement of Micali’s fair contract signing protocol. Proc. of ICANN’04. Sydney: IEEE Press, 2004: 176-187.
[11] Chien H Y. 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.
[12] Cao T, Bertino E, Lei H. Security analysis of the SASI protocol. IEEE Transactions on Dependable and Secure Computing, 2009, 6(1): 73-77.
[13]卿斯汉.安全协议20年研究进展.软件学报, 2003, 14(10): 1740-1752.
[14]王育民,刘建伟.通信网的安全——理论与技术.西安:西安电子科技大学出版社, 1999.
[15]王亚弟,束妮娜,韩继红等.密码协议形式化分析.北京:机械工业出版社, 2006.
[16] Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory, 1983, 29(2): 198-208.
[17] Mao W B著.王继林,伍前红译.现代密码学理论与实践.北京:电子工业出版社,2004.
[18] Martinez S, Valls M, Roig C, et al. A secure elliptic curve-based RFID protocol. Jouranl of Computer Science and Technology, 2009, 24(2): 309-318.
[19] Lo N W, Yeh K H. Cryptanalysis of two three-party encrypted key exchange protocols. Computer Standards & Interfaces, 2009, 31(6): 1167-1174.
[20] Peris P, Cesar J, Esteves M, et al. Cryptanalysis of a novel authentication protocol conformingto EPC-C1G2 standard. Computer Standards & Interfaces, 2009, 31(2): 372-380.
[21] Huang H F. A simple three-party password-based key exchange protocol. International Journal of Communication Systems, 2009, 22(2): 113-119.
[22]张辉,侯朝焕,王东辉.一种基于部分ID的新型RFID安全隐私相互认证协议.电子与信息学报, 2009, 31(4): 853-856.
[23] Gritzalis S,Spinellis D, Georgiadis P. Security protocols over open networks and distributed systems: formal methods for their analysis, design, and verification. Computer Communications, 1999, 22(8): 695-707.
[24] Burrows M, Abadi M, Needham R. A logic of authentication. ACM Transactions on Computer Systems, 1990, 8(1): 18-36.
[25] CCITT. CCITT draft recommendation X.509. The directory-authentication framework, Version 7, 1987.
[26] Otway D, Rees D. Efficient and timely mutual authentication. ACM Operating System Review, 1987, 21(1): 8-10.
[27] Gong L, Needham R, Yahalom R. Reasoning about belief in authentication protocols. In IEEE Computer Society Symposium in Security and Privacy, Oakland, CA: IEEE Press, 1990: 234-248.
[28] Abadi, Tuttle M R. A semantics for a logic of cryptographic. Proc. of the 10th ACM Symposium on Principles of Distributed Computing, Columbia: ACM Press, 1991: 201-216.
[29] van Oorschot P. Extending authentication logics of belief to key agreement protocols. Proc. of the First ACM Conference on Computer and Communications Security, New York: ACM Press, 1993: 232-243.
[30] Syverson P, van Oorshot. On unifying some authentication protocol logics. Proc. of the 1994 IEEE Computer Society Foundations Workshop VII, Los Alamitos: IEEE Press, 1994: 14-28.
[31] Mao W B, Boyd C. Towards the formal analysis of security protocols. Proc. of the Computer Security Foundation Workshop VI, Franconia: IEEE Press, 1993: 147-158.
[32] Kailar R. Accountability in electronic commerce protocols. IEEE Transactions on software engineering, 1996, 22(5): 33-47.
[33] Kessler V, Neumann H. A sound logic for analyzing electronic commerce protocols. Proc. of the 5th European Symposium on Research in Computer Security, Belgium: Springer-Verlag, 1998: 345-360.
[34] Kessler V, Wedel G. Formal semantics for authentication logics, Proc. of the 4th European Symposium on Research in Computer Security, Rome: Springer-Verlag, 1996: 219-241.
[35]苏开乐,吕关锋,陈清亮.基于知识结构的认证协议验证.中国科学E辑:信息科学, 2005, 35(4): 337-351.
[36]赵华伟.两种安全协议形式化理论的研究.山东大学,博士学位论文, 2006.
[37] Sidhu D. Authentication protocols for computer networks. Computer Networks and ISDN Systems, 1986, 11(1): 297-310.
[38] Varadharajan V. Verification of network security protocols. Computers & Security, 1989, 8(1): 693-708.
[39] Kemmerer R. Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications, 1989, 7(4): 448-457.
[40] Roscoe A W. Modeling and verifying key-exchange protocols using CSP & FDR. Proc. of the 1995 IEEE Computer Security Foundations Workshop, Boston: IEEE Press, 1995: 98-107.
[41] Dill D L, Drexler A J, Hu A J, et al. Protocol verification as a hardware design aid. Proc. of the IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE Press, Cambridge: IEEE Press, 1992: 522-525.
[42] Meadows C. The NRL protocol analyzer: an overview. Journal of Logic Programming, 1996, 26(2): 113-131.
[43] Millen J. The interrogator model. Proc. of the 1995 IEEE Symposium on Security and Privacy, Oakland, CA: IEEE Press, 1995: 251-260.
[44] Bolignano D. An approach to the formal verification of cryptographic protocols. Proc. of the Third ACM Conference on Computer and Communications Security, New Delhi: ACM Press, 1996: 106-118.
[45] Paulson L. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998, 6(1): 85-128.
[46] Paulson L. Isabelle: a generic theorem plover. Proc. of LNCS 828, Belgium: Springer-Verlag, 1994.
[47] Fabrega J T, Herzog J C, Guttman J D. Strand spaces: proving security protocols correct. Journal of Computer Security, 1999, 7(2): 191-230.
[48] Song D X, Berezin S, Perrig A. Athena: a novel approach to efficient automatic security protocol analysis. Journal of Computer Security, 2001, 9(1): 47-74.
[49]刘东喜.安全协议的自动验证技术研究.上海交通大学,博士学位论文, 2002.
[50]任侠.形式化方法在安全协议验证领域内的应用研究.中国科技大学,博士学位论文, 2003.
[51]李莉.安全协议的形式化分析及验证技术研究.武汉大学,博士学位论文, 2004.
[52]李谢华.基于串空间模型的安全协议形式化验证方法的研究.上海交通大学,博士学位论文, 2007.
[53] Liu Dongxi, Li Xiaoyong, Bai Yingcai. An attack-finding algorithm for security protocols. Journal of Computer Science and Technology, 2002, 17(4): 450-563.
[54] Guttman J D. Security protocol design via authentication tests. 15th IEEE Computer Security Foundations Workshop (CSFW-15), Nova Scotia: IEEE Press, 2002: 92-103.
[55]杨明,罗军舟.基于认证测试的安全协议分析.软件学报, 2006, 17(1): 148-156.
[56] Zhao Huawei, Zhang Wenyu. Definitions and analysis of integrity in strand spaces model. International Symposium on Electronic Commerce and Security, Washington: IEEE Press, 2008: 153-158.
[57] Froschle S. Adding branching to the strand space model. Electronic Notes in Theoretical Computer Science, 2009, 242(1): 139-159.
[58] Wang Hong, Ma Jianping, Chen Bo. Formal analysis of fairness in E-payment protocol based on strand space. WISM’09, LNCS5854, Berlin: Springer-Verlag, 2009: 469-478.
[59] Yang Jie, Ma Xianheng, Li Yi. Enhanced Strand Space for secure protocol analysis, Conference on Anti-counterfeiting, Security, and Identification in Communication, Hong Kong: IEEE Press, 2009: 374-377.
[60] Guo Yuyan, Wei Shimin. Strand space model of amended NS protocol and its analysis, World Congress on Computer Science and Information Engineering, Los Angeles: IEEE Press, 2009: 439-442.
[61] Bellare M, Rogaway P. Entity authentication and key distribution. Advances in Cryptology- CRYPTO’93, Berlin: Springer-Verlag, 1993: 232-249.
[62] Bellare M, Rogaway P. Provably secure session key distribution: the three party case. Proc. of the 27th ACM Symposium on the Theory of Computing, New York: ACM Press, 1995: 57-66.
[63] Bellare M, Pointcheval D, Rogaway P. Authenticated key exchange secure against dictionary attacks. Advances in Cryptology- Eurocrypt 2000, Berlin: Springer-Verlag, 2000: 139-155.
[64] Bresson E, Chevassut O, Pointcheval D. Dynamic group Diffie-Hellman key exchange under standard assumptions. Advances in Cryptology- Eurocrypt’02, Berlin: Springer-Verlag, 2002: 321-336.
[65] Abdalla M, Fouque P A, Pointcheval D. Password-based authenticated key exchange in the three-party setting. IEEE Proceedings - Information Security, 2006, 153(1): 27-39.
[66] Bellare M, Canetti R, Krawczyk H. A modular approach to the design and analysis of authentication and key-exchange protocols. Proc. of the 30th Annual Symp. on the Theory of Computing, New York: ACM Press, 1998: 419-428.
[67] Canetti R, Krawczyk H. Analysis of key exchange protocols and their use for building secure channels. Proc. of Eurocrypt’01, Berlin: Springer-Verlag, 2001: 453-474.
[68]李兴华,马建峰,文相在.基于身份密码系统下Canetti-Krawczyk模型的安全扩展.中国科学E辑:信息科学, 2004, 34(10): 106-113.
[69]张帆,无线网络安全协议的形式化分析方法.西安电子科技大学,博士学位论文, 2007.
[70]冯登国,陈伟东.基于口令的安全协议的模块化设计与分析.中国科学E辑:信息科学, 2007, 37(2): 223-237.
[71] Canetti R. Universally composable security: a new paradigm for cryptographic protocols. Proc. of the 42nd IEEE Symposium on Foundations of Computer Science, Oakland, CA: IEEE Press, 2001: 136-145.
[72] Barak B, Canetti R, Nielsen J N, et al. Universally composable protocols with relaxed set-up assumptions. Proc. of 45th FOCS, Washington: IEEE Press, 2004: 186-195.
[73] Yao A, Yao F F, Zhao Y. A note on universal composable zero knowledge in common reference string model. Proc. of TAMC’07, Shanghai: IEEE Press, 2007: 462-473.
[74] Kurosawa K, Furukawa J. Universally composable undeniable signature. Proc. of ICALP’08, Berlin: Springer-Verlag, 2008: 524-535.
[75] Hu Zhenyu, Jiang Jiangchun, Sun Fuchun. Using IND-CVA for constructing secure communication. Science in China Series F: Information Sciences, 2009, 52(10): 1801-1811.
[76]雷飞宇, UC安全多方计算模型及其典型应用研究.上海交通大学,博士学位论文, 2007.
[77] Yao A, Yao F F, Zhao Y. A note on universal composable zero knowledge in common reference string model. TAMC’07, Shanghai: Springer-Verlag, 2007: 462-473.
[78]张帆,马建峰,文相在.通用可组合的匿名HASH认证模型.中国科学E辑:信息科学, 2007, 37(2): 272-284.
[79]杨超,曹春杰,马建峰.通用可组合安全的Mesh网络认证协议.西安电子科技大学学报, 2007, 34(5): 814-817.
[80]冯涛.通用可复合密码协议理论及其应用研究.西安电子科技大学,博士学位论文, 2009.
[81]贾洪勇.安全协议的可组合性分析与证明.北京邮电大学,博士学位论文, 2009.
[82] Abadi M, Rogaway P. Reconciling two views of cryptography: the computational soundness of formal encryption. Journal of Cryptology. 2002, 15(2): 103-127.
[83] Micciancio D, Warinschi B. Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. Journal of Computer Security, 2004, 12(1): 99-129.
[84] Gligor V, Horvitz D O. Weak key authenticity and the computational completeness of formal encryption. 23rd Annual Int’l Cryptology Conference, Berlin: Springer-Verlag, 2003: 530-547.
[85] Micciancio D, Warinschi B. Soundness of formal encryption in the presence of active adversaries. Theory of Cryptography Conference. Berlin: Springer-Verlag, 2004: 133-151.
[86] Herzog J. Computational soundness for standard assumptions of formal cryptography. Massachusetts Institute of Technology, Ph. D. dissertation, 2004.
[87] Millen J, Shmatikov V. Symbolic protocol analysis with products and Diffie-Hellman exponentiation. Proc. of 16th IEEE Computer Security Foundations Workshop, New York: IEEE Press, 2003: 47-61.
[88] Abadi M, Cortier V. Deciding knowledge in security protocols under equational theories. Theoretical Computer Science, 2006, 2(1): 2-32.
[89] Canetti R, Herzog J. Universally composable symbolic analysis of mutual authentication and key-exchange protocols. Theory of Cryptography Conference, Berlin: Springer-Verlag, 2006: 380-403.
[90]田园,王颖,金峰等,基于刚性与相似性概念的密码协议分析方法.计算机学报, 2009, 32(4): 618-634.
[91] Lowe G. A hierarchy of authentication specifications. In 10th Computer Security Foundations Workshop Proceedings, Massachusetts: IEEE Press, 1997: 31-43.
[92] Goldreich O. Foundations of Cryptography. Cambridge: Cambridge University Press, 2001.
[93] Lomas T, Li Gong, Saltzer J, et al. Reducing risks from poorly chosen keys. ACM Operating Systems Review, 1989, 23(5): 14-18.
[94] Bellovin S, Merritt M. Augumented encrypted key exchange: a password-based protocol secure against dictionary attacks and password file compromise. Proc. of CCS’93, New York: ACM Press, 1993: 244-250.
[95] Wu T. A real world analysis of Kerberos password security. Proc. of the Symposium on Network and Distributed Systems Security (NDSS’99), San Diego: IEEE Press, 1999: 3-5.
[96]李莉,薛锐,张焕国等.基于口令认证的密钥交换协议的安全性分析.电子学报, 2005, 33(1): 166-170.
[97] Gong L, Mark T. Lomas, et al. Protecting poorly chosen secrets from guessing attacks. IEEE Journal on Selected Areas in Communications, 1993, 11(5): 648-656.
[98] Halevi S, Krawczyk H. Public-key cryptography and password protocols. ACM Transaction on Information and System Security, 1999, 2(3): 230-268.
[99] Boyko V, Mackenzie P, Patel S. Provably secure password authenticated key exchange using diffie-hellman. Proc. of Advances in Cryptology– Eurocrypt 2000, Berlin: Springer-Verlag, 2000: 156-171.
[100] Katz J, Ostrovsky R, Yung M. Efficient password-authenticated key exchange using human-memorable passwords. Proc. of Advances in Cryptology– Eurocrypt 2001, Berlin: Springer-Verlag, 2001: 475-494.
[101] Malladi S, Alves-Foss J, Malladi S. Preventing guessing attacks using fingerprint biometrics. 16th IEEE Computer Security Foundations Workshop, Washington: IEEE Press, 2003: 24-30.
[102] Lowe G. Analyzing protocols subject to guessing attack. Journal of Computer Security, 2004, 12(1): 83-98.
[103] Corin R, Doumen J, Etalle S. Analyzing password protocol security against off-line dictionary attacks. Electronic Notes in Theoretical Computer Science, 2005, 121(4): 47-63.
[104]龙士工,罗文俊,袁超伟等.串空间模型中的口令猜测攻击.北京邮电大学学报, 2007, 30(1): 62-65.
[105]毛晨晓,罗文坚,王煦法.分析安全协议猜测攻击的模态逻辑方法.计算机学报, 2007, 30(6): 924-933.
[106] Abdalla M, Catalano D, Chevalier C. Efficient two-party password-based key exchange protocols in the UC framework. Cryptographers’Track at the RSA Conference 2008, San Francisco: ACM Press, 2008: 335-351.
[107]谭示崇.口令认证密钥协商协议的研究.西安电子科技大学,博士学位论文, 2009.
[108] Delaune S, Jacquemard F. A theory of dictionary Attacks and its Complexity. Proc. of the 17th Computer Security Foundations Workshop, Pacific Grove: IEEE Press, 2004: 2-15.
[109] Hwang M S, Lo J W, Liu C H. Simple authenticated key agreement and protected password change protocol. Compute Security, 2005, 24(2): 500-504.
[110] Wang C I, Fan C I, Guan D J. Cryptanalysis on Chang-Yang- Hwang protected password change protocol. Advances in Cryptology– Eurocrypt 2005, Berlin: Springer-Verlag, 2005: 147-209.
[111] Lin C L, Sun H M, and Hwang T. Three party-encrypted key exchange: attacks and a solution. ACM Operating System Review, 2000, 34(4): 12-20.
[112] Sun H M, Chen B, and Hwang T. Secure key agreement protocols for three-party against guessing attacks. The Journal of Systems and Software, 2005, 75(2): 63-68.
[113] Steiner M, Tsudik G, and Wainder M. Refinement and extension of encrypted key exchange. ACM Operation Systems Review, 1995, 29(3): 22-30.
[114] Ota H, Yoneyama K, and Kiyomoto S, et al. Universally composable client-to-client general authenticated key exchange. Transactions of Information Processing Society of Japan, 2007, 48(9): 3073-3088.
[115] Even S. A randomized protocol for signing contracts. Communications of the ACM, 1985, 28(6): 637-647.
[116]熊焰,张伟超,苗付友等.一种基于计算能力的无需可信第三方公平非抵赖信息交换协议.电子学报, 2006, 34(3): 563-566.
[117] Coffey T, Non-repudiation with mandatory proof of receipt. Computer Communication Review, 1996, 26(1): 6-17.
[118] Han S, Chang E, Dillon T. Secure e-transactions protocol using intelligent mobile agents with fair privacy. Studies in Computational Intelligence, 2007, 37(3): 307-326.
[119] Oniz C, Savas E, Levi A. An optimistic fair e-commerce protocol for large e-goods. Proc. of the 7th IEEE International Symposium on Computer Networks, Nevada: IEEE Press, 2006: 214-219.
[120] Liang Xiaohui, Cao Zhenfu, Lu Rongxing. Efficient and secure protocol in fair document exchange. Computer Standards & Interfaces, 2008, 30(3): 167-176.
[121]樊利民,廖建新.公平的移动小额支付协议.电子与信息学报, 2007, 29(11): 2659-2602.
[122] Asokan N, Shoup V, Waidner M. Optimistic fair exchange of digital signatures, IEEE Journal on Selected Areas in Communications, 2000, 18(4): 593-610.
[123] Almudena A, Juan M, Izquierdo A. A formal analysis of fairness and non-repudiation in the RSA-CEGD protocol. International Conference on Computational Science and Its Applications, Singapore: IEEE Press, 2005: 1309-1318.
[124]文静华,李祥,张焕国等.基于ATL的公平电子商务协议形式化分析.电子与信息学报, 2007, 29(4): 901-905.
[125] Sornkhom P, Permpoontanalarp Y. Security analysis of Micali’s fair contract signing protocol by using colored petri nets. Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing, Australia: IEEE Press, 2008: 329-334.
[126] Aybek M, Steve K, Eike R. Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model. International Conference on Financial Cryptography and Data Security, Roseau: IEEE Press, 2005: 255-269.
[127] Okada Y, Manabe Y, Okamoto T. An optimistic fair exchange protocol and its security in the universal composability framework. Int. J. of Applied Cryptography, 2008, 1(1): 70-78.
[128] Chaum D, Damgard I, Pedersen T. Convertible undeniable signatures. In CRYPTO’90, Berlin: Springer-Verlag, 1990: 189-205.
[129] Boyd C, Foo E. Off-line fair payment protocols using convertible signatures. Advances in Cryptology ASIACRYPT'98, Berlin: Springer-Verlag, 1998: 271-285.
[130] Park J M, Edwin K P, Siegel H J. Constructing fair-exchange protocols for e-commerce via distributed computation of RSA signatures. Proc. of the 20th Annual-Symposium on Principles of Distributed Computing. USA: ACM Press, 2003: 172-181.
[131] Garfinkel S L, Juels A, Pappu R. RFID privacy: an overview of problems and proposed solutions. Security & Privacy Magazine, 2005, 3(3): 34-43.
[132] Juels A, Ronald L, Rivest R, et al. The blocker tag: selective blocking of RFID tags for consumer privacy. 10th Conference on Computer and communications security. Washington: ACM Press, 2003: 103-111.
[133] Karjoth G, Paul A, Moskowitz. Disabling RFID tags with visible confirmation: clipped tags are silenced. ACM Workshop on Privacy in Electronic Society. Alexandria: ACM Press, 2005: 27-30.
[134] Hopper N J, Blum M. Secure human identification protocols. 7th International Conference on the Theory and Application of Cryptology and Information Security. Berlin: Springer-Verlag, 2001: 52-66.
[135] Gilbert H, Matthew R, Sibert H. An active attack against HB+: a provably secure lightweight authentication protocol. IEE Electronics Letters, 2005, 41(21): 1169-1170.
[136] Sarma S E, Weis S A, Engels D W. Radio-frequency identification: secure risks and challenges. RSA Laboratories Cryptobytes, 2003, 6(1): 2-9.
[137] Weis S A, Sarma S E, Rivest R, et, al. Security and privacy aspects of low-cost radio frequency identification systems. Proc. of the 1st International Conference on Security in Pervasive Computing. Berlin: Springer-Verlag, 2004: 201-212.
[138]周永彬,冯登国. RFID安全协议的设计和分析.计算机学报, 2006, 29(4): 581-589.
[139] Lee S M, Hwang Y J, Lee D H. Efficient authentication for low-cost RFID systems. Proc. of the International Conference on Computational Science and Its Applications (ICCSA2005). Berlin: Springer-Verlag, 2005: 619-627.
[140] Molnar D, Soppera A, Wagner D. A scalable, delegatable pseudonym protocol enabling ownership transfer of RFID tags. Workshop on Selected Areas in Cryptography. Berlin: Springer-Verlag, 2006: 276-290.
[141] van Le T, Burmester M, Medeiros B. Universally composable and forward secure RFID authentication and authenticated key exchange. Proc. of the 2nd ACM Symposium on Information, Computer and Communications Security. New York: ACM, 2007: 242-252.
[142] Tsudik G. YA-TRAP: yet another trivial RFID authentication protocol. Proc. of the 4th annual IEEE International Conference on Pervasive Computing and Communications Workshops. Washington: IEEE Press, 2006: 640-651.
[143] Kim H S, Choi J Y. The design and verification of RFID authentication protocol for ubiquitous computing. Proc. of the 18th International Workshop on Database and Expert Systems Applications. Washington: IEEE Press, 2007: 693-697.
[144] Burmester M, van Le T, Medeiros B. Provably secure ubiquitous systems: Universally composable RFID authentication protocols. Proc. of the 2nd International Conference on Security and Privacy in Networks. Maryland: IEEE Press, 2006: 176-186.
[145]邓淼磊,黄照鹤,周利华等.认证协议中数据同步的分析.计算机科学, 2010, 37(3): 83-85.
[146]丁振华,李锦涛,冯波.基于Hash函数的RFID安全认证协议研究.计算机研究与发展, 2009, 46(4): 583-592.
[147]丁治国. RFID关键技术研究与实现.中国科学技术大学,博士学位论文, 2009.
[148] EPC Class 1 Gen 2 standard. http://www.epcglobalinc.org/standards/uhfc1g2/
[149] Duc D C, Park J, Lee H, et al. Enhancing security of EPCglobal Gen-2 RFID tag against traceability and cloning. Symposium on Cryptography and Information Security, Hiroshima: ACM Press, 2006: 269-277.
[150] Chien H Y, Chen C H. Mutual authentication protocol for RFID conforming to EPC Class 1 Generation 2 standards. Computer Standards & Interfaces, 2007, 26(2): 254-259.
[151] Cai Q L, Zhan Y J, Wang Y H. A minimalist mutual authentication protocol for RFID system & BAN logic analysis. ISECS International Colloquium Computing, Communication, Control, and Management, Guangzhou: IEEE Press, 2008: 449-453.
[152] Choi E Y, Lee D H, Lin J. Anti-cloning protocol suitable to EPCglobal Class-1 Generation-2 RFID systems. Computer Standards & Interfaces, 2009, 31(6): 1124-1130.
[153] Seo D H, Baek J M, Cho D S. Secure RFID authentication scheme for EPC Class Gen2. International Conference on Ubiquitous Information Management and Communication, Suwon: IEEE Press, 2009: 221-227.
[154] Sun H M, Ting W C. A Gen2-based RFID authentication protocol for security and privacy. IEEE Transactions on Mobile Computing, 2009, 8(1): 1-11
[155] Tan C C, Sheng B, Li Q. Serverless search and authentication protocols for RFID. 5th Annual IEEE International Conference on Pervasive Computing and Communications, New York: IEEE Press, 2007: 34-41.
[156] Ahamed S, Rahman F, Hoque E, et al. S3PR: secure serverless search protocols for RFID. International Conference on Information Security and Assurance, Hawaii: IEEE Press, 2008: 187-192.
[157] Li Yingjiu, Ding Xuhua. Protecting RFID communications in supply chains. Proc. of the ACM Symposium on Information, Computer, and Communications Security, Singapore: ACM Press, 2007: 234-241.
[158]张帆,孙璇,马建峰等.供应链环境下通用可组合安全的RFID通信协议.计算机学报, 2008, 31(10): 1754-1767.
[159] Juels A, Pappu R, Parno B. Unidirectional key distribution across time and space with applications to rfid security. 17th USENIX Security Symposium, San Jose: ACM Press, 2008: 75-90.
[160] Han S H, Chu C H. Tamper detection in RFID-enabled supply chains using fragile watermarking. International Conference on RFID, Las Vegas: IEEE Press, 2008: 111-117.
[161] Canetti R. Universally composable signature, certification and authentication. 17th IEEE computer security foundations workshop. Dallas: IEEE Press, 2004: 219-245.
[162] Coppersmith D, Krawczyk H, Mansour Y. The shrinking generator. Proc. Advances in Cryptology (CRYPTO 1994), Berlin: Springer-Verlag, 1994: 22-39.
[163] Burmester M, Munilla J. A flyweight RFID authentication protocol. 5th Workshop on RFID Security, Leuven: IEEE Press, 2009: 1-13.
[164] Rotter P. A framework for assessing RFID system security and privacy risks. Pervasive Computing, 2008, 7(4): 70-77.
[165] Yamamoto A, Suzuki S, Hada H. A tamper detection method for RFID tag data. IEEE RFID 2008, Las Vegas, NV: IEEE Press, 2008: 51-57.
[166] Lin J, Oh H, Kim S. A new hash-based RFID mutual authentication protocol providing enhanced user privacy protection. In ISPEC 2008, Berlin: Springer-Verlag, 2008: 278-280.
[167] Juels A, Weis S. Defining strong privacy for RFID. In International Conference on Pervasive Computing and Communications, New York: IEEE Press, 2007: 342-347.
[168] Garcia F D, Hasuo I, Pieters W, et al. Provable anonymity. In FMSE, Virginia: IEEE Press, 2005: 63-72.
[169] Ouafi K, Phan R. Traceable privacy of recent provably-secure RFID protocols. In ACNS’08, New York: ACM Press, 2008: 479-489.
[170] Ha J, Moon S, Zhou J, Ha J. A new formal proof model for RFID location privacy. In ESORICS, Berlin: Springer-Verlag, 2008: 267-281.
[171] van Deursen T, Radomirovic S. On a new formal proof model for RFID location privacy. Information Processing Letters, 2009, 110(2): 57-61.
[172] Feldhofer M, Dominikus S, Wolkerstorfer J. Strong authentication for RFID systems using the AES algorithm. In CHES’04, Berlin: Springer-Verlag, 2004: 357-370.
[2] Denning D E, Sacco G M. Timestamps in key distribution protocols. Communications of the ACM, 1981, 24(8): 533-536.
[3] Choi K Y, Hwang J Y, Lee D H. Efficient ID-based group key agreement with bilinear maps. Proc. of Public Key Cryptography (PKC’04), Singapore: Springer-Verlag, 2004: 130-144.
[4] Zhang F G, Chen X F. Attack on an ID-based authenticated group key agreement scheme from PKC 2004. Information Processing Letters, 2004. 91(4): 191-193.
[5] Lu R, Cao Z. Simple three-party key exchange protocol. Computer & Security, 2007, 26(1): 94-97.
[6] Guo H, Li Z, Mu Y, et al. Cryptanalysis of simple three-party key exchange protocol. Computers & Security, 2008, 27(1): 16-21.
[7] Phan R C, Yau W, Goi B. Cryptanalysis of simple three-party key exchange protocol. Information Sciences, 2008, 178(13): 2849-2856.
[8] Nam J, Paik J, and Kang H, et al. An off-line dictionary attack on a simple three-party key exchange protocol. IEEE Communications Letters, 2009, 13(3): 205-208.
[9] Micali S. Simple and fast optimistic protocols for fair electronic exchange. Proc. of Symposium on Principles of Distributed Computing, Boston: ACM Press, 2003: 12-19.
[10] Bao Feng, Wang Guilin, Zhou Jianying, et al. Analysis and improvement of Micali’s fair contract signing protocol. Proc. of ICANN’04. Sydney: IEEE Press, 2004: 176-187.
[11] Chien H Y. 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.
[12] Cao T, Bertino E, Lei H. Security analysis of the SASI protocol. IEEE Transactions on Dependable and Secure Computing, 2009, 6(1): 73-77.
[13]卿斯汉.安全协议20年研究进展.软件学报, 2003, 14(10): 1740-1752.
[14]王育民,刘建伟.通信网的安全——理论与技术.西安:西安电子科技大学出版社, 1999.
[15]王亚弟,束妮娜,韩继红等.密码协议形式化分析.北京:机械工业出版社, 2006.
[16] Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory, 1983, 29(2): 198-208.
[17] Mao W B著.王继林,伍前红译.现代密码学理论与实践.北京:电子工业出版社,2004.
[18] Martinez S, Valls M, Roig C, et al. A secure elliptic curve-based RFID protocol. Jouranl of Computer Science and Technology, 2009, 24(2): 309-318.
[19] Lo N W, Yeh K H. Cryptanalysis of two three-party encrypted key exchange protocols. Computer Standards & Interfaces, 2009, 31(6): 1167-1174.
[20] Peris P, Cesar J, Esteves M, et al. Cryptanalysis of a novel authentication protocol conformingto EPC-C1G2 standard. Computer Standards & Interfaces, 2009, 31(2): 372-380.
[21] Huang H F. A simple three-party password-based key exchange protocol. International Journal of Communication Systems, 2009, 22(2): 113-119.
[22]张辉,侯朝焕,王东辉.一种基于部分ID的新型RFID安全隐私相互认证协议.电子与信息学报, 2009, 31(4): 853-856.
[23] Gritzalis S,Spinellis D, Georgiadis P. Security protocols over open networks and distributed systems: formal methods for their analysis, design, and verification. Computer Communications, 1999, 22(8): 695-707.
[24] Burrows M, Abadi M, Needham R. A logic of authentication. ACM Transactions on Computer Systems, 1990, 8(1): 18-36.
[25] CCITT. CCITT draft recommendation X.509. The directory-authentication framework, Version 7, 1987.
[26] Otway D, Rees D. Efficient and timely mutual authentication. ACM Operating System Review, 1987, 21(1): 8-10.
[27] Gong L, Needham R, Yahalom R. Reasoning about belief in authentication protocols. In IEEE Computer Society Symposium in Security and Privacy, Oakland, CA: IEEE Press, 1990: 234-248.
[28] Abadi, Tuttle M R. A semantics for a logic of cryptographic. Proc. of the 10th ACM Symposium on Principles of Distributed Computing, Columbia: ACM Press, 1991: 201-216.
[29] van Oorschot P. Extending authentication logics of belief to key agreement protocols. Proc. of the First ACM Conference on Computer and Communications Security, New York: ACM Press, 1993: 232-243.
[30] Syverson P, van Oorshot. On unifying some authentication protocol logics. Proc. of the 1994 IEEE Computer Society Foundations Workshop VII, Los Alamitos: IEEE Press, 1994: 14-28.
[31] Mao W B, Boyd C. Towards the formal analysis of security protocols. Proc. of the Computer Security Foundation Workshop VI, Franconia: IEEE Press, 1993: 147-158.
[32] Kailar R. Accountability in electronic commerce protocols. IEEE Transactions on software engineering, 1996, 22(5): 33-47.
[33] Kessler V, Neumann H. A sound logic for analyzing electronic commerce protocols. Proc. of the 5th European Symposium on Research in Computer Security, Belgium: Springer-Verlag, 1998: 345-360.
[34] Kessler V, Wedel G. Formal semantics for authentication logics, Proc. of the 4th European Symposium on Research in Computer Security, Rome: Springer-Verlag, 1996: 219-241.
[35]苏开乐,吕关锋,陈清亮.基于知识结构的认证协议验证.中国科学E辑:信息科学, 2005, 35(4): 337-351.
[36]赵华伟.两种安全协议形式化理论的研究.山东大学,博士学位论文, 2006.
[37] Sidhu D. Authentication protocols for computer networks. Computer Networks and ISDN Systems, 1986, 11(1): 297-310.
[38] Varadharajan V. Verification of network security protocols. Computers & Security, 1989, 8(1): 693-708.
[39] Kemmerer R. Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications, 1989, 7(4): 448-457.
[40] Roscoe A W. Modeling and verifying key-exchange protocols using CSP & FDR. Proc. of the 1995 IEEE Computer Security Foundations Workshop, Boston: IEEE Press, 1995: 98-107.
[41] Dill D L, Drexler A J, Hu A J, et al. Protocol verification as a hardware design aid. Proc. of the IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE Press, Cambridge: IEEE Press, 1992: 522-525.
[42] Meadows C. The NRL protocol analyzer: an overview. Journal of Logic Programming, 1996, 26(2): 113-131.
[43] Millen J. The interrogator model. Proc. of the 1995 IEEE Symposium on Security and Privacy, Oakland, CA: IEEE Press, 1995: 251-260.
[44] Bolignano D. An approach to the formal verification of cryptographic protocols. Proc. of the Third ACM Conference on Computer and Communications Security, New Delhi: ACM Press, 1996: 106-118.
[45] Paulson L. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998, 6(1): 85-128.
[46] Paulson L. Isabelle: a generic theorem plover. Proc. of LNCS 828, Belgium: Springer-Verlag, 1994.
[47] Fabrega J T, Herzog J C, Guttman J D. Strand spaces: proving security protocols correct. Journal of Computer Security, 1999, 7(2): 191-230.
[48] Song D X, Berezin S, Perrig A. Athena: a novel approach to efficient automatic security protocol analysis. Journal of Computer Security, 2001, 9(1): 47-74.
[49]刘东喜.安全协议的自动验证技术研究.上海交通大学,博士学位论文, 2002.
[50]任侠.形式化方法在安全协议验证领域内的应用研究.中国科技大学,博士学位论文, 2003.
[51]李莉.安全协议的形式化分析及验证技术研究.武汉大学,博士学位论文, 2004.
[52]李谢华.基于串空间模型的安全协议形式化验证方法的研究.上海交通大学,博士学位论文, 2007.
[53] Liu Dongxi, Li Xiaoyong, Bai Yingcai. An attack-finding algorithm for security protocols. Journal of Computer Science and Technology, 2002, 17(4): 450-563.
[54] Guttman J D. Security protocol design via authentication tests. 15th IEEE Computer Security Foundations Workshop (CSFW-15), Nova Scotia: IEEE Press, 2002: 92-103.
[55]杨明,罗军舟.基于认证测试的安全协议分析.软件学报, 2006, 17(1): 148-156.
[56] Zhao Huawei, Zhang Wenyu. Definitions and analysis of integrity in strand spaces model. International Symposium on Electronic Commerce and Security, Washington: IEEE Press, 2008: 153-158.
[57] Froschle S. Adding branching to the strand space model. Electronic Notes in Theoretical Computer Science, 2009, 242(1): 139-159.
[58] Wang Hong, Ma Jianping, Chen Bo. Formal analysis of fairness in E-payment protocol based on strand space. WISM’09, LNCS5854, Berlin: Springer-Verlag, 2009: 469-478.
[59] Yang Jie, Ma Xianheng, Li Yi. Enhanced Strand Space for secure protocol analysis, Conference on Anti-counterfeiting, Security, and Identification in Communication, Hong Kong: IEEE Press, 2009: 374-377.
[60] Guo Yuyan, Wei Shimin. Strand space model of amended NS protocol and its analysis, World Congress on Computer Science and Information Engineering, Los Angeles: IEEE Press, 2009: 439-442.
[61] Bellare M, Rogaway P. Entity authentication and key distribution. Advances in Cryptology- CRYPTO’93, Berlin: Springer-Verlag, 1993: 232-249.
[62] Bellare M, Rogaway P. Provably secure session key distribution: the three party case. Proc. of the 27th ACM Symposium on the Theory of Computing, New York: ACM Press, 1995: 57-66.
[63] Bellare M, Pointcheval D, Rogaway P. Authenticated key exchange secure against dictionary attacks. Advances in Cryptology- Eurocrypt 2000, Berlin: Springer-Verlag, 2000: 139-155.
[64] Bresson E, Chevassut O, Pointcheval D. Dynamic group Diffie-Hellman key exchange under standard assumptions. Advances in Cryptology- Eurocrypt’02, Berlin: Springer-Verlag, 2002: 321-336.
[65] Abdalla M, Fouque P A, Pointcheval D. Password-based authenticated key exchange in the three-party setting. IEEE Proceedings - Information Security, 2006, 153(1): 27-39.
[66] Bellare M, Canetti R, Krawczyk H. A modular approach to the design and analysis of authentication and key-exchange protocols. Proc. of the 30th Annual Symp. on the Theory of Computing, New York: ACM Press, 1998: 419-428.
[67] Canetti R, Krawczyk H. Analysis of key exchange protocols and their use for building secure channels. Proc. of Eurocrypt’01, Berlin: Springer-Verlag, 2001: 453-474.
[68]李兴华,马建峰,文相在.基于身份密码系统下Canetti-Krawczyk模型的安全扩展.中国科学E辑:信息科学, 2004, 34(10): 106-113.
[69]张帆,无线网络安全协议的形式化分析方法.西安电子科技大学,博士学位论文, 2007.
[70]冯登国,陈伟东.基于口令的安全协议的模块化设计与分析.中国科学E辑:信息科学, 2007, 37(2): 223-237.
[71] Canetti R. Universally composable security: a new paradigm for cryptographic protocols. Proc. of the 42nd IEEE Symposium on Foundations of Computer Science, Oakland, CA: IEEE Press, 2001: 136-145.
[72] Barak B, Canetti R, Nielsen J N, et al. Universally composable protocols with relaxed set-up assumptions. Proc. of 45th FOCS, Washington: IEEE Press, 2004: 186-195.
[73] Yao A, Yao F F, Zhao Y. A note on universal composable zero knowledge in common reference string model. Proc. of TAMC’07, Shanghai: IEEE Press, 2007: 462-473.
[74] Kurosawa K, Furukawa J. Universally composable undeniable signature. Proc. of ICALP’08, Berlin: Springer-Verlag, 2008: 524-535.
[75] Hu Zhenyu, Jiang Jiangchun, Sun Fuchun. Using IND-CVA for constructing secure communication. Science in China Series F: Information Sciences, 2009, 52(10): 1801-1811.
[76]雷飞宇, UC安全多方计算模型及其典型应用研究.上海交通大学,博士学位论文, 2007.
[77] Yao A, Yao F F, Zhao Y. A note on universal composable zero knowledge in common reference string model. TAMC’07, Shanghai: Springer-Verlag, 2007: 462-473.
[78]张帆,马建峰,文相在.通用可组合的匿名HASH认证模型.中国科学E辑:信息科学, 2007, 37(2): 272-284.
[79]杨超,曹春杰,马建峰.通用可组合安全的Mesh网络认证协议.西安电子科技大学学报, 2007, 34(5): 814-817.
[80]冯涛.通用可复合密码协议理论及其应用研究.西安电子科技大学,博士学位论文, 2009.
[81]贾洪勇.安全协议的可组合性分析与证明.北京邮电大学,博士学位论文, 2009.
[82] Abadi M, Rogaway P. Reconciling two views of cryptography: the computational soundness of formal encryption. Journal of Cryptology. 2002, 15(2): 103-127.
[83] Micciancio D, Warinschi B. Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. Journal of Computer Security, 2004, 12(1): 99-129.
[84] Gligor V, Horvitz D O. Weak key authenticity and the computational completeness of formal encryption. 23rd Annual Int’l Cryptology Conference, Berlin: Springer-Verlag, 2003: 530-547.
[85] Micciancio D, Warinschi B. Soundness of formal encryption in the presence of active adversaries. Theory of Cryptography Conference. Berlin: Springer-Verlag, 2004: 133-151.
[86] Herzog J. Computational soundness for standard assumptions of formal cryptography. Massachusetts Institute of Technology, Ph. D. dissertation, 2004.
[87] Millen J, Shmatikov V. Symbolic protocol analysis with products and Diffie-Hellman exponentiation. Proc. of 16th IEEE Computer Security Foundations Workshop, New York: IEEE Press, 2003: 47-61.
[88] Abadi M, Cortier V. Deciding knowledge in security protocols under equational theories. Theoretical Computer Science, 2006, 2(1): 2-32.
[89] Canetti R, Herzog J. Universally composable symbolic analysis of mutual authentication and key-exchange protocols. Theory of Cryptography Conference, Berlin: Springer-Verlag, 2006: 380-403.
[90]田园,王颖,金峰等,基于刚性与相似性概念的密码协议分析方法.计算机学报, 2009, 32(4): 618-634.
[91] Lowe G. A hierarchy of authentication specifications. In 10th Computer Security Foundations Workshop Proceedings, Massachusetts: IEEE Press, 1997: 31-43.
[92] Goldreich O. Foundations of Cryptography. Cambridge: Cambridge University Press, 2001.
[93] Lomas T, Li Gong, Saltzer J, et al. Reducing risks from poorly chosen keys. ACM Operating Systems Review, 1989, 23(5): 14-18.
[94] Bellovin S, Merritt M. Augumented encrypted key exchange: a password-based protocol secure against dictionary attacks and password file compromise. Proc. of CCS’93, New York: ACM Press, 1993: 244-250.
[95] Wu T. A real world analysis of Kerberos password security. Proc. of the Symposium on Network and Distributed Systems Security (NDSS’99), San Diego: IEEE Press, 1999: 3-5.
[96]李莉,薛锐,张焕国等.基于口令认证的密钥交换协议的安全性分析.电子学报, 2005, 33(1): 166-170.
[97] Gong L, Mark T. Lomas, et al. Protecting poorly chosen secrets from guessing attacks. IEEE Journal on Selected Areas in Communications, 1993, 11(5): 648-656.
[98] Halevi S, Krawczyk H. Public-key cryptography and password protocols. ACM Transaction on Information and System Security, 1999, 2(3): 230-268.
[99] Boyko V, Mackenzie P, Patel S. Provably secure password authenticated key exchange using diffie-hellman. Proc. of Advances in Cryptology– Eurocrypt 2000, Berlin: Springer-Verlag, 2000: 156-171.
[100] Katz J, Ostrovsky R, Yung M. Efficient password-authenticated key exchange using human-memorable passwords. Proc. of Advances in Cryptology– Eurocrypt 2001, Berlin: Springer-Verlag, 2001: 475-494.
[101] Malladi S, Alves-Foss J, Malladi S. Preventing guessing attacks using fingerprint biometrics. 16th IEEE Computer Security Foundations Workshop, Washington: IEEE Press, 2003: 24-30.
[102] Lowe G. Analyzing protocols subject to guessing attack. Journal of Computer Security, 2004, 12(1): 83-98.
[103] Corin R, Doumen J, Etalle S. Analyzing password protocol security against off-line dictionary attacks. Electronic Notes in Theoretical Computer Science, 2005, 121(4): 47-63.
[104]龙士工,罗文俊,袁超伟等.串空间模型中的口令猜测攻击.北京邮电大学学报, 2007, 30(1): 62-65.
[105]毛晨晓,罗文坚,王煦法.分析安全协议猜测攻击的模态逻辑方法.计算机学报, 2007, 30(6): 924-933.
[106] Abdalla M, Catalano D, Chevalier C. Efficient two-party password-based key exchange protocols in the UC framework. Cryptographers’Track at the RSA Conference 2008, San Francisco: ACM Press, 2008: 335-351.
[107]谭示崇.口令认证密钥协商协议的研究.西安电子科技大学,博士学位论文, 2009.
[108] Delaune S, Jacquemard F. A theory of dictionary Attacks and its Complexity. Proc. of the 17th Computer Security Foundations Workshop, Pacific Grove: IEEE Press, 2004: 2-15.
[109] Hwang M S, Lo J W, Liu C H. Simple authenticated key agreement and protected password change protocol. Compute Security, 2005, 24(2): 500-504.
[110] Wang C I, Fan C I, Guan D J. Cryptanalysis on Chang-Yang- Hwang protected password change protocol. Advances in Cryptology– Eurocrypt 2005, Berlin: Springer-Verlag, 2005: 147-209.
[111] Lin C L, Sun H M, and Hwang T. Three party-encrypted key exchange: attacks and a solution. ACM Operating System Review, 2000, 34(4): 12-20.
[112] Sun H M, Chen B, and Hwang T. Secure key agreement protocols for three-party against guessing attacks. The Journal of Systems and Software, 2005, 75(2): 63-68.
[113] Steiner M, Tsudik G, and Wainder M. Refinement and extension of encrypted key exchange. ACM Operation Systems Review, 1995, 29(3): 22-30.
[114] Ota H, Yoneyama K, and Kiyomoto S, et al. Universally composable client-to-client general authenticated key exchange. Transactions of Information Processing Society of Japan, 2007, 48(9): 3073-3088.
[115] Even S. A randomized protocol for signing contracts. Communications of the ACM, 1985, 28(6): 637-647.
[116]熊焰,张伟超,苗付友等.一种基于计算能力的无需可信第三方公平非抵赖信息交换协议.电子学报, 2006, 34(3): 563-566.
[117] Coffey T, Non-repudiation with mandatory proof of receipt. Computer Communication Review, 1996, 26(1): 6-17.
[118] Han S, Chang E, Dillon T. Secure e-transactions protocol using intelligent mobile agents with fair privacy. Studies in Computational Intelligence, 2007, 37(3): 307-326.
[119] Oniz C, Savas E, Levi A. An optimistic fair e-commerce protocol for large e-goods. Proc. of the 7th IEEE International Symposium on Computer Networks, Nevada: IEEE Press, 2006: 214-219.
[120] Liang Xiaohui, Cao Zhenfu, Lu Rongxing. Efficient and secure protocol in fair document exchange. Computer Standards & Interfaces, 2008, 30(3): 167-176.
[121]樊利民,廖建新.公平的移动小额支付协议.电子与信息学报, 2007, 29(11): 2659-2602.
[122] Asokan N, Shoup V, Waidner M. Optimistic fair exchange of digital signatures, IEEE Journal on Selected Areas in Communications, 2000, 18(4): 593-610.
[123] Almudena A, Juan M, Izquierdo A. A formal analysis of fairness and non-repudiation in the RSA-CEGD protocol. International Conference on Computational Science and Its Applications, Singapore: IEEE Press, 2005: 1309-1318.
[124]文静华,李祥,张焕国等.基于ATL的公平电子商务协议形式化分析.电子与信息学报, 2007, 29(4): 901-905.
[125] Sornkhom P, Permpoontanalarp Y. Security analysis of Micali’s fair contract signing protocol by using colored petri nets. Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing, Australia: IEEE Press, 2008: 329-334.
[126] Aybek M, Steve K, Eike R. Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model. International Conference on Financial Cryptography and Data Security, Roseau: IEEE Press, 2005: 255-269.
[127] Okada Y, Manabe Y, Okamoto T. An optimistic fair exchange protocol and its security in the universal composability framework. Int. J. of Applied Cryptography, 2008, 1(1): 70-78.
[128] Chaum D, Damgard I, Pedersen T. Convertible undeniable signatures. In CRYPTO’90, Berlin: Springer-Verlag, 1990: 189-205.
[129] Boyd C, Foo E. Off-line fair payment protocols using convertible signatures. Advances in Cryptology ASIACRYPT'98, Berlin: Springer-Verlag, 1998: 271-285.
[130] Park J M, Edwin K P, Siegel H J. Constructing fair-exchange protocols for e-commerce via distributed computation of RSA signatures. Proc. of the 20th Annual-Symposium on Principles of Distributed Computing. USA: ACM Press, 2003: 172-181.
[131] Garfinkel S L, Juels A, Pappu R. RFID privacy: an overview of problems and proposed solutions. Security & Privacy Magazine, 2005, 3(3): 34-43.
[132] Juels A, Ronald L, Rivest R, et al. The blocker tag: selective blocking of RFID tags for consumer privacy. 10th Conference on Computer and communications security. Washington: ACM Press, 2003: 103-111.
[133] Karjoth G, Paul A, Moskowitz. Disabling RFID tags with visible confirmation: clipped tags are silenced. ACM Workshop on Privacy in Electronic Society. Alexandria: ACM Press, 2005: 27-30.
[134] Hopper N J, Blum M. Secure human identification protocols. 7th International Conference on the Theory and Application of Cryptology and Information Security. Berlin: Springer-Verlag, 2001: 52-66.
[135] Gilbert H, Matthew R, Sibert H. An active attack against HB+: a provably secure lightweight authentication protocol. IEE Electronics Letters, 2005, 41(21): 1169-1170.
[136] Sarma S E, Weis S A, Engels D W. Radio-frequency identification: secure risks and challenges. RSA Laboratories Cryptobytes, 2003, 6(1): 2-9.
[137] Weis S A, Sarma S E, Rivest R, et, al. Security and privacy aspects of low-cost radio frequency identification systems. Proc. of the 1st International Conference on Security in Pervasive Computing. Berlin: Springer-Verlag, 2004: 201-212.
[138]周永彬,冯登国. RFID安全协议的设计和分析.计算机学报, 2006, 29(4): 581-589.
[139] Lee S M, Hwang Y J, Lee D H. Efficient authentication for low-cost RFID systems. Proc. of the International Conference on Computational Science and Its Applications (ICCSA2005). Berlin: Springer-Verlag, 2005: 619-627.
[140] Molnar D, Soppera A, Wagner D. A scalable, delegatable pseudonym protocol enabling ownership transfer of RFID tags. Workshop on Selected Areas in Cryptography. Berlin: Springer-Verlag, 2006: 276-290.
[141] van Le T, Burmester M, Medeiros B. Universally composable and forward secure RFID authentication and authenticated key exchange. Proc. of the 2nd ACM Symposium on Information, Computer and Communications Security. New York: ACM, 2007: 242-252.
[142] Tsudik G. YA-TRAP: yet another trivial RFID authentication protocol. Proc. of the 4th annual IEEE International Conference on Pervasive Computing and Communications Workshops. Washington: IEEE Press, 2006: 640-651.
[143] Kim H S, Choi J Y. The design and verification of RFID authentication protocol for ubiquitous computing. Proc. of the 18th International Workshop on Database and Expert Systems Applications. Washington: IEEE Press, 2007: 693-697.
[144] Burmester M, van Le T, Medeiros B. Provably secure ubiquitous systems: Universally composable RFID authentication protocols. Proc. of the 2nd International Conference on Security and Privacy in Networks. Maryland: IEEE Press, 2006: 176-186.
[145]邓淼磊,黄照鹤,周利华等.认证协议中数据同步的分析.计算机科学, 2010, 37(3): 83-85.
[146]丁振华,李锦涛,冯波.基于Hash函数的RFID安全认证协议研究.计算机研究与发展, 2009, 46(4): 583-592.
[147]丁治国. RFID关键技术研究与实现.中国科学技术大学,博士学位论文, 2009.
[148] EPC Class 1 Gen 2 standard. http://www.epcglobalinc.org/standards/uhfc1g2/
[149] Duc D C, Park J, Lee H, et al. Enhancing security of EPCglobal Gen-2 RFID tag against traceability and cloning. Symposium on Cryptography and Information Security, Hiroshima: ACM Press, 2006: 269-277.
[150] Chien H Y, Chen C H. Mutual authentication protocol for RFID conforming to EPC Class 1 Generation 2 standards. Computer Standards & Interfaces, 2007, 26(2): 254-259.
[151] Cai Q L, Zhan Y J, Wang Y H. A minimalist mutual authentication protocol for RFID system & BAN logic analysis. ISECS International Colloquium Computing, Communication, Control, and Management, Guangzhou: IEEE Press, 2008: 449-453.
[152] Choi E Y, Lee D H, Lin J. Anti-cloning protocol suitable to EPCglobal Class-1 Generation-2 RFID systems. Computer Standards & Interfaces, 2009, 31(6): 1124-1130.
[153] Seo D H, Baek J M, Cho D S. Secure RFID authentication scheme for EPC Class Gen2. International Conference on Ubiquitous Information Management and Communication, Suwon: IEEE Press, 2009: 221-227.
[154] Sun H M, Ting W C. A Gen2-based RFID authentication protocol for security and privacy. IEEE Transactions on Mobile Computing, 2009, 8(1): 1-11
[155] Tan C C, Sheng B, Li Q. Serverless search and authentication protocols for RFID. 5th Annual IEEE International Conference on Pervasive Computing and Communications, New York: IEEE Press, 2007: 34-41.
[156] Ahamed S, Rahman F, Hoque E, et al. S3PR: secure serverless search protocols for RFID. International Conference on Information Security and Assurance, Hawaii: IEEE Press, 2008: 187-192.
[157] Li Yingjiu, Ding Xuhua. Protecting RFID communications in supply chains. Proc. of the ACM Symposium on Information, Computer, and Communications Security, Singapore: ACM Press, 2007: 234-241.
[158]张帆,孙璇,马建峰等.供应链环境下通用可组合安全的RFID通信协议.计算机学报, 2008, 31(10): 1754-1767.
[159] Juels A, Pappu R, Parno B. Unidirectional key distribution across time and space with applications to rfid security. 17th USENIX Security Symposium, San Jose: ACM Press, 2008: 75-90.
[160] Han S H, Chu C H. Tamper detection in RFID-enabled supply chains using fragile watermarking. International Conference on RFID, Las Vegas: IEEE Press, 2008: 111-117.
[161] Canetti R. Universally composable signature, certification and authentication. 17th IEEE computer security foundations workshop. Dallas: IEEE Press, 2004: 219-245.
[162] Coppersmith D, Krawczyk H, Mansour Y. The shrinking generator. Proc. Advances in Cryptology (CRYPTO 1994), Berlin: Springer-Verlag, 1994: 22-39.
[163] Burmester M, Munilla J. A flyweight RFID authentication protocol. 5th Workshop on RFID Security, Leuven: IEEE Press, 2009: 1-13.
[164] Rotter P. A framework for assessing RFID system security and privacy risks. Pervasive Computing, 2008, 7(4): 70-77.
[165] Yamamoto A, Suzuki S, Hada H. A tamper detection method for RFID tag data. IEEE RFID 2008, Las Vegas, NV: IEEE Press, 2008: 51-57.
[166] Lin J, Oh H, Kim S. A new hash-based RFID mutual authentication protocol providing enhanced user privacy protection. In ISPEC 2008, Berlin: Springer-Verlag, 2008: 278-280.
[167] Juels A, Weis S. Defining strong privacy for RFID. In International Conference on Pervasive Computing and Communications, New York: IEEE Press, 2007: 342-347.
[168] Garcia F D, Hasuo I, Pieters W, et al. Provable anonymity. In FMSE, Virginia: IEEE Press, 2005: 63-72.
[169] Ouafi K, Phan R. Traceable privacy of recent provably-secure RFID protocols. In ACNS’08, New York: ACM Press, 2008: 479-489.
[170] Ha J, Moon S, Zhou J, Ha J. A new formal proof model for RFID location privacy. In ESORICS, Berlin: Springer-Verlag, 2008: 267-281.
[171] van Deursen T, Radomirovic S. On a new formal proof model for RFID location privacy. Information Processing Letters, 2009, 110(2): 57-61.
[172] Feldhofer M, Dominikus S, Wolkerstorfer J. Strong authentication for RFID systems using the AES algorithm. In CHES’04, Berlin: Springer-Verlag, 2004: 357-370.