电子商务协议安全性的形式化分析方法研究
|
摘要
为了保障电子商务活动中各方的利益不被侵害,需要利用基于密码技术的电子商务协议来保证商务活动的安全性,因此对电子商务协议的安全性的形式化分析是一个至关重要的有难度的问题。
针对电子商务协议安全性的形式化分析方法的研究晚于对传统的密码协议的形式化分析方法的研究,目前主要的分析方法有：Kailar逻辑,SVO逻辑,基于SMV的模型检测,基于ATL／ATS博弈逻辑系统的分析方法,以及卿斯汉等学者提出的对两方或者多方电子商务协议和公平交换协议进行分析、证明的方法。这些方法分别从协议的消息语义、协议结构角度对协议进行建模与分析。综合考虑协议的消息和结构两个因素的形式化分析方法较少。当前,对电子商务协议的形式化分析方法的研究依然是一个热点领域。
本文首先对主要的博弈逻辑：ATL逻辑、ATEL逻辑、ATL-A／ATEL-A逻辑、多代理逻辑等,进行了研究,发现他们对博弈主体的状态转移的建模方式采用固定的步骤。本文提出了一个智能代理博弈主体模型(IA),在IA中,一个博弈主体的状态由博弈主体根据其接收的消息按照逻辑推理规则进行状态的更新,在每一个状态下,根据推理规则推演出当前可发送消息集合。多个IA构成了一个基于消息的并发博弈系统(MCGS),这个系统中每一步的迁移是通过两个动作完成,分别是：各个IA的收发消息,以及各IA根据自己接收的消息按逻辑推理规则更新自身状态。整个系统的策略使用基于ATL扩展的ATL-B逻辑进行表达。IA,MCGS,ATL-B共同构成了一个对系统进行建模的工具,称为MIAG(多智能体博弈)系统,这个系统的特点是各博弈主体之间只通过消息交互,每个主体有自己的认知推理逻辑规则用以更新状态,与其他博弈逻辑相比,博弈主体具有动态的状态迁移特性。
基于MIAG模型,本文构建了一个电子商务协议分析的新模型,其主要特点是在博弈主体中引入了针对电子商务协议的逻辑推理规则用于更新博弈主体的认知状态；使用ATL-B策略公式表达不同的安全目标,使其能够适应对不同目的的电子商务协议的建模要求。在新模型中,将协议主体分成诚实主体与非诚实主体两个集合,分析过程依次针对诚实主体的各个协议运行迹分析非诚实方是否存在攻击策略。本文总结了四种典型的非诚实方攻击策略,使得本文的分析模型能够比之前的模型更切合实际的形式化非诚实主体的能力。
应用电子商务协议分析的新模型,本文对一个公平交换协议Nenadi04和一个无需中央机构的电子投票协议Su-Vote协议进行了分析,发现了协议中存在的漏洞,说明了新模型的有效性。在对Nenadi04协议的分析中,利用新模型发现了发方不可否认证据不满足可追究性的要求,也发现了协议中发起方可以利用并发多个协议实例来混淆应答方对恢复子协议接收消息的识别,从而破坏协议的公平性。这个协议实例说明了新模型能够同时处理对消息和协议结构的分析。对Su-Vote协议的分析中发现非诚实的投票人能够篡改投票结果并能够控制协议是否终止
本文最后研究了公平交换协议的一种基础签名算法——并发签名,提出并定义了并发签名的可追踪性以保证签名方与签署消息之间的唯一绑定关系,防止签名被滥用。基于学者王贵林提出的一个完美并发签名方案,本文设计了一个满足可追踪性的并发签名方案,并基于此方案设计了一个无需第三方的公平交换协议。
E-commerce protocol is designed to fulfill business flow and prtotect the attender's profit using cryptography technical. So, it is a common sense that the formal analysis of the security of E-commerce protocols is an important and difficult problem.
The study of formal analysis methods for E-commerce protocol security is later than that for traditional cryptographic protocol. There are many active formal analysis methods for E-commerce protocol, such as:Kailar logic, SVO logic, model checking using SMV, game analysis based on ATL/ATS system and methods proposed by Prof. Si-Han Qing, which could be used to analyze or prove the security of two party or multiple party fair exchange protocols. Some of these methods focus on the analysis of the message or focus on the structure of the protocol. Few formal analysis method could consider the message and the structure of a protocol at the same time. At present, formal analysis methods of E-commerce protocol is still a hot research area.
The first part of this paper researchs the major game logic systems, for example:ATL, ATEL, ATL-A/ATEL-A, MMAL, and found that these game logic system model the status of game agent with fixed state machine. Based on this finding, IA(Intelligent Agent) model is proposed, in which the agent update its status based on message he received and the logical inference rules. And in every status, the agent reason about what could he send using the inference rules. Multiple IAs constitute one MCGS(Message based Concurrent Game System). ATL-B, which includes epistemic logic propositions, extended from ATL, is used to model the system strategies. IA, MCGS, ATL-B together constitute a tool of modeling the system, known as the MIAG (Multiple Intelligent Agent Game) system which is characterized by that the game agent interact through message only and each agent has its own logical inference rules for the renewal of its state.
In the second part, Using MIAG, this paper built a new E-commerce protocol analysis model, in which the game agent update its epistemic state using the logical inference rules; ATL-B strategy formula could express different security goals, for different E-commerce protocol. In the new model, participates are divided into honest agent set and dishonest agent set. Then, given every trace of the honest agent in the target protocol, the strategy of dishonest agent are analyzed to check weather it has strategy to get more benefit then the honest agent. In this paper, four typical attack strategies are identified which is more reality then those defined in the other formal analysis methods proposed before.
In third part, one fair exchange protocol, Nenadi04, and one non-central E-voting protocol, Su-Vot are analysised using the new model. Flaws are found in these protocols, which confirmed the validity of the new model. When analyzing Nenadi04, we found that the non-repudiation evidence dose not satisfy accountability and also, the initiator of Nenadi04 could launch a number of recovery sub-protocols to confuse the responder with messages for different instance, thereby break the fairness of Nenadi04. The analysis of Nenadi04 exemplified that the new model could analyze fair exchange protocols from both the message and structure point of view at the same time. The dishonest voter in Su-Vote protocol could modify the voting result and have strategy to control weather the protocol could finish in time.
In the last part of this paper, we propose and define the traceability of concurrent signature to bind the signer and message together to prevent the abuseness. Based on improved Perfect Concurrent Signature proposed by Guilin Wang, this paper designed one concurrent signature scheme, which satisfy the traceability, based on which one fair exchange protocol without trusted third party is proposed.
针对电子商务协议安全性的形式化分析方法的研究晚于对传统的密码协议的形式化分析方法的研究,目前主要的分析方法有：Kailar逻辑,SVO逻辑,基于SMV的模型检测,基于ATL／ATS博弈逻辑系统的分析方法,以及卿斯汉等学者提出的对两方或者多方电子商务协议和公平交换协议进行分析、证明的方法。这些方法分别从协议的消息语义、协议结构角度对协议进行建模与分析。综合考虑协议的消息和结构两个因素的形式化分析方法较少。当前,对电子商务协议的形式化分析方法的研究依然是一个热点领域。
本文首先对主要的博弈逻辑：ATL逻辑、ATEL逻辑、ATL-A／ATEL-A逻辑、多代理逻辑等,进行了研究,发现他们对博弈主体的状态转移的建模方式采用固定的步骤。本文提出了一个智能代理博弈主体模型(IA),在IA中,一个博弈主体的状态由博弈主体根据其接收的消息按照逻辑推理规则进行状态的更新,在每一个状态下,根据推理规则推演出当前可发送消息集合。多个IA构成了一个基于消息的并发博弈系统(MCGS),这个系统中每一步的迁移是通过两个动作完成,分别是：各个IA的收发消息,以及各IA根据自己接收的消息按逻辑推理规则更新自身状态。整个系统的策略使用基于ATL扩展的ATL-B逻辑进行表达。IA,MCGS,ATL-B共同构成了一个对系统进行建模的工具,称为MIAG(多智能体博弈)系统,这个系统的特点是各博弈主体之间只通过消息交互,每个主体有自己的认知推理逻辑规则用以更新状态,与其他博弈逻辑相比,博弈主体具有动态的状态迁移特性。
基于MIAG模型,本文构建了一个电子商务协议分析的新模型,其主要特点是在博弈主体中引入了针对电子商务协议的逻辑推理规则用于更新博弈主体的认知状态；使用ATL-B策略公式表达不同的安全目标,使其能够适应对不同目的的电子商务协议的建模要求。在新模型中,将协议主体分成诚实主体与非诚实主体两个集合,分析过程依次针对诚实主体的各个协议运行迹分析非诚实方是否存在攻击策略。本文总结了四种典型的非诚实方攻击策略,使得本文的分析模型能够比之前的模型更切合实际的形式化非诚实主体的能力。
应用电子商务协议分析的新模型,本文对一个公平交换协议Nenadi04和一个无需中央机构的电子投票协议Su-Vote协议进行了分析,发现了协议中存在的漏洞,说明了新模型的有效性。在对Nenadi04协议的分析中,利用新模型发现了发方不可否认证据不满足可追究性的要求,也发现了协议中发起方可以利用并发多个协议实例来混淆应答方对恢复子协议接收消息的识别,从而破坏协议的公平性。这个协议实例说明了新模型能够同时处理对消息和协议结构的分析。对Su-Vote协议的分析中发现非诚实的投票人能够篡改投票结果并能够控制协议是否终止
本文最后研究了公平交换协议的一种基础签名算法——并发签名,提出并定义了并发签名的可追踪性以保证签名方与签署消息之间的唯一绑定关系,防止签名被滥用。基于学者王贵林提出的一个完美并发签名方案,本文设计了一个满足可追踪性的并发签名方案,并基于此方案设计了一个无需第三方的公平交换协议。
E-commerce protocol is designed to fulfill business flow and prtotect the attender's profit using cryptography technical. So, it is a common sense that the formal analysis of the security of E-commerce protocols is an important and difficult problem.
The study of formal analysis methods for E-commerce protocol security is later than that for traditional cryptographic protocol. There are many active formal analysis methods for E-commerce protocol, such as:Kailar logic, SVO logic, model checking using SMV, game analysis based on ATL/ATS system and methods proposed by Prof. Si-Han Qing, which could be used to analyze or prove the security of two party or multiple party fair exchange protocols. Some of these methods focus on the analysis of the message or focus on the structure of the protocol. Few formal analysis method could consider the message and the structure of a protocol at the same time. At present, formal analysis methods of E-commerce protocol is still a hot research area.
The first part of this paper researchs the major game logic systems, for example:ATL, ATEL, ATL-A/ATEL-A, MMAL, and found that these game logic system model the status of game agent with fixed state machine. Based on this finding, IA(Intelligent Agent) model is proposed, in which the agent update its status based on message he received and the logical inference rules. And in every status, the agent reason about what could he send using the inference rules. Multiple IAs constitute one MCGS(Message based Concurrent Game System). ATL-B, which includes epistemic logic propositions, extended from ATL, is used to model the system strategies. IA, MCGS, ATL-B together constitute a tool of modeling the system, known as the MIAG (Multiple Intelligent Agent Game) system which is characterized by that the game agent interact through message only and each agent has its own logical inference rules for the renewal of its state.
In the second part, Using MIAG, this paper built a new E-commerce protocol analysis model, in which the game agent update its epistemic state using the logical inference rules; ATL-B strategy formula could express different security goals, for different E-commerce protocol. In the new model, participates are divided into honest agent set and dishonest agent set. Then, given every trace of the honest agent in the target protocol, the strategy of dishonest agent are analyzed to check weather it has strategy to get more benefit then the honest agent. In this paper, four typical attack strategies are identified which is more reality then those defined in the other formal analysis methods proposed before.
In third part, one fair exchange protocol, Nenadi04, and one non-central E-voting protocol, Su-Vot are analysised using the new model. Flaws are found in these protocols, which confirmed the validity of the new model. When analyzing Nenadi04, we found that the non-repudiation evidence dose not satisfy accountability and also, the initiator of Nenadi04 could launch a number of recovery sub-protocols to confuse the responder with messages for different instance, thereby break the fairness of Nenadi04. The analysis of Nenadi04 exemplified that the new model could analyze fair exchange protocols from both the message and structure point of view at the same time. The dishonest voter in Su-Vote protocol could modify the voting result and have strategy to control weather the protocol could finish in time.
In the last part of this paper, we propose and define the traceability of concurrent signature to bind the signer and message together to prevent the abuseness. Based on improved Perfect Concurrent Signature proposed by Guilin Wang, this paper designed one concurrent signature scheme, which satisfy the traceability, based on which one fair exchange protocol without trusted third party is proposed.
引文
[1]T.Dierks, E.Rescorla. RFC5246:The Transport Layer Security (TLS) Protocol Version 1.2, www.ietf.org/rfc/rfc5246.txt.
[2]Dolev D,Yao A. On the security of public key protocols[J]. IEEE Transactions on Information Theory.1983, Vol.29(2):198-208.
[3]卿斯汉,安全协议20年研究进展[J].软件学报.2003,Vol.14(10)：1740-1752
[4]Needham R, Schroeder M. Using encryption for authentication in large networks of computers [J]. Communications of the ACM.1978, Vol.21(12): 993-999.
[5]Lowe G. An attack on the Needham-Schroeder public-key authentication protocol [J]. Information Processing Letters; 1995, Vol.56:131-133.
[6]Landweber, L. H., et al. Research Computer Networks and Their Interconnection[J]. IEEE Commun.1986, Vol.24(5):5-17.
[7]谢希仁,陈鸣,张兴元,计算机网络.版次.出版者,1994.
[8]Carl A. Sunshine. Formal methods for communication protocol specification and verification. A Rand Note prepared for the DEFENSE ADVANCED RESEARCH PROJECT AGENCY and the NATIONAL BUREAU OF STANDARDS, Nov.1979
[9]Bruce Schneier著,应用密码学——协议、算法与C源程序.吴世忠,祝世雄,张文政译.机械工业出版社,2000.
[10]Burrows M,Abadi M,Needham R. A logic of authentication[J]. ACM Transactions on Computer Systems.1990, Vol.8(1):18-36.
[11]范红,冯登国,安全协议理论与方法.第一版.科学出版社,2003.
[12]C. Neuman, T. Yu, S. Hartman. RFC4120:The Kerberos Network Authentication Service (V5). http://www.ietf.org/rfc/rfc4120.txt.
[13]C. Kaufman, P. Hoffman, Y. Nir, P. Eronen. IKEv2 draft-ietf-ipsecme-ikev2bis-03:Internet Key Exchange Protocol. http://www.ietf.org/internet-drafts/draft-ietf-ipsecme-ikev2bis-03.txt.
[14]Kremer S and Markowitch O. Optimistic non-repudiable information exchange[C].21st Symp on Infomration Theory in the Benelux. Wassennar. The Netherlands.2000:139-146.
[15]Clark J,Jacob J. A survey of authentication protocol literature:Version 1.0. 1997. http://www-users.cs.york.ac.uk/-jac/Security Protocols Review.
[16]Satyanarayanan M. Integrating security in a large distributed system[R].Technical Report,CMU-CS,CMU,1987:87-179.
[17]Otway D,Rees O. Efficient and timely mutual authentication[J]. Operating Systems Review.1987, Vol.21(1):8-10.
[18]Denning D,Sacco G. Timestamps in key distribution protocols[J]. Communications of the ACM.1981, Vol.24(8):533-536.
[19]Woo T,Lam S.A lesson on authentication protocol design[J]. Operating Systems Review.1994, Vol.28(3):24-37.
[20]Neuman BC,Stubblebine SG. A note on the use of timestamps as nonces[J]. Operating Systems Review.1993, Vol.27(2):10-14.
[21]Kao IL,Chow R.An efficient and secure authentication protocol using uncertified keys[J]. Operating Systems Review.1995, Vol.29(3):14-21.
[22]Diffie W,Hellman ME.New directions in cryptography[J]. IEEE Transactions on Information Theory.1976, IT-22(6):644-654.
[23]SPORE. Security protocols library. http://www.lsv.ens-cachan.fr/spore.
[24]李国民.群密钥协商协议的分析与设计[D].西南交通大学博士论文.2008.
[25]Even,O.Golderieh, and A.Lempel. A Randomized Protocol for Signing Contracts[J]. Communications of the ACM.1985, Vol.28(6):637-647.
[26]T.Okamoto and K.Ohta. How to Simultaneously exehange secrets by general assumption[C]. Poreeedings of the ACM Conference on Computer and Communications Security.1994:184-192.
[27]T.Tedriek. How to exehange half a bit[C]. in:D.Chaum(Ed.), Advances in Cryptology:Proceedings of Cryptot83, Plenum Press, New York and London. 1984,1983:147-151.
[28]Tedrick. Fair exehange of secrets[C]. in:G.R.Blakley, D.C.Chaum(EdS.), Advances in Cryptology:Poreeedings of Crypto84.1985, Vol.196 of Lectuer Notes in Computer Science:434-438. Springe-Verlag.
[29]M.Ben-Or, O.Goldreich, S.Micali and R.Rivest. A fair protocol for signing contracts[J]. IEEE Transaction on Information Theory.1990, IT-36(1):40-46.
[30]M.O.Rabin. Tarnsaction protection by beacons[R]. Aiken Computation Lab. Harverd University Cambridge, MA, Tech Rep:29-81.1981.
[31]HENNING P and FELIX C G. 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,Darmstadt, Germany, March 1999.
[32]Alireza Bahreman and Doug Tygar. Certified electronic mail[C]. In Symposium on Network and Distributed Systems Security. Internet Society, 1994:3-19.
[33]Jianying Zhou and Dieter Gollman. Certified electronic mail[C]. In Computer Security,1996, Vol.1146 LNCS:160-171.
[34]Jianying Zhou and Dieter Gollman. A fair non-repudiation protocol[C]. In IEEE Symposium on Research in Security and Privacy, pages 55-61. IEEE Computer Society, Technical Committee on Security and Privacy, IEEE Computer Secuirty Press, May 1996.
[35]Robert H. Deng, Li Gong, Aurel A. Lazar, and Weiguo Wang. Practical Protocols for certified electronic mail[J]. Jounal of Network and System Management.1996, Vol.4(3):279-297.
[36]Benjiamin Cox, Doug Tygar, and Marvin Sirbu. NetBill Security and Transaction protocol[C]. First UNIX workshop of Electronic Commerce:77-88, 1995.
[37]ASOKAN N, SHOUP V, WAIDNER M. Optimistic fair exchange of digital signatures[J]. IEEE Journal on Selected Areas in Communication.2000, Vol.18(4):593-610
[38]STEVE.K, OLIVIER. M, and ZHOU JY. An intensive survey of fair non-repudiation protocols [J]. Computer Communications. 2002,Vol.25(17):1606-1621.
[39]STEVE K. Formal Analysis of Optimistic Fair Exchange Protocols [D]. Ph.D theme,Bruxelles, Universit'e Libre de Bruxelles Facult'e des Sciences.2004
[40]L. Chen, C. Kudla, and K. G. Paterson. Concurrent signatures[C]. In: Eurocrypt'04.2004, LNCS 3027:287-305. Spriger-Verlag.
[41]W. Susilo, Y. Mu, and F. Zhang. Perfect concurrent signature schemes[C]. In: Information and Communications Security (ICICS'04).2004, LNCS 3269:14-26. Spriger-Verlag.
[42]W. Susilo and Y. Mu. Tripartite concurrent signatures[C], IFIP/SEC'05.2005: 425-441.
[43]Dongyvu Tonien, Willy Susilo and ReihanehSafavi-Naini. Multi-party Concurrent Signatures[C]. ISC006.2006, LNCS 4176:131-145. Springer-Verlag.
[44]Wang Gui-lin, Bao Feng, Zhou Jian-ying.The fairness of perfect concurrent signatures[C]. In:ICICS'06.2006, LNCS 4307:435-451. Springer-Verlag.
[45]S.S.M. Chow and W.Susilo. Generic construction of (identity-based) perfect concurrent signatures [C]. ICICS'05.2005, LNCS 3783:194-206. Springer-Verlag..
[46]张馨文,王尚平,王晓峰.基于身份的多方同时签名[C].中国密码会2007：325～327.西南交通大学出版社.
[47]Dengguo Feng, Weidong Chen. Security Model and Modular Design of Fair Authenticated Key Exchange Protocols [C].3rd SKLOIS Workshop of Security protocols. Beijing, Sep.2007.
[48]陈广辉,卿斯汉,齐志峰,杨义先.新颖的基于并发签名的公平交易协议[J].通信学报.2008,Vol.29(7)：39-43.
[49]秦志光,罗绪成.P2P共享系统中无需专用TTP的公平交换协议[J].电子科技大学学报.2006,Vol.35(4)：698-701.
[50]赵洋,秦志光,蓝天,王佳昊.一种适用于P2P环境的乐观公平交换协议[J].计算机应用.2007,Vol.27(8)：1881—1883.
[51]张青.具特殊协议的数字签名和公平交换协议研究[D].北京邮电大学博士论文.2007.
[52]张福泰.具有分布式半可信第三方的公平交换协议[J].计算机工程.2006,Vo1.32(3)：14-16.
[53]刘景伟.电子商务中的公平交换协议研究[D].西安电子科技大学博士论文.2007.
[54]王彩芬,贾爱库,刘军龙,于成尊.基于签密的多方认证邮件协议[J].电子学报.2005,Vol.33(11)：2070-2073.
[55]Abadi M, Needham R. Prudent engineering practice for cryptographic protocol [R]. Research Report 125. Palo Auto:Digital Equipment Corporation System Research Center,1994.
[56]Anderson R, Needham R. Programming Satan's computer [C]. Computer Science Today -- Recent Trends and Developments.1995, Lecture Notes in Computer Science, Vol.1000. Springer-Verlag.1995:426-440.
[57]Syverson P. Limitations on design principles for public key protocols [C]. IEEE Symposium on Security and Privacy.1996:62-72.
[58]Gritzalis S, Spinellis D. Cryptographic protocols over open distributed systems: a taxonomy of flaws and related protocol analysis tools [C]. In Proc of 16th International Conference on Computer Safety, Reliability and Security: SAFECOMP'97, European Workshop on Industrial Computer Systems:TC-7. Springer Verlag.1997:123-137.
[59]Gritzalis S, Spinellis D, and Georgiadis P. Security protocols over open networks and distributed systems:formal methods for their analysis, design, and verification [J]. Computer Communications.1999, Vol.22(8):695-707.
[60]Abadi M, Tuttle M R. A semantics for a logic of authentication (extended abstract) [C]. In Proceedings of the 10th Annual ACM Symposium On Principles of Distributed Computing, Montreal, Quebec, Canada,1991: 201-216.
[61]Gong Li. A note on redundancy in encrypted messages [J]. Computer Communication Review.1990,Vol.20(5):18-22.
[62]Wenbo Mao, Colin Boyd. Towards the formal analysis of security protocols[C]. Proceedings of the Computer Security Foundations Workshop VI. IEEE Computer Society Press.1993:147-158.
[63]Anderson R, Needham R. Robustness principles for public key protocols [C]. Proceedings of the 15th Annual International Cryptology Conference on Advances in Cryptology.1995:236-247.
[64]Bugliesi M, Focardi R, and Maffei M. Principles for entity authentication [C].Proceedings of 5th International Conference Perspectives of System Informatics (PSI2003).2003:294-307.
[65]莫燕,张玉清,李学干.关于安全协议设计原则的研究[J].计算机工程,2005,31(24)：183-185.
[66]王芷玲,张玉清,杨波.公平交换协议设计原则[J].中国科学院研究生院学报.2006,Vol.23(4)：555-560.
[67]陶宏才.安全协议结构及其范式研究[D].西南交通大学博士学位论文.2007.
[68]M.Bellare and P.Rogaway. Entrity authentication and key distribution[C]. In D.Stinson, Editor, Advances in Cryptology-Proceedings of CRYPTO'93, Vol.773 of LNCS. Springer-Verlag.1994:232-249.
[69]http://www.di.ens.fr/-blanchet/formacrypt/,2008-12-21
[70]周永斌,张震峰,卿斯汉,季庆光.基于RSA签名的优化公平交换协议[J].软件学报.2004,Vol.15(7)：1049-1055.
[71]李平,李锋,卢新国,吴佳英.一种公平交换协议的攻击算法分析[J].计算机工程与应用.2005,33：145-147.
[72]CByod, WMoa. On a limitation of BAN lgoic. In Advnaces of CyrPotlogy-EUROCRYPT93. Vol765 of LNCS. Springer-Verlag. 1993:240-247.
[73]L Gong, R Needham, R Yahalom. Reasoning about belief in cryptographic protocols[C]. In IEEE Symposium on Research in Security and Privacy. IEEE Computer Society Press.1990:234-248.
[74]P.Syverson and P.VAN Orschot. On unifying some cryptographic protocol logics [C]. Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy.1994:14-28.
[75]缪祥华.一种分析和设计安全协议的新逻辑[D].西南交通大学博士学位论文.2006.
[76]E. Saul and A.C.M. Hutchison. An Environment to Facilitate the Teaching of GNY-Based Security Protocol Analysis Techniques[C]. In Proceedings of the Second World Conference in Information Security Education. Perth, Western Australia. Edith Cowen University.2001:285-305.
[77]Ronald L. RivestAdi Shamir, and David A Wagner. Timed-lock puzzles and timed-release Crypto. MIT/LCS/TR-684. MIT Laboratary for Computer Science.1996.
[78]T.Coffey and P.Saidha, Logic for Veirifying Public-key Cryptographic Protocols[J]. IEEE Proc. Computers and Digital Techniques,1997, Vol.144 (1): 28-32.
[79]A.D.Rubin, Nonmonotomic Cryptographic Protocols[R], CITI Technical Report 93-9, Center for Information Technology Integration. Dept of Electronic Engineering and Computer Science Unversity of Michigan, Nov 1993.
[80]E.Clarke, O.Grumbergm, and D.Peled. Mdel Checking. MIT Press,1999.
[81]G.Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR[C]. In Proc. Tools and Algorithms for the Construction and Analysis of System(TACAS), Vol.1055 of LNCS, Springer-Verlag, 1996:147-166.
[82]A.W.Roscoe. Model-checking CSP[C]. In A Classical Mind:Essays in Honorof C.A.R.Hoare. Prentice-Hall.1994:353-378.
[83]A.W.Roscoe. Modelling and verifing key-exchange protocols using CSP and FDR[C]. In 8th IEEE Computer Security Foundations Workshop. IEEE Computer Society,1995:98-107.
[84]Gavin Lowe. Casper:a compiler for the analysis of security protocols[C]. In Simon Forley, Editor,10th Computer Security Foundations Workshop. Rockport, Massachusetts, USA. IEEE Computer Society Press.1997:18-30.
[85]Jonathan K.Millen. CAPSL:Common Authentication Protocol Specification Language. Proceedings of the 1996 workshop on New security paradigms. ACM.1996:132
[86]Steve Brackin, Catherine Meadows, and Jonathan K.Millen. CAPSL interface for the NRL protocol analyzer[C]. In IEEE Symposium on Appliction-Specific Systems and Software Engineering Technology(ASSET 1999),1999:64
[87]Sidhu D. Authentication protocols for computer networks[J]. Computer Networks and ISDN System.1986,11:297-310.
[88]Mitchell J C, Mitchell M, Stern U. Automated analysis of cryptographic protocols using [C]. Proceedings of the 1997 IEEE Symposium on Seuciryt and Privacy. IEEE Computer Society Press.1997:141-151.
[89]Bolognesi T, Brinksma E. Introduction to the ISO specification language LOTOS[J]. Computer Netowrks and ISDN systems.1987,14:25-59
[90]Varadharajan V. Verification of network security protocols[J]. Computer and Security.1989,8:693-708.
[91]Kemerer R A. Analyzing encryption protocols using formal verification techniques [J]. IEEE Journal on Selected Areas of Communications.1989, Vol.7(4):448-457.
[92]Scheid J, Holtsberg S. Ina Jo specitification language reference manual [R]. System Development Group, Unisys Corporation, CA,1988.
[93]Ghezzi C, Kemmerer R. ASTRAL:An assertion language for specifying real-time systems [C]. Proceedings of the Third European Software Engineering Conference.1991:122-146.
[94]J.K.Millen. The Interrogator model. Proceedings of the 1995 IEEE Symposium on Security and Privacy.1995:251-260.
[95]Clarke E.M., Jha S., Marrero W. Verifying security protocos with Brutus[J]. ACM Transactions on Software Engineering and Methodology,.2000, Vol.9(4):443-487.
[96]Meadows C. A model of computation for the NRL protocol analyzer[C]. In: Proceedings of the 1994 Computer Security Foundation Workshop. Franconia, NH, USA.1994:84-89.
[97]Zhang Yuqing, Li Jihong, Xiao Guozhen. An Approach to the Formal Verification of the Two-party Cryptographic Protocols. ACM Operating System Review. ACM.1999.33(4):48-51.
[98]SMV. School of Computer Science of Camegie Mellon University,1998. Available via URL:http://www.cs.cmu.edu/-model-check/
[99]张玉清、朱宏儒、肖国镇.密码协议的SMV分析：实例研究[J].计算机工程.1999, Vol.25.Special Issue:156-158.
[100]吴立军,苏开乐.多智能系统时态认知规范的模型检测算法[J].软件学报.2004,Vol.15(7):1012-1020.
[101]Su kaile, Lu Guanfeng, Chen Qingliang. Knowledge structure approach to verificiation of authentication protocols[J]. Science in China, Ser.E, Information Science.2005, Vol.48(4):513-532.
[102]骆翔宇.多智能体系统的符号模型检测[D].中山大学博士学位论文.2006.
[103]陈清亮.基于本地会话的安全协议验证逻辑及算法[D].中山大学博士学位论文.2007.
[104]http://www.cs.sysu.edu.cn/-skl/spv.htm
[105]袁崇义.Petri网原理.电子工业出版社,1998：10-30
[106]罗军舟,顾冠群,谢俊清.Petri网协议分析器[J].计算机学报.1997,Vo1.20(3)：206-212.
[107]刘培顺.判决PN机理论及其在入侵检测中的应用[D].西南交通大学博士学位论文.2005.
[108]B B Nieh,S E Tavares.Modelling and analyzing cryptographic protocols using Petri nets[C]. Advances in cryptology AUSCRYPT'92.1992,Vol.718 of LNCS:275-295. Springer Verlag.
[109]C M Morton. A Modular Approach to Evaluating Cryptographic Protocols using Petri Nets[D]. Kingston, Ontario, Canada:Queen's University.1993.
[110]张广胜,吴哲辉.基于时间Petri网的密码协议分析[J].系统仿真学报.2003,Vol.15增刊：11-16.
[111]刘道斌,郭莉,白硕.基于Petri网的安全协议形式化分析[J].电子学报.2004,Vol.32(11)：1926-1929.
[112]郑君杰,肖军模,杨明等.基于有色Petri网的安全协议的安全性仿真[J].系统仿真学报.2006,Vol.18(11)：3294-3296.
[113]L.C.Paulson. Proving Properties of Security Protocols by Induction[C]. In Proc of the 10th Computer Security Foundation Workshop(CSFW10). 1997:70-83. IEEE Computer Society Press.
[114]G.Bella and L.C.Paulson. Kerberos version iv:inductive analysis of the secrecy goal[C]. In Jean-Jacques Quisquater et al., editor, Computer Security-ESORICS 98.1998, Vol.1485 of LNCS:361-375. Springer.
[115]G.Bella, F.Massacci, L.C.Paulson and P.Tramontano. Formal verification of cardholder registration in SET[C]. In Ecuppens, editor, Computer Security-ESORICS2000.2000, Vol.1895 of LNCS:159-174. Springer.
[116]F.Javier Thayer Fabrega, Jonathan C.Herzog, Joshua D.Gutman. Stand Space:Why is Security Protocol Correct?[C]. In:Proc 18th IEEE Symposium on Reearch in Security and Privacy. IEEE Computer Society Press. 1998:160-171.
[117]F.Javier Thayer Fabrega, Jonathan C.Herzog, Joshua D.Gutman. Hoest Ideals on Strand Spaces[C]. In:Proc 11th IEEE Computer Security Foundations Workshop(CSFW). IEEE Computer Society Press,1998:66-78.
[118]F. Javier Thayer Fabrega, Jonathan C. Herzog, Joshua D. Guttman. Strand Spaces:Proving Security Protocols Correct[J]. Journal of Computer Security. 1999,7:191-230.
[119]D.X.Song. Athena:a New Efficient Automatic Checker for Security Protocol Analysis[C]. In 12th IEEE Computer Security Foundation Workshop(CSFW12). Mordano, Italy. IEEE Computer Society Press.1999: 192-202.
[120]http://www.di.ens.fr/-blanchet/index-eng.html
[121]李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述.计算机研究与发展.2004,Vol.41(7)：1098-1103.
[122]Martin Abadi, Andrew D. Gordon. A Calculus for Cryptographic Protocols The Spi Calculus[C]. Fourth ACM Conference on Computer and Communications Security.1997:pp36-47.
[123]怀进鹏,李先贤.密码协议的代数模型及其安全性[J].中国科学.E辑.2003,Vol.33(12)：1087-1106.
[124]李建新,李先贤,卓继亮,怀进鹏.SPA：新的高校安全协议分析系统[J].计算机学报.2005,Vol.28(3)：309-318.
[125]李梦君.安全协议形式化验证技术的研究与实现[D].国防科技大学博士学位论文.2005.
[126]李梦君,李舟军,陈火旺.安全协议的扩展Horn逻辑模型及其验证方法[J].计算机学报.2006,Vol.29(9)：1666-1678.
[127]龙士工.串空间理论及其在安全协议分析中的应用研究[D].贵州大学博士学位论文.2007.
[128]Wenbo Mao著.现代密码学理论与实践.王继林,伍前红等译.第二版.电子工业出版社.2004.7
[129]S.Goldwasser, S.Micali. Probabilistic encryption[J]. Journal of Coputer and System Sciences.1984,28:170-199.
[130]冯登国.可证明安全性理论与方法研究[J].软件学报.2005,Vol.16(10)：1743-1756.
[131]http://www.di.ens.fr/-blanchet/formacrypt/description.html#Turuani05
[132]B.Blanchet, A.D.Jaggard, A.Scedrov. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos[C]. ASIACCS'08,2008:18-20. Tokyo.
[133]赵华伟.两种安全协议形式化理论的研究[D].山东大学博士学位论文.2006.
[134]Rajashekar Kailar. Accountability in electronic ecommerceprotocos[J]. IEEE Transactions on Software Engineering.1996, Vol.22(5):313-328.
[135]周典萃,卿斯汉,周展飞.Kailar逻辑的缺陷[J].软件学报.1999,Vol.10(12)：1238-1245.
[136]周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具[J].软件学报.2001,Vol.12(9：1318-1328.
[137]周勇.一种验证非否认协议的新方法[J].电子与信息学报.2007,Vol.29(10)：2493-2497
[138]缪祥华,何大可.Kailar逻辑的串空间语义[J].计算机科学.2006,Vol.33(3)：87-88.
[139]Jianying Zhou, Dieter Gollman. Towards Verification of Non-repudiation protocols[C]. In Proceedings of 1998 International Refinement Workshop and Formal Methods Pacific.1998:370-380.
[140]黎波涛,罗军舟.不可否认协议时限性的形式化分析[J].软件学报.2006,Vol.17(7)：1510-1516.
[141]Steve A. Schneider. Formal Analysis of a non-repudiation protocol[C]. In 11th IEEE Computer Security Foundations Workshop.1998. Washington-Brussels-Tokyo,1998:54-65.
[142]Giampaolo Bella, Lawrence C.Paulson. Mechanical proofs about a non-repudiation protocol[J]. In Richard J.Boulton and Paul B. Jackson, editors, Theorem Proving in Higher Order Logics,2001, Vol.2152 LNCS:91-104. Springer-Verlag.
[143]Vitaly Shmatikov, John Mitchell. Finite-State Analysis of two contract Signing Protocols[J]. Theoretical Computer Science, Special issues on Theoretical Foundations of Security Analysiss and Desgin.2002, Vol.283(2):419-450.
[144]Paul hankes Drielsma, Sebastian ModerSheim. The ASW Protocol Revisited:A Unified View[J]. Electr. Notes Theor.Comput. Sci.2005, Vol.125(1):145-161.
[145]文静华,李祥,张焕国,等.基于ATL的电子商务协议形式化分析[J].电子与信息学报.2007,Vol.29(4)：901-905.
[146]文静华,张梅,李祥.基于博弈的电子商务协议分析[J],通信学报.2006,Vol.27(3)：73-78.
[147]卿斯汉.电子商务协议中的可信第三方角色[J].软件学报.2003,Vol.14(11)：1936-1943.
[148]卿斯汉,李改成.公平交换协议的一个形式化模型[J].中国科学E辑信息科学.2005,Vol.35(2)：161-172.
[149]卿斯汉,李改成.多方公平交换协议的形式化分析和设计[J].中国科学E辑信息科学.2006,Vol.36(6)：598-616.
[150]卿斯汉.一种电子商务协议形式化分析方法[J],软件学报.2005,Vol.16(10)：1757-1765.
[151]邢育红.公平交换协议分析方法研究[D].山东大学博士学位论文.2005.
[152]沈海峰,薛锐,黄河燕.用串空间分析公平交换协议[J].小型微型计算机系统.2006,Vol.27(1)：62-68.
[153]顾永跟,李国强,王国钧.基于类pi演算的电子支付协议安全性形式化研究[J].计算机应用研究.2006,3：22-24.
[154]Rajeev Alur, Thomas A. Henzinger, Orna Kupferman. Alternating-time Temporal Logic[C]. Proceedings of the 38th Annual Symposium on Foundations of Computer Science(FOCS) IEEE Computer Society Press, 1997:100-109.
[155]Rajeev Alur, Thomas A. Henzinger, Orna Kupferman. Alternating-time Temporal Logic[J]. Journal of the ACM.2002,49:672-713.
[156]Xianwei Lai, Shanli Hu, Zhengyuan Ning. An Improved Formal Framework of Actions, Individual Intention and Group Intenstion for Multi-agent systems. Proceedings of the IEEE/WIC/ACM International conference on Intelligent Agent Technology(IAT06). IEEE Computer Society Washington, DC, USA.2006:420-423.
[157]宁正元,胡山立,赖贤伟.交互时态信念逻辑及其模型检测[J].南京大学学报(自然科学).2008,Vol.44(2)：171-178.
[158]Moore, R.C. A formal Theory of Knowledge and Action[R], Technical note No.320. SRI INTERNATIONAL MENLO PARK CA ARTIFICIAL INTELLIGENCE CENTER.1984.
[159]Wiebe Van Der Hoek, Michael Wooldridge, Cooperation. Knowledge and Time:Alternating-time Temporal Epistemic Logic and its Applications. Studia Logics.2003,75:125-157.
[160]Vlentin Goranko, Wojciech Jamroga and Gover van Drimmelen. Axiomatic systems for Alternating-Time Temporal Epistemic Logics[C]. Proceedings of the 6th Conference on Logic and the Foundations of Game andDecision Theory(LOFT'04).2004:1-4.
[161]Thomas Agotnes. Action and knowledge in alternating-time temporal logic[J]. Synthese.2006, Vol.149(2):377-409.
[162]Luigi Sauro, Jelle Gerbrandy, Weibe van der Hoek. Reasoning about action and cooperation[C]. AAMAS'06. ACM Press.2006:185-192.
[163]R.C.Moore. Reasoning about knowledge and action[C]. In Proceedings of the Fifth International Joint Conference on Artificial Intelligence(IJCAI-77). Cambridge, MA,1977:223-227.
[164]M.Pauly. A Modal Logic for Coalitional Power in Games[J]. Journal of Logic and Computation.2002,12:146-166.
[165]W.van der Hoek and M.Wooldridge. On the logic of cooperation and propositional controo[J]. Artificial Intelligence.2005, Vol.64(1-2):81-119.
[166]卓继亮,李先贤,李建欣,怀进鹏.安全协议的攻击分类及其安全性评估[J].计算机研究与发展.2005,Vol.42(7)：1100-1107
[167]Syverson P. A taxonomy of replay attacks[C], Proceedings of the 1994 IEEE Computer Security Foundations Workshop VII. Los Alamitos:IEEE Computer Society Press,1994:187-191.
[168]A. Nenadi'c, N. Zhang, S. Barton. A security protocol for certified e-goods delivery[C]. Proc. IEEE Int. Conf. Information Technology, Coding, and Computing (ITCC'04):22-28.2004. Las Vegas, NV, USA. IEEE Computer Society.
[169]Almudena Alcaide, Juan M.Estevez-Tapiador, Antonio Izquierdo, and Jose M. Sierra. A formal analysis of fairness and Non-repudiation in the RSA-CEGD Protoco[C]. O.Gervasi et. al. (Eds):ICCSA2005; LNCS 3483:1309-1318,2005, Springer-Verlag.
[170]Chaum DL. Untraceable electronic mail, return addresses, and digital pseudonyms[J]. Communications of the ACM.1981, Vol.24(2):84-90.
[171]Atsushi Fujioka, Tatsuaki Okamoto, and Kazui Ohta. A practical secret voting scheme for large scale elections[C]. In J. Seberry and Y. Zheng, editors, Advances in Cryptology— AUSCRYPT'92.1992, Vol.718 of LNCS: 244-251, Springer.
[172]仲红,黄刘生,罗永龙.安全电子选举研究[J].安徽大学学报(自然科学版).2007,Vol.31(3)：20-25
[173]陈晓峰,王继林,王育民.基于办信任模型的无收据的电子投票[J].计算机学报.2003,Vol.26(5)：557-562.
[174]苏云学,逯海军,祝跃飞.一个无需中央机构的电子投票协议[J].计算机工程.2004,Vol.30(11)：96-97.
[175]Alexander Prosser, Robert Krimmer, The Dimensions of Electronic Voting Technology[C]. Law, Politics and Society, Workshop of the ESF TED Programme together with GI and OCG.2004,21-28. in Schloβ Hofen/Bregenz, Lake of Constance, Austria.
[176]王思佳,韩玮,陈克非,电子选举研究的挑战与进展[J],计算机工程,Vol.32(15)：7-9,2006.
[2]Dolev D,Yao A. On the security of public key protocols[J]. IEEE Transactions on Information Theory.1983, Vol.29(2):198-208.
[3]卿斯汉,安全协议20年研究进展[J].软件学报.2003,Vol.14(10)：1740-1752
[4]Needham R, Schroeder M. Using encryption for authentication in large networks of computers [J]. Communications of the ACM.1978, Vol.21(12): 993-999.
[5]Lowe G. An attack on the Needham-Schroeder public-key authentication protocol [J]. Information Processing Letters; 1995, Vol.56:131-133.
[6]Landweber, L. H., et al. Research Computer Networks and Their Interconnection[J]. IEEE Commun.1986, Vol.24(5):5-17.
[7]谢希仁,陈鸣,张兴元,计算机网络.版次.出版者,1994.
[8]Carl A. Sunshine. Formal methods for communication protocol specification and verification. A Rand Note prepared for the DEFENSE ADVANCED RESEARCH PROJECT AGENCY and the NATIONAL BUREAU OF STANDARDS, Nov.1979
[9]Bruce Schneier著,应用密码学——协议、算法与C源程序.吴世忠,祝世雄,张文政译.机械工业出版社,2000.
[10]Burrows M,Abadi M,Needham R. A logic of authentication[J]. ACM Transactions on Computer Systems.1990, Vol.8(1):18-36.
[11]范红,冯登国,安全协议理论与方法.第一版.科学出版社,2003.
[12]C. Neuman, T. Yu, S. Hartman. RFC4120:The Kerberos Network Authentication Service (V5). http://www.ietf.org/rfc/rfc4120.txt.
[13]C. Kaufman, P. Hoffman, Y. Nir, P. Eronen. IKEv2 draft-ietf-ipsecme-ikev2bis-03:Internet Key Exchange Protocol. http://www.ietf.org/internet-drafts/draft-ietf-ipsecme-ikev2bis-03.txt.
[14]Kremer S and Markowitch O. Optimistic non-repudiable information exchange[C].21st Symp on Infomration Theory in the Benelux. Wassennar. The Netherlands.2000:139-146.
[15]Clark J,Jacob J. A survey of authentication protocol literature:Version 1.0. 1997. http://www-users.cs.york.ac.uk/-jac/Security Protocols Review.
[16]Satyanarayanan M. Integrating security in a large distributed system[R].Technical Report,CMU-CS,CMU,1987:87-179.
[17]Otway D,Rees O. Efficient and timely mutual authentication[J]. Operating Systems Review.1987, Vol.21(1):8-10.
[18]Denning D,Sacco G. Timestamps in key distribution protocols[J]. Communications of the ACM.1981, Vol.24(8):533-536.
[19]Woo T,Lam S.A lesson on authentication protocol design[J]. Operating Systems Review.1994, Vol.28(3):24-37.
[20]Neuman BC,Stubblebine SG. A note on the use of timestamps as nonces[J]. Operating Systems Review.1993, Vol.27(2):10-14.
[21]Kao IL,Chow R.An efficient and secure authentication protocol using uncertified keys[J]. Operating Systems Review.1995, Vol.29(3):14-21.
[22]Diffie W,Hellman ME.New directions in cryptography[J]. IEEE Transactions on Information Theory.1976, IT-22(6):644-654.
[23]SPORE. Security protocols library. http://www.lsv.ens-cachan.fr/spore.
[24]李国民.群密钥协商协议的分析与设计[D].西南交通大学博士论文.2008.
[25]Even,O.Golderieh, and A.Lempel. A Randomized Protocol for Signing Contracts[J]. Communications of the ACM.1985, Vol.28(6):637-647.
[26]T.Okamoto and K.Ohta. How to Simultaneously exehange secrets by general assumption[C]. Poreeedings of the ACM Conference on Computer and Communications Security.1994:184-192.
[27]T.Tedriek. How to exehange half a bit[C]. in:D.Chaum(Ed.), Advances in Cryptology:Proceedings of Cryptot83, Plenum Press, New York and London. 1984,1983:147-151.
[28]Tedrick. Fair exehange of secrets[C]. in:G.R.Blakley, D.C.Chaum(EdS.), Advances in Cryptology:Poreeedings of Crypto84.1985, Vol.196 of Lectuer Notes in Computer Science:434-438. Springe-Verlag.
[29]M.Ben-Or, O.Goldreich, S.Micali and R.Rivest. A fair protocol for signing contracts[J]. IEEE Transaction on Information Theory.1990, IT-36(1):40-46.
[30]M.O.Rabin. Tarnsaction protection by beacons[R]. Aiken Computation Lab. Harverd University Cambridge, MA, Tech Rep:29-81.1981.
[31]HENNING P and FELIX C G. 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,Darmstadt, Germany, March 1999.
[32]Alireza Bahreman and Doug Tygar. Certified electronic mail[C]. In Symposium on Network and Distributed Systems Security. Internet Society, 1994:3-19.
[33]Jianying Zhou and Dieter Gollman. Certified electronic mail[C]. In Computer Security,1996, Vol.1146 LNCS:160-171.
[34]Jianying Zhou and Dieter Gollman. A fair non-repudiation protocol[C]. In IEEE Symposium on Research in Security and Privacy, pages 55-61. IEEE Computer Society, Technical Committee on Security and Privacy, IEEE Computer Secuirty Press, May 1996.
[35]Robert H. Deng, Li Gong, Aurel A. Lazar, and Weiguo Wang. Practical Protocols for certified electronic mail[J]. Jounal of Network and System Management.1996, Vol.4(3):279-297.
[36]Benjiamin Cox, Doug Tygar, and Marvin Sirbu. NetBill Security and Transaction protocol[C]. First UNIX workshop of Electronic Commerce:77-88, 1995.
[37]ASOKAN N, SHOUP V, WAIDNER M. Optimistic fair exchange of digital signatures[J]. IEEE Journal on Selected Areas in Communication.2000, Vol.18(4):593-610
[38]STEVE.K, OLIVIER. M, and ZHOU JY. An intensive survey of fair non-repudiation protocols [J]. Computer Communications. 2002,Vol.25(17):1606-1621.
[39]STEVE K. Formal Analysis of Optimistic Fair Exchange Protocols [D]. Ph.D theme,Bruxelles, Universit'e Libre de Bruxelles Facult'e des Sciences.2004
[40]L. Chen, C. Kudla, and K. G. Paterson. Concurrent signatures[C]. In: Eurocrypt'04.2004, LNCS 3027:287-305. Spriger-Verlag.
[41]W. Susilo, Y. Mu, and F. Zhang. Perfect concurrent signature schemes[C]. In: Information and Communications Security (ICICS'04).2004, LNCS 3269:14-26. Spriger-Verlag.
[42]W. Susilo and Y. Mu. Tripartite concurrent signatures[C], IFIP/SEC'05.2005: 425-441.
[43]Dongyvu Tonien, Willy Susilo and ReihanehSafavi-Naini. Multi-party Concurrent Signatures[C]. ISC006.2006, LNCS 4176:131-145. Springer-Verlag.
[44]Wang Gui-lin, Bao Feng, Zhou Jian-ying.The fairness of perfect concurrent signatures[C]. In:ICICS'06.2006, LNCS 4307:435-451. Springer-Verlag.
[45]S.S.M. Chow and W.Susilo. Generic construction of (identity-based) perfect concurrent signatures [C]. ICICS'05.2005, LNCS 3783:194-206. Springer-Verlag..
[46]张馨文,王尚平,王晓峰.基于身份的多方同时签名[C].中国密码会2007：325～327.西南交通大学出版社.
[47]Dengguo Feng, Weidong Chen. Security Model and Modular Design of Fair Authenticated Key Exchange Protocols [C].3rd SKLOIS Workshop of Security protocols. Beijing, Sep.2007.
[48]陈广辉,卿斯汉,齐志峰,杨义先.新颖的基于并发签名的公平交易协议[J].通信学报.2008,Vol.29(7)：39-43.
[49]秦志光,罗绪成.P2P共享系统中无需专用TTP的公平交换协议[J].电子科技大学学报.2006,Vol.35(4)：698-701.
[50]赵洋,秦志光,蓝天,王佳昊.一种适用于P2P环境的乐观公平交换协议[J].计算机应用.2007,Vol.27(8)：1881—1883.
[51]张青.具特殊协议的数字签名和公平交换协议研究[D].北京邮电大学博士论文.2007.
[52]张福泰.具有分布式半可信第三方的公平交换协议[J].计算机工程.2006,Vo1.32(3)：14-16.
[53]刘景伟.电子商务中的公平交换协议研究[D].西安电子科技大学博士论文.2007.
[54]王彩芬,贾爱库,刘军龙,于成尊.基于签密的多方认证邮件协议[J].电子学报.2005,Vol.33(11)：2070-2073.
[55]Abadi M, Needham R. Prudent engineering practice for cryptographic protocol [R]. Research Report 125. Palo Auto:Digital Equipment Corporation System Research Center,1994.
[56]Anderson R, Needham R. Programming Satan's computer [C]. Computer Science Today -- Recent Trends and Developments.1995, Lecture Notes in Computer Science, Vol.1000. Springer-Verlag.1995:426-440.
[57]Syverson P. Limitations on design principles for public key protocols [C]. IEEE Symposium on Security and Privacy.1996:62-72.
[58]Gritzalis S, Spinellis D. Cryptographic protocols over open distributed systems: a taxonomy of flaws and related protocol analysis tools [C]. In Proc of 16th International Conference on Computer Safety, Reliability and Security: SAFECOMP'97, European Workshop on Industrial Computer Systems:TC-7. Springer Verlag.1997:123-137.
[59]Gritzalis S, Spinellis D, and Georgiadis P. Security protocols over open networks and distributed systems:formal methods for their analysis, design, and verification [J]. Computer Communications.1999, Vol.22(8):695-707.
[60]Abadi M, Tuttle M R. A semantics for a logic of authentication (extended abstract) [C]. In Proceedings of the 10th Annual ACM Symposium On Principles of Distributed Computing, Montreal, Quebec, Canada,1991: 201-216.
[61]Gong Li. A note on redundancy in encrypted messages [J]. Computer Communication Review.1990,Vol.20(5):18-22.
[62]Wenbo Mao, Colin Boyd. Towards the formal analysis of security protocols[C]. Proceedings of the Computer Security Foundations Workshop VI. IEEE Computer Society Press.1993:147-158.
[63]Anderson R, Needham R. Robustness principles for public key protocols [C]. Proceedings of the 15th Annual International Cryptology Conference on Advances in Cryptology.1995:236-247.
[64]Bugliesi M, Focardi R, and Maffei M. Principles for entity authentication [C].Proceedings of 5th International Conference Perspectives of System Informatics (PSI2003).2003:294-307.
[65]莫燕,张玉清,李学干.关于安全协议设计原则的研究[J].计算机工程,2005,31(24)：183-185.
[66]王芷玲,张玉清,杨波.公平交换协议设计原则[J].中国科学院研究生院学报.2006,Vol.23(4)：555-560.
[67]陶宏才.安全协议结构及其范式研究[D].西南交通大学博士学位论文.2007.
[68]M.Bellare and P.Rogaway. Entrity authentication and key distribution[C]. In D.Stinson, Editor, Advances in Cryptology-Proceedings of CRYPTO'93, Vol.773 of LNCS. Springer-Verlag.1994:232-249.
[69]http://www.di.ens.fr/-blanchet/formacrypt/,2008-12-21
[70]周永斌,张震峰,卿斯汉,季庆光.基于RSA签名的优化公平交换协议[J].软件学报.2004,Vol.15(7)：1049-1055.
[71]李平,李锋,卢新国,吴佳英.一种公平交换协议的攻击算法分析[J].计算机工程与应用.2005,33：145-147.
[72]CByod, WMoa. On a limitation of BAN lgoic. In Advnaces of CyrPotlogy-EUROCRYPT93. Vol765 of LNCS. Springer-Verlag. 1993:240-247.
[73]L Gong, R Needham, R Yahalom. Reasoning about belief in cryptographic protocols[C]. In IEEE Symposium on Research in Security and Privacy. IEEE Computer Society Press.1990:234-248.
[74]P.Syverson and P.VAN Orschot. On unifying some cryptographic protocol logics [C]. Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy.1994:14-28.
[75]缪祥华.一种分析和设计安全协议的新逻辑[D].西南交通大学博士学位论文.2006.
[76]E. Saul and A.C.M. Hutchison. An Environment to Facilitate the Teaching of GNY-Based Security Protocol Analysis Techniques[C]. In Proceedings of the Second World Conference in Information Security Education. Perth, Western Australia. Edith Cowen University.2001:285-305.
[77]Ronald L. RivestAdi Shamir, and David A Wagner. Timed-lock puzzles and timed-release Crypto. MIT/LCS/TR-684. MIT Laboratary for Computer Science.1996.
[78]T.Coffey and P.Saidha, Logic for Veirifying Public-key Cryptographic Protocols[J]. IEEE Proc. Computers and Digital Techniques,1997, Vol.144 (1): 28-32.
[79]A.D.Rubin, Nonmonotomic Cryptographic Protocols[R], CITI Technical Report 93-9, Center for Information Technology Integration. Dept of Electronic Engineering and Computer Science Unversity of Michigan, Nov 1993.
[80]E.Clarke, O.Grumbergm, and D.Peled. Mdel Checking. MIT Press,1999.
[81]G.Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR[C]. In Proc. Tools and Algorithms for the Construction and Analysis of System(TACAS), Vol.1055 of LNCS, Springer-Verlag, 1996:147-166.
[82]A.W.Roscoe. Model-checking CSP[C]. In A Classical Mind:Essays in Honorof C.A.R.Hoare. Prentice-Hall.1994:353-378.
[83]A.W.Roscoe. Modelling and verifing key-exchange protocols using CSP and FDR[C]. In 8th IEEE Computer Security Foundations Workshop. IEEE Computer Society,1995:98-107.
[84]Gavin Lowe. Casper:a compiler for the analysis of security protocols[C]. In Simon Forley, Editor,10th Computer Security Foundations Workshop. Rockport, Massachusetts, USA. IEEE Computer Society Press.1997:18-30.
[85]Jonathan K.Millen. CAPSL:Common Authentication Protocol Specification Language. Proceedings of the 1996 workshop on New security paradigms. ACM.1996:132
[86]Steve Brackin, Catherine Meadows, and Jonathan K.Millen. CAPSL interface for the NRL protocol analyzer[C]. In IEEE Symposium on Appliction-Specific Systems and Software Engineering Technology(ASSET 1999),1999:64
[87]Sidhu D. Authentication protocols for computer networks[J]. Computer Networks and ISDN System.1986,11:297-310.
[88]Mitchell J C, Mitchell M, Stern U. Automated analysis of cryptographic protocols using [C]. Proceedings of the 1997 IEEE Symposium on Seuciryt and Privacy. IEEE Computer Society Press.1997:141-151.
[89]Bolognesi T, Brinksma E. Introduction to the ISO specification language LOTOS[J]. Computer Netowrks and ISDN systems.1987,14:25-59
[90]Varadharajan V. Verification of network security protocols[J]. Computer and Security.1989,8:693-708.
[91]Kemerer R A. Analyzing encryption protocols using formal verification techniques [J]. IEEE Journal on Selected Areas of Communications.1989, Vol.7(4):448-457.
[92]Scheid J, Holtsberg S. Ina Jo specitification language reference manual [R]. System Development Group, Unisys Corporation, CA,1988.
[93]Ghezzi C, Kemmerer R. ASTRAL:An assertion language for specifying real-time systems [C]. Proceedings of the Third European Software Engineering Conference.1991:122-146.
[94]J.K.Millen. The Interrogator model. Proceedings of the 1995 IEEE Symposium on Security and Privacy.1995:251-260.
[95]Clarke E.M., Jha S., Marrero W. Verifying security protocos with Brutus[J]. ACM Transactions on Software Engineering and Methodology,.2000, Vol.9(4):443-487.
[96]Meadows C. A model of computation for the NRL protocol analyzer[C]. In: Proceedings of the 1994 Computer Security Foundation Workshop. Franconia, NH, USA.1994:84-89.
[97]Zhang Yuqing, Li Jihong, Xiao Guozhen. An Approach to the Formal Verification of the Two-party Cryptographic Protocols. ACM Operating System Review. ACM.1999.33(4):48-51.
[98]SMV. School of Computer Science of Camegie Mellon University,1998. Available via URL:http://www.cs.cmu.edu/-model-check/
[99]张玉清、朱宏儒、肖国镇.密码协议的SMV分析：实例研究[J].计算机工程.1999, Vol.25.Special Issue:156-158.
[100]吴立军,苏开乐.多智能系统时态认知规范的模型检测算法[J].软件学报.2004,Vol.15(7):1012-1020.
[101]Su kaile, Lu Guanfeng, Chen Qingliang. Knowledge structure approach to verificiation of authentication protocols[J]. Science in China, Ser.E, Information Science.2005, Vol.48(4):513-532.
[102]骆翔宇.多智能体系统的符号模型检测[D].中山大学博士学位论文.2006.
[103]陈清亮.基于本地会话的安全协议验证逻辑及算法[D].中山大学博士学位论文.2007.
[104]http://www.cs.sysu.edu.cn/-skl/spv.htm
[105]袁崇义.Petri网原理.电子工业出版社,1998：10-30
[106]罗军舟,顾冠群,谢俊清.Petri网协议分析器[J].计算机学报.1997,Vo1.20(3)：206-212.
[107]刘培顺.判决PN机理论及其在入侵检测中的应用[D].西南交通大学博士学位论文.2005.
[108]B B Nieh,S E Tavares.Modelling and analyzing cryptographic protocols using Petri nets[C]. Advances in cryptology AUSCRYPT'92.1992,Vol.718 of LNCS:275-295. Springer Verlag.
[109]C M Morton. A Modular Approach to Evaluating Cryptographic Protocols using Petri Nets[D]. Kingston, Ontario, Canada:Queen's University.1993.
[110]张广胜,吴哲辉.基于时间Petri网的密码协议分析[J].系统仿真学报.2003,Vol.15增刊：11-16.
[111]刘道斌,郭莉,白硕.基于Petri网的安全协议形式化分析[J].电子学报.2004,Vol.32(11)：1926-1929.
[112]郑君杰,肖军模,杨明等.基于有色Petri网的安全协议的安全性仿真[J].系统仿真学报.2006,Vol.18(11)：3294-3296.
[113]L.C.Paulson. Proving Properties of Security Protocols by Induction[C]. In Proc of the 10th Computer Security Foundation Workshop(CSFW10). 1997:70-83. IEEE Computer Society Press.
[114]G.Bella and L.C.Paulson. Kerberos version iv:inductive analysis of the secrecy goal[C]. In Jean-Jacques Quisquater et al., editor, Computer Security-ESORICS 98.1998, Vol.1485 of LNCS:361-375. Springer.
[115]G.Bella, F.Massacci, L.C.Paulson and P.Tramontano. Formal verification of cardholder registration in SET[C]. In Ecuppens, editor, Computer Security-ESORICS2000.2000, Vol.1895 of LNCS:159-174. Springer.
[116]F.Javier Thayer Fabrega, Jonathan C.Herzog, Joshua D.Gutman. Stand Space:Why is Security Protocol Correct?[C]. In:Proc 18th IEEE Symposium on Reearch in Security and Privacy. IEEE Computer Society Press. 1998:160-171.
[117]F.Javier Thayer Fabrega, Jonathan C.Herzog, Joshua D.Gutman. Hoest Ideals on Strand Spaces[C]. In:Proc 11th IEEE Computer Security Foundations Workshop(CSFW). IEEE Computer Society Press,1998:66-78.
[118]F. Javier Thayer Fabrega, Jonathan C. Herzog, Joshua D. Guttman. Strand Spaces:Proving Security Protocols Correct[J]. Journal of Computer Security. 1999,7:191-230.
[119]D.X.Song. Athena:a New Efficient Automatic Checker for Security Protocol Analysis[C]. In 12th IEEE Computer Security Foundation Workshop(CSFW12). Mordano, Italy. IEEE Computer Society Press.1999: 192-202.
[120]http://www.di.ens.fr/-blanchet/index-eng.html
[121]李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述.计算机研究与发展.2004,Vol.41(7)：1098-1103.
[122]Martin Abadi, Andrew D. Gordon. A Calculus for Cryptographic Protocols The Spi Calculus[C]. Fourth ACM Conference on Computer and Communications Security.1997:pp36-47.
[123]怀进鹏,李先贤.密码协议的代数模型及其安全性[J].中国科学.E辑.2003,Vol.33(12)：1087-1106.
[124]李建新,李先贤,卓继亮,怀进鹏.SPA：新的高校安全协议分析系统[J].计算机学报.2005,Vol.28(3)：309-318.
[125]李梦君.安全协议形式化验证技术的研究与实现[D].国防科技大学博士学位论文.2005.
[126]李梦君,李舟军,陈火旺.安全协议的扩展Horn逻辑模型及其验证方法[J].计算机学报.2006,Vol.29(9)：1666-1678.
[127]龙士工.串空间理论及其在安全协议分析中的应用研究[D].贵州大学博士学位论文.2007.
[128]Wenbo Mao著.现代密码学理论与实践.王继林,伍前红等译.第二版.电子工业出版社.2004.7
[129]S.Goldwasser, S.Micali. Probabilistic encryption[J]. Journal of Coputer and System Sciences.1984,28:170-199.
[130]冯登国.可证明安全性理论与方法研究[J].软件学报.2005,Vol.16(10)：1743-1756.
[131]http://www.di.ens.fr/-blanchet/formacrypt/description.html#Turuani05
[132]B.Blanchet, A.D.Jaggard, A.Scedrov. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos[C]. ASIACCS'08,2008:18-20. Tokyo.
[133]赵华伟.两种安全协议形式化理论的研究[D].山东大学博士学位论文.2006.
[134]Rajashekar Kailar. Accountability in electronic ecommerceprotocos[J]. IEEE Transactions on Software Engineering.1996, Vol.22(5):313-328.
[135]周典萃,卿斯汉,周展飞.Kailar逻辑的缺陷[J].软件学报.1999,Vol.10(12)：1238-1245.
[136]周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具[J].软件学报.2001,Vol.12(9：1318-1328.
[137]周勇.一种验证非否认协议的新方法[J].电子与信息学报.2007,Vol.29(10)：2493-2497
[138]缪祥华,何大可.Kailar逻辑的串空间语义[J].计算机科学.2006,Vol.33(3)：87-88.
[139]Jianying Zhou, Dieter Gollman. Towards Verification of Non-repudiation protocols[C]. In Proceedings of 1998 International Refinement Workshop and Formal Methods Pacific.1998:370-380.
[140]黎波涛,罗军舟.不可否认协议时限性的形式化分析[J].软件学报.2006,Vol.17(7)：1510-1516.
[141]Steve A. Schneider. Formal Analysis of a non-repudiation protocol[C]. In 11th IEEE Computer Security Foundations Workshop.1998. Washington-Brussels-Tokyo,1998:54-65.
[142]Giampaolo Bella, Lawrence C.Paulson. Mechanical proofs about a non-repudiation protocol[J]. In Richard J.Boulton and Paul B. Jackson, editors, Theorem Proving in Higher Order Logics,2001, Vol.2152 LNCS:91-104. Springer-Verlag.
[143]Vitaly Shmatikov, John Mitchell. Finite-State Analysis of two contract Signing Protocols[J]. Theoretical Computer Science, Special issues on Theoretical Foundations of Security Analysiss and Desgin.2002, Vol.283(2):419-450.
[144]Paul hankes Drielsma, Sebastian ModerSheim. The ASW Protocol Revisited:A Unified View[J]. Electr. Notes Theor.Comput. Sci.2005, Vol.125(1):145-161.
[145]文静华,李祥,张焕国,等.基于ATL的电子商务协议形式化分析[J].电子与信息学报.2007,Vol.29(4)：901-905.
[146]文静华,张梅,李祥.基于博弈的电子商务协议分析[J],通信学报.2006,Vol.27(3)：73-78.
[147]卿斯汉.电子商务协议中的可信第三方角色[J].软件学报.2003,Vol.14(11)：1936-1943.
[148]卿斯汉,李改成.公平交换协议的一个形式化模型[J].中国科学E辑信息科学.2005,Vol.35(2)：161-172.
[149]卿斯汉,李改成.多方公平交换协议的形式化分析和设计[J].中国科学E辑信息科学.2006,Vol.36(6)：598-616.
[150]卿斯汉.一种电子商务协议形式化分析方法[J],软件学报.2005,Vol.16(10)：1757-1765.
[151]邢育红.公平交换协议分析方法研究[D].山东大学博士学位论文.2005.
[152]沈海峰,薛锐,黄河燕.用串空间分析公平交换协议[J].小型微型计算机系统.2006,Vol.27(1)：62-68.
[153]顾永跟,李国强,王国钧.基于类pi演算的电子支付协议安全性形式化研究[J].计算机应用研究.2006,3：22-24.
[154]Rajeev Alur, Thomas A. Henzinger, Orna Kupferman. Alternating-time Temporal Logic[C]. Proceedings of the 38th Annual Symposium on Foundations of Computer Science(FOCS) IEEE Computer Society Press, 1997:100-109.
[155]Rajeev Alur, Thomas A. Henzinger, Orna Kupferman. Alternating-time Temporal Logic[J]. Journal of the ACM.2002,49:672-713.
[156]Xianwei Lai, Shanli Hu, Zhengyuan Ning. An Improved Formal Framework of Actions, Individual Intention and Group Intenstion for Multi-agent systems. Proceedings of the IEEE/WIC/ACM International conference on Intelligent Agent Technology(IAT06). IEEE Computer Society Washington, DC, USA.2006:420-423.
[157]宁正元,胡山立,赖贤伟.交互时态信念逻辑及其模型检测[J].南京大学学报(自然科学).2008,Vol.44(2)：171-178.
[158]Moore, R.C. A formal Theory of Knowledge and Action[R], Technical note No.320. SRI INTERNATIONAL MENLO PARK CA ARTIFICIAL INTELLIGENCE CENTER.1984.
[159]Wiebe Van Der Hoek, Michael Wooldridge, Cooperation. Knowledge and Time:Alternating-time Temporal Epistemic Logic and its Applications. Studia Logics.2003,75:125-157.
[160]Vlentin Goranko, Wojciech Jamroga and Gover van Drimmelen. Axiomatic systems for Alternating-Time Temporal Epistemic Logics[C]. Proceedings of the 6th Conference on Logic and the Foundations of Game andDecision Theory(LOFT'04).2004:1-4.
[161]Thomas Agotnes. Action and knowledge in alternating-time temporal logic[J]. Synthese.2006, Vol.149(2):377-409.
[162]Luigi Sauro, Jelle Gerbrandy, Weibe van der Hoek. Reasoning about action and cooperation[C]. AAMAS'06. ACM Press.2006:185-192.
[163]R.C.Moore. Reasoning about knowledge and action[C]. In Proceedings of the Fifth International Joint Conference on Artificial Intelligence(IJCAI-77). Cambridge, MA,1977:223-227.
[164]M.Pauly. A Modal Logic for Coalitional Power in Games[J]. Journal of Logic and Computation.2002,12:146-166.
[165]W.van der Hoek and M.Wooldridge. On the logic of cooperation and propositional controo[J]. Artificial Intelligence.2005, Vol.64(1-2):81-119.
[166]卓继亮,李先贤,李建欣,怀进鹏.安全协议的攻击分类及其安全性评估[J].计算机研究与发展.2005,Vol.42(7)：1100-1107
[167]Syverson P. A taxonomy of replay attacks[C], Proceedings of the 1994 IEEE Computer Security Foundations Workshop VII. Los Alamitos:IEEE Computer Society Press,1994:187-191.
[168]A. Nenadi'c, N. Zhang, S. Barton. A security protocol for certified e-goods delivery[C]. Proc. IEEE Int. Conf. Information Technology, Coding, and Computing (ITCC'04):22-28.2004. Las Vegas, NV, USA. IEEE Computer Society.
[169]Almudena Alcaide, Juan M.Estevez-Tapiador, Antonio Izquierdo, and Jose M. Sierra. A formal analysis of fairness and Non-repudiation in the RSA-CEGD Protoco[C]. O.Gervasi et. al. (Eds):ICCSA2005; LNCS 3483:1309-1318,2005, Springer-Verlag.
[170]Chaum DL. Untraceable electronic mail, return addresses, and digital pseudonyms[J]. Communications of the ACM.1981, Vol.24(2):84-90.
[171]Atsushi Fujioka, Tatsuaki Okamoto, and Kazui Ohta. A practical secret voting scheme for large scale elections[C]. In J. Seberry and Y. Zheng, editors, Advances in Cryptology— AUSCRYPT'92.1992, Vol.718 of LNCS: 244-251, Springer.
[172]仲红,黄刘生,罗永龙.安全电子选举研究[J].安徽大学学报(自然科学版).2007,Vol.31(3)：20-25
[173]陈晓峰,王继林,王育民.基于办信任模型的无收据的电子投票[J].计算机学报.2003,Vol.26(5)：557-562.
[174]苏云学,逯海军,祝跃飞.一个无需中央机构的电子投票协议[J].计算机工程.2004,Vol.30(11)：96-97.
[175]Alexander Prosser, Robert Krimmer, The Dimensions of Electronic Voting Technology[C]. Law, Politics and Society, Workshop of the ESF TED Programme together with GI and OCG.2004,21-28. in Schloβ Hofen/Bregenz, Lake of Constance, Austria.
[176]王思佳,韩玮,陈克非,电子选举研究的挑战与进展[J],计算机工程,Vol.32(15)：7-9,2006.