乐观公平交换协议形式化逻辑及其自动证明技术
|
摘要
随着Internet的日益发展与普及,电子信息交换已成为现代经济生活的主要形式之一,它是在任意两个互不信任的主体之间以一种公平的方式来交换电子数据。实现公平电子信息交换的协议被称为公平交换协议,公平性成为这类型协议的基本安全属性,目标是实现数据交换而又不会使一方比另一方有获取更多信息的优势,促使互不信任的合作伙伴公平完成交换。
公平交换协议是一类重要的安全协议,而其设计是一个众所周知的难题,常常因为一些细微的问题产生安全缺陷。目前已有一些分析公平交换协议的形式化方法,最典型和得到广泛应用的是信任逻辑方法。许多研究者采用扩展的信任逻辑方法成功分析了在线可信第三方公平交换协议的不可否认性。由于信任逻辑方法自身固有的缺陷,难以用于分析乐观型公平交换协议的公平性和时限性等性质。
乐观型公平交换协议是目前公平交换协议研究领域的热点之一,是一种兼顾公平和效率的公平交换协议形式。在乐观型公平交换协议中,可信第三方不再直接参与数据交换,只需要扮演争端解决者的角色。交易过程中对可信第三方的请求次数远远低于其它类型的公平交换协议,避免了针对可信第三方的拒绝服务攻击。但是,乐观型公平交换协议引入了分支协议结构,协议执行存在多种可能结果,使得对该类型协议的形式化分析更加复杂和困难。
本文研究工作围绕乐观型公平交换协议及其形式化分析技术展开,主要包括三方面内容:第一,对公平交换协议及其形式化技术进行研究综述;第二,研究乐观公平交换协议形式化模型、逻辑及其自动证明技术;第三,研究乐观公平交换协议在电子商务中的应用和实现技术。论文主要工作和创新性成果如下:
1.对公平交换协议的基本理论和基本性质进行综述和分析,对其中一些重要性质进行重新定义,如公平性等。
2.对主要的公平交换协议形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。
3.提出一种新的乐观公平交换协议形式化模型,将信道错误转化为攻击行为,将协议参与者分为诚实与不诚实两类,将入侵者与不诚实参与者的共谋归结为两类Dolev-Yao入侵者。新模型不再单独考虑信道错误,简化了问题空间。
4.提出一种乐观公平交换协议形式化逻辑。新逻辑采用信任逻辑的句法结构,定义乐观公平交换协议为具有Kripke语义结构的演化系统。案例分析显示,新逻辑被成功用于分析乐观型公平交换协议的公平性和时限性。
5.基于自动定理证明器Isabelle,研究实现本文模型和逻辑的自动定理证明技术。采用Paulson归纳法实现更为主动的攻击者,将攻击者主动获取知识的能力描述为对消息进行解析和组合的归纳函数。将信道假设对应为不诚实参与者的行为,以降低协议模拟的复杂度。
6.提出双授权部分盲签名概念,解决电子支付中银行经理滥用职权恶意签发电子钱币的问题。设计实现采用双授权的部分盲签名机制,在随机预言机模型下证明新签名机制是安全的。对比分析表明,新机制具有较高的计算性能。
7.提出新的乐观型电子支付协议。新协议采用双授权部分盲签名机制,同时实现电子现金离线支付(支付阶段无须银行在线支持)和乐观型公平交换。具有复杂结构的安全协议形式化技术研究正在蓬勃发展,本文研究工作对促进这一研究领域发展和电子商务安全具有一定的理论和实用意义。
With the increasing development of Internet, Internet-based electronic information exchange has become one of major forms of modern economic life. Electronic information exchange switches electronic data in a fair way between two un-trusted entities. A protocol achieving fair exchange of electronic information is known as a fair exchange protocol. Fairness is the basic security property of fair exchange protocols. The goal of a fair exchange protocol is to achieve the data exchange and not to leave any advantages over parties, and urges two un-trusted partners to complete a fair exchange.
As is known to all, a secure security protocol designing is hard. A slight fault may even drive great flaws. Fair exchange protocol is of an important security protocol. So far, there are some formal methods for analyzing fair exchange protocols. The widely used method is the belief logic. Many researchers using the extended belief logic method successfully analyzed the non-repudiation of some online trusted third party fair exchange protocols. For the inherent defects in the belief logic method, it is difficult to analyze the fairness, timeliness and other properties of optimistic fair exchange protocol.
Currently, the analyzing and designing of optimistic fair exchange protocol is one of the hottest research fields. The optimistic fair exchange protocol keeps a balance between fairness and efficiency. In the optimistic fair exchange protocol, the trusted third party only plays the arbiter instead of directly involving in the process of data exchange. So, during the transaction process, the number of requesting on the trusted third party is much lower than those of other types of fair exchange protocol, which avoids denial service attacks on the trusted third party. However, the optimistic fair exchange protocol leads to a branch structure, and there are several possible outcomes which make the protocols’formal analysis turns to be more complex and difficult.
This dissertation studies the optimistic fair exchange protocol and its formal analysis techniques, including three following aspects: first, a literature review of fair exchange protocols and their formal techniques; second, a research of formal model, logic and automatic proof techniques of optimistic fair exchange protocols; third, a study of security and applications techniques of optimistic fair exchange protocols in e-commerce. The main study and innovative results of this dissertation are as follows:
1. Basic theories and properties of fair exchange protocols are reviewed and analyzed, and some important properties are re-defined, such as fairness and the like.
2. The main methods of formal analysis of fair exchange protocols are reviewed, and the advantages, disadvantages and problems of each method are discussed as well.
3. A new formal model of optimistic fair exchange protocols is proposed. The new formal model turns channel errors into channel attacks, divides the protocol participants into honesty ones and dishonesty ones, and attributes the conspiracy between intruders and dishonest participants as two types of Dolev-Yao intruders. Case analysis shows that the new model simplifies the problem space.
4. A formal logic of optimistic fair exchange protocols is proposed. The new logic adopts the syntax structure of the belief logic, and defines optimistic fair exchange protocols as the evolution system with the Kripke semantic structure. Case analysis shows that the new logic has been successfully used to analyze the fairness and timeliness of optimistic fair exchange protocols.
5. Based on Isabelle, an interactive theorem proving framework, the automatic theorem proving technology of logics and models in this dissertation are achieved. A more active attacker is achieved using Paulson induction, and the ability of the attacker to acquire knowledge initiatively is described as the inductive function to parsing and combining messages. The channel assuming is modeled as the behaviors of dishonest participants in order to reduce the complexity of the simulation protocol.
6. The concept of dual authorizing in partially blind signature is put forward, which solves a problem, that is, bank manager in the abuse of power maliciously issues e-coins in electronic payments. A scheme of partially blind signature with dual authorizing is designed, and its security is proved under the random oracle model. Comparative analysis shows that the new mechanism has a high computational performance.
7. A new optimistic electronic payment protocol is introduced. The scheme of partially blind signature with dual authorizing is employed, while off-line electronic cash payments (no need of online bank payment support) and optimistic fair exchange are achieved.
The studies of formal technology in security protocols with the complex structure and e-commerce security are booming. There are some theoretical and practical significance in this dissertation for promoting those research fields.
公平交换协议是一类重要的安全协议,而其设计是一个众所周知的难题,常常因为一些细微的问题产生安全缺陷。目前已有一些分析公平交换协议的形式化方法,最典型和得到广泛应用的是信任逻辑方法。许多研究者采用扩展的信任逻辑方法成功分析了在线可信第三方公平交换协议的不可否认性。由于信任逻辑方法自身固有的缺陷,难以用于分析乐观型公平交换协议的公平性和时限性等性质。
乐观型公平交换协议是目前公平交换协议研究领域的热点之一,是一种兼顾公平和效率的公平交换协议形式。在乐观型公平交换协议中,可信第三方不再直接参与数据交换,只需要扮演争端解决者的角色。交易过程中对可信第三方的请求次数远远低于其它类型的公平交换协议,避免了针对可信第三方的拒绝服务攻击。但是,乐观型公平交换协议引入了分支协议结构,协议执行存在多种可能结果,使得对该类型协议的形式化分析更加复杂和困难。
本文研究工作围绕乐观型公平交换协议及其形式化分析技术展开,主要包括三方面内容:第一,对公平交换协议及其形式化技术进行研究综述;第二,研究乐观公平交换协议形式化模型、逻辑及其自动证明技术;第三,研究乐观公平交换协议在电子商务中的应用和实现技术。论文主要工作和创新性成果如下:
1.对公平交换协议的基本理论和基本性质进行综述和分析,对其中一些重要性质进行重新定义,如公平性等。
2.对主要的公平交换协议形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。
3.提出一种新的乐观公平交换协议形式化模型,将信道错误转化为攻击行为,将协议参与者分为诚实与不诚实两类,将入侵者与不诚实参与者的共谋归结为两类Dolev-Yao入侵者。新模型不再单独考虑信道错误,简化了问题空间。
4.提出一种乐观公平交换协议形式化逻辑。新逻辑采用信任逻辑的句法结构,定义乐观公平交换协议为具有Kripke语义结构的演化系统。案例分析显示,新逻辑被成功用于分析乐观型公平交换协议的公平性和时限性。
5.基于自动定理证明器Isabelle,研究实现本文模型和逻辑的自动定理证明技术。采用Paulson归纳法实现更为主动的攻击者,将攻击者主动获取知识的能力描述为对消息进行解析和组合的归纳函数。将信道假设对应为不诚实参与者的行为,以降低协议模拟的复杂度。
6.提出双授权部分盲签名概念,解决电子支付中银行经理滥用职权恶意签发电子钱币的问题。设计实现采用双授权的部分盲签名机制,在随机预言机模型下证明新签名机制是安全的。对比分析表明,新机制具有较高的计算性能。
7.提出新的乐观型电子支付协议。新协议采用双授权部分盲签名机制,同时实现电子现金离线支付(支付阶段无须银行在线支持)和乐观型公平交换。具有复杂结构的安全协议形式化技术研究正在蓬勃发展,本文研究工作对促进这一研究领域发展和电子商务安全具有一定的理论和实用意义。
With the increasing development of Internet, Internet-based electronic information exchange has become one of major forms of modern economic life. Electronic information exchange switches electronic data in a fair way between two un-trusted entities. A protocol achieving fair exchange of electronic information is known as a fair exchange protocol. Fairness is the basic security property of fair exchange protocols. The goal of a fair exchange protocol is to achieve the data exchange and not to leave any advantages over parties, and urges two un-trusted partners to complete a fair exchange.
As is known to all, a secure security protocol designing is hard. A slight fault may even drive great flaws. Fair exchange protocol is of an important security protocol. So far, there are some formal methods for analyzing fair exchange protocols. The widely used method is the belief logic. Many researchers using the extended belief logic method successfully analyzed the non-repudiation of some online trusted third party fair exchange protocols. For the inherent defects in the belief logic method, it is difficult to analyze the fairness, timeliness and other properties of optimistic fair exchange protocol.
Currently, the analyzing and designing of optimistic fair exchange protocol is one of the hottest research fields. The optimistic fair exchange protocol keeps a balance between fairness and efficiency. In the optimistic fair exchange protocol, the trusted third party only plays the arbiter instead of directly involving in the process of data exchange. So, during the transaction process, the number of requesting on the trusted third party is much lower than those of other types of fair exchange protocol, which avoids denial service attacks on the trusted third party. However, the optimistic fair exchange protocol leads to a branch structure, and there are several possible outcomes which make the protocols’formal analysis turns to be more complex and difficult.
This dissertation studies the optimistic fair exchange protocol and its formal analysis techniques, including three following aspects: first, a literature review of fair exchange protocols and their formal techniques; second, a research of formal model, logic and automatic proof techniques of optimistic fair exchange protocols; third, a study of security and applications techniques of optimistic fair exchange protocols in e-commerce. The main study and innovative results of this dissertation are as follows:
1. Basic theories and properties of fair exchange protocols are reviewed and analyzed, and some important properties are re-defined, such as fairness and the like.
2. The main methods of formal analysis of fair exchange protocols are reviewed, and the advantages, disadvantages and problems of each method are discussed as well.
3. A new formal model of optimistic fair exchange protocols is proposed. The new formal model turns channel errors into channel attacks, divides the protocol participants into honesty ones and dishonesty ones, and attributes the conspiracy between intruders and dishonest participants as two types of Dolev-Yao intruders. Case analysis shows that the new model simplifies the problem space.
4. A formal logic of optimistic fair exchange protocols is proposed. The new logic adopts the syntax structure of the belief logic, and defines optimistic fair exchange protocols as the evolution system with the Kripke semantic structure. Case analysis shows that the new logic has been successfully used to analyze the fairness and timeliness of optimistic fair exchange protocols.
5. Based on Isabelle, an interactive theorem proving framework, the automatic theorem proving technology of logics and models in this dissertation are achieved. A more active attacker is achieved using Paulson induction, and the ability of the attacker to acquire knowledge initiatively is described as the inductive function to parsing and combining messages. The channel assuming is modeled as the behaviors of dishonest participants in order to reduce the complexity of the simulation protocol.
6. The concept of dual authorizing in partially blind signature is put forward, which solves a problem, that is, bank manager in the abuse of power maliciously issues e-coins in electronic payments. A scheme of partially blind signature with dual authorizing is designed, and its security is proved under the random oracle model. Comparative analysis shows that the new mechanism has a high computational performance.
7. A new optimistic electronic payment protocol is introduced. The scheme of partially blind signature with dual authorizing is employed, while off-line electronic cash payments (no need of online bank payment support) and optimistic fair exchange are achieved.
The studies of formal technology in security protocols with the complex structure and e-commerce security are booming. There are some theoretical and practical significance in this dissertation for promoting those research fields.
引文
[1] R. Anderson. Why Information Security is Hard - an Economic Perspective [C]. Proceedings of the 17th Annual Computer Security Applications Conference. New Orleans, Louisiana, December. 2001. http://www.ftp.cl.cam.ac.uk/ftp/users/rja14/econ.pdf.
[2] M. Bishop. Introduction to Computer Security [M]. Massachusetts: Addison-Wesley. 2005.
[3] R. Kauffman, C. Wood. 2007. Revolutionary research strategies for e-business: A philosophy of science view in the age of the Internet [EB/OL]. http://www.misrc. umn.edu/ workingpapers/ fullPapers/2006/0614_113006.pdf
[4] T. Sandholm. Unenforced e-commerce transactions [J]. IEEE Internet Computing, 1997. 1(6):47– 54.
[5] S. Even, Y. Yacobi. Relations among public key signature systems [R]. Technical Report 175, Computer Science Dept., Technion, Haifa, Isreal, Mar. 1980.
[6] R. Needham, M. Schroeder. Using encryption for authentication in large networks of computers [J]. Communications of the ACM, 1978. 21(12): 993~999.
[7] D. Denning, G. Sacco. Timestamps in key distribution protocols [J]. Communications of the ACM, 1981. 24(8):533~536.
[8] G. Lowe. Breaking and fixing the Needham-Schroder public-key protocol using FDR [C]. In: Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science. Springer-Verlag, 1996:147~166.
[9]林语堂.人生的盛宴[M].长沙:湖南文艺出版社.2002.
[10] B. Chellas. Modal Logic: An Introduction [M]. Cambridge University Press, Cambridge. 1980.
[11] P. Blackburn, M. de Rijke, Y. Venema. Modal Logic [M]. Cambridge: Cambridge University Press. 2001.
[12] Y. Venema. Temporal Logic [M]. In Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell. 2001.
[13] A. Pnueli. The temporal semantics of concurrent programs [J]. In Theoretical Computer Science, 1981. 13: 1–20.
[14] E. Clarke, E. Emerson. Design and synthesis of synchronization skeletons for branching-time temporal logic [C]. In Proceedings of Workshop on Logic of Programs, volume 131 of LNCS, Springer-Verlag. 1981:52–71.
[15] E. Emerson. Temporal and modal logic [J]. In van Leeuwen, J., editor, Handbook ofTheoretical Computer Science, 1990. 996–1071. Elsevier Science Publishers.
[16] E. Emerson, J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time [J]. Journal of Computer and System Sciences, 1985. 30(1):1–24.
[17] G. Arora, M. Hanneghan, M. Merabti. P2p commercial digital content exchange [J]. Electronic Commerce Research and Applications, 2005. 4:250-263.
[18] F. Lin, H. Lo, C. Wang. Can a P2P File-Sharing Network Become an e-Marketplace [C]. Proceedings of the 41st Hawaii International Conference on System Sciences (HICSS 2008), Waikoloa, Big Island, Hawaii, IEEE, 2008:298-307.
[19] C. Li, B. Yu, K. Sycara. An incentive mechanism for message relaying in unstructured peer-to-peer systems [J]. Electronic Commerce Research and Applications, 2009. 8: 315–326.
[20] S. Kremer, O. Markowitch, J. Zhou. An intensive survey of non-repudiation protocols [J]. Computer Communications, 2002. 25(17):1606–1621.
[21] S. Kremer. Formal Analysis of Optimistic Fair Exchange Protocols [Ph.D. Thesis]. Universit′e Libre de Bruxelles. 2003.
[22] P. Ezhilchelvan, S. Shrivastava. A family of trusted third party based fair-exchange protocols [J]. IEEE Trans. Dependable Secur. Comput., 2005. 2(4):273–286.
[23] M. Ben-Or, O. Goldreich, S. Micali, R.L. Rivest. A fair protocol for signing contracts [J]. IEEE Transaction on Information Theory, 1990. 36(1):40–46.
[24] M. Blum. How to exchange (secret) keys [J]. ACM Transactions on Computer Systems, 1983. 1(2):175–193.
[25] S. Even. Protocol for signing contracts [C]. In Allen Gersho, editor, Advances in Cryptology: A Report on Crypto 81, 1982. 148–153.
[26] S. Even, O. Goldreich, A. Lempel. A randomized protocol for signing contracts [J]. Communications of the ACM, 1985. 28(6):637–647.
[27] J.A. Garay, M. Jakobsson, P. MacKenzie. Abuse-free optimistic contract signing[C]. In: Proc. Advances in Cryptology-Crypto’99, 1999:449~466.
[28] P. Syverson. Weakly secret bit commitment: Applications to lotteries and fair exchange [C]. In 11th IEEE Computer Security Foundations Workshop, 1998:2–13.
[29] H. Pagnia, F.C. G?rtner. On the impossibility of fair exchange without a trusted third party [R]. Technical Report TUD-BS-1999-02, Darmstadt University of Technology, Darmstadt, Germany. 1999.
[30] A. Bahreman, D. Tygar. Certified electronic mail [C]. In Symposium on Network and Distributed Systems Security, 1994: 3–19. Internet Society.
[31] J. Zhou, D. Gollmann. Certified electronic mail. In Computer Security[C]. ESORICS 1996,volume 1146 of LNCS, 1996:160–171.
[32] B. Cox, D. Tygar, M. Sirbu. NetBill security and transaction protocol [C]. In USENIX Association, editor, First USENIX Workshop of Electronic Commerce, 1995:77–88. USENIX.
[33] H. Deng, L. Gong, A. Lazar, W. Wang. Practical protocols for certified electronic mail [J]. Journal of Network and System Management, 1996. 4(3):279–297.
[34] J. Zhou, D. Gollmann. A fair non-repudiation protocol [C]. In IEEE Symposium on Research in Security and Privacy, Research in Security and Privacy, 1996: 55–61. IEEE Computer Society.
[35] J. Zhou, D. Gollmann. An efficient non-repudiation protocol [C]. In 10th IEEE Computer Security Foundations Workshop, 1997: 126–132. IEEE Computer Society Press.
[36] J. Zhou, D. Gollmann. Evidence and non-repudiation [J]. Journal of Network and Computer Applications, 1997. 20:267–281.
[37] J. Zhou, D. Gollmann. Towards verification of non-repudiation protocols [C]. In International Refinement Workshop and Formal Methods Pacific, 1998: 370–380, Canberra, Australia.
[38] M. K. Franklin, M. K. Reiter. Fair exchange with a semi-trusted third party [C]. In 4th ACM Conference on Computer and Communications Security, 1997:1–5. ACM Press.
[39] N. Asokan. Fairness in Electronic Commerce [D]. PhD thesis, University of Waterloo. 1998.
[40] N. Asokan, B. Baum-Waidner, M. Schunter, M. Waidner. Optimistic synchronous multi-party contract signing [R]. Research Report RZ 3089, IBM Research Division. 1998.
[41] N. Asokan, M. Schunter, M. Waidner. Optimistic protocols for multiparty fair exchange [R]. Research Report RZ 2892 (# 90840), IBM Research. 1996.
[42] N. Asokan, M. Schunter, M. Waidner. Optimistic protocols for fair exchange [C]. In Tsutomu Matsumoto, editor, 4th ACM Conference on Computer and Communications Security, 1997: 8–17, Zurich, Switzerland, ACM Press.
[43] N. Asokan, V. Shoup, M. Waidner. Asynchronous protocols for optimistic fair exchange. In IEEE Symposium on Research in Security and Privacy, 1998: 86–99, Oakland, CA, Technical Committee on Security and Privacy, IEEE Computer Society Press.
[44] N. Asokan, V. Shoup, M. Waidner. Optimistic fair exchange of digital signatures [C]. In Advances in Cryptology—Eurocrypt, volume 1403 of LNCS, 1998:591–606.
[45] N. Asokan, V. Shoup, M. Waidner. Optimistic fair exchange of digital signatures [J]. IEEE Journal on Selected Areas in Communications, 2000. 18(4):593–610.
[46] F. Bao, R.H. Deng, W. Mao. Efficient and practical fair exchange protocols with off-line TTP [C]. Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, IEEEComputer Society, California, 1998:77~85.
[47] C. Boyd, E. Foo. Off-line fair payment protocols using convertible signatures [C]. In Advances in Cryptology—Asiacrypt 1998, volume 1514 of LNCS, 1998:271–285. Springer- Verlag.
[48] J. Hernandez-Ardieta, A. Gonzalez-Tablas, B. Alvarez. An optimistic fair exchange protocol based on signature policies [J]. computers & security. 2008. 27(10):309~322.
[49] Q. Huang, G. Yang, D. S. Wong, W. Susilo. Ambiguous optimistic fair exchange [C]. In Advances in Cryptology - ASIACRYPT 2008, Springer LNCS 5350, 2008:74–89.
[50] H. Pagnia, H. Vogt, F.C. G?rtner. 2003. Fair Exchange [J]. The Computer Journal, 46(1): 55~76.
[51] B. Pfitzmann, M. Schunter, M. Waidner. Optimal efficiency of optimistic contract signing [C]. In Seventeenth Annual ACM Symposium on Principles of Distributed Computing, 1998:113–122, New York, ACM.
[52] E. M. Schunter. Optimistic Fair Exchange [D]. PhD thesis, Universit¨at des Saarlandes. 2000.
[53] H. Vogt, H. Pagnia, F. C. G?rtner. Modular fair exchange protocols for electronic commerce [C]. In 15th Annual Computer Security Applications Conference, 1999: 3–11, Phoenix, Arizona, IEEE Computer Society Press.
[54] G. Wang. Generic non-repudiation protocols supporting transparent off-line TTP [J]. Journal of Computer Security, 2006. 14(5):441–467.
[55] G. Wang. An Abuse-Free Fair Contract-Signing Protocol Based on the RSA Signature [J]. IEEE Transactions on Information Forensics and Security, 2010. 5 (1): 158-168.
[56] J. Zhou, K. Lam. Securing digital signatures for non-repudiation [J]. Computer Communications, 1999. 22(8):710–716.
[57] V. Shmatikov, J. Mitchell. Analysis of a fair exchange protocol [C]. In Symposium on Network and Distributed Systems Security (NDSS 2000), 2000: 119-128, San Diego, CA, Internet Society.
[58] V. Shmatikov, J. Mitchell. Analysis of abuse-free contract Signing [C]. Notes In Financial Cryptography 2000, volume 1962 of LNCS, 2000: 174-191, Anguilla, BritishweSt Indies, Springer-Verlag.
[59] V. Shmatikov, J. Mitchell. Finite-state analysis of two contract signing protocols [J]. Theoretical Computer Science. 2002. 283(02): 419~450.
[60] S. Gürgens, C. Rudolph. Security analysis of (un-) fair non-repudiation protocols [C]. In FASec’02, volume 2629 of LNCS, 2003:97–114. Springer.
[61] D. P. Hankes, S. M?dersheim, L. Viganò. A Formalization of Off-Line Guessing for SecurityProtocol Analysis [C], in F. Baader, A. Voronkov (eds), Proceedings of LPAR’04, vol.3452 of LNAI, Springer, 2005:363–379.
[62] A. Armando, R. Carbone, L. Compagna. LTL model checking for security protocols [C]. In CSF, 2007:385–396.
[63] I. Ray, I. Ray, N. Natarajan. An anonymous and failure resilient fair-exchange e-commerce protocol [J]. Decision Support Systems, 2005. 39(3):267~292.
[64] D. Dolev, A.C. Yao. On the security of public key protocols [J]. IEEE Transactions on Information Theory, 1983. 29(2): 198~208.
[65] K. Kim, S. Park, J. Baek. Improving fairness and privacy of Zhou-Gollmann’s fair non- repudiation protocol [C]. In: Gong K, Niu Z, eds. 2000 IEEE Int’l Conf. on Communication. Beijing: IEEE Computer Society Press, 2000:1743?1747.
[66]黎波涛,罗军舟.不可否认协议时限性的形式化分析[J].软件学报, 2006. 17(7):1510-1516.
[67] M. Burrows, M. Abadi, R. Needham. A logic of authentication [C]. In: Proceedings of the Royal Society of London A, Vol 426. 1989:233~271.
[68] S.P. Miller, C. Neuman, J.I. Schiller, J.H. Saltzer. Kerberos authentication and authorization system [R]. Project Athena Technical Plan Section E.2.1, MIT. 1987.
[69] L. Gong, R. Needham, R. Yahalom. Reasoning about Belief in Cryptographic Protocols [C]. In : Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy , 1990. 234~248. Los Alamitos ,California : IEEE Computer Society Press.
[70] M. Abadi, M. R. Tuttle. A Semantics for a Logic of Authentication [C]. In : Proceeding of the Tenth ACM Symposium on Principles of Distributed Computing. ACM Press, 1991: 201~216.
[71] P. C. van Oorschot. Extending Cryptographic Logics of Belief to Key Agreement Protocols (Extended Abstract) [C]. In Proceedings of the First ACM Conference on Computer and Communications Security, 1993:232~243.
[72] P. F. Syverson, P. C. van Oorschot. On Unified Some Cryptographic Protocol Logics [C]. In: Proc. of the’94 IEEE Computer Society Symp. on Security and Privacy. Oakland: IEEE Computer Society Press, 1994:14?28.
[73] P. F. Syverson, P. C. van Oorschot. A Unified Cryptographic Protocol Logics [R]. NRL Publication 5540~227, Naval Research Lab. 1996.
[74] R. Kailar. Accountability in electronic commerce protocols [J]. IEEE Trans. on Software Engineering, 1996. 22(5):313-328.
[75]卿斯汉.一种新型的非否认协议[J].软件学报. 2000.11(10): 1338-1343.
[76]李先贤,怀进鹏.公平的非否认密码协议及其形式分析与应用[J].软件学报, 2000. 11 (12): 1628? 1634.
[77]周典萃,卿斯汉,周展飞. Kailar逻辑的缺陷[J].软件学报, 1999. 10(12):171?173.
[78]周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具[J].软件学报, 2001. 12(09): 171? 173.
[79]汪学明.多方安全协议的形式化分析方法研究与应用[D].博士学位论文,贵州大学. 2008.
[80] C. Hoare. Communicating Sequential Processes [M]. Prentice Hall International Englewoo d Cliff S, NJ. 1985.
[81] A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR [C]. In 8th IEEE Computer Security Foundations Workshop, 1995. 98–107. IEEE Computer Society.
[82] S. A. Schneider. Verifying authentication protocols with CSP [C]. In Simon Foley, editor, 10th IEEE Computer Security Foundations Workshop, 1997: 3–17, Rockport, Massachusetts, USA, June IEEE Computer Society Press.
[83] S. A. Schneider. Formal analysis of a non-repudiation protocol [C]. In 11th IEEE Computer Security Foundations Workshop, 1998: 54–65, Washington - Brussels -Tokyo, IEEE.
[84] N. Evans, S. A.Schneider. Verifying security protocols with PVS: widening the rank function approach [J]. J Log Algebr Program, 2005. 64(2):253-284.
[85] K. Wei, J. Heather. Towards verification of timed non-repudiation protocols [C]. FAST 2005.San Francisco, CA, USA, 2005. 244-257.
[86]韩志耕,罗军舟,王良民.不可否认协议分析的增广CSP方法[J].通信学报. 2008. 29(10): 8-18.
[87] D.L. Dill, A.J. Drexler, A.J. Hu, C.H. Yang. Protocol verification as a hardware design aid [C]. Proceedings of the 1992 IEEE International Conference on Computer Design: VLSI in Computer Sand Processors, 1992. 522-525, IEEE Computer Society Press.
[88] J.C. Mitchell, M. Mitchell, U. Stern. Automated Analysis of Cryptographic Protocols USing MurΦ[C]. Proceedings of the 1997 IEEE Sympossium on Security and Privacy, 1997. 141-151, IEEE Computer Society Press.
[89] M. Tatebayashi, N. MatSuzaki, D. Neuman. Key distribution protocol for digital mobile communication Systems [C]. Proceedings of CRYPTO'89, 1990. 324-333, Springer Verlag.
[90] J. Kohl, B. Neuman, T. TSo. The evolution of the Kerberos authentication Service ver.5 [C]. Distributed Open Systems (Brazier F., JohanSen D. EdS.), 1994. 78-94 IEEE Computer Society Press.
[91] S. Kremer, O. Markowitch. A multi-party non-repudiation protocol [C]. In 15th International Conference on Information Security—Sec 2000, IFIP World Computer Congress, 2000: 271–280, Beijing, China, Kluwer Academic.
[92] S. Kremer, O. Markowitch. Optimistic non-repudiable information exchange [C]. In J.Biemond, editor, 21st Symp. on Information Theory in the Benelux, 2000: 139–146, Wassenaar, The Netherlands, Werkgemeenschap Informatieen Communicatie theorie, Enschede.
[93] S. Kremer, O. Markowitch. Selective receipt in certified e-mail [C]. In Advances in Cryptology—Indocrypt 2001, Lecture Notes in Computer Science. Springer-Verlag. 2001.
[94] S. Kremer, O. Markowitch. Fair multi-party non-repudiation [J]. International Journal on Information Security, 2003.1(4):223–235.
[95] S. Kremer, J. Raskin. A game-based verification of nonrepudiation and fair exchange protocols [C]. In Kim G. Larsen and Mogens Nielsen, editors, Concurrency Theory—CONCUR 2001, volume 2154 of LNCS, 2001: 551–565, Aalborg, Denmark, Springer-Verlag.
[96] S. Kremer, J. Raskin. Game analysis of abuse-free contract signing [C]. In Steve A. Schneider, editor, 15th IEEE Computer Security Foundations Workshop, 2002: 206–220, Cape B reton, Nova Scotia, Canada, IEEE Computer Society Press.
[97] S. Kremer, J. Raskin. A game-based verification of non-repudiation and fair exchange protocols [J]. Journal of Computer Security. 2003.11(3): 399~429.
[98] R. Alur, T. A. Henzinger, O. Kupferman. Alternating-time temporal logic [C]. In 38th Annual Symposium on Foundations of Computer Science, 1997: 100–109. IEEE Computer Society Press.
[99] P. H. DrieISma, S. ModerSheim. The ASW Protocol Revisited: A Unified View [J]. Electr. Notes Theor. Comput. Sci. 2005. 125(1):145-161.
[100] M.T. Dashti. Keeping fairness alive [D]. Ph.D. Thesis. Vrije Universiteit Amsterdam. 2008.
[101] S. Basagiannis, P. Katsaros, A. Pombortsis. Intrusion Attack Tactics for the model checking of e-commerce security guarantees [C]. In Proc. of the 26th International Conference on Computer Safety, Reliability and Security (SAFECOMP), LNCS 4680, 2007: 238-251. Nuremberg, Germany, Springer Verlag.
[102] L.C. Paulson. Proving Properties of Security Protocols by Induction [C]. Proceedings of the IEEE Computer Security Foundations Workshop X. I EEE Computer Society Press, 1997. 70-83.
[103] L.C. Paulson. The inductive approach to verifying cryptographic protocols [J]. Journal of Computer Security, 1998. (6):85~128.
[104] M. Wenzel. The Isabelle/Isar Reference Manual [EB/OL]. 2011. http://www.cl.cam.ac.uk/ research/ hvg /Isabelle/documentation.html.
[105] G. Bella, C. Longo, L. C. Paulson. Verifying second-level security protocols [C]. In Theoremproving in higher order logics: TPHOLs 2003, D. Basin and B. Wolff, Eds. LNCS 2758. Springer-Verlag, New York. 2003:352–366.
[106] G. Bella, L. C. Paulson. Mechanical proofs about a nonrepudiation protocol [C]. InTheorem proving in higher order logics: TPHOLs 2001, R. J. Boulton and P. B. Jackson, Eds. LNCS, vol. 2152. Springer-Verlag, New York. 2001.91–104.
[107] G. Bella, L. C. Paulson. Accountability protocols: Formalized and verified [J]. ACM Transactions on Information and System Security, 2006. Vol. 9, No. 2, 138–161.
[108] F.J. Thayer, J.C. Herzog, J.D. Guttman. Strand spaces: Why is a security protocol correct? [C] In: Proceedings of the 1998 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998. 160~171.
[109] F.J. Thayer, J.C. Herzog, J.D. Guttman. Strand spaces: Honest ideals on strand spaces [C]. In: Proceedings of the 1998 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1998. 66~77.
[110] F.J. Thayer, J.C. Herzog, J.D. Guttman. Strand spaces: Proving security protocols correct [J]. Journal of Computer Security, 1999. 7: 191~230.
[111] C. Meadows. A Model of Computation for the NRL Protocol Analyzer [C]. In: Proc. of the 7th Computer Security Foudations Workshop.IEEE Computer Society Press. 1994.
[112] D. Song. Athena: A new efficient automatic checker for Security protocol Analysis [C]. ln: Proceedings of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999. 192-202.
[113] J. D. Guttman. Fair exchange in strand spaces [C]. In M. Boreale and S. Kremer, editors, SecCo: 7th International Workshop on Security Issues in Concurrency, EPTCS. Electronic Proceedings in Theoretical Computer Science. 2009.
[114] J. D. Guttman. State and Progress in Strand Spaces: Proving Fair Exchange [EB/OL]. 2010. Journal of Automated Reasoning manuscript, http://web.cs.wpi.edu/~guttman/spiss/spiss.pdf
[115] I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov. A meta-notation for protocol analysis [C]. Proceedings of the 12th IEEE Computer Security Foundations Workshop: CSFW’99, IEEE Computer Society Press, 1999: 55–69.
[116] N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov. Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security, 2004. 12(2):247–311.
[117]卿斯汉.电子商务协议中的可信第三方角色[J].软件学报, 2003. 14(11):1936-1943.
[118]卿斯汉,李改成.公平交换协议的一个形式化模型.中国科学(E辑) [J], 2005. 35(2): 161~ 172.
[119]陈庆锋,白硕,王驹,等.电子商务安全协议及其非单调动态逻辑验证[J].软件学报, 2000.11(2): 240~250.
[120]白硕,隋立颖,陈庆锋等.安全协议的验证逻辑[J].软件学报. 2000, 11(2):213~221.
[121] J. Cederquist, M. T. Dashti. An intruder model for verifying liveness in security protocols [C]. In M. Winslett, A. D. Gordon, D. Sands (eds), FMSE, ACM, 2006: 23-32.
[122] D. K?hler, R. Küsters, T. Truderung. Infinite State AMC-Model Checking for Cryptographic Protocols [C]. Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007), IEEE, Computer Society Press, 2007: 181-190.
[123] Q. Zhang, K. Markantonakis, K. Mayes. A practical fair-exchange e-payment protocol for anonymous purchase and physical delivery [C]. In: Proceedings of IEEE international conference on computers ystems and applications, Dubai, UAE, 2006. p.851–858.
[124] J. Grau. Online privacy and security: the fear factor [EB/OL]. 2006. http://www.emarketer. com/ Reports/All/Privacy_retail_apr06.aspx
[125] C. Costello, H. Hisil, C. Boyd, Nieto, G. Juan, Wong, K. Kenneth. Faster pairings on special Weierstrass curves [C]. In: Proceeding of the Second International Conference on Pairing-based Cryptography, Pairing 2009, LNCS, 5671. Springer, New York, 2009: 89–101.
[126] M. Scott, N. Benger, M. Charlemagne, D. Perez, E.J. Kachisa. Fast hashing to G2 on pairing-friendly curves [C]. In: Proceeding of the Second International Conference on Pairing-based Cryptography, Pairing 2009. LNCS, 5671. Springer, New York, 2009: 102–113.
[127] D. Chaum. Blind signatures for untraceable payments [C]. In: Advances in Cryptology: Proceedings of Crypt’82. Plenum, NY, 1983: 199–203.
[128] C. Fan, W. Chen. An efficient blind signature scheme for information hiding [J]. International Journal of Electronic Commerce. 2001. 6 (1):93–100.
[129] C. Chang, Y. Lai. A flexible date-attachment scheme on E-cash [J]. Computers and Security. 2003. 22 (2):160-166.
[130] W. Juang. RO-cash: An efficient and practical recoverable pre-paid offline e-cash scheme using bilinear pairings [J]. The Journal of Systems and Software. 2010. 83: 638–645.
[131] C. Popescu, H. Oros. An off-line electronic cash system based on bilinear pairings [C]. In: 14th International Workshop on Systems, Signals and Image Processing and 6th EURASIP Conference focused on Speech and Image Processing, Multimedia Communications and Services, 2007: 438-440.
[132] L. Zhang, F. Zhang, B. Qin, S. Liu. Provably-secure electronic cash based on certificate- less partially-blind signatures [J]. Electronic Commerce Research and Applications. 2011. doi:10.1016/j.elerap.2011.01.004.
[133] M. Abe, E. Fujisaki. How to date blind signatures [C]. In: Proceedings of advances incryptology: Asiacrypt’96, LNCS, vol.1163. Berlin, Germany: Springer, 1999.244–251.
[134] S. Chow, L. Hui, S. Yiu, K. Chow. Two improved partially blind signature schemes from bilinear pairings [C]. Proceedings of the Information Security and Privacy, 2004. LNCS, Volume 3574, 2004. 355-411.
[135] W. Stallings. Cryptography and Network Security [C]. Third ed. Prentice Hall International. 2003.
[136] F. Zhang, R. Safavi-Naini, W. Susilo. An efficient signature scheme from bilinear pairings and its applications [C]. In: Goos, G., Hartmanis, J., van Leeuwen, J. (Eds.), Public Key Cryptography-PKC 2004, LNCS, vol. 2947. Springer, New York, 2004: 277–290.
[137] K. Liu, P. Tsang, S. Wong. Recoverable and untraceable E-cash [C]. In: Second European PKI Workshop: Research and Applications, LNCS 3545. Springer, New York, 2005: 206–214.
[138] D. Pointcheval, J, Stern. Security Arguments for Digital Signatures and Blind Signatures [J]. Journal of Cryptology: The Journal of the International Association for Cryptologic Research, 2000. 13(3):361–396.
[139] N. Koblitz, A. Menezes, S. Vanstone. The state of elliptic curve cryptography [J]. Designs, Codes and Cryptography, 2000. 19, 173-193.
[140] C. Fan, W. Sun, V. S. Huang. Provably secure randomized blind signature scheme based on bilinear pairing [J]. Computers and Mathematics with Applications 2010, (60): 285-293.
[141] A. Boldyreva. Threshold signatures, multisignatures and blind signatures based on the Gap-Diffie-Hellman-group signature scheme [C]. In: Proceeding of PKC'03, in: LNCS, vol. 2567, 2003. p. 31-46.
[142] H. Elkamchouchi, Y. Abouelseoud. A new blind identity-based signature scheme [C], In: Proceeding of CCNS 2008, IEEE, 2008: 1102-1106.
[143] Y. Yu, S. Zheng, Y. Yang. ID-based blind signatrue and proxy blind signature without thrusted PKG [C]. In: Proceeding of CSICC 2008, LNCS, 2008: 821-824.
[144] F. Zhang, K. Kim. Efficient ID-based blind signature and proxy signature from bilinear pairings [C]. In: Proceeding of ACISP 2003, in: LNCS, vol. 2727, 2003: 312-323.
[145] S. Lin, D. Liu. An incentive-based electronic payment scheme for digital content transactions over the Internet [J]. Journal of Network and Computer Applications. 2009. 32: 589–598.
[146] C. Fan, S. Huang, P Ho, C. Lei. Fair anonymous rewarding based on electronic cash [J]. The Journal of Systems and Software. 2009. 82: 1168–1176.
[2] M. Bishop. Introduction to Computer Security [M]. Massachusetts: Addison-Wesley. 2005.
[3] R. Kauffman, C. Wood. 2007. Revolutionary research strategies for e-business: A philosophy of science view in the age of the Internet [EB/OL]. http://www.misrc. umn.edu/ workingpapers/ fullPapers/2006/0614_113006.pdf
[4] T. Sandholm. Unenforced e-commerce transactions [J]. IEEE Internet Computing, 1997. 1(6):47– 54.
[5] S. Even, Y. Yacobi. Relations among public key signature systems [R]. Technical Report 175, Computer Science Dept., Technion, Haifa, Isreal, Mar. 1980.
[6] R. Needham, M. Schroeder. Using encryption for authentication in large networks of computers [J]. Communications of the ACM, 1978. 21(12): 993~999.
[7] D. Denning, G. Sacco. Timestamps in key distribution protocols [J]. Communications of the ACM, 1981. 24(8):533~536.
[8] G. Lowe. Breaking and fixing the Needham-Schroder public-key protocol using FDR [C]. In: Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science. Springer-Verlag, 1996:147~166.
[9]林语堂.人生的盛宴[M].长沙:湖南文艺出版社.2002.
[10] B. Chellas. Modal Logic: An Introduction [M]. Cambridge University Press, Cambridge. 1980.
[11] P. Blackburn, M. de Rijke, Y. Venema. Modal Logic [M]. Cambridge: Cambridge University Press. 2001.
[12] Y. Venema. Temporal Logic [M]. In Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell. 2001.
[13] A. Pnueli. The temporal semantics of concurrent programs [J]. In Theoretical Computer Science, 1981. 13: 1–20.
[14] E. Clarke, E. Emerson. Design and synthesis of synchronization skeletons for branching-time temporal logic [C]. In Proceedings of Workshop on Logic of Programs, volume 131 of LNCS, Springer-Verlag. 1981:52–71.
[15] E. Emerson. Temporal and modal logic [J]. In van Leeuwen, J., editor, Handbook ofTheoretical Computer Science, 1990. 996–1071. Elsevier Science Publishers.
[16] E. Emerson, J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time [J]. Journal of Computer and System Sciences, 1985. 30(1):1–24.
[17] G. Arora, M. Hanneghan, M. Merabti. P2p commercial digital content exchange [J]. Electronic Commerce Research and Applications, 2005. 4:250-263.
[18] F. Lin, H. Lo, C. Wang. Can a P2P File-Sharing Network Become an e-Marketplace [C]. Proceedings of the 41st Hawaii International Conference on System Sciences (HICSS 2008), Waikoloa, Big Island, Hawaii, IEEE, 2008:298-307.
[19] C. Li, B. Yu, K. Sycara. An incentive mechanism for message relaying in unstructured peer-to-peer systems [J]. Electronic Commerce Research and Applications, 2009. 8: 315–326.
[20] S. Kremer, O. Markowitch, J. Zhou. An intensive survey of non-repudiation protocols [J]. Computer Communications, 2002. 25(17):1606–1621.
[21] S. Kremer. Formal Analysis of Optimistic Fair Exchange Protocols [Ph.D. Thesis]. Universit′e Libre de Bruxelles. 2003.
[22] P. Ezhilchelvan, S. Shrivastava. A family of trusted third party based fair-exchange protocols [J]. IEEE Trans. Dependable Secur. Comput., 2005. 2(4):273–286.
[23] M. Ben-Or, O. Goldreich, S. Micali, R.L. Rivest. A fair protocol for signing contracts [J]. IEEE Transaction on Information Theory, 1990. 36(1):40–46.
[24] M. Blum. How to exchange (secret) keys [J]. ACM Transactions on Computer Systems, 1983. 1(2):175–193.
[25] S. Even. Protocol for signing contracts [C]. In Allen Gersho, editor, Advances in Cryptology: A Report on Crypto 81, 1982. 148–153.
[26] S. Even, O. Goldreich, A. Lempel. A randomized protocol for signing contracts [J]. Communications of the ACM, 1985. 28(6):637–647.
[27] J.A. Garay, M. Jakobsson, P. MacKenzie. Abuse-free optimistic contract signing[C]. In: Proc. Advances in Cryptology-Crypto’99, 1999:449~466.
[28] P. Syverson. Weakly secret bit commitment: Applications to lotteries and fair exchange [C]. In 11th IEEE Computer Security Foundations Workshop, 1998:2–13.
[29] H. Pagnia, F.C. G?rtner. On the impossibility of fair exchange without a trusted third party [R]. Technical Report TUD-BS-1999-02, Darmstadt University of Technology, Darmstadt, Germany. 1999.
[30] A. Bahreman, D. Tygar. Certified electronic mail [C]. In Symposium on Network and Distributed Systems Security, 1994: 3–19. Internet Society.
[31] J. Zhou, D. Gollmann. Certified electronic mail. In Computer Security[C]. ESORICS 1996,volume 1146 of LNCS, 1996:160–171.
[32] B. Cox, D. Tygar, M. Sirbu. NetBill security and transaction protocol [C]. In USENIX Association, editor, First USENIX Workshop of Electronic Commerce, 1995:77–88. USENIX.
[33] H. Deng, L. Gong, A. Lazar, W. Wang. Practical protocols for certified electronic mail [J]. Journal of Network and System Management, 1996. 4(3):279–297.
[34] J. Zhou, D. Gollmann. A fair non-repudiation protocol [C]. In IEEE Symposium on Research in Security and Privacy, Research in Security and Privacy, 1996: 55–61. IEEE Computer Society.
[35] J. Zhou, D. Gollmann. An efficient non-repudiation protocol [C]. In 10th IEEE Computer Security Foundations Workshop, 1997: 126–132. IEEE Computer Society Press.
[36] J. Zhou, D. Gollmann. Evidence and non-repudiation [J]. Journal of Network and Computer Applications, 1997. 20:267–281.
[37] J. Zhou, D. Gollmann. Towards verification of non-repudiation protocols [C]. In International Refinement Workshop and Formal Methods Pacific, 1998: 370–380, Canberra, Australia.
[38] M. K. Franklin, M. K. Reiter. Fair exchange with a semi-trusted third party [C]. In 4th ACM Conference on Computer and Communications Security, 1997:1–5. ACM Press.
[39] N. Asokan. Fairness in Electronic Commerce [D]. PhD thesis, University of Waterloo. 1998.
[40] N. Asokan, B. Baum-Waidner, M. Schunter, M. Waidner. Optimistic synchronous multi-party contract signing [R]. Research Report RZ 3089, IBM Research Division. 1998.
[41] N. Asokan, M. Schunter, M. Waidner. Optimistic protocols for multiparty fair exchange [R]. Research Report RZ 2892 (# 90840), IBM Research. 1996.
[42] N. Asokan, M. Schunter, M. Waidner. Optimistic protocols for fair exchange [C]. In Tsutomu Matsumoto, editor, 4th ACM Conference on Computer and Communications Security, 1997: 8–17, Zurich, Switzerland, ACM Press.
[43] N. Asokan, V. Shoup, M. Waidner. Asynchronous protocols for optimistic fair exchange. In IEEE Symposium on Research in Security and Privacy, 1998: 86–99, Oakland, CA, Technical Committee on Security and Privacy, IEEE Computer Society Press.
[44] N. Asokan, V. Shoup, M. Waidner. Optimistic fair exchange of digital signatures [C]. In Advances in Cryptology—Eurocrypt, volume 1403 of LNCS, 1998:591–606.
[45] N. Asokan, V. Shoup, M. Waidner. Optimistic fair exchange of digital signatures [J]. IEEE Journal on Selected Areas in Communications, 2000. 18(4):593–610.
[46] F. Bao, R.H. Deng, W. Mao. Efficient and practical fair exchange protocols with off-line TTP [C]. Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, IEEEComputer Society, California, 1998:77~85.
[47] C. Boyd, E. Foo. Off-line fair payment protocols using convertible signatures [C]. In Advances in Cryptology—Asiacrypt 1998, volume 1514 of LNCS, 1998:271–285. Springer- Verlag.
[48] J. Hernandez-Ardieta, A. Gonzalez-Tablas, B. Alvarez. An optimistic fair exchange protocol based on signature policies [J]. computers & security. 2008. 27(10):309~322.
[49] Q. Huang, G. Yang, D. S. Wong, W. Susilo. Ambiguous optimistic fair exchange [C]. In Advances in Cryptology - ASIACRYPT 2008, Springer LNCS 5350, 2008:74–89.
[50] H. Pagnia, H. Vogt, F.C. G?rtner. 2003. Fair Exchange [J]. The Computer Journal, 46(1): 55~76.
[51] B. Pfitzmann, M. Schunter, M. Waidner. Optimal efficiency of optimistic contract signing [C]. In Seventeenth Annual ACM Symposium on Principles of Distributed Computing, 1998:113–122, New York, ACM.
[52] E. M. Schunter. Optimistic Fair Exchange [D]. PhD thesis, Universit¨at des Saarlandes. 2000.
[53] H. Vogt, H. Pagnia, F. C. G?rtner. Modular fair exchange protocols for electronic commerce [C]. In 15th Annual Computer Security Applications Conference, 1999: 3–11, Phoenix, Arizona, IEEE Computer Society Press.
[54] G. Wang. Generic non-repudiation protocols supporting transparent off-line TTP [J]. Journal of Computer Security, 2006. 14(5):441–467.
[55] G. Wang. An Abuse-Free Fair Contract-Signing Protocol Based on the RSA Signature [J]. IEEE Transactions on Information Forensics and Security, 2010. 5 (1): 158-168.
[56] J. Zhou, K. Lam. Securing digital signatures for non-repudiation [J]. Computer Communications, 1999. 22(8):710–716.
[57] V. Shmatikov, J. Mitchell. Analysis of a fair exchange protocol [C]. In Symposium on Network and Distributed Systems Security (NDSS 2000), 2000: 119-128, San Diego, CA, Internet Society.
[58] V. Shmatikov, J. Mitchell. Analysis of abuse-free contract Signing [C]. Notes In Financial Cryptography 2000, volume 1962 of LNCS, 2000: 174-191, Anguilla, BritishweSt Indies, Springer-Verlag.
[59] V. Shmatikov, J. Mitchell. Finite-state analysis of two contract signing protocols [J]. Theoretical Computer Science. 2002. 283(02): 419~450.
[60] S. Gürgens, C. Rudolph. Security analysis of (un-) fair non-repudiation protocols [C]. In FASec’02, volume 2629 of LNCS, 2003:97–114. Springer.
[61] D. P. Hankes, S. M?dersheim, L. Viganò. A Formalization of Off-Line Guessing for SecurityProtocol Analysis [C], in F. Baader, A. Voronkov (eds), Proceedings of LPAR’04, vol.3452 of LNAI, Springer, 2005:363–379.
[62] A. Armando, R. Carbone, L. Compagna. LTL model checking for security protocols [C]. In CSF, 2007:385–396.
[63] I. Ray, I. Ray, N. Natarajan. An anonymous and failure resilient fair-exchange e-commerce protocol [J]. Decision Support Systems, 2005. 39(3):267~292.
[64] D. Dolev, A.C. Yao. On the security of public key protocols [J]. IEEE Transactions on Information Theory, 1983. 29(2): 198~208.
[65] K. Kim, S. Park, J. Baek. Improving fairness and privacy of Zhou-Gollmann’s fair non- repudiation protocol [C]. In: Gong K, Niu Z, eds. 2000 IEEE Int’l Conf. on Communication. Beijing: IEEE Computer Society Press, 2000:1743?1747.
[66]黎波涛,罗军舟.不可否认协议时限性的形式化分析[J].软件学报, 2006. 17(7):1510-1516.
[67] M. Burrows, M. Abadi, R. Needham. A logic of authentication [C]. In: Proceedings of the Royal Society of London A, Vol 426. 1989:233~271.
[68] S.P. Miller, C. Neuman, J.I. Schiller, J.H. Saltzer. Kerberos authentication and authorization system [R]. Project Athena Technical Plan Section E.2.1, MIT. 1987.
[69] L. Gong, R. Needham, R. Yahalom. Reasoning about Belief in Cryptographic Protocols [C]. In : Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy , 1990. 234~248. Los Alamitos ,California : IEEE Computer Society Press.
[70] M. Abadi, M. R. Tuttle. A Semantics for a Logic of Authentication [C]. In : Proceeding of the Tenth ACM Symposium on Principles of Distributed Computing. ACM Press, 1991: 201~216.
[71] P. C. van Oorschot. Extending Cryptographic Logics of Belief to Key Agreement Protocols (Extended Abstract) [C]. In Proceedings of the First ACM Conference on Computer and Communications Security, 1993:232~243.
[72] P. F. Syverson, P. C. van Oorschot. On Unified Some Cryptographic Protocol Logics [C]. In: Proc. of the’94 IEEE Computer Society Symp. on Security and Privacy. Oakland: IEEE Computer Society Press, 1994:14?28.
[73] P. F. Syverson, P. C. van Oorschot. A Unified Cryptographic Protocol Logics [R]. NRL Publication 5540~227, Naval Research Lab. 1996.
[74] R. Kailar. Accountability in electronic commerce protocols [J]. IEEE Trans. on Software Engineering, 1996. 22(5):313-328.
[75]卿斯汉.一种新型的非否认协议[J].软件学报. 2000.11(10): 1338-1343.
[76]李先贤,怀进鹏.公平的非否认密码协议及其形式分析与应用[J].软件学报, 2000. 11 (12): 1628? 1634.
[77]周典萃,卿斯汉,周展飞. Kailar逻辑的缺陷[J].软件学报, 1999. 10(12):171?173.
[78]周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具[J].软件学报, 2001. 12(09): 171? 173.
[79]汪学明.多方安全协议的形式化分析方法研究与应用[D].博士学位论文,贵州大学. 2008.
[80] C. Hoare. Communicating Sequential Processes [M]. Prentice Hall International Englewoo d Cliff S, NJ. 1985.
[81] A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR [C]. In 8th IEEE Computer Security Foundations Workshop, 1995. 98–107. IEEE Computer Society.
[82] S. A. Schneider. Verifying authentication protocols with CSP [C]. In Simon Foley, editor, 10th IEEE Computer Security Foundations Workshop, 1997: 3–17, Rockport, Massachusetts, USA, June IEEE Computer Society Press.
[83] S. A. Schneider. Formal analysis of a non-repudiation protocol [C]. In 11th IEEE Computer Security Foundations Workshop, 1998: 54–65, Washington - Brussels -Tokyo, IEEE.
[84] N. Evans, S. A.Schneider. Verifying security protocols with PVS: widening the rank function approach [J]. J Log Algebr Program, 2005. 64(2):253-284.
[85] K. Wei, J. Heather. Towards verification of timed non-repudiation protocols [C]. FAST 2005.San Francisco, CA, USA, 2005. 244-257.
[86]韩志耕,罗军舟,王良民.不可否认协议分析的增广CSP方法[J].通信学报. 2008. 29(10): 8-18.
[87] D.L. Dill, A.J. Drexler, A.J. Hu, C.H. Yang. Protocol verification as a hardware design aid [C]. Proceedings of the 1992 IEEE International Conference on Computer Design: VLSI in Computer Sand Processors, 1992. 522-525, IEEE Computer Society Press.
[88] J.C. Mitchell, M. Mitchell, U. Stern. Automated Analysis of Cryptographic Protocols USing MurΦ[C]. Proceedings of the 1997 IEEE Sympossium on Security and Privacy, 1997. 141-151, IEEE Computer Society Press.
[89] M. Tatebayashi, N. MatSuzaki, D. Neuman. Key distribution protocol for digital mobile communication Systems [C]. Proceedings of CRYPTO'89, 1990. 324-333, Springer Verlag.
[90] J. Kohl, B. Neuman, T. TSo. The evolution of the Kerberos authentication Service ver.5 [C]. Distributed Open Systems (Brazier F., JohanSen D. EdS.), 1994. 78-94 IEEE Computer Society Press.
[91] S. Kremer, O. Markowitch. A multi-party non-repudiation protocol [C]. In 15th International Conference on Information Security—Sec 2000, IFIP World Computer Congress, 2000: 271–280, Beijing, China, Kluwer Academic.
[92] S. Kremer, O. Markowitch. Optimistic non-repudiable information exchange [C]. In J.Biemond, editor, 21st Symp. on Information Theory in the Benelux, 2000: 139–146, Wassenaar, The Netherlands, Werkgemeenschap Informatieen Communicatie theorie, Enschede.
[93] S. Kremer, O. Markowitch. Selective receipt in certified e-mail [C]. In Advances in Cryptology—Indocrypt 2001, Lecture Notes in Computer Science. Springer-Verlag. 2001.
[94] S. Kremer, O. Markowitch. Fair multi-party non-repudiation [J]. International Journal on Information Security, 2003.1(4):223–235.
[95] S. Kremer, J. Raskin. A game-based verification of nonrepudiation and fair exchange protocols [C]. In Kim G. Larsen and Mogens Nielsen, editors, Concurrency Theory—CONCUR 2001, volume 2154 of LNCS, 2001: 551–565, Aalborg, Denmark, Springer-Verlag.
[96] S. Kremer, J. Raskin. Game analysis of abuse-free contract signing [C]. In Steve A. Schneider, editor, 15th IEEE Computer Security Foundations Workshop, 2002: 206–220, Cape B reton, Nova Scotia, Canada, IEEE Computer Society Press.
[97] S. Kremer, J. Raskin. A game-based verification of non-repudiation and fair exchange protocols [J]. Journal of Computer Security. 2003.11(3): 399~429.
[98] R. Alur, T. A. Henzinger, O. Kupferman. Alternating-time temporal logic [C]. In 38th Annual Symposium on Foundations of Computer Science, 1997: 100–109. IEEE Computer Society Press.
[99] P. H. DrieISma, S. ModerSheim. The ASW Protocol Revisited: A Unified View [J]. Electr. Notes Theor. Comput. Sci. 2005. 125(1):145-161.
[100] M.T. Dashti. Keeping fairness alive [D]. Ph.D. Thesis. Vrije Universiteit Amsterdam. 2008.
[101] S. Basagiannis, P. Katsaros, A. Pombortsis. Intrusion Attack Tactics for the model checking of e-commerce security guarantees [C]. In Proc. of the 26th International Conference on Computer Safety, Reliability and Security (SAFECOMP), LNCS 4680, 2007: 238-251. Nuremberg, Germany, Springer Verlag.
[102] L.C. Paulson. Proving Properties of Security Protocols by Induction [C]. Proceedings of the IEEE Computer Security Foundations Workshop X. I EEE Computer Society Press, 1997. 70-83.
[103] L.C. Paulson. The inductive approach to verifying cryptographic protocols [J]. Journal of Computer Security, 1998. (6):85~128.
[104] M. Wenzel. The Isabelle/Isar Reference Manual [EB/OL]. 2011. http://www.cl.cam.ac.uk/ research/ hvg /Isabelle/documentation.html.
[105] G. Bella, C. Longo, L. C. Paulson. Verifying second-level security protocols [C]. In Theoremproving in higher order logics: TPHOLs 2003, D. Basin and B. Wolff, Eds. LNCS 2758. Springer-Verlag, New York. 2003:352–366.
[106] G. Bella, L. C. Paulson. Mechanical proofs about a nonrepudiation protocol [C]. InTheorem proving in higher order logics: TPHOLs 2001, R. J. Boulton and P. B. Jackson, Eds. LNCS, vol. 2152. Springer-Verlag, New York. 2001.91–104.
[107] G. Bella, L. C. Paulson. Accountability protocols: Formalized and verified [J]. ACM Transactions on Information and System Security, 2006. Vol. 9, No. 2, 138–161.
[108] F.J. Thayer, J.C. Herzog, J.D. Guttman. Strand spaces: Why is a security protocol correct? [C] In: Proceedings of the 1998 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998. 160~171.
[109] F.J. Thayer, J.C. Herzog, J.D. Guttman. Strand spaces: Honest ideals on strand spaces [C]. In: Proceedings of the 1998 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1998. 66~77.
[110] F.J. Thayer, J.C. Herzog, J.D. Guttman. Strand spaces: Proving security protocols correct [J]. Journal of Computer Security, 1999. 7: 191~230.
[111] C. Meadows. A Model of Computation for the NRL Protocol Analyzer [C]. In: Proc. of the 7th Computer Security Foudations Workshop.IEEE Computer Society Press. 1994.
[112] D. Song. Athena: A new efficient automatic checker for Security protocol Analysis [C]. ln: Proceedings of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999. 192-202.
[113] J. D. Guttman. Fair exchange in strand spaces [C]. In M. Boreale and S. Kremer, editors, SecCo: 7th International Workshop on Security Issues in Concurrency, EPTCS. Electronic Proceedings in Theoretical Computer Science. 2009.
[114] J. D. Guttman. State and Progress in Strand Spaces: Proving Fair Exchange [EB/OL]. 2010. Journal of Automated Reasoning manuscript, http://web.cs.wpi.edu/~guttman/spiss/spiss.pdf
[115] I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov. A meta-notation for protocol analysis [C]. Proceedings of the 12th IEEE Computer Security Foundations Workshop: CSFW’99, IEEE Computer Society Press, 1999: 55–69.
[116] N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov. Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security, 2004. 12(2):247–311.
[117]卿斯汉.电子商务协议中的可信第三方角色[J].软件学报, 2003. 14(11):1936-1943.
[118]卿斯汉,李改成.公平交换协议的一个形式化模型.中国科学(E辑) [J], 2005. 35(2): 161~ 172.
[119]陈庆锋,白硕,王驹,等.电子商务安全协议及其非单调动态逻辑验证[J].软件学报, 2000.11(2): 240~250.
[120]白硕,隋立颖,陈庆锋等.安全协议的验证逻辑[J].软件学报. 2000, 11(2):213~221.
[121] J. Cederquist, M. T. Dashti. An intruder model for verifying liveness in security protocols [C]. In M. Winslett, A. D. Gordon, D. Sands (eds), FMSE, ACM, 2006: 23-32.
[122] D. K?hler, R. Küsters, T. Truderung. Infinite State AMC-Model Checking for Cryptographic Protocols [C]. Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007), IEEE, Computer Society Press, 2007: 181-190.
[123] Q. Zhang, K. Markantonakis, K. Mayes. A practical fair-exchange e-payment protocol for anonymous purchase and physical delivery [C]. In: Proceedings of IEEE international conference on computers ystems and applications, Dubai, UAE, 2006. p.851–858.
[124] J. Grau. Online privacy and security: the fear factor [EB/OL]. 2006. http://www.emarketer. com/ Reports/All/Privacy_retail_apr06.aspx
[125] C. Costello, H. Hisil, C. Boyd, Nieto, G. Juan, Wong, K. Kenneth. Faster pairings on special Weierstrass curves [C]. In: Proceeding of the Second International Conference on Pairing-based Cryptography, Pairing 2009, LNCS, 5671. Springer, New York, 2009: 89–101.
[126] M. Scott, N. Benger, M. Charlemagne, D. Perez, E.J. Kachisa. Fast hashing to G2 on pairing-friendly curves [C]. In: Proceeding of the Second International Conference on Pairing-based Cryptography, Pairing 2009. LNCS, 5671. Springer, New York, 2009: 102–113.
[127] D. Chaum. Blind signatures for untraceable payments [C]. In: Advances in Cryptology: Proceedings of Crypt’82. Plenum, NY, 1983: 199–203.
[128] C. Fan, W. Chen. An efficient blind signature scheme for information hiding [J]. International Journal of Electronic Commerce. 2001. 6 (1):93–100.
[129] C. Chang, Y. Lai. A flexible date-attachment scheme on E-cash [J]. Computers and Security. 2003. 22 (2):160-166.
[130] W. Juang. RO-cash: An efficient and practical recoverable pre-paid offline e-cash scheme using bilinear pairings [J]. The Journal of Systems and Software. 2010. 83: 638–645.
[131] C. Popescu, H. Oros. An off-line electronic cash system based on bilinear pairings [C]. In: 14th International Workshop on Systems, Signals and Image Processing and 6th EURASIP Conference focused on Speech and Image Processing, Multimedia Communications and Services, 2007: 438-440.
[132] L. Zhang, F. Zhang, B. Qin, S. Liu. Provably-secure electronic cash based on certificate- less partially-blind signatures [J]. Electronic Commerce Research and Applications. 2011. doi:10.1016/j.elerap.2011.01.004.
[133] M. Abe, E. Fujisaki. How to date blind signatures [C]. In: Proceedings of advances incryptology: Asiacrypt’96, LNCS, vol.1163. Berlin, Germany: Springer, 1999.244–251.
[134] S. Chow, L. Hui, S. Yiu, K. Chow. Two improved partially blind signature schemes from bilinear pairings [C]. Proceedings of the Information Security and Privacy, 2004. LNCS, Volume 3574, 2004. 355-411.
[135] W. Stallings. Cryptography and Network Security [C]. Third ed. Prentice Hall International. 2003.
[136] F. Zhang, R. Safavi-Naini, W. Susilo. An efficient signature scheme from bilinear pairings and its applications [C]. In: Goos, G., Hartmanis, J., van Leeuwen, J. (Eds.), Public Key Cryptography-PKC 2004, LNCS, vol. 2947. Springer, New York, 2004: 277–290.
[137] K. Liu, P. Tsang, S. Wong. Recoverable and untraceable E-cash [C]. In: Second European PKI Workshop: Research and Applications, LNCS 3545. Springer, New York, 2005: 206–214.
[138] D. Pointcheval, J, Stern. Security Arguments for Digital Signatures and Blind Signatures [J]. Journal of Cryptology: The Journal of the International Association for Cryptologic Research, 2000. 13(3):361–396.
[139] N. Koblitz, A. Menezes, S. Vanstone. The state of elliptic curve cryptography [J]. Designs, Codes and Cryptography, 2000. 19, 173-193.
[140] C. Fan, W. Sun, V. S. Huang. Provably secure randomized blind signature scheme based on bilinear pairing [J]. Computers and Mathematics with Applications 2010, (60): 285-293.
[141] A. Boldyreva. Threshold signatures, multisignatures and blind signatures based on the Gap-Diffie-Hellman-group signature scheme [C]. In: Proceeding of PKC'03, in: LNCS, vol. 2567, 2003. p. 31-46.
[142] H. Elkamchouchi, Y. Abouelseoud. A new blind identity-based signature scheme [C], In: Proceeding of CCNS 2008, IEEE, 2008: 1102-1106.
[143] Y. Yu, S. Zheng, Y. Yang. ID-based blind signatrue and proxy blind signature without thrusted PKG [C]. In: Proceeding of CSICC 2008, LNCS, 2008: 821-824.
[144] F. Zhang, K. Kim. Efficient ID-based blind signature and proxy signature from bilinear pairings [C]. In: Proceeding of ACISP 2003, in: LNCS, vol. 2727, 2003: 312-323.
[145] S. Lin, D. Liu. An incentive-based electronic payment scheme for digital content transactions over the Internet [J]. Journal of Network and Computer Applications. 2009. 32: 589–598.
[146] C. Fan, S. Huang, P Ho, C. Lei. Fair anonymous rewarding based on electronic cash [J]. The Journal of Systems and Software. 2009. 82: 1168–1176.