电子商务安全协议的设计与形式化分析
|
摘要
随着计算机网络的飞速发展,电子商务逐渐成为人们进行商务活动的新模式。电子商务安全协议是构建电子商务安全环境的基础,是保障电子商务顺利应用与发展的关键技术。电子商务安全协议是以密码学为基础的消息交换协议,参与者采取的一系列步骤去完成某一任务,其目的是在网络信道不可靠的情况下,确保通信安全以及传输数据的安全。
电子商务安全协议除了需满足传统安全协议所需满足的认证性、保密性和完整性外,还需满足可追究性、公平性、时限性及匿名性等安全属性。因此电子商务安全协议的设计与分析面临着诸多困难和挑战,也成为了信息安全领域中的一个重要课题,具有重要的理论意义和现实应用价值。
本文主要围绕电子商务安全协议的设计以及形式化分析技术展开研究,取得了些研究成果。
对电子商务安全协议的基本概念、分类及其安全属性进行了综述和分析,对电子商务安全协议安全性设计及形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。
指出了一个认证电子邮件协议在可追究性和公平性上存在的安全缺陷,在此基础上提出了一种基于在线第三方的认证电子邮件协议,以满足认证电子邮件的一般安全特性。利用扩展Kailar逻辑对该协议进行分析,说明该协议满足不可否认性及公平性,并具有抗篡改、重放等攻击、及第三方无法获得邮件内容等优点。
采用组合协议分析方法及PCL逻辑分析了ECS2协议的弱公平性。指出了ZZW协议存在不满足保密性、可追究性和公平性的安全缺陷,并提出了改进方案。提出一种结合组合协议分析以及Kailar逻辑的分析思路,用于分析基于离线第三方的电子商务安全协议的可追究性及公平性,并分析了改进后的ZZW协议,证明了该协议能够弥补原协议的安全隐患。
针对移动环境中网络及计算条件受限的情况,在考虑有效性和支付效率的基础上,设计了一个适应于移动环境的公平移动支付协议。该协议由认证、支付、恢复、结算四个子协议构成。在认证协议中通过基于Hash函数的动态ID机制满足了双向认证、有限的匿名性和不可追踪性,并获取不可伪造性的、可重用的支付证书。在支付过程中基于变色龙Hash函数和双Hash链,实现了交易的匿名性、可追究性和公平性。最后利用Kailar逻辑对协议的可追究性和公平性进行了形式化分析,结果表明,协议在保持较高执行效率的同时能满足可追究性和公平性,适用于在移动环境以及类似的通信、计算条件受限的环境中使用。
针对一般信念逻辑难于分析乐观公平交换协议的公平性和时限性的现状,将乐观公平交换协议定义为类似于Kripke结构的状态转换系统,对扩展Kailar逻辑增加了时间限定条件及状态转换分析。在分析不可否认证据有效性的基础上,通过考察主体认知及信仰的转换过程,达到分析乐观公平交换协议的公平性和时限性的目的。同时,对一个典型的乐观公平交换协议进行了分析,发现了该协议存在的两个安全缺陷,并给出了改进方案。
指出了一个典型的多方认证邮件协议存在不满足公平性、可追究性以及个别不诚实参与方行为会导致整个协议执行失败等安全隐患。基于签密方案,对该协议进行了改进,并利用Kailar逻辑对改进后的协议的安全属性进行了分析。研究结果表明,该协议能够满足保密性、不可否认性及公平性,并具有抗篡改、重放、合谋等攻击的特点。
本文的研究工作对于电子商务安全协议的设计以及形式化分析技术有一定的理论和实用意义,同时对于提高电子商务活动的安全性也具有一定的价值。
With the rapid development of network technology, Electronic commerce (E-commerce) has become a new model for ordinary business. E-commerce security protocol is cornerstones of building security e-commerce environment and works as a kind of the kernel technology for application and development of e-commerce successfully. E-commerce security protocol is a message exchange protocol based on cryptography. The participants adopted a series of steps to accomplish a task in these protocols which is ensured the security communication and data transmission security in unreliable network channel.
E-commerce security protocols need to fulfill some special security attributes such as non-repudiation, fairness, timeliness and anonymity besides other attributes in traditional security protocols like authentication, confidentiality and integrity. Therefore, the design and formal analysis of E-commerce security protocols has been facing many difficulties and challenges and has been becoming an important research direction in the area of information security. Furthermore, the design and formal analysis of E-commerce security protocols has important theoretical and application value.
This paper make further study on the design and formal analysis of E-commerce security protocols. The main works and results are as follows:
Basic theories, classification and security attributes of E-commerce security protocols are reviewed and analyzed. Simultaneously, the main methods of formal analysis for e-commerce security protocols are reviewed, and the advantages, disadvantages and problems of each method are discussed.
The security flaws of a certified E-mail protocol have been pointed out. In order to meet the general security attributes in certified E-mail protocol, an improved protocol was proposed based on Online TTP. The improved protocol analyzed by extended Kailar logic can achieve the non-repudiation, fairness as well as the other advantages that it can resist the attacks as distort, replay and the TTP can't read the E-mail.
The method of compositional analysis and PCL logic is introduced, and the weak fairness of ECS2is analyzed by this method. Aiming at to remedy the lack of fairness and non-repudiation of a typical certified mail protocol(ZZW protocol), an improved certified mail protocol with transparent semi-trusted third party is proposed. To improve the protocol analysis efficiency, a method applying Kailar logic in compositional analysis is proposed for analyzing the improved protocol. The analysis results indicate the improved protocol can meet fairness and non-repudiation.
Considering the condition of network and the calculation capability of mobile terminal is limited in the mobile environment, the novel fair mobile payment protocol was proposed. The protocol is composed of four sub-protocols:authentication, payment, recovery and withdraw. In authentication sub-protocol, the dynamic ID mechanism based on the hash function is adopted to satisfy mutual authentication, the limited anonymity and intractability, and the unforgeable and reusable payment certificate is obtained. In the process of payment, the attribute of anonymity, non-repudiation and fairness, is achieved based on Chameleon Hash functions and double Hash chain. Finally, through formal analyzing the security attributes by Kailar logic, the result declares that of the protocol can fulfill the non-repudiation and fairness based on the higher efficiency in the implementation. The protocol can be applied to mobile environment and similar communication and calculate conditions constrained environments.
Aiming at the circumstance that generic faith logic is difficult to analyze the fairness and timeliness of optimistic fair exchange protocol, we defined the optimistic fair exchange protocol as a state transition system with a structure similar to Kripke, and added time limit conditions and state transition analysis into extended Kailar Logic. By means of discussing the conversion process of cognition and faith of principals based on the investigation of validity of non-repudiation evidence, the fairness and timeliness of the protocol is analyzed. We analyzed a typical optimistic fair exchange protocol. Two flaws of the protocol are discovered and an improved protocol was proposed.
The security flaws of a Multi-Party certified E-mail protocol have been pointed out. We declare the protocol can not meet fairness, non-repudiation and the security risks that the implementation of the protocol will be led to failure by individual acts of dishonesty. An improved protocol was proposed based on signcryption scheme. Through the analysis by Kailar logic, it is can be seen the improved protocol can achieve the non-repudiation, fairness. Furthermore, it has advantage of resisting the attacks as distort, replay and conspiracy.
There are some theoretical and practical significance in design and formal analysis of e-commerce security protocols in this paper. Simultaneously, the studies of this paper also have some value for promoting the security of e-commerce.
电子商务安全协议除了需满足传统安全协议所需满足的认证性、保密性和完整性外,还需满足可追究性、公平性、时限性及匿名性等安全属性。因此电子商务安全协议的设计与分析面临着诸多困难和挑战,也成为了信息安全领域中的一个重要课题,具有重要的理论意义和现实应用价值。
本文主要围绕电子商务安全协议的设计以及形式化分析技术展开研究,取得了些研究成果。
对电子商务安全协议的基本概念、分类及其安全属性进行了综述和分析,对电子商务安全协议安全性设计及形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。
指出了一个认证电子邮件协议在可追究性和公平性上存在的安全缺陷,在此基础上提出了一种基于在线第三方的认证电子邮件协议,以满足认证电子邮件的一般安全特性。利用扩展Kailar逻辑对该协议进行分析,说明该协议满足不可否认性及公平性,并具有抗篡改、重放等攻击、及第三方无法获得邮件内容等优点。
采用组合协议分析方法及PCL逻辑分析了ECS2协议的弱公平性。指出了ZZW协议存在不满足保密性、可追究性和公平性的安全缺陷,并提出了改进方案。提出一种结合组合协议分析以及Kailar逻辑的分析思路,用于分析基于离线第三方的电子商务安全协议的可追究性及公平性,并分析了改进后的ZZW协议,证明了该协议能够弥补原协议的安全隐患。
针对移动环境中网络及计算条件受限的情况,在考虑有效性和支付效率的基础上,设计了一个适应于移动环境的公平移动支付协议。该协议由认证、支付、恢复、结算四个子协议构成。在认证协议中通过基于Hash函数的动态ID机制满足了双向认证、有限的匿名性和不可追踪性,并获取不可伪造性的、可重用的支付证书。在支付过程中基于变色龙Hash函数和双Hash链,实现了交易的匿名性、可追究性和公平性。最后利用Kailar逻辑对协议的可追究性和公平性进行了形式化分析,结果表明,协议在保持较高执行效率的同时能满足可追究性和公平性,适用于在移动环境以及类似的通信、计算条件受限的环境中使用。
针对一般信念逻辑难于分析乐观公平交换协议的公平性和时限性的现状,将乐观公平交换协议定义为类似于Kripke结构的状态转换系统,对扩展Kailar逻辑增加了时间限定条件及状态转换分析。在分析不可否认证据有效性的基础上,通过考察主体认知及信仰的转换过程,达到分析乐观公平交换协议的公平性和时限性的目的。同时,对一个典型的乐观公平交换协议进行了分析,发现了该协议存在的两个安全缺陷,并给出了改进方案。
指出了一个典型的多方认证邮件协议存在不满足公平性、可追究性以及个别不诚实参与方行为会导致整个协议执行失败等安全隐患。基于签密方案,对该协议进行了改进,并利用Kailar逻辑对改进后的协议的安全属性进行了分析。研究结果表明,该协议能够满足保密性、不可否认性及公平性,并具有抗篡改、重放、合谋等攻击的特点。
本文的研究工作对于电子商务安全协议的设计以及形式化分析技术有一定的理论和实用意义,同时对于提高电子商务活动的安全性也具有一定的价值。
With the rapid development of network technology, Electronic commerce (E-commerce) has become a new model for ordinary business. E-commerce security protocol is cornerstones of building security e-commerce environment and works as a kind of the kernel technology for application and development of e-commerce successfully. E-commerce security protocol is a message exchange protocol based on cryptography. The participants adopted a series of steps to accomplish a task in these protocols which is ensured the security communication and data transmission security in unreliable network channel.
E-commerce security protocols need to fulfill some special security attributes such as non-repudiation, fairness, timeliness and anonymity besides other attributes in traditional security protocols like authentication, confidentiality and integrity. Therefore, the design and formal analysis of E-commerce security protocols has been facing many difficulties and challenges and has been becoming an important research direction in the area of information security. Furthermore, the design and formal analysis of E-commerce security protocols has important theoretical and application value.
This paper make further study on the design and formal analysis of E-commerce security protocols. The main works and results are as follows:
Basic theories, classification and security attributes of E-commerce security protocols are reviewed and analyzed. Simultaneously, the main methods of formal analysis for e-commerce security protocols are reviewed, and the advantages, disadvantages and problems of each method are discussed.
The security flaws of a certified E-mail protocol have been pointed out. In order to meet the general security attributes in certified E-mail protocol, an improved protocol was proposed based on Online TTP. The improved protocol analyzed by extended Kailar logic can achieve the non-repudiation, fairness as well as the other advantages that it can resist the attacks as distort, replay and the TTP can't read the E-mail.
The method of compositional analysis and PCL logic is introduced, and the weak fairness of ECS2is analyzed by this method. Aiming at to remedy the lack of fairness and non-repudiation of a typical certified mail protocol(ZZW protocol), an improved certified mail protocol with transparent semi-trusted third party is proposed. To improve the protocol analysis efficiency, a method applying Kailar logic in compositional analysis is proposed for analyzing the improved protocol. The analysis results indicate the improved protocol can meet fairness and non-repudiation.
Considering the condition of network and the calculation capability of mobile terminal is limited in the mobile environment, the novel fair mobile payment protocol was proposed. The protocol is composed of four sub-protocols:authentication, payment, recovery and withdraw. In authentication sub-protocol, the dynamic ID mechanism based on the hash function is adopted to satisfy mutual authentication, the limited anonymity and intractability, and the unforgeable and reusable payment certificate is obtained. In the process of payment, the attribute of anonymity, non-repudiation and fairness, is achieved based on Chameleon Hash functions and double Hash chain. Finally, through formal analyzing the security attributes by Kailar logic, the result declares that of the protocol can fulfill the non-repudiation and fairness based on the higher efficiency in the implementation. The protocol can be applied to mobile environment and similar communication and calculate conditions constrained environments.
Aiming at the circumstance that generic faith logic is difficult to analyze the fairness and timeliness of optimistic fair exchange protocol, we defined the optimistic fair exchange protocol as a state transition system with a structure similar to Kripke, and added time limit conditions and state transition analysis into extended Kailar Logic. By means of discussing the conversion process of cognition and faith of principals based on the investigation of validity of non-repudiation evidence, the fairness and timeliness of the protocol is analyzed. We analyzed a typical optimistic fair exchange protocol. Two flaws of the protocol are discovered and an improved protocol was proposed.
The security flaws of a Multi-Party certified E-mail protocol have been pointed out. We declare the protocol can not meet fairness, non-repudiation and the security risks that the implementation of the protocol will be led to failure by individual acts of dishonesty. An improved protocol was proposed based on signcryption scheme. Through the analysis by Kailar logic, it is can be seen the improved protocol can achieve the non-repudiation, fairness. Furthermore, it has advantage of resisting the attacks as distort, replay and conspiracy.
There are some theoretical and practical significance in design and formal analysis of e-commerce security protocols in this paper. Simultaneously, the studies of this paper also have some value for promoting the security of e-commerce.
引文
[1]B Schneier.Applied Cryptography:Protocols, Algorithms, and Source Code in C, Second Edition. John Wiley&Sons, Inc.1996.
[2]A Freier. The SSL protocol version 3.0 [J]. http://wp.netscape.com/eng/ss13/ draft302.txt,1996.
[3]SET Secure Electronic Transaction Specification Book 1:Business Description, Version 1.01997. http://www.setco.org/download.html#spec
[4]SET Secure Electronic Transaction Specification Book 2:Programmer's Guide, Version 1.01997, http://www.setco.org/download.html#spec
[5]SET Secure Electronic Transaction Specification Book 3:Formal Protocol Definition Version 1.0.1997. http://www.setco.org/download.html#spec
[6]K O'Toole. The Internet Billing Server:Transaction Protocol Alternatives[D]. Carnegie Mellon University. Information Networking Institute,1994.
[7]N Asokan, V Shoup, Waidner M. Asynchronous protocols for optimistic fair exchange[C]//Security and Privacy,1998. Proceedings.1998 IEEE Symposium on IEEE,1998:86-99.
[8]卿斯汉.安全协议20年研究进展[J].软件学报,2003,14(10)：1740-1752.
[9]R M Needham, M D Schroeder. Using encryption for authentication in large networks of computers [J]. Communications of the ACM,1978,21(12):993-999.
[10]G Lowe. An attack on the Needham-Schroeder public-key authentication protocol[J]. Information processing letters,1995,56(3):131-133.
[11]薛锐,冯登国.安全协议的形式化分析技术与方法[J].计算机学报,2006,29(1)：1-20.
[12]M Burrows, M Abadi, R M Needham. A logic of authentication[J]. Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences,1989,426(1871): 233-271.
[13]TYC Woo, SS Lam. A semantic model for authentication protocols[C]//Research in Security and Privacy,1993. Proceedings.1993 IEEE Computer Society Symposium on. IEEE,1993:178-194.
[14]R Kemmerer, C Meadows, J Millen. Three systems for cryptographic protocol analysis[J]. Journal of CRYPTOLOGY,1994,7(2):79-130.
[15]D Dolev, A Yao. On the security of public key protocols[J]. Information Theory, IEEE Transactions on,1983,29(2):198-208.
[16]CCITT R X.509:The Directory Authentication Framework[J].1988.
[17]SP Miller, BC Neuman, JI Schiller, et al. Kerberos authentication and authorization system[C]//In Project Athena Technical Plan.1987.
[18]L Gong, R Needham, R Yahalom. Reasoning about belief in cryptographic protocols[C] //Research in Security and Privacy,1990. Proceedings.,1990 IEEE Computer Society Symposium on. IEEE,1990:234-248.
[19]M Abadi, MR Turtle. A semantics for a logic of authentication[C]//Proceedings of the tenth annual ACM symposium on Principles of distributed computing. ACM,1991: 201-216.
[20]P van Oorschot. Extending cryptographic logics of belief to key agreement protocols[C] //Proceedings of the 1 st ACM Conference on Computer and Communications Security. ACM,1993:232-243.
[21]P Syverson. A taxonomy of replay attacks cryptographic protocols[C]//Computer Security Foundations Workshop Ⅶ,1994. CSFW 7. Proceedings. IEEE,1994: 187-191.
[22]P Bieber. A logic of communication in hostile environment[C]//Computer Security Foundations Workshop Ⅲ,1990. Proceedings. IEEE,1990:14-22.
[23]P Syverson. Formal semantics for logics of cryptographic protocols[C]//Computer Security Foundations Workshop Ⅲ,1990. Proceedings. IEEE,1990:32-41.
[24]S Gurgens. SG logic-a formal analysis technique for authentication protocols[C]// Security Protocols. Springer Berlin Heidelberg,1998:159-176.
[25]R Kailar. Accountability in electronic commerce protocols[J]. Software Engineering, IEEE Transactions on,1996,22(5):313-328.
[26]周典萃,卿斯汉,周展飞.Kailar逻辑的缺陷[J].软件学报,1999,10(12)：1238-1245.
[27]周典萃,卿斯汉,周展飞.一种分析电子商务安全协议的新工具[J].软件学报,2001,12(9)：1318-1328.
[28]卿斯汉.一种电子商务安全协议形式化分析方法[J].软件学报,2005,16(10)：1757-1765.
[29]刘冬梅,卿斯汉,马恒太,等.一种离线TTP公平非否认协议的安全性分析方法[J].计算机研究与发展,2011,48(4)：656-665.
[30]黎波涛,罗军舟.不可否认协议时限性的形式化分析[J].软件学报,2006,17(7)：1510-1516.
[31]J Zhou, D Gollman. A fair non-repudiation protocol[C]//Security and Privacy,1996. Proceedings 1996 IEEE Symposium on. IEEE,1996:55-61.
[32]韩志耕,罗军舟.多方不可否认协议时限性分析与改进[J].电子学报,2009,37(2)：377-381.
[33]S Kremer, O Markowitch. Fair multi-party non-repudiation protocols[J]. International Journal of Information Security,2003,1(4):223-235.
[34]陈明,吴开贵,吴长泽,等.公平交换协议形式逻辑[J].Journal of Software,2011, 22(3).
[35]雷新锋,刘军,肖军模.时间相关密码协议逻辑及其形式化语义[J].软件学报,2011,22(003)：534-557.
[36]CAR Hoare. Communicating sequential processes[M]//Programming Languages. Springer Berlin Heidelberg,1983:306-317.
[37]G Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR[M]//Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg,1996:147-166.
[38]JC Mitchell, M Mitchell, Stern U. Automated analysis of cryptographic protocols using Murcp[C]//Security and Privacy,1997. Proceedings.,1997 IEEE Symposium on. IEEE,1997:141-151.
[39]D Basin, S Modersheim, L Vigano. OFMC:A symbolic model checker for security protocols[J]. International Journal of Information Security,2005,4(3):181-208.
[40]JK Millen, SC Clark, Freedman S B. The interrogator:Protocol secuity analysis[J]. Software Engineering, IEEE Transactions on,1987 (2):274-288.
[41]C Meadows. The NRL protocol analyzer:An overview[J]. The Journal of Logic Programming,1996,26(2):113-131.
[42]S Schneider. Formal analysis of a non-repudiation protocol[C]//Computer Security Foundations Workshop,1998. Proceedings.11th IEEE. IEEE,1998:54-65.
[43]N Evans, S Schneider. Verifying security protocols with PVS:widening the rank function approach[J]. The Journal of Logic and Algebraic Programming,2005,64(2): 253-284.
[44]K Wei, J Heather. Towards verification of timed non-repudiation protocols[M]// Formal Aspects in Security and Trust. Springer Berlin Heidelberg,2006:244-257.
[45]韩志耕,罗军舟,王良民.不可否认协议分析的增广CSP方法[J].通信学报,2008,29(10)：8-18.
[46]V Shmatikov, JC Mitchell. Analysis of a fair exchange protocol [C]//Proceedings of the Seventh Annual Symposium on Network and Distributed System Security (NDSS 2000).2000.
[47]V Shmatikov, JC Mitchell. Finite-state analysis of two contract signing protocols[J]. Theoretical Computer Science,2002,283(2):419-450.
[48]JA Garay, M Jakobsson, P MacKenzie. Abuse-free optimistic contract signing[C]// Advances in Cryptology-CRYPTO'99. Springer Berlin Heidelberg,1999:449-466.
[49]S Kremer, JF Raskin. Game analysis of abuse-free contract signing[C]//Computer Security Foundations Workshop,2002. Proceedings.15th IEEE. IEEE,2002:206-220.
[50]S Kremer, JF Raskin. A game-based verification of non-repudiation and fair exchange protocols[J]. Journal of Computer Security,2003,11(3):399-429.
[51]R Alur, TA Henzinger, Mang F Y C, et al. MOCHA:Modularity in model checking[C] //Computer Aided Verification. Springer Berlin Heidelberg,1998:521-525.
[52]文静华,李祥,张焕国,等.基于ATL的公平电子商务安全协议形式化分析[J].电子与信息学报,2007,29(4)：901-905.
[53]J Zhou, R Deng, F Bao. Evolution of fair non-repudiation with TTP[C]//Information Security and Privacy. Springer Berlin Heidelberg,1999:258-269.
[54]LC Paulson. Proving properties of security protocols by induction[C]//Computer Security Foundations Workshop,1997. Proceedings.,10th. IEEE,1997:70-83.
[55]LC Paulson. The inductive approach to verifying cryptographic protocols [J]. Journal of computer security,1998,6(1):85-128.
[56]M Wenzel. The isabelle/isar reference manual, http://www.cl.cam.ac.ul/research/hvg /Isabelle/documentation.html.
[57]G Bella, LC Paulson. Mechanical proofs about a non-repudiation protocol[M]// Theorem Proving in Higher Order Logics. Springer Berlin Heidelberg,2001:91-104.
[58]G Bella, LC Paulson. Accountability protocols:Formalized and verified[J]. ACM Transactions on Information and System Security (TISSEC),2006,9(2):138-161.
[59]M Abadi, AD Gordon. A calculus for cryptographic protocols:The spi calculus[C]// Proceedings of the 4th ACM conference on Computer and communications security. ACM,1997:36-47.
[60]R Milner, J Parrow, Walker D. A calculus of mobile processes, i[J]. Information and computation,1992,100(1):1-40.
[61]C Haack, A Jeffrey. Pattern-matching spi-calculus[J]. Information and Computation, 2006,204(8):1195-1263.
[62]M Bugliesi, R Focardi, M Maffei. Compositional analysis of authentication protocols[M]//Programming Languages and Systems. Springer Berlin Heidelberg, 2004:140-154.
[63]顾永跟,傅育熙.基于进程演算和知识推理的安全协议形式化分析[J].计算机研究与发展,2006,43(5)：953-958.
[64]顾永跟,傅育熙,朱涵.基于可达关系的安全协议保密性分析[J].计算机学报,2007,30(2)：255-261.
[65]顾永跟,李国强,王国钧.基于类pi演算的电子支付协议安全性形式化研究[J].计算机应用研究,2006,3：007.
[66]李援,蒋建国,王焕宝.spi演算证明协议非可否认性[J].通信学报,2009,5：014.
[67]J Zhou, D Gollmann. An efficient non-repudiation protocol [C]//Computer Security Foundations Workshop,1997. Proceedings.10th. IEEE,1997:126-132.
[68]FJT Fabrega, JC Herzog, JD Guttman. Strand spaces:Why is a security protocol correct?[C]//Security and Privacy,1998. Proceedings.1998 IEEE Symposium on. IEEE,1998:160-171.
[69]FJT Fabrega, JC Herzog, JD Guttman. Strand spaces:Proving security protocols correct[J]. Journal of computer security,1999,7(2):191-230.
[70]沈海峰,薛锐,黄河燕.用串空间分析公平交换协议[J].小型微型计算机系统,2006,27(1)：62-68.
[71]Hong Wang, Chen Wang, Yin Weijing. Formal analysis of SET registration protocol based on strand space. In Proceedings of the Conferences on International Management, Innovation Management and Industrial Engineering, pp.594-498,2009.
[72]Liu Wengqi, Yang Jianhua, Li Zhixin. Fairness analysis of electronic commerce protocol based on strand space. In Proceedings of the 5th International Conferences on Intelligent Information Hiding and Multimedia Signal Processing, pp.714-717,2009.
[73]Deng Zhenrong, Huang Wenming, Dong Rongsheng, Luo Xiangyu. Interest property of E-commerce protocols and ites verification in strand space model. In Proceedings of WGEC'09, pp.280-283,2009.
[74]Li Xiangdong, Guo Qingpu, Wang Qingxian. Analysis of offline fair exchange protocols in strand spaces. In Proceedings of the International Conferences on Compoutational Intelligence and Security, pp.272-276,2008
[75]JD Guttman. Fair exchange in strand spaces [C]//In 7th International Workshop on Security Issues in Concurrency, EPTCS. Electronic Proceedings in Theoretical Computer Science.2009:46-60.
[76]JD Guttman. State and progress in strand spaces:Proving fair exchange[J]. Journal of Automated Reasoning,2012,48(2):159-195.
[77]I Cervesato, NA Durgin, PD Lincoln, et al. A meta-notation for protocol analysis[C] //Computer Security Foundations Workshop,1999. Proceedings of the 12th IEEE. IEEE,1999:55-69.
[78]M Bozzano. A Logic-Based Approach to Model Checking of Parameterized and Infinite-State Systems[D]. PhD thesis, DISI, Universita di Genova,2002.
[79]G Wang. Generic non-repudiation protocols supporting transparent off-line TTP[J]. Journal of Computer Security,2006,14(5):441-467.
[80]M Boreale. Symbolic trace analysis of cryptographic protocols[M]//Automata, Languages and Programming. Springer Berlin Heidelberg,2001:667-681.
[81]卿斯汉,李改成.公平交换协议的一个形式化模型[J].中国科学：E辑,2005,35(2)：161-172.
[82]卿斯汉,李改成.多方公平交换协议的形式化分析和设计[J].中国科学：E辑,2006,36(6)：598-616.
[83]冯登国.可证明安全性理论与方法研究[J].软件学报,2005,16(10).
[84]薛锐,雷新锋.安全协议：信息安全保障的灵魂——安全协议分析研究现状与发展趋势[J].中国科学院院刊,2011,26(3)：287-296.
[85]M Bellare, P Rogaway. Random oracles are practical:A paradigm for designing efficient protocols[C]//Proceedings of the 1st ACM conference on Computer and communications security. ACM,1993:62-73.
[86]M Bellare, R Canetti, H Krawczyk. A modular approach to the design and analysis of authentication and key exchange protocols [C]//Proceedings of the thirtieth annual ACM symposium on Theory of computing. ACM,1998:419-428.
[87]R Canetti, H Krawczyk. Analysis of key-exchange protocols and their use for building secure channels[M]//Advances in Cryptology-EUROCRYPT 2001. Springer Berlin Heidelberg,2001:453-474.
[88]B LaMacchia, K Lauter, A Mityagin. Stronger security of authenticated key exchange [M]//Provable Security. Springer Berlin Heidelberg,2007:1-16.
[89]M Abadi, P Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption[J]. Journal of cryptology,2002,15(2):103-127.
[90]D Micciancio, B Warinschi. Soundness of formal encryption in the presence of active adversaries[M]//Theory of Cryptography. Springer Berlin Heidelberg,2004:133-151.
[91]R Canetti. Universally composable security:A new paradigm for cryptographic protocols[C]//Foundations of Computer Science,2001. Proceedings.42nd IEEE Symposium on. IEEE,2001:136-145.
[92]M Backes, B Pfitzmann, M Waidner. A composable cryptographic library with nested operations[C]//Proceedings of the 10th ACM conference on Computer and communications security. ACM,2003:220-230.
[93]A Datta. Security analysis of network protocols:compositional reasoning and complexity-theoretic foundations[D]. PhD Thesis, Stanford University, September 2005.
[94]A Datta, A Derek, JC Mitchell, et al. A derivation system for security protocols and its logical formalization[C]//Computer Security Foundations Workshop,2003. Proceedings.16th IEEE.2003:109-125.
[95]A Datta, A Derek, JC Mitchell, et al. Secure protocol composition[C]//Proceedings of the 2003 ACM workshop on Formal methods in security engineering. ACM,2003: 11-23.
[96]M Backes, A Datta, A Derek, et al. Compositional analysis of contract-signing protocols[J]. Theoretical Computer Science,2006,367(1):33-56.
[97]R Canetti, J Herzog. Universally composable symbolic security analysis[J]. Journal of cryptology,2011,24(1):83-147.
[98]谢鸿波.安全协议形式化分析方法的关键技术研究[D].博士论文,电子科技大学,2011.
[99]王育民,刘建伟.通信网的安全——理论与技术.西安电子科技大学出版社.1999.
[100]D Otway, O Rees. Efficient and timely mutual authentication[J]. ACM SIGOPS Operating Systems Review,1987,21(1):8-10.
[101]LC Paulson. Relations between secrets:Two formal analyses of the Yahalom protocol[J]. Journal of Computer Security,2001,9(3):197-216.
[102]DE Denning, GM Sacco. Timestamps in key distribution protocols[J]. Communications of the ACM,1981,24(8):533-536.
[103]TYC Woo, SS Lam. A lesson on authentication protocol design[J]. ACM SIGOPS Operating Systems Review,1994,28(3):24-37.
[104]D Harkins, D Carrel. The internet key exchange (IKE)[R]. RFC 2409, november, 1998.
[105]S Kremer, O Markowitch. Optimistic non-repudiable information exchange[C]// Symposium On Information Theory In The Benelux. Werkgemeenschap voor Informatie-en Communicatietheorie; 2000:139-146.
[106]JA Clark, JL Jacob. A Survey of Authentication Protocol Literature:Version 1.0[J]. 1997.
[107]ISO/IEC. Information technology security techniques entity authentication mechanisms part 2:Entity authentication using symmetric techniques.1993.
[108]M Satyanarayanan. Integrating security in a large distributed system[J]. ACM Transactions on Computer Systems (TOCS),1989,7(3):247-280.
[109]ISO/IEC. Information technology security techniques entity authentication mechanisms part 4:Entity authentication using cryptographic check functions.1993.
[110]Neuman B C, Stubblebine S G. A note on the use of timestamps as nonces[J]. ACM SIGOPS Operating Systems Review,1993,27(2):10-14.
[111]I Kao, R Chow. An efficient and secure authentication protocol using uncertified keys[J]. ACM SIGOPS Operating Systems Review,1995,29(3):14-21.
[112]ISO/IEC. Information technology security techniques entity authentication mechanisms part 3:Entity authentication using a public key algorithm.1995.
[113]M Blum. Coin flipping by telephone a protocol for solving impossible problemsfJ]. ACM SIGACTNews,1983,15(1):23-27.
[114]G Lowe. Towards a completeness result for model checking of security protocols[J]. Journal of computer security,1999,7(2):89-146.
[115]王芷玲,张玉清,杨波.公平交换协议设计原则[J].中国科学院研究生院学报,2006,23(4)：555-560.
[116]G Arora, M Hanneghan, Merabti M. P2P commercial digital content exchange[J]. Electronic Commerce Research and Applications,2005,4(3):250-263.
[117]F Lin, H Lo, C Wang. Can a P2P File-Sharing Network Become an e-Marketplace[C]// Hawaii International Conference on System Sciences, Proceedings of the 41st Annual. IEEE,2008:298-298.
[118]Cuihong Lia, Bin Yu, Katia Sycarac. An incentive mechanism for message relaying in unstructured peer-to-peer systems [J]. Electronic Commerce Research and Applications, 2009,8(6):315-326.
[119]卿斯汉.电子商务安全协议中的可信第三方角色[J].软件学报,2003,14(11)：1936-1943.
[120]M Ben-Or, O Goldreich, S Micali, et al. A fair protocol for signing contracts[J]. Information Theory, IEEE Transactions on,1990,36(1):40-46.
[121]P Syverson. Weakly secret bit commitment:Applications to lotteries and fair exchange[C]//Computer Security Foundations Workshop,1998. Proceedings.11th IEEE. IEEE,1998:2-13.
[122]H Pagnia, FC Gartner. On the impossibility of fair exchange without a trusted third party[R]. Technical Report TUD-BS-1999-02, Darmstadt University of Technology, Department of Computer Science,1999
[123]陈明.乐观公平交换协议形式化逻辑及其自动证明技术[D].博士论文,重庆大学,2011.
[124]A Bahreman, JD Tygar. Certified electronic mail[D]. Carnegie Mellon University, 1992.
[125]B Cox, JD Tygar, Sirbu M. NetBill security and transaction protocol[C]//Proceedings of the First USENIX Workshop on Electronic commerce.1995,13.
[126]RH Deng, L Gong, AA Lazar, et al. Practical protocols for certified electronic mail[J]. Journal of network and systems management,1996,4(3):279-297.
[127]J Zhou, D Gollmann. Evidence and non-repudiation [J]. Journal of Network and Computer Applications,1997,20(3):267-281.
[128]Zhou J, Gollmann D. Towards verification of non-repudiation protocols[C]// Proceedings of 1998 International Refinement Workshop and Formal Methods Pacific. Canberra, Australia,1998:370-380.
[129]N Asokan. Fairness in Electronic Commerce [D]. PhD thesis, University of Waterloo. 1998.
[130]N Asokan, M Schunter, M Waidner. Optimistic protocols for fair exchange[C]// Proceedings of the 4th ACM conference on Computer and communications security. ACM,1997:7-17.
[131]N Asokan, V Shoup, M Waidner. Optimistic fair exchange of digital signatures [J]. Selected Areas in Communications, IEEE Journal on,2000,18(4):593-610.
[132]F Bao, RH Deng, W Mao. Efficient and practical fair exchange protocols with off-line TTP[C]//Security and Privacy,1998. Proceedings.1998 IEEE Symposium on. IEEE, 1998:77-85.
[133]H Vogt, H Pagnia, FC Gartner. Modular fair exchange protocols for electronic commerce[C]//Cornputer Security Applications Conference,1999.(ACSAC'99) Proceedings.15th Annual. IEEE,1999:3-11.
[134]J Zhou, KY Lam. Securing digital signatures for non-repudiation[J]. Computer Communications,1999,22(8):710-716.
[135]H Pagnia, H Vogt, FC Gartner. Fair exchange[J]. The Computer Journal,2003,46(1): 55-75.
[136]JL Hernandez-Ardieta, AI Gonzalez-Tablas, Alvarez B R. An optimistic fair exchange protocol based on signature policies[J]. Computers & Security,2008,27(7):309-322.
[137]U Carlsen. Cryptographic protocol flaws:know your enemy[C]//Computer Security Foundations Workshop VII,1994. CSFW 7. Proceedings. IEEE,1994:192-200.
[138]BW Long. Formal verification of type flaw attacks in security protocols[C]//Software Engineering Conference,2003. Tenth Asia-Pacific. IEEE,2003:415-424.
[139]J Heather, G Lowe, S Schneider. How to prevent type flaw attacks on security protocols[J]. Journal of Computer Security,2003,11(2):217-244.
[140]C Meadows. Identifying potential type confusion in authenticated messages[R]. NAVAL RESEARCH LAB WASHINGTON DC,2002.
[141]K Steve. Formal analysis of optimistic fair exchange protocols[D]. Bruxelles: Universit'Libre de Bruxelles Facul'e des Sciences,2004.
[142]M Abadi, R Needham. Prudent engineering practice for cryptographic protocols[C]// Research in Security and Privacy,1994. Proceedings.,1994 IEEE Computer Society Symposium on. IEEE,1994:122-136.
[143]王亚弟,束妮娜,韩继红,王娜.密码协议形式化分析.北京：机械工业出版社,2007.
[144]陈莉.电子商务安全协议的设计与分析[D].博士论文,信息工程大学,2009.
[145]闫丽丽.基于串空间理论的安全协议研究[D].西南交通大学,2012.
[146]B Schneier, J Riordan. A certified e-mail protocol[C]//Computer Security Applications Conference,1998. Proceedings.14th Annual. IEEE,1998:347-352.
[147]M Abadi, N Glew, B Home, et al. Certified email with a light on-line trusted third party:Design and implementation[C]//Proceedings of the 1 lth international conference on World Wide Web.2002:387-395.
[148]J Zhou, R Deng, F Bao. Some remarks on a fair exchange protocol[C]//Public Key Cryptography. Springer Berlin Heidelberg,2000:46-57.
[149]彭红艳,李肖坚,夏春和等.一种面向电子邮件的不可否认协议及其形式化分析[J].计算机研究与发展,2006,43(11)：1914-1919.
[150]崔军,刘琦,张振涛,等.可转换认证加密的安全邮件协议[J].电子科技大学学报,2010,39(4)：598-602.
[151]S Micali. Simple and fast optimistic protocols for fair electronic exchange[C]// Proceedings of the twenty-second annual symposium on Principles of distributed computing. ACM,2003:12-19.
[152]F Bao, G Wang, J Zhou, et al. Analysis and improvement of Micali's fair contract signing protocol[C]//Information Security and Privacy. Springer Berlin Heidelberg, 2004:176-187.
[153]张青,张龙,温巧燕,等.基于签密的认证邮件协议.电子科技大学学报,2008,37(2)：282-284
[154]RL Rivest, A Shamir. Pay Word and Micro Mint:Two Simple Micropayment Schemes[C]//Proceedings of International Workshop on Security Protocols. Berlin, Springer Berlin Heidelberg,1997:69-87.
[155]J Hao, J Zou, Y Dai. A Real-time Payment Scheme for SIP Service Based on Hash Chain[C]//Proceedings of IEEE International Conference on e-Business Engineering (ICEBE'08), New York:IEEE Prees,2008:279-286.
[156]A Esmaeeli, M Shajari. Mv payword:Secure and Efficient Payword-based Micropayment Scheme[C]//Proceedings of IEEE Second International Conference on Applications of Digital Information and Web Technologies (ICADIWT'09).New York: IEEE Prees,2009:609-614.
[157]X Zhao, Y Lv, W He. A Novel Micropayment Scheme with Complete Anonymity[C] //Proceedings of 5th International Conference on Information Assurance and Security (IAS'092009). New York:IEEE Prees,2009:638-642.
[158]L Buttyan. Removing the Financial Incentive to Cheat In Micropayment Schemes [J]. Electronics Letters,2000,36(2):132-133.
[159]樊利民,廖建新.公平的移动小额支付协议[J].电子与信息学报,2007,29(11)：2599-2602.
[160]姜楠,杨日璟,林正奎,等.基于混沌双Hash链的移动微支付协议[J].吉林大学学报(工学版),2010,40(2)：581～585.
[161]李方伟,闫少军,万丽.一种新型的电子商务微支付方案[J].重庆邮电大学学报(自然科学版),2011,23(5)：612～615.
[162]D Luo, J Zhang. Efficient Self-fair Exchange Anonymous E-payment Protocol [J] Journal of Computational Information Systems,2011,7(4):1302-1309.
[163]T Lan. Secure Mechanism Based on Concurrent Signature for Mobile Payment Services[C]//Proceedings of IEEE 3rd International Conference on Communication Software and Networks (ICCSN2011). New York:IEEE Prees,2011:435-438.
[164]K Fan, Y Wang, H Li. Fairness Electronic Payment Protocol [J]. International Journal of Grid and Utility Computing,2012,3(1):53-58.
[165]W Li, Q Wen, Q Su, et al. An Efficient and Secure Mobile Payment Protocol for Restricted Connectivity Scenarios in Vehicular Ad hoc Network [J].Computer Communications,2012,35(2):188-195.
[166]JS Wang, FY Yang, I Paik. A Novel E-cash Payment Protocol Using Trapdoor Hash Function on Smart Mobile Devices [J]. International Journal of Computer Science and Network Security,2011,11(6):12-19.
[167]API Deya, LH Rotger, MP Capella, et al. Anonymous, Fair and Untraceable Micropayment Scheme:Application to LBS [J]. IEEE Latin America Transactions, (Revista IEEE America Latina),2012,10(3):1774-1784.
[168]HT Liaw, JF Lin, WC Wu. A New Electronic Traveler's Check Scheme Based on One-Way Hash FunctionS[J]. Electronic Commerce Research and Applications,2008, 6(4):499-508.
[169]JH Yang, CC Chang. A Low Computational Cost Electronic Payment Scheme for Mobile Commerce with Large-scale Mobile Users [J]. Wireless Personal Communications,2012,63(1):83-99.
[170]KH Krawczy, T Rabin. Chameleon Hashing and Signatures[C]//Proceedings of Network and Distributed System Security Symposium (NDSS).2000:143-154.
[171]杨小东,王彩芬.高效的在线/离线代理重签名方案[J].电子与信息学报,2011,33(12)：2916～2921
[172]胡汉平,李曦,王祖喜等.实现电子支付的方法、系统及移动终端：中国,200710090259[P],2007-9-12
[173]P Lin, HY Chen, Y Fang, et al. A Secure Mobile Electronic Payment Architecture Platform for Wireless Mobile Networks [J]. IEEE Transactions on Wireless Communications,2008,7(7):2705-2713.
[174]L Chen, Z Cheng, SMART N P. Identity-based Key Agreement Protocols from Pairings [J]. International Journal of Information Security,2007,6(4):213-241
[175]Christian H, Alan J. Timed Spi-calculus with types for secrecy and authenticity [C], Abadi M, Alfaro L, eds. Proc. of the CONCUR 2005 Concurrency Theory, Berlin, 2005, LNCS 3653, Springer-Verlag,202-216.
[176]J Cederquist, R Corin, MT Dashti. On the quest for impartiality:Design and analysis of a fair non-repudiation protocol Information and Communications security [J]. Lecture Notes in Computer Science, Volume 3783. Berlin:Springer.2005:27-39.
[177]M Franklin, G Tsudik. Secure group barter:Multi-party fair exchange with semi-trusted neutral parties[C]//Financial Cryptography. Springer Berlin Heidelberg, 1998:90-102.
[178]S Kremer, O Markowitch. A multi-party non-repudiation protocol[M]//Information Security for Global Information Infrastructures. Springer US,2000:271-280.
[179]S Kremer, O Markowitch. A multi-party optimistic non-repudiation protocol[M] //Information Security and Cryptology-ICISC 2000. Springer Berlin Heidelberg, 2001:109-122.
[180]韩志耕,罗军舟.一个公平的多方不可否认协议[J].计算机学报,2008,31(10)：1705-1715.
[181]王彩芬,贾爱库,刘军龙等.基于签密的多方认证邮件协议[J].电子学报,2005,33(11)：2070-2073
[2]A Freier. The SSL protocol version 3.0 [J]. http://wp.netscape.com/eng/ss13/ draft302.txt,1996.
[3]SET Secure Electronic Transaction Specification Book 1:Business Description, Version 1.01997. http://www.setco.org/download.html#spec
[4]SET Secure Electronic Transaction Specification Book 2:Programmer's Guide, Version 1.01997, http://www.setco.org/download.html#spec
[5]SET Secure Electronic Transaction Specification Book 3:Formal Protocol Definition Version 1.0.1997. http://www.setco.org/download.html#spec
[6]K O'Toole. The Internet Billing Server:Transaction Protocol Alternatives[D]. Carnegie Mellon University. Information Networking Institute,1994.
[7]N Asokan, V Shoup, Waidner M. Asynchronous protocols for optimistic fair exchange[C]//Security and Privacy,1998. Proceedings.1998 IEEE Symposium on IEEE,1998:86-99.
[8]卿斯汉.安全协议20年研究进展[J].软件学报,2003,14(10)：1740-1752.
[9]R M Needham, M D Schroeder. Using encryption for authentication in large networks of computers [J]. Communications of the ACM,1978,21(12):993-999.
[10]G Lowe. An attack on the Needham-Schroeder public-key authentication protocol[J]. Information processing letters,1995,56(3):131-133.
[11]薛锐,冯登国.安全协议的形式化分析技术与方法[J].计算机学报,2006,29(1)：1-20.
[12]M Burrows, M Abadi, R M Needham. A logic of authentication[J]. Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences,1989,426(1871): 233-271.
[13]TYC Woo, SS Lam. A semantic model for authentication protocols[C]//Research in Security and Privacy,1993. Proceedings.1993 IEEE Computer Society Symposium on. IEEE,1993:178-194.
[14]R Kemmerer, C Meadows, J Millen. Three systems for cryptographic protocol analysis[J]. Journal of CRYPTOLOGY,1994,7(2):79-130.
[15]D Dolev, A Yao. On the security of public key protocols[J]. Information Theory, IEEE Transactions on,1983,29(2):198-208.
[16]CCITT R X.509:The Directory Authentication Framework[J].1988.
[17]SP Miller, BC Neuman, JI Schiller, et al. Kerberos authentication and authorization system[C]//In Project Athena Technical Plan.1987.
[18]L Gong, R Needham, R Yahalom. Reasoning about belief in cryptographic protocols[C] //Research in Security and Privacy,1990. Proceedings.,1990 IEEE Computer Society Symposium on. IEEE,1990:234-248.
[19]M Abadi, MR Turtle. A semantics for a logic of authentication[C]//Proceedings of the tenth annual ACM symposium on Principles of distributed computing. ACM,1991: 201-216.
[20]P van Oorschot. Extending cryptographic logics of belief to key agreement protocols[C] //Proceedings of the 1 st ACM Conference on Computer and Communications Security. ACM,1993:232-243.
[21]P Syverson. A taxonomy of replay attacks cryptographic protocols[C]//Computer Security Foundations Workshop Ⅶ,1994. CSFW 7. Proceedings. IEEE,1994: 187-191.
[22]P Bieber. A logic of communication in hostile environment[C]//Computer Security Foundations Workshop Ⅲ,1990. Proceedings. IEEE,1990:14-22.
[23]P Syverson. Formal semantics for logics of cryptographic protocols[C]//Computer Security Foundations Workshop Ⅲ,1990. Proceedings. IEEE,1990:32-41.
[24]S Gurgens. SG logic-a formal analysis technique for authentication protocols[C]// Security Protocols. Springer Berlin Heidelberg,1998:159-176.
[25]R Kailar. Accountability in electronic commerce protocols[J]. Software Engineering, IEEE Transactions on,1996,22(5):313-328.
[26]周典萃,卿斯汉,周展飞.Kailar逻辑的缺陷[J].软件学报,1999,10(12)：1238-1245.
[27]周典萃,卿斯汉,周展飞.一种分析电子商务安全协议的新工具[J].软件学报,2001,12(9)：1318-1328.
[28]卿斯汉.一种电子商务安全协议形式化分析方法[J].软件学报,2005,16(10)：1757-1765.
[29]刘冬梅,卿斯汉,马恒太,等.一种离线TTP公平非否认协议的安全性分析方法[J].计算机研究与发展,2011,48(4)：656-665.
[30]黎波涛,罗军舟.不可否认协议时限性的形式化分析[J].软件学报,2006,17(7)：1510-1516.
[31]J Zhou, D Gollman. A fair non-repudiation protocol[C]//Security and Privacy,1996. Proceedings 1996 IEEE Symposium on. IEEE,1996:55-61.
[32]韩志耕,罗军舟.多方不可否认协议时限性分析与改进[J].电子学报,2009,37(2)：377-381.
[33]S Kremer, O Markowitch. Fair multi-party non-repudiation protocols[J]. International Journal of Information Security,2003,1(4):223-235.
[34]陈明,吴开贵,吴长泽,等.公平交换协议形式逻辑[J].Journal of Software,2011, 22(3).
[35]雷新锋,刘军,肖军模.时间相关密码协议逻辑及其形式化语义[J].软件学报,2011,22(003)：534-557.
[36]CAR Hoare. Communicating sequential processes[M]//Programming Languages. Springer Berlin Heidelberg,1983:306-317.
[37]G Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR[M]//Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg,1996:147-166.
[38]JC Mitchell, M Mitchell, Stern U. Automated analysis of cryptographic protocols using Murcp[C]//Security and Privacy,1997. Proceedings.,1997 IEEE Symposium on. IEEE,1997:141-151.
[39]D Basin, S Modersheim, L Vigano. OFMC:A symbolic model checker for security protocols[J]. International Journal of Information Security,2005,4(3):181-208.
[40]JK Millen, SC Clark, Freedman S B. The interrogator:Protocol secuity analysis[J]. Software Engineering, IEEE Transactions on,1987 (2):274-288.
[41]C Meadows. The NRL protocol analyzer:An overview[J]. The Journal of Logic Programming,1996,26(2):113-131.
[42]S Schneider. Formal analysis of a non-repudiation protocol[C]//Computer Security Foundations Workshop,1998. Proceedings.11th IEEE. IEEE,1998:54-65.
[43]N Evans, S Schneider. Verifying security protocols with PVS:widening the rank function approach[J]. The Journal of Logic and Algebraic Programming,2005,64(2): 253-284.
[44]K Wei, J Heather. Towards verification of timed non-repudiation protocols[M]// Formal Aspects in Security and Trust. Springer Berlin Heidelberg,2006:244-257.
[45]韩志耕,罗军舟,王良民.不可否认协议分析的增广CSP方法[J].通信学报,2008,29(10)：8-18.
[46]V Shmatikov, JC Mitchell. Analysis of a fair exchange protocol [C]//Proceedings of the Seventh Annual Symposium on Network and Distributed System Security (NDSS 2000).2000.
[47]V Shmatikov, JC Mitchell. Finite-state analysis of two contract signing protocols[J]. Theoretical Computer Science,2002,283(2):419-450.
[48]JA Garay, M Jakobsson, P MacKenzie. Abuse-free optimistic contract signing[C]// Advances in Cryptology-CRYPTO'99. Springer Berlin Heidelberg,1999:449-466.
[49]S Kremer, JF Raskin. Game analysis of abuse-free contract signing[C]//Computer Security Foundations Workshop,2002. Proceedings.15th IEEE. IEEE,2002:206-220.
[50]S Kremer, JF Raskin. A game-based verification of non-repudiation and fair exchange protocols[J]. Journal of Computer Security,2003,11(3):399-429.
[51]R Alur, TA Henzinger, Mang F Y C, et al. MOCHA:Modularity in model checking[C] //Computer Aided Verification. Springer Berlin Heidelberg,1998:521-525.
[52]文静华,李祥,张焕国,等.基于ATL的公平电子商务安全协议形式化分析[J].电子与信息学报,2007,29(4)：901-905.
[53]J Zhou, R Deng, F Bao. Evolution of fair non-repudiation with TTP[C]//Information Security and Privacy. Springer Berlin Heidelberg,1999:258-269.
[54]LC Paulson. Proving properties of security protocols by induction[C]//Computer Security Foundations Workshop,1997. Proceedings.,10th. IEEE,1997:70-83.
[55]LC Paulson. The inductive approach to verifying cryptographic protocols [J]. Journal of computer security,1998,6(1):85-128.
[56]M Wenzel. The isabelle/isar reference manual, http://www.cl.cam.ac.ul/research/hvg /Isabelle/documentation.html.
[57]G Bella, LC Paulson. Mechanical proofs about a non-repudiation protocol[M]// Theorem Proving in Higher Order Logics. Springer Berlin Heidelberg,2001:91-104.
[58]G Bella, LC Paulson. Accountability protocols:Formalized and verified[J]. ACM Transactions on Information and System Security (TISSEC),2006,9(2):138-161.
[59]M Abadi, AD Gordon. A calculus for cryptographic protocols:The spi calculus[C]// Proceedings of the 4th ACM conference on Computer and communications security. ACM,1997:36-47.
[60]R Milner, J Parrow, Walker D. A calculus of mobile processes, i[J]. Information and computation,1992,100(1):1-40.
[61]C Haack, A Jeffrey. Pattern-matching spi-calculus[J]. Information and Computation, 2006,204(8):1195-1263.
[62]M Bugliesi, R Focardi, M Maffei. Compositional analysis of authentication protocols[M]//Programming Languages and Systems. Springer Berlin Heidelberg, 2004:140-154.
[63]顾永跟,傅育熙.基于进程演算和知识推理的安全协议形式化分析[J].计算机研究与发展,2006,43(5)：953-958.
[64]顾永跟,傅育熙,朱涵.基于可达关系的安全协议保密性分析[J].计算机学报,2007,30(2)：255-261.
[65]顾永跟,李国强,王国钧.基于类pi演算的电子支付协议安全性形式化研究[J].计算机应用研究,2006,3：007.
[66]李援,蒋建国,王焕宝.spi演算证明协议非可否认性[J].通信学报,2009,5：014.
[67]J Zhou, D Gollmann. An efficient non-repudiation protocol [C]//Computer Security Foundations Workshop,1997. Proceedings.10th. IEEE,1997:126-132.
[68]FJT Fabrega, JC Herzog, JD Guttman. Strand spaces:Why is a security protocol correct?[C]//Security and Privacy,1998. Proceedings.1998 IEEE Symposium on. IEEE,1998:160-171.
[69]FJT Fabrega, JC Herzog, JD Guttman. Strand spaces:Proving security protocols correct[J]. Journal of computer security,1999,7(2):191-230.
[70]沈海峰,薛锐,黄河燕.用串空间分析公平交换协议[J].小型微型计算机系统,2006,27(1)：62-68.
[71]Hong Wang, Chen Wang, Yin Weijing. Formal analysis of SET registration protocol based on strand space. In Proceedings of the Conferences on International Management, Innovation Management and Industrial Engineering, pp.594-498,2009.
[72]Liu Wengqi, Yang Jianhua, Li Zhixin. Fairness analysis of electronic commerce protocol based on strand space. In Proceedings of the 5th International Conferences on Intelligent Information Hiding and Multimedia Signal Processing, pp.714-717,2009.
[73]Deng Zhenrong, Huang Wenming, Dong Rongsheng, Luo Xiangyu. Interest property of E-commerce protocols and ites verification in strand space model. In Proceedings of WGEC'09, pp.280-283,2009.
[74]Li Xiangdong, Guo Qingpu, Wang Qingxian. Analysis of offline fair exchange protocols in strand spaces. In Proceedings of the International Conferences on Compoutational Intelligence and Security, pp.272-276,2008
[75]JD Guttman. Fair exchange in strand spaces [C]//In 7th International Workshop on Security Issues in Concurrency, EPTCS. Electronic Proceedings in Theoretical Computer Science.2009:46-60.
[76]JD Guttman. State and progress in strand spaces:Proving fair exchange[J]. Journal of Automated Reasoning,2012,48(2):159-195.
[77]I Cervesato, NA Durgin, PD Lincoln, et al. A meta-notation for protocol analysis[C] //Computer Security Foundations Workshop,1999. Proceedings of the 12th IEEE. IEEE,1999:55-69.
[78]M Bozzano. A Logic-Based Approach to Model Checking of Parameterized and Infinite-State Systems[D]. PhD thesis, DISI, Universita di Genova,2002.
[79]G Wang. Generic non-repudiation protocols supporting transparent off-line TTP[J]. Journal of Computer Security,2006,14(5):441-467.
[80]M Boreale. Symbolic trace analysis of cryptographic protocols[M]//Automata, Languages and Programming. Springer Berlin Heidelberg,2001:667-681.
[81]卿斯汉,李改成.公平交换协议的一个形式化模型[J].中国科学：E辑,2005,35(2)：161-172.
[82]卿斯汉,李改成.多方公平交换协议的形式化分析和设计[J].中国科学：E辑,2006,36(6)：598-616.
[83]冯登国.可证明安全性理论与方法研究[J].软件学报,2005,16(10).
[84]薛锐,雷新锋.安全协议：信息安全保障的灵魂——安全协议分析研究现状与发展趋势[J].中国科学院院刊,2011,26(3)：287-296.
[85]M Bellare, P Rogaway. Random oracles are practical:A paradigm for designing efficient protocols[C]//Proceedings of the 1st ACM conference on Computer and communications security. ACM,1993:62-73.
[86]M Bellare, R Canetti, H Krawczyk. A modular approach to the design and analysis of authentication and key exchange protocols [C]//Proceedings of the thirtieth annual ACM symposium on Theory of computing. ACM,1998:419-428.
[87]R Canetti, H Krawczyk. Analysis of key-exchange protocols and their use for building secure channels[M]//Advances in Cryptology-EUROCRYPT 2001. Springer Berlin Heidelberg,2001:453-474.
[88]B LaMacchia, K Lauter, A Mityagin. Stronger security of authenticated key exchange [M]//Provable Security. Springer Berlin Heidelberg,2007:1-16.
[89]M Abadi, P Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption[J]. Journal of cryptology,2002,15(2):103-127.
[90]D Micciancio, B Warinschi. Soundness of formal encryption in the presence of active adversaries[M]//Theory of Cryptography. Springer Berlin Heidelberg,2004:133-151.
[91]R Canetti. Universally composable security:A new paradigm for cryptographic protocols[C]//Foundations of Computer Science,2001. Proceedings.42nd IEEE Symposium on. IEEE,2001:136-145.
[92]M Backes, B Pfitzmann, M Waidner. A composable cryptographic library with nested operations[C]//Proceedings of the 10th ACM conference on Computer and communications security. ACM,2003:220-230.
[93]A Datta. Security analysis of network protocols:compositional reasoning and complexity-theoretic foundations[D]. PhD Thesis, Stanford University, September 2005.
[94]A Datta, A Derek, JC Mitchell, et al. A derivation system for security protocols and its logical formalization[C]//Computer Security Foundations Workshop,2003. Proceedings.16th IEEE.2003:109-125.
[95]A Datta, A Derek, JC Mitchell, et al. Secure protocol composition[C]//Proceedings of the 2003 ACM workshop on Formal methods in security engineering. ACM,2003: 11-23.
[96]M Backes, A Datta, A Derek, et al. Compositional analysis of contract-signing protocols[J]. Theoretical Computer Science,2006,367(1):33-56.
[97]R Canetti, J Herzog. Universally composable symbolic security analysis[J]. Journal of cryptology,2011,24(1):83-147.
[98]谢鸿波.安全协议形式化分析方法的关键技术研究[D].博士论文,电子科技大学,2011.
[99]王育民,刘建伟.通信网的安全——理论与技术.西安电子科技大学出版社.1999.
[100]D Otway, O Rees. Efficient and timely mutual authentication[J]. ACM SIGOPS Operating Systems Review,1987,21(1):8-10.
[101]LC Paulson. Relations between secrets:Two formal analyses of the Yahalom protocol[J]. Journal of Computer Security,2001,9(3):197-216.
[102]DE Denning, GM Sacco. Timestamps in key distribution protocols[J]. Communications of the ACM,1981,24(8):533-536.
[103]TYC Woo, SS Lam. A lesson on authentication protocol design[J]. ACM SIGOPS Operating Systems Review,1994,28(3):24-37.
[104]D Harkins, D Carrel. The internet key exchange (IKE)[R]. RFC 2409, november, 1998.
[105]S Kremer, O Markowitch. Optimistic non-repudiable information exchange[C]// Symposium On Information Theory In The Benelux. Werkgemeenschap voor Informatie-en Communicatietheorie; 2000:139-146.
[106]JA Clark, JL Jacob. A Survey of Authentication Protocol Literature:Version 1.0[J]. 1997.
[107]ISO/IEC. Information technology security techniques entity authentication mechanisms part 2:Entity authentication using symmetric techniques.1993.
[108]M Satyanarayanan. Integrating security in a large distributed system[J]. ACM Transactions on Computer Systems (TOCS),1989,7(3):247-280.
[109]ISO/IEC. Information technology security techniques entity authentication mechanisms part 4:Entity authentication using cryptographic check functions.1993.
[110]Neuman B C, Stubblebine S G. A note on the use of timestamps as nonces[J]. ACM SIGOPS Operating Systems Review,1993,27(2):10-14.
[111]I Kao, R Chow. An efficient and secure authentication protocol using uncertified keys[J]. ACM SIGOPS Operating Systems Review,1995,29(3):14-21.
[112]ISO/IEC. Information technology security techniques entity authentication mechanisms part 3:Entity authentication using a public key algorithm.1995.
[113]M Blum. Coin flipping by telephone a protocol for solving impossible problemsfJ]. ACM SIGACTNews,1983,15(1):23-27.
[114]G Lowe. Towards a completeness result for model checking of security protocols[J]. Journal of computer security,1999,7(2):89-146.
[115]王芷玲,张玉清,杨波.公平交换协议设计原则[J].中国科学院研究生院学报,2006,23(4)：555-560.
[116]G Arora, M Hanneghan, Merabti M. P2P commercial digital content exchange[J]. Electronic Commerce Research and Applications,2005,4(3):250-263.
[117]F Lin, H Lo, C Wang. Can a P2P File-Sharing Network Become an e-Marketplace[C]// Hawaii International Conference on System Sciences, Proceedings of the 41st Annual. IEEE,2008:298-298.
[118]Cuihong Lia, Bin Yu, Katia Sycarac. An incentive mechanism for message relaying in unstructured peer-to-peer systems [J]. Electronic Commerce Research and Applications, 2009,8(6):315-326.
[119]卿斯汉.电子商务安全协议中的可信第三方角色[J].软件学报,2003,14(11)：1936-1943.
[120]M Ben-Or, O Goldreich, S Micali, et al. A fair protocol for signing contracts[J]. Information Theory, IEEE Transactions on,1990,36(1):40-46.
[121]P Syverson. Weakly secret bit commitment:Applications to lotteries and fair exchange[C]//Computer Security Foundations Workshop,1998. Proceedings.11th IEEE. IEEE,1998:2-13.
[122]H Pagnia, FC Gartner. On the impossibility of fair exchange without a trusted third party[R]. Technical Report TUD-BS-1999-02, Darmstadt University of Technology, Department of Computer Science,1999
[123]陈明.乐观公平交换协议形式化逻辑及其自动证明技术[D].博士论文,重庆大学,2011.
[124]A Bahreman, JD Tygar. Certified electronic mail[D]. Carnegie Mellon University, 1992.
[125]B Cox, JD Tygar, Sirbu M. NetBill security and transaction protocol[C]//Proceedings of the First USENIX Workshop on Electronic commerce.1995,13.
[126]RH Deng, L Gong, AA Lazar, et al. Practical protocols for certified electronic mail[J]. Journal of network and systems management,1996,4(3):279-297.
[127]J Zhou, D Gollmann. Evidence and non-repudiation [J]. Journal of Network and Computer Applications,1997,20(3):267-281.
[128]Zhou J, Gollmann D. Towards verification of non-repudiation protocols[C]// Proceedings of 1998 International Refinement Workshop and Formal Methods Pacific. Canberra, Australia,1998:370-380.
[129]N Asokan. Fairness in Electronic Commerce [D]. PhD thesis, University of Waterloo. 1998.
[130]N Asokan, M Schunter, M Waidner. Optimistic protocols for fair exchange[C]// Proceedings of the 4th ACM conference on Computer and communications security. ACM,1997:7-17.
[131]N Asokan, V Shoup, M Waidner. Optimistic fair exchange of digital signatures [J]. Selected Areas in Communications, IEEE Journal on,2000,18(4):593-610.
[132]F Bao, RH Deng, W Mao. Efficient and practical fair exchange protocols with off-line TTP[C]//Security and Privacy,1998. Proceedings.1998 IEEE Symposium on. IEEE, 1998:77-85.
[133]H Vogt, H Pagnia, FC Gartner. Modular fair exchange protocols for electronic commerce[C]//Cornputer Security Applications Conference,1999.(ACSAC'99) Proceedings.15th Annual. IEEE,1999:3-11.
[134]J Zhou, KY Lam. Securing digital signatures for non-repudiation[J]. Computer Communications,1999,22(8):710-716.
[135]H Pagnia, H Vogt, FC Gartner. Fair exchange[J]. The Computer Journal,2003,46(1): 55-75.
[136]JL Hernandez-Ardieta, AI Gonzalez-Tablas, Alvarez B R. An optimistic fair exchange protocol based on signature policies[J]. Computers & Security,2008,27(7):309-322.
[137]U Carlsen. Cryptographic protocol flaws:know your enemy[C]//Computer Security Foundations Workshop VII,1994. CSFW 7. Proceedings. IEEE,1994:192-200.
[138]BW Long. Formal verification of type flaw attacks in security protocols[C]//Software Engineering Conference,2003. Tenth Asia-Pacific. IEEE,2003:415-424.
[139]J Heather, G Lowe, S Schneider. How to prevent type flaw attacks on security protocols[J]. Journal of Computer Security,2003,11(2):217-244.
[140]C Meadows. Identifying potential type confusion in authenticated messages[R]. NAVAL RESEARCH LAB WASHINGTON DC,2002.
[141]K Steve. Formal analysis of optimistic fair exchange protocols[D]. Bruxelles: Universit'Libre de Bruxelles Facul'e des Sciences,2004.
[142]M Abadi, R Needham. Prudent engineering practice for cryptographic protocols[C]// Research in Security and Privacy,1994. Proceedings.,1994 IEEE Computer Society Symposium on. IEEE,1994:122-136.
[143]王亚弟,束妮娜,韩继红,王娜.密码协议形式化分析.北京：机械工业出版社,2007.
[144]陈莉.电子商务安全协议的设计与分析[D].博士论文,信息工程大学,2009.
[145]闫丽丽.基于串空间理论的安全协议研究[D].西南交通大学,2012.
[146]B Schneier, J Riordan. A certified e-mail protocol[C]//Computer Security Applications Conference,1998. Proceedings.14th Annual. IEEE,1998:347-352.
[147]M Abadi, N Glew, B Home, et al. Certified email with a light on-line trusted third party:Design and implementation[C]//Proceedings of the 1 lth international conference on World Wide Web.2002:387-395.
[148]J Zhou, R Deng, F Bao. Some remarks on a fair exchange protocol[C]//Public Key Cryptography. Springer Berlin Heidelberg,2000:46-57.
[149]彭红艳,李肖坚,夏春和等.一种面向电子邮件的不可否认协议及其形式化分析[J].计算机研究与发展,2006,43(11)：1914-1919.
[150]崔军,刘琦,张振涛,等.可转换认证加密的安全邮件协议[J].电子科技大学学报,2010,39(4)：598-602.
[151]S Micali. Simple and fast optimistic protocols for fair electronic exchange[C]// Proceedings of the twenty-second annual symposium on Principles of distributed computing. ACM,2003:12-19.
[152]F Bao, G Wang, J Zhou, et al. Analysis and improvement of Micali's fair contract signing protocol[C]//Information Security and Privacy. Springer Berlin Heidelberg, 2004:176-187.
[153]张青,张龙,温巧燕,等.基于签密的认证邮件协议.电子科技大学学报,2008,37(2)：282-284
[154]RL Rivest, A Shamir. Pay Word and Micro Mint:Two Simple Micropayment Schemes[C]//Proceedings of International Workshop on Security Protocols. Berlin, Springer Berlin Heidelberg,1997:69-87.
[155]J Hao, J Zou, Y Dai. A Real-time Payment Scheme for SIP Service Based on Hash Chain[C]//Proceedings of IEEE International Conference on e-Business Engineering (ICEBE'08), New York:IEEE Prees,2008:279-286.
[156]A Esmaeeli, M Shajari. Mv payword:Secure and Efficient Payword-based Micropayment Scheme[C]//Proceedings of IEEE Second International Conference on Applications of Digital Information and Web Technologies (ICADIWT'09).New York: IEEE Prees,2009:609-614.
[157]X Zhao, Y Lv, W He. A Novel Micropayment Scheme with Complete Anonymity[C] //Proceedings of 5th International Conference on Information Assurance and Security (IAS'092009). New York:IEEE Prees,2009:638-642.
[158]L Buttyan. Removing the Financial Incentive to Cheat In Micropayment Schemes [J]. Electronics Letters,2000,36(2):132-133.
[159]樊利民,廖建新.公平的移动小额支付协议[J].电子与信息学报,2007,29(11)：2599-2602.
[160]姜楠,杨日璟,林正奎,等.基于混沌双Hash链的移动微支付协议[J].吉林大学学报(工学版),2010,40(2)：581～585.
[161]李方伟,闫少军,万丽.一种新型的电子商务微支付方案[J].重庆邮电大学学报(自然科学版),2011,23(5)：612～615.
[162]D Luo, J Zhang. Efficient Self-fair Exchange Anonymous E-payment Protocol [J] Journal of Computational Information Systems,2011,7(4):1302-1309.
[163]T Lan. Secure Mechanism Based on Concurrent Signature for Mobile Payment Services[C]//Proceedings of IEEE 3rd International Conference on Communication Software and Networks (ICCSN2011). New York:IEEE Prees,2011:435-438.
[164]K Fan, Y Wang, H Li. Fairness Electronic Payment Protocol [J]. International Journal of Grid and Utility Computing,2012,3(1):53-58.
[165]W Li, Q Wen, Q Su, et al. An Efficient and Secure Mobile Payment Protocol for Restricted Connectivity Scenarios in Vehicular Ad hoc Network [J].Computer Communications,2012,35(2):188-195.
[166]JS Wang, FY Yang, I Paik. A Novel E-cash Payment Protocol Using Trapdoor Hash Function on Smart Mobile Devices [J]. International Journal of Computer Science and Network Security,2011,11(6):12-19.
[167]API Deya, LH Rotger, MP Capella, et al. Anonymous, Fair and Untraceable Micropayment Scheme:Application to LBS [J]. IEEE Latin America Transactions, (Revista IEEE America Latina),2012,10(3):1774-1784.
[168]HT Liaw, JF Lin, WC Wu. A New Electronic Traveler's Check Scheme Based on One-Way Hash FunctionS[J]. Electronic Commerce Research and Applications,2008, 6(4):499-508.
[169]JH Yang, CC Chang. A Low Computational Cost Electronic Payment Scheme for Mobile Commerce with Large-scale Mobile Users [J]. Wireless Personal Communications,2012,63(1):83-99.
[170]KH Krawczy, T Rabin. Chameleon Hashing and Signatures[C]//Proceedings of Network and Distributed System Security Symposium (NDSS).2000:143-154.
[171]杨小东,王彩芬.高效的在线/离线代理重签名方案[J].电子与信息学报,2011,33(12)：2916～2921
[172]胡汉平,李曦,王祖喜等.实现电子支付的方法、系统及移动终端：中国,200710090259[P],2007-9-12
[173]P Lin, HY Chen, Y Fang, et al. A Secure Mobile Electronic Payment Architecture Platform for Wireless Mobile Networks [J]. IEEE Transactions on Wireless Communications,2008,7(7):2705-2713.
[174]L Chen, Z Cheng, SMART N P. Identity-based Key Agreement Protocols from Pairings [J]. International Journal of Information Security,2007,6(4):213-241
[175]Christian H, Alan J. Timed Spi-calculus with types for secrecy and authenticity [C], Abadi M, Alfaro L, eds. Proc. of the CONCUR 2005 Concurrency Theory, Berlin, 2005, LNCS 3653, Springer-Verlag,202-216.
[176]J Cederquist, R Corin, MT Dashti. On the quest for impartiality:Design and analysis of a fair non-repudiation protocol Information and Communications security [J]. Lecture Notes in Computer Science, Volume 3783. Berlin:Springer.2005:27-39.
[177]M Franklin, G Tsudik. Secure group barter:Multi-party fair exchange with semi-trusted neutral parties[C]//Financial Cryptography. Springer Berlin Heidelberg, 1998:90-102.
[178]S Kremer, O Markowitch. A multi-party non-repudiation protocol[M]//Information Security for Global Information Infrastructures. Springer US,2000:271-280.
[179]S Kremer, O Markowitch. A multi-party optimistic non-repudiation protocol[M] //Information Security and Cryptology-ICISC 2000. Springer Berlin Heidelberg, 2001:109-122.
[180]韩志耕,罗军舟.一个公平的多方不可否认协议[J].计算机学报,2008,31(10)：1705-1715.
[181]王彩芬,贾爱库,刘军龙等.基于签密的多方认证邮件协议[J].电子学报,2005,33(11)：2070-2073
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |