网络协议安全性分析中的逻辑化方法研究
|
摘要
安全协议是建造网络安全环境的重要基石,是保证网络安全的核心技术。设计和证明安全协议自身的正确性和安全性,成为网络安全的基础。形式化分析方法已被证明是用于分析、设计和验证安全协议的重要方法,对安全协议的形式化分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。
虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击,但是这些分析方法还存在许多缺陷。有些形式化分析方法自身不太完善,存在一定的局限性,不能分析和验证某些类型安全协议的安全性:有些只能分析安全协议的不安全性,不能给出协议安全性的精确证明。
在总结安全协议现存各种缺陷的基础上,根据缺陷产生各种原因将缺陷分为:过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。同时把针对安全协议的各种攻击方法可分为:重放消息型攻击、猜测口令型攻击、分析密码型攻击、并行会话型攻击、格式缺陷型攻击和身份绑定型攻击等六类。
Burrows,Abadi和Needham提出的BAN逻辑开创了用逻辑化方法分析安全协议安全性的新纪元。由于该方法是对现实协议分析方法的抽象,逻辑处理的符号集是对现实具体协议的抽象;其初始假设、断言集合等均是从现实世界中抽象出来的要素。因此,其狭窄的符号集合定义也就决定了该方法存在不能分析某些类型协议安全性的缺陷,如:不能发现由于时间同步问题而导致的协议缺陷。另外使用BAN逻辑对安全协议分析时,很多初始假设是不合理的,如消息不可伪造假设就非常不合理,这些假设的不合理,妨碍了该分析方法的正确应用。BAN逻辑还存在非严谨的理想化步骤缺陷;语义不清晰缺陷;非严密的环境模型缺陷和无法有效预测对协议存在的攻击等缺陷。
1995年由Raiashekar Kailar提出的Kailar逻辑主要用于描述和分析电子商务协议,但是它只能分析电子商务协议的可追究性,无法分析电子商务协议的另一个重要特性——公平性。与BAN逻辑一样,使用Kailar逻辑分析协议之前同样需要引入一些初始假设,而初始假设的引入仍然是一个非形式化的过程,具有一定的人为性,其不准确会导致安全协议分析的失败。另外,用Kailar逻辑解释协议语义时,只能解释签名的明文消息,这样限制了其使用范围,对某些安全协议不能分析。
针对BAN类逻辑和Kailar逻辑的弱点,设计了一种新的安全协议分析逻辑CPL(Cryptographic Protocols Logic),CPL不但可用于分析协议的安全性,还可用来设计安全协议,即CPL逻辑把分析和设计安全协议纳入同一个逻辑体系中,消除了用不同方法分别设计和分析安全协议,将导致结果不一致性的缺陷,同时也简化了分析和设计安全协议时对初始条件和安全协议最终目标分别进行形式化的过程和步骤,提高了分析和设计安全协议的效率。
定义了CPL逻辑的基本符号、给出了CPL逻辑用于分析协议安全性的六类二十五条逻辑分析规则和用于设计安全协议的二十九条逻辑设计规则。分析规则和设计规则可分别用于安全协议的分析和安全协议的设计。给出了基于Kripke的CPL逻辑的语义,并利用逻辑语义对CPL系统自身的正确性进行了详细证明。运用新逻辑的分析规则和协议运行的初始条件以及安全协议的执行步骤分析安全协议的安全性。运用新逻辑的设计规则和协议运行的初始条件以及协议的最终目标设计出满足安全要求的安全协议。使用新逻辑分析了两个不同类型协议的安全性——密钥建立协议和身份认证协议。
Working as a kind of kernel technology for the secure network communication, the security protocols are the foundation in building up a safe internet environment. Therefore, the correctness and security of protocols play a crucial role in network environment. However, it remains to be solved on the security and design of the protocols to better meet the demands of the safety. A formalized method, thereafter, has been proved to be effective in analyzing and testing verification of the protocols, which so far has become a focus in the field of formal study.
Although the formal method has succeeded in finding flaws and attacks of many security protocols, it still suffers from lots of problems, such as the faultiness of the formal method itself, which can not suit the verification of some security protocols. On the other hand, some others can only presume the insecurity of cryptographic protocols rather than the credible verification of security objectives.
In terms of the causes and attacking methods accordingly, there are 7 types of deficiencies, i.e. protocol deficiency, password/key deficiency, outdated information deficiency, internal protocol deficiency, parallel communication deficiency, code system deficiency and other deficiencies. In the meanwhile, 6 types of attacks in security protocols have been classified: information-reissuing attacking, presuming attacking, code-analyzing attacking, parallel communication attacking, type deficiency attacking and binding attacking.
BAN logic, the foundation of the logic analysis, put forward by Burrow, Abadi and Needham, forms the landmark in analyzing security protocols. However, the narrow definition of symbol muster proves that there are some deficiencies which can not be analyzed, for the reasoning method of BAN logic is as a matter of fact abstracted from the real protocol analysis method and the symbol cluster of the logic process is abstracted from the real protocols. For example, it can not analyze the protocol deficiency by time synchronization, or it can not analyze the protocol with special password conversion method, etc. Besides, many illogic initial presumptions exist in BAN logic, which limits seriously the method into practice. Take the presumption that the news can not be forged as an example. Finally, some other deficiencies exist in BAN logic: non- standard idealized process deficiency, reasoning rule deficiency, lacking-in-clear- semantic deficiency, lacking-in-environment-model deficiency and lacking-in-effective-exploring -attacking deficiency, etc
As an important logic in studying and analyzing electronic business protocols, Kailar logic has flaws as follows: 1) Kailar logic can only study the pursuitability rather than the impartiality of the protocol; 2) As some presumptions will be introduced before the reasoning of Kailar logic, which is a non-standard process, improper introduction of presumption, therefore, will lead to the failure of protocol analysis; 3) The applicable range could be restricted when Kailar logic can only explain those signatory explicit information.
To sum up, a new logic of security protocol analysis---CPL, that is, Cryptographic Protocols Logic---has been designed, which can not only analyze but also design the security protocols. Thus, the new logic integrates the analysis and design into one logic frame, avoiding the potential disagreement owing to the different methods in analyzing and designing, simplifying the steps of initialized conditions and objectives in the formalized process of analyzing and designing security protocol, improving the efficiency of the analyzing and designing. CPL gives the primary symbols, reasoning and composition rules, among of which, the two rules can be used in analyzing and designing respectively in security protocols. The analysis process of the security protocols can test the safety of the protocol by way of the reasoning rules and initialized conditions and executive steps in analyzing the security of the protocols. The design process can design the security protocols by way of the composition rules and initialized conditions and objectives in protocol operation. Two kinds of protocols, i.e. password protocols and identification protocols have been illustrated on the basis of the new logic.
虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击,但是这些分析方法还存在许多缺陷。有些形式化分析方法自身不太完善,存在一定的局限性,不能分析和验证某些类型安全协议的安全性:有些只能分析安全协议的不安全性,不能给出协议安全性的精确证明。
在总结安全协议现存各种缺陷的基础上,根据缺陷产生各种原因将缺陷分为:过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。同时把针对安全协议的各种攻击方法可分为:重放消息型攻击、猜测口令型攻击、分析密码型攻击、并行会话型攻击、格式缺陷型攻击和身份绑定型攻击等六类。
Burrows,Abadi和Needham提出的BAN逻辑开创了用逻辑化方法分析安全协议安全性的新纪元。由于该方法是对现实协议分析方法的抽象,逻辑处理的符号集是对现实具体协议的抽象;其初始假设、断言集合等均是从现实世界中抽象出来的要素。因此,其狭窄的符号集合定义也就决定了该方法存在不能分析某些类型协议安全性的缺陷,如:不能发现由于时间同步问题而导致的协议缺陷。另外使用BAN逻辑对安全协议分析时,很多初始假设是不合理的,如消息不可伪造假设就非常不合理,这些假设的不合理,妨碍了该分析方法的正确应用。BAN逻辑还存在非严谨的理想化步骤缺陷;语义不清晰缺陷;非严密的环境模型缺陷和无法有效预测对协议存在的攻击等缺陷。
1995年由Raiashekar Kailar提出的Kailar逻辑主要用于描述和分析电子商务协议,但是它只能分析电子商务协议的可追究性,无法分析电子商务协议的另一个重要特性——公平性。与BAN逻辑一样,使用Kailar逻辑分析协议之前同样需要引入一些初始假设,而初始假设的引入仍然是一个非形式化的过程,具有一定的人为性,其不准确会导致安全协议分析的失败。另外,用Kailar逻辑解释协议语义时,只能解释签名的明文消息,这样限制了其使用范围,对某些安全协议不能分析。
针对BAN类逻辑和Kailar逻辑的弱点,设计了一种新的安全协议分析逻辑CPL(Cryptographic Protocols Logic),CPL不但可用于分析协议的安全性,还可用来设计安全协议,即CPL逻辑把分析和设计安全协议纳入同一个逻辑体系中,消除了用不同方法分别设计和分析安全协议,将导致结果不一致性的缺陷,同时也简化了分析和设计安全协议时对初始条件和安全协议最终目标分别进行形式化的过程和步骤,提高了分析和设计安全协议的效率。
定义了CPL逻辑的基本符号、给出了CPL逻辑用于分析协议安全性的六类二十五条逻辑分析规则和用于设计安全协议的二十九条逻辑设计规则。分析规则和设计规则可分别用于安全协议的分析和安全协议的设计。给出了基于Kripke的CPL逻辑的语义,并利用逻辑语义对CPL系统自身的正确性进行了详细证明。运用新逻辑的分析规则和协议运行的初始条件以及安全协议的执行步骤分析安全协议的安全性。运用新逻辑的设计规则和协议运行的初始条件以及协议的最终目标设计出满足安全要求的安全协议。使用新逻辑分析了两个不同类型协议的安全性——密钥建立协议和身份认证协议。
Working as a kind of kernel technology for the secure network communication, the security protocols are the foundation in building up a safe internet environment. Therefore, the correctness and security of protocols play a crucial role in network environment. However, it remains to be solved on the security and design of the protocols to better meet the demands of the safety. A formalized method, thereafter, has been proved to be effective in analyzing and testing verification of the protocols, which so far has become a focus in the field of formal study.
Although the formal method has succeeded in finding flaws and attacks of many security protocols, it still suffers from lots of problems, such as the faultiness of the formal method itself, which can not suit the verification of some security protocols. On the other hand, some others can only presume the insecurity of cryptographic protocols rather than the credible verification of security objectives.
In terms of the causes and attacking methods accordingly, there are 7 types of deficiencies, i.e. protocol deficiency, password/key deficiency, outdated information deficiency, internal protocol deficiency, parallel communication deficiency, code system deficiency and other deficiencies. In the meanwhile, 6 types of attacks in security protocols have been classified: information-reissuing attacking, presuming attacking, code-analyzing attacking, parallel communication attacking, type deficiency attacking and binding attacking.
BAN logic, the foundation of the logic analysis, put forward by Burrow, Abadi and Needham, forms the landmark in analyzing security protocols. However, the narrow definition of symbol muster proves that there are some deficiencies which can not be analyzed, for the reasoning method of BAN logic is as a matter of fact abstracted from the real protocol analysis method and the symbol cluster of the logic process is abstracted from the real protocols. For example, it can not analyze the protocol deficiency by time synchronization, or it can not analyze the protocol with special password conversion method, etc. Besides, many illogic initial presumptions exist in BAN logic, which limits seriously the method into practice. Take the presumption that the news can not be forged as an example. Finally, some other deficiencies exist in BAN logic: non- standard idealized process deficiency, reasoning rule deficiency, lacking-in-clear- semantic deficiency, lacking-in-environment-model deficiency and lacking-in-effective-exploring -attacking deficiency, etc
As an important logic in studying and analyzing electronic business protocols, Kailar logic has flaws as follows: 1) Kailar logic can only study the pursuitability rather than the impartiality of the protocol; 2) As some presumptions will be introduced before the reasoning of Kailar logic, which is a non-standard process, improper introduction of presumption, therefore, will lead to the failure of protocol analysis; 3) The applicable range could be restricted when Kailar logic can only explain those signatory explicit information.
To sum up, a new logic of security protocol analysis---CPL, that is, Cryptographic Protocols Logic---has been designed, which can not only analyze but also design the security protocols. Thus, the new logic integrates the analysis and design into one logic frame, avoiding the potential disagreement owing to the different methods in analyzing and designing, simplifying the steps of initialized conditions and objectives in the formalized process of analyzing and designing security protocol, improving the efficiency of the analyzing and designing. CPL gives the primary symbols, reasoning and composition rules, among of which, the two rules can be used in analyzing and designing respectively in security protocols. The analysis process of the security protocols can test the safety of the protocol by way of the reasoning rules and initialized conditions and executive steps in analyzing the security of the protocols. The design process can design the security protocols by way of the composition rules and initialized conditions and objectives in protocol operation. Two kinds of protocols, i.e. password protocols and identification protocols have been illustrated on the basis of the new logic.
引文
[1] Dekker M. Security of the Internet, the Froehlich/Kent Encyclopedia of telecommunications, 1997, Vol. 15: 231-255
[2] Schneier B. Applied Cryptography. Second Edtion. New York: John Wiley&Sons, Inc., 1996. 1-784
[3] Needham R, Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978, 21(12):993-999
[4] Qing SH. Cryptography and Computer Network Security. Beijing: Tsinghua University Press, 2001.127-147 (in Chinese)
[5] Qing SH. Formal analysis of authentication protocols. Journal of Software, 1996, 7:107-114 (in Chinese with English abstract)
[6] D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 1983,29(2): 198-208
[7] J. Millen, S. Clark, and S. Freedman. The Interrogator: protocol security analysis. IEEE Transactions on Software Engineering, 1987,13(2): 274-288
[8] D.Longley and S. Rigby. An automatic search for security flaws in key management schemes. Computers&Security, 1992,11:75-89
[9] Huanbao Wang, Yousheng Zhang, Yuan Li. Modeling for Security Verification of a Cryptographic Protocol with MAC Payload. In: Proc of ICIC2005. LNCS, Vol 3645.Springer-Verlag, 2005. 538-547
[10] B. B.Nieh. Modeling and Analysis of Cryptographic Protocols Using Petri Nets: [Master's Thesis Electrical Engin]. Kingston, Canada Queen's univ., 1992
[11] D.Dolev, S. Even, and R. Karp. On the Security of Ping-Pong Protocols. Information and Control, 1982. 57-68
[12] A. Datta, A. Derek, and J. C. Mitchell. A Derivation System for Security Protocols and its Logical Foundation. In: 16th IEEE Computer Security Foundations Workshop (CSFW03). 2003. 109-125
[13] W. Mao and C. Boyd. Classification of Cryptographic Techniques in Authentication Protocols. In: Selected Areas in Cryptograpy (SAC'94). Kingston, Ontario, Canada. May 1994. 95-106
[14] Li Gong, Roger Needham, and Raphael Yahalom. Reasoning About Belief in Cryptographic Protocols. In: Proceedings 1990 IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society, May 1990. 234-248
[15] Martin Abadi and Mark R. Turtle. A Semantics for a Logic of Authentication (Extended Abstract). In: Proceedings of the 10th Annual ACM Symposium On Principles of Distributed Computing. Montreal, Quebec, Canada: August 1991. 201-216
[16] P. van Oorschot. Extending cryptographic logics of belief to key agreement protocols. In: Proceedings of the First ACM Conference on Computers and Communications Security, 1993.232-243
[17] Wenbo Mao and Colin Boyd. Towards the Formal Analysis of Security Protocols. In: Proceedings of the Computer Security Foundations Workshop VI. IEEE Computer Society Press, 1993.147-158
[18] Paul Syverson and Paul C. van Oorshot. On Unifying some Cryptographic Protocol Logics. In: Proceedings of the IEEE 1994 Computer Society Symposium on Security and Privacy. IEEE Computer Society, May 1994. 14-28
[19] Stephen H. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. In: DIMACS Workshop on Design and Formal Verification of Security protocols, September 1997
[20] R. Kailar. Accountability in Electronic Commerce Protocols. IEEE Transaction on Software Engineering, 1996,22(5): 313-328
[21]Blanchet B.From Secrecy to Authentication in Security Protocols.In:Proc of the 9~(th) International Static Analysis Symposium.Madrid,2002.242-259
[22]J.Alves-Foss and T.Soule.A Weakest Precondition Calculus for Analysis of Cryptographic Protocols.In DIMACS Workshop on Design and Formal Verification of Security Protocols,September 1997
[23]B.B.Nieh.Modeling and Analysis of Cryptographic Protocols Using Petri Nets:[Master's Thesis,Electrical Engin]Kingston,Canada:Queen's univ.,1992
[24]刘东喜,赵玉源,李小勇等.基于对象Petri网的网络认证协议表示及分析.见:1999信息安全国际会议(InfoSecu'99)论文集.1999.159-160
[25]F.Germeau and G.Leduc.Model-based Design and Verification of Security Protocols using LOTOS.In DIMACS Workshop on Design and Formal Verification of Security Protocols,September 1997
[26]M.Debbabi,M.Mejri,N.Tawbi.A New Algorithm for the Automatic Verification of Authentication Protocols:From Specifications to Flaws and Attack Scenarios.In:DIMACS Workshop on Design and Formal Verification of Security protocols,September 1997
[27]Gavin Lowe.Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR.In:Proceedings of TACAS(Tools and Algorithms for the Construction and Analysis of Systems).volume 1055,Springer Verlag,1996.147-166
[28]Steve Schneider.Security Properties and CSP.In:Proceedings of the 1996 IEEE Symposium on Security and Privacy.IEEE Computer Society Press,May 1996.174-187
[29]A.W.Rosoe.Intensional Specification of Security Protocols.In:Proceedings of the 9~(th) IEEE Computer Security Foundations Workshop(CSFW9).IEEE Computer Society Press,June 1996.28-36
[30]A.W.Roscoe and M.H.Goldsmith.The Perfect "Spy" for Model-Checking Cryptoprotocols.In:DIMACS Workshop on Design and Formal Verification of Security protocols.September 1997
[31]C.Mitchell,M.Mitchell,and U.Stern.Automated Analysis of Cryptographic Protocols using Murφ.In:Proceedings of the IEEE Symposium on Security and Privacy,May 1997.141-151
[32]Zhe Dang and Richard A.Kemmerer.Using the ASTRAL Model Checker for Cryptographic Protocol Analysis.In:DIMACS Workshop on Design and Formal Verification of Security Protocols,September 1997
[33]Gavin Lowe.Some New Attacks upon Security Protocols.In:Proceedings of the Computer Security Foundations Workshop Ⅷ.IEEE Computer Society Press,1996
[34]Gavin Lowe.Casper:A compiler for the analysis of security protocols.In:Proceedings of 10~(th) IEEE Computer Security Foundations Workshop.IEEE Computer Society Press,1997.18-30
[35]G.Lowe,A.Roscoe.Using CSP to detect errors in the TMN protocol.IEEE Transactions on Software Engineering.1997,23(10):659-669
[36]Denis Treek and Borka Jerman Blazie.A Formal Language for Security Services Base Modelling and Analysis.Computer Networks.1995,18(12):921-928
[37]Gavin Lowe.Towards a Completeness Result for Model Checking of Security Protocols(Extended Abstract).In Proceedings of 11~(th) IEEE Computer Security Foundations Workshop.Rockport Massachusetts,June 1998
[38]R.Kemmerer,C.Meadows,and J.Millen.Three systems for cryptographic protocol analysis.Journal of Cryptology,1994,7(2):79-130
[39]Giampaolo Bella and Lawrence C Paulson.Using Isabelle to Prove Properties of the Kerberos Authentication System.In:DIMACS Workshop on Design and Formal Verification of Security protocols.September 1997
[40]Abadi M,Blanchet B.Analyzing security protocols with secrecy types and logic programs. In: Proc of the 29th ACM Symposium on Principles of Programming Languages (POPL'02) Portland, Oregon: ACM Press, 2002. 33-44
[41] B Blanchet. From secrecy to authenticity in security protocols. In: Proc of the 9th Int'I Static Analysis Symposium (SAS'02). LNCS, Vol 2477. Madrid, Spain: Springer-Verlag, 2002. 242-259
[42] Satyanarayanan M. Integrating security in a large distributed system. Technical Report, CMU-CS,CMU,(1987): 87-179
[43] R. Kemmerer, C. Meadows, and J. Millen. Three systems for cryptographic protocol analysis. Journal of Cryptology, 1994.7(2):79-130
[44] Caires L, Cardeli L. A partial logic for concurrency (Part I). In: Proc of the 4 International Conference on Theoretical Aspects of Computer Science (TACS 2001). LNCS, Vol 2215. Springer-Verlag, 2001. 1-37
[45] Caires L, Cardeli L. A partial logic for concurrency (Part II). In: Proc of the 13 International Conference on Concurrency Theory (CONCUR 2002). LNCS, Vol 2421. Springer-Verlag, 2002. 209-225
[46] Martin Abadi and Roger Needham. Prudent Engineering Practice for Cryptographic Protocols. IEEE Transactions on Software Engineering, January 1996,22(1): 6-15
[47] Li Gong and Paul Syverson. Fail-Stop Protocols: An Approach to Designing Secure Protocols. In Proceedings of the 5th International Working Conference on Dependable Computing for Critical Applications. September 1995. 44-55
[48] M. Burrows, M. Abadi, and R. Needham. A logic of authentication Research Report 39. ACM transactions on Computer System, Feb. 1990, 8(1): 18-36
[49] F.Javier Thayer Fabrega, Jonathan C.Herzog, Joshua D. Guttman. Honest Ideals on Strand Spaces. In: Proc 11~(th) IEEE Computer Security Foundations Workshop (CSFW). IEEE Computer Society Press, 1998
[50] Dan M. Nessett. A critique of the Burrows, Abadi and Needham Logic. Operating Systems Review.April 1990,Vol.24,No.2:35-38
[51]R.Needham and M.Schroeder.Using encryption for authentication in large networks of computers.Communications of the ACM,1978,21(12):993-998
[52]Kailar R.Accountability in electronic commerce protocols.IEEE Transactions on Software Engineering,1996,22(5):313-328
[53]周典萃,卿斯汉,周展飞.Kailar逻辑的缺陷.软件学报,1999,10(2):1238-1245
[54]冯登国著.密码分析学.北京:清华大学出版社,2000.115-122
[55]S.Brackin.An Interface Specification Language for Automatically Analyzing Cryptographic Protocols.Internet Society Symposium on Network and Distributed System Security.San Diego,CA.1997
[56]卿斯汉.密码学与计算机网络安全.北京:清华大学出版社,2000.127-147
[57]王贵林,卿斯汉,周展飞.认证协议的一些新攻击方法.软件学报,2001,12(6):907-913
[58]J.Zhou,D,Gollmann.A fair Non-repudiation protocol.In:Proceeding of 1996IEEE symposium on security and privacy.Okland,Clifomia,May 1996.55-61
[59]周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具.软件学报,2001,2(9):1318-1328
[60]Feng Bao,Robert H.Deng,and Wenbo Mao.Efficient and Practical Fair Exchange Protocols with Off-Line TTP.In:Proceeding Of The 1998 IEEE symposium on security and privacy.1998.77-85
[61]R.H.Deng,L.Gong,A.A.Lazar.Practical Protocols for Certified Electronic Mail.Journal of network and systems management,1996,4(3):279-297
[62]Woo T.Y.C.and Lam S.S.A lesson on authentication protocol design.Operating Systems Review,1994,24-37
[63]Butyan L.,Staamami S.,and Wilhelm U.A simple logic for authentication protocol design.In 11th IEEE Computer Security Foundations Workshop,1998.153-162
[64] Gong L. and Syverson P. Fail-Stop Protocols: An Approach to Designing Security Protocols. In: R. K. Iyer, M. Morganti, Fuchs W. K, and V. Gligor, editors. Dependable Computing for Critical Applications 5. IEEE Computer Society, 1998, 79-100
[65] Perrig A. and Song D. X. Looking for diamonds in the desert: Extending automatic protocol generation to three-party authentication and key agreement protocols. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, 2000
[66] Perrig A. and Song D. X. On a First Step to the Automatic Generation of Security Protocols. In Network and Distributed System Security Symposium, February 2000
[67] Schneier B. Applied Cryptography. Secoond Edtion. John Wiley&Sons, Inc., 1996
[68] L.Gong, R.Needham, R.Yahalom. Reasoning about Belief in Cryptographic Protocols. In: Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos ,California: IEEE Computer Society Press, 1990: 234-248
[69] N.A.Dargin, J.C.Mitchell. Analysis of Security Protocols. In: M.Broy, R.Steinbruggen editors. Calculational System Design. IOS Press, 1999.369-395
[70] J.Millen. Applications of Term Rewrite to Cryptography Protocol Analysis. In Kokichi Futatsugi editor, the 3rd international Workshop on Rewriting Logic and its Applications, 2000
[71] Ulf Carlsen. Generating Formal Cryptographic Protocol Specifications. In 1994 IEEE Computer society Symposium on Research in Security and Privacy. Oakland, Califonia. 1994. 137-146
[72] Einar Snekkenes. Formal Specification and Analysis of Cryptographic Protocols. [PhD thesis, Faculty of Mathematics and Natural Sciences]. University of Oslo. Norwegian Defence Research Establishment. 1995
[73]C.A.R Hoare.Communicating Sequential Processes.Prentice Hall International Series in Computer Science.London:Prentice Hall,1985
[74]Martin Abadi and Andrew D.Gordon.A Calculus for Cryptographic Protocols:The Spi Calculus.In:Proceedings of the 4th ACM Conference on Computer and Communications Security,1997
[75]Catherine Meadows.Representing partial knowledge in an algebraic security model.Proceedings of the Computer Security Foundation Workshop Ⅱ.1990.23-31
[76]M.Abadi and Z.Manna.Temporal Logic Programming.In:1987 Symposium on Logic Programming.IEEE Computer Society Press,1987.4-16
[77]Z.Manna and A.Pnueli.The Temporal Logic of Reactive and Concurent System Specification.New York:Springer-Verlag,1992
[78]F.Javier Thayer Fabrega,Jonathan C.Herzog and Joshua D.Guttman.Strand Spaces:Why is security protocol corect? In Proceedings of the 1998 IEEE Symposium on Security and Privacy.IEEE Computer Society Press,1998.160-171
[79]F Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Guttman.Strand Spaces:Proving Security Protocols Correct.Journal of Computer Security,1999,7(2-3):191-230
[80]白硕,隋立颖等.安全协议的验证逻辑.软件学报,2000.11(2):213-221
[81]J.Millen.The Interrogator model.In IEEE Symposium on Security and Privacy.IEEE Computer Society,1995.251-260
[82]C.Meadows.Language generation and verification in the NRL protocol analyzer.In:9th IEEE Computer Security Foundations Workshop.IEEE Computer Society,1996.48-61
[83]L.C.Paulson.The Inductive Approach to Verifying Cryptographic Protocols.Journal of Computer Security,1998.6(1-2):85-128
[84] S.H.Brackin. an Interface Specification Language for Automatically Analyzing Cryptographic Protocols. In Symposium on Network and Distributed System Security. 1997.40-51
[85] P. Syverson, C. Meadows, C. Iliano. Dolev-Yao is no better than Machiavelli. in: P. Degano (Ed.), Proc. 1st Workshop on Issues in the Theory of Security-WITS'00. Geneva, Switzerland. 2000. 87-92
[86] Daniel M. Nesset. A Critique of the Burrows, Abadi and Needham Logic. ACM Operating Systems Review. April 1990.24(2): 35-38
[87] C. Bo , W. Mao. On a Limitation of BAN Logic. In Advances in Cryptology-EUROCRYPT93. Volume 765 of Lecture Notes in Computer Science. Springer-Verlag, 1993.240-247
[88] Xu Shouhuai, Zhang Gendu and Zhu Hong. On the Properties of Cryptographic Protocols and the Weaknesses of the BAN-like logics. Operating Systems Review, October 1997: 12-23
[89] Paul C van Oorschot. Extending cryptographic Logics of belief to key agreement protocols. In Proceedings of the First ACM Conference on Computers and Communications security. 1993. 232-243
[90] Volker Kessler and Gabriele Wedel. AUTLOG-An advanced logic of authentication. In Proceedings of the Computer Security Foundations Workshop VII. IEEE Computer Society Press, June 1994. 90-99
[91] C. Meadows. Invariant generation techniques in cryptographic protocol analysis. In PCSFW:Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer Society Press, 2000
[92] C. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, February 1996, 26(2): 113-131
[93] G. Lowe. A hierarchy of authentication speci/cation, in: Proc. 10 Computer Security Foundation Workshop. New York: IEEE Press, 1997:31-43.
[94]Steve Schneider.Verifying authentication protocols in CSR.IEEE Transactions on Software Engineering,1998.24(9):741-758
[95]van der Meyden R,Su Kaile.Symbolic model checking the knowledge of the dining cryptographers.In:Proc of the 17"th IEEE Computer Security Foundation Workshop,2004.280-291
[96]范红,冯登国.一个非否认协议ZG的形式化分析.电子学报,2005,33(1):171-173
[97]G.Lowe.Some new attacks upon security protocols.In:Proceedings of 9th IEEE Computer Security Foundations Workshop.1996.162-169
[98]GBella,F.Massacci,L.C.Paulson.The Verification of an Industrial Payment Protocol:The SET Purchase Phase.In:VAtluri ed.9th ACM Conference on Computer and Comunications Security.ACM Press,2002.12-20
[99]Lawrence C.Paulson.Proving properties of security protocols induction.In:10th IEEE Computer Security Foundations Workshop.IEEE Computer Society Press,1997.70-83
[100]Bart De Decker and Frank Piessens.CryptoLog:A Theorem Prover for Cryptographic Protocols.In DIMACS Workshop on Design and Formal Verification of Security protocols,September 1997
[101]D.Bolignano.An approach for the formal verification of cryptographic protocols.In ACM Conference on Computer and Communications Security.ACM Press,1996.106-118
[102]Blancher B.An efficient cryptographic protocol verifier based on prolog rules.In:Proc of the 14th Computer Security Foundation Workshop(CSFW14).Cape Breton,Nova Scotia,Canada:IEEE Computer Society Press,2001.82-96
[103]B Blanchet.From secrecy to authenticity in security protocols.In:Proc of the 9th Int'I Static Analysis Symposium(SAS'02).LNCS,Vol 2477.Madrid,Spain:Springer-Verlag,2002.242-259
[104]F.Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Gutmian.Honest ideals on strand spaces.In:Proceedings of the 11th IEEE Computer Security Foundations Workshop.IEEE Computer Society Press,June 1998
[105]G.Lowe.Casper:a compiler for the analysis of security protocols.Journal of Computer Security,1998,6(1):53-84
[106]F.Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Guttman.Mixed strand space.Proceedings of the 12~(th) IEEE Computer Security Foundations Workshop.Mordano,Italy:IEEE Computer Society Press,1999.72-82
[107]M.Bellare,PRogaway.Random Oracles are Practical.In:Proceedings of 1st Annual Conference on Computer and Communications Security.ACM Press,1993.154-164
[108]T.Woo and S.Lam.A semantic model for authentication protocols.Proceedings of the 1993 IEEE Computer Society Symposium on Research in Security and Privacy.May 1993.178-194
[109]Paul Syverson and Catherine Meadows.Formal Requirements for Key Distribution Protocols.In A.De Santis.Advances in Cryptology-EUROCRYPT '94.University of Perugia,Italy.Springer-Vedag,1994.325-331
[110]Rohit Chadha,Max Kanovich,Andre Scedrov.Inductive methods and contract signing protocols.In:Proc of the 8th ACM Conference on Computer and Communications Security.Philadelphia,PA:ACM Press,2001.176-185
[11]Catherine Meadows and Paul Syverson.A formal specification of requirements for payment transactions in the SET protocol.In R.Hirschfeld editor.Financial Cryptography,FC'98.Springer-Verlag,LNCS 1465,1998.122-140
[112]周展飞,周典萃,王贵林等.电子商务协议的公平性.电子学报,2000.28(9)
[113]陈庆锋,白硕,王驹.电子商务协议及其非单调动态逻辑验证.软件学报,200111(2):240-250
[114]A.W.Roscoe.Intensional specifications of security protocols.In:J.Guttman ed. Proceedings of 9th IEEE Computer Security Foundations Workshop.Los Alamitos,California:IEEE Computer Society,1996.28-38
[115]A D Gordon,A Jeffrey.Authenticity by typing for security protocols.In:Proc of the 14~(th) Computer Security Foundation Workshop(CSFW14).Cape Breton,Nova Scotia,Canada:IEEE Computer Society Press,2001.145-159
[116]G.Lowe.Hierarchy of Authentication Specifications.In:J.Guttman.10th IEEE Computer Security Foundations Workshop Proceedings.CA:IEEE Computer Society Press,1997.31-43
[117]C.Meadows.Open Issues in Formal Methods for Cryptographic Protocol Analysis.Proceedings of the DISCEX 2000.IEEE Computer Society Press,2000.237-250
[118]Dawn Song,Sergey Berezin,Adrian Perrig.Athena:a New Eficient Automatic Checker for Security Protocol Analysis.In:12th IEEE Computer Security Foundations Workshop.IEEE Computer Society,1999.192-202.
[119]D.E.Denning and G.M.Sacco.Timestamps in key distribution protocols.Communications of the ACM.1981.24(8):533-536
[120]U.Carlsen.Using Logic to Detect Implementation-Dependent Flaws.In:Proceeding of the 9~(th) IEEE Annual Computer Security Applications Conference.IEEE Computer Society Press,1993.64-73
[121]P.Y.A.Ryan,S.Schneider.Process algebra and non-interference.In:Proc.CSFW'99,New York:IEEE Press,1999.214-227
[122]T.Hwang and Yung-Hsiang Chen.On the security of SPLICE/AS:The authentication system in WIDE Internet Information Processing Letters,1995.53:97-101
[123]R.Morris.Password Security:A Case History.Communications of the ACM 1979.22(11):497-594
[124]P.Janson,R.Molva.Security in Open Networks and Distributed Systems. Computer Networks and ISDN System 1991.22(5):323-346
[125]J.Trado and K.Alagappan.SPX:Global authentication using public key certificates.In Proc.14~(th) National Computer Security Conference.NIST/NCSC.Baltimore,1991
[126]L.Gong.Optimal Authentication Protocols Resistant to Password Guessing Attack.In Proceedings of the 1995 IEEE Computer Security Foundationd Workshop Ⅷ.IEEE Computer Society Press,1995.24-29
[127]Michael Burrows and Martin Abadi and Roger Needham.BAN concrete Andrew Secure RPC.Last modified November 14,2002
[128]P.Syverson.A Taxonomy of Reply Attack.In Proceedings of the 1994 IEEE Computer Security Foundations Workshop.IEEE Computer Society Press,1994.187-191
[129]R.C.Neuman and S.G..Stubblebine.A Note on the Use of Timestamps as Nonces.Operating System Review,1993.27(2):10-14
[130]C.Bodei,M.Buchholtz,P Degano,R Nielson etc.Nielson.Automatic Validation of Protocol Narration.In Proceedings of the 16th computer security foundations workshop.IEEE computer society press,2003.126-140
[131]Emina Torlak,Marten van Dijk,Blaise Gassend,etc.Knowledge Flow Analysis for Security Protocols.Computer Science and Artificial Intelligence Laboratory,August 8,2005
[132]Mikael Buchholtz,Hanne Riis Nielson,Flemming Nielson.A Calculus for Control Flow Analysis of Security Protocols.Information Society Technology program of the European Commisssion.2004
[133]卿斯汉,李改成.公平交换协议的一个形式化模型.中国科学(E辑),2005,35(2):161-172
[134]James Heather,Gavin Lowe,and Steve Schneider.How to Prevent Type Flaw Attacks on Security Protocols.In:Proceedings of 13th IEEE Computer Security Foundations Workshop.2000.255-268
[135]James Heather,Gavin Lowe,Steve Schneider.How to prevent type flaw attacks on security protocols.Journal of Computer Security,2003.11(2)
[136]P.J Broadfoot and A.W.Roscoe.Internalising agents in CSP protocol models.Workshop on Issues in the Theory of Security(WITS'02).Protland Oregon,USA.2002
[137]Giampaolo Bella,Fabio Massacci and L.C.Paulson.An overview of the verification of SET.International Journal of Information Security,2005,4:17-28
[138]苏开乐,岳伟亚 等.实例化空间:一种新的安全协议验证逻辑的语义模型.计算机学报,2006,29(9):1657-1665
[139]Scott D.Stoller and Fred B.Schneider.Automated Analysis of Fault-Tolerance in Distributed Systems.Formal Methods in System Design,2005,26(2):183-196
[140]N.Li and J.C.Mitchell.Understanding SPKI/SDSI Using First-Order Logic.IEEE Computer Security Foundations Workshop.Pacific Grove,California,2003.89-103
[141]Joshua D.Guttman,F.Javier Thayer.Protocol Independence through Disjoint Eneryption.In:Proceedings of the 13th IEEE Computer Security Foundations Workshop(CSFW'00).2000.03-05
[142]毛晨晓,罗文坚,王熙法.分析安全协议猜测攻击的模态逻辑方法.计算机学报,2007,30(6):924-933
[143]F Butler,I Cervesato,A Jaggard,and A Scedrov.A formal analysis of some properties of Kerberos V using MSR.In:Proc of the 15~(th) Computer Security Foundations Workshop.IEEE Computer Society Press,2002
[144]B.Blanchet,M.Abadi,C.Fournet.Automated verification of selected equivalences for security protocols.In:20th IEEE Symposium on Logic in Computer Science.June 2005.331-340
[145]侯峻峰,张磊,黄连生.一种新的安全协议形式化验证方法.计算机研究与发 展,2004,41(8):1415-1420
[146]乔海燕.安全协议验证的归纳方法与串空间形式化比较.计算机研究与发展,2008,45:137-142
[147]胡成军,郑援,沈昌祥.密码协议的秘密性证明.计算机学报,2003,26(3):1-6
[148]Durgin N.,Mitchell J.,Pavlovic D.A compositional logic for proving security properties of protocols.Journal of Computer Security,2003,11(4):677-721
[149]Joshua D Guttman.Security Protocol Design Via Authentication Tests.In:Proc of the 15th Computer Security Foundations Workshop.IEEE Computer Society Press,2002
[150]J C Herzog.The Diffie-Hellman Key Agreement Scheme in the Strand Space Model.In:Proc of 16th IEEE Computer Security Foundations Workshop.IEEE CS Press,2003
[151]Boreale M,Buscemi M.Experimenting with STA,a tool for automatic analysis of security protocols.In:Proc of the 2002 ACM Symposium on Applied Computing.Madrid,Spain,2002.281-285
[152]Huanbao Wang,Yousheng Zhang,and Yuan Li.Structural Control Operators for Composing Diagrams of Strand Spaces of Concurrent Cryptographic Protocols.In:Proc of WCICA2006.2006
[153]J.Borgstrom,S.Briais,U.Nestmann.Symbolic Bisimulation in the Spi Calculus.In CONCUR 2004,vol3170 of LNCS,Springer,Aug.2004.161-176
[154]李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述.计算机研究与发展,2004,41(7):1097-1103
[155]薛锐,冯登国.安全协议的形式化分析技术与方法.计算机学报,2006,29(1):1-20
[156]冯登国,陈伟东.基于口令的安全协议的模块化设计与分析.中国科学 E辑:信息科学,2007,37(2):223-237
[2] Schneier B. Applied Cryptography. Second Edtion. New York: John Wiley&Sons, Inc., 1996. 1-784
[3] Needham R, Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978, 21(12):993-999
[4] Qing SH. Cryptography and Computer Network Security. Beijing: Tsinghua University Press, 2001.127-147 (in Chinese)
[5] Qing SH. Formal analysis of authentication protocols. Journal of Software, 1996, 7:107-114 (in Chinese with English abstract)
[6] D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 1983,29(2): 198-208
[7] J. Millen, S. Clark, and S. Freedman. The Interrogator: protocol security analysis. IEEE Transactions on Software Engineering, 1987,13(2): 274-288
[8] D.Longley and S. Rigby. An automatic search for security flaws in key management schemes. Computers&Security, 1992,11:75-89
[9] Huanbao Wang, Yousheng Zhang, Yuan Li. Modeling for Security Verification of a Cryptographic Protocol with MAC Payload. In: Proc of ICIC2005. LNCS, Vol 3645.Springer-Verlag, 2005. 538-547
[10] B. B.Nieh. Modeling and Analysis of Cryptographic Protocols Using Petri Nets: [Master's Thesis Electrical Engin]. Kingston, Canada Queen's univ., 1992
[11] D.Dolev, S. Even, and R. Karp. On the Security of Ping-Pong Protocols. Information and Control, 1982. 57-68
[12] A. Datta, A. Derek, and J. C. Mitchell. A Derivation System for Security Protocols and its Logical Foundation. In: 16th IEEE Computer Security Foundations Workshop (CSFW03). 2003. 109-125
[13] W. Mao and C. Boyd. Classification of Cryptographic Techniques in Authentication Protocols. In: Selected Areas in Cryptograpy (SAC'94). Kingston, Ontario, Canada. May 1994. 95-106
[14] Li Gong, Roger Needham, and Raphael Yahalom. Reasoning About Belief in Cryptographic Protocols. In: Proceedings 1990 IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society, May 1990. 234-248
[15] Martin Abadi and Mark R. Turtle. A Semantics for a Logic of Authentication (Extended Abstract). In: Proceedings of the 10th Annual ACM Symposium On Principles of Distributed Computing. Montreal, Quebec, Canada: August 1991. 201-216
[16] P. van Oorschot. Extending cryptographic logics of belief to key agreement protocols. In: Proceedings of the First ACM Conference on Computers and Communications Security, 1993.232-243
[17] Wenbo Mao and Colin Boyd. Towards the Formal Analysis of Security Protocols. In: Proceedings of the Computer Security Foundations Workshop VI. IEEE Computer Society Press, 1993.147-158
[18] Paul Syverson and Paul C. van Oorshot. On Unifying some Cryptographic Protocol Logics. In: Proceedings of the IEEE 1994 Computer Society Symposium on Security and Privacy. IEEE Computer Society, May 1994. 14-28
[19] Stephen H. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. In: DIMACS Workshop on Design and Formal Verification of Security protocols, September 1997
[20] R. Kailar. Accountability in Electronic Commerce Protocols. IEEE Transaction on Software Engineering, 1996,22(5): 313-328
[21]Blanchet B.From Secrecy to Authentication in Security Protocols.In:Proc of the 9~(th) International Static Analysis Symposium.Madrid,2002.242-259
[22]J.Alves-Foss and T.Soule.A Weakest Precondition Calculus for Analysis of Cryptographic Protocols.In DIMACS Workshop on Design and Formal Verification of Security Protocols,September 1997
[23]B.B.Nieh.Modeling and Analysis of Cryptographic Protocols Using Petri Nets:[Master's Thesis,Electrical Engin]Kingston,Canada:Queen's univ.,1992
[24]刘东喜,赵玉源,李小勇等.基于对象Petri网的网络认证协议表示及分析.见:1999信息安全国际会议(InfoSecu'99)论文集.1999.159-160
[25]F.Germeau and G.Leduc.Model-based Design and Verification of Security Protocols using LOTOS.In DIMACS Workshop on Design and Formal Verification of Security Protocols,September 1997
[26]M.Debbabi,M.Mejri,N.Tawbi.A New Algorithm for the Automatic Verification of Authentication Protocols:From Specifications to Flaws and Attack Scenarios.In:DIMACS Workshop on Design and Formal Verification of Security protocols,September 1997
[27]Gavin Lowe.Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR.In:Proceedings of TACAS(Tools and Algorithms for the Construction and Analysis of Systems).volume 1055,Springer Verlag,1996.147-166
[28]Steve Schneider.Security Properties and CSP.In:Proceedings of the 1996 IEEE Symposium on Security and Privacy.IEEE Computer Society Press,May 1996.174-187
[29]A.W.Rosoe.Intensional Specification of Security Protocols.In:Proceedings of the 9~(th) IEEE Computer Security Foundations Workshop(CSFW9).IEEE Computer Society Press,June 1996.28-36
[30]A.W.Roscoe and M.H.Goldsmith.The Perfect "Spy" for Model-Checking Cryptoprotocols.In:DIMACS Workshop on Design and Formal Verification of Security protocols.September 1997
[31]C.Mitchell,M.Mitchell,and U.Stern.Automated Analysis of Cryptographic Protocols using Murφ.In:Proceedings of the IEEE Symposium on Security and Privacy,May 1997.141-151
[32]Zhe Dang and Richard A.Kemmerer.Using the ASTRAL Model Checker for Cryptographic Protocol Analysis.In:DIMACS Workshop on Design and Formal Verification of Security Protocols,September 1997
[33]Gavin Lowe.Some New Attacks upon Security Protocols.In:Proceedings of the Computer Security Foundations Workshop Ⅷ.IEEE Computer Society Press,1996
[34]Gavin Lowe.Casper:A compiler for the analysis of security protocols.In:Proceedings of 10~(th) IEEE Computer Security Foundations Workshop.IEEE Computer Society Press,1997.18-30
[35]G.Lowe,A.Roscoe.Using CSP to detect errors in the TMN protocol.IEEE Transactions on Software Engineering.1997,23(10):659-669
[36]Denis Treek and Borka Jerman Blazie.A Formal Language for Security Services Base Modelling and Analysis.Computer Networks.1995,18(12):921-928
[37]Gavin Lowe.Towards a Completeness Result for Model Checking of Security Protocols(Extended Abstract).In Proceedings of 11~(th) IEEE Computer Security Foundations Workshop.Rockport Massachusetts,June 1998
[38]R.Kemmerer,C.Meadows,and J.Millen.Three systems for cryptographic protocol analysis.Journal of Cryptology,1994,7(2):79-130
[39]Giampaolo Bella and Lawrence C Paulson.Using Isabelle to Prove Properties of the Kerberos Authentication System.In:DIMACS Workshop on Design and Formal Verification of Security protocols.September 1997
[40]Abadi M,Blanchet B.Analyzing security protocols with secrecy types and logic programs. In: Proc of the 29th ACM Symposium on Principles of Programming Languages (POPL'02) Portland, Oregon: ACM Press, 2002. 33-44
[41] B Blanchet. From secrecy to authenticity in security protocols. In: Proc of the 9th Int'I Static Analysis Symposium (SAS'02). LNCS, Vol 2477. Madrid, Spain: Springer-Verlag, 2002. 242-259
[42] Satyanarayanan M. Integrating security in a large distributed system. Technical Report, CMU-CS,CMU,(1987): 87-179
[43] R. Kemmerer, C. Meadows, and J. Millen. Three systems for cryptographic protocol analysis. Journal of Cryptology, 1994.7(2):79-130
[44] Caires L, Cardeli L. A partial logic for concurrency (Part I). In: Proc of the 4 International Conference on Theoretical Aspects of Computer Science (TACS 2001). LNCS, Vol 2215. Springer-Verlag, 2001. 1-37
[45] Caires L, Cardeli L. A partial logic for concurrency (Part II). In: Proc of the 13 International Conference on Concurrency Theory (CONCUR 2002). LNCS, Vol 2421. Springer-Verlag, 2002. 209-225
[46] Martin Abadi and Roger Needham. Prudent Engineering Practice for Cryptographic Protocols. IEEE Transactions on Software Engineering, January 1996,22(1): 6-15
[47] Li Gong and Paul Syverson. Fail-Stop Protocols: An Approach to Designing Secure Protocols. In Proceedings of the 5th International Working Conference on Dependable Computing for Critical Applications. September 1995. 44-55
[48] M. Burrows, M. Abadi, and R. Needham. A logic of authentication Research Report 39. ACM transactions on Computer System, Feb. 1990, 8(1): 18-36
[49] F.Javier Thayer Fabrega, Jonathan C.Herzog, Joshua D. Guttman. Honest Ideals on Strand Spaces. In: Proc 11~(th) IEEE Computer Security Foundations Workshop (CSFW). IEEE Computer Society Press, 1998
[50] Dan M. Nessett. A critique of the Burrows, Abadi and Needham Logic. Operating Systems Review.April 1990,Vol.24,No.2:35-38
[51]R.Needham and M.Schroeder.Using encryption for authentication in large networks of computers.Communications of the ACM,1978,21(12):993-998
[52]Kailar R.Accountability in electronic commerce protocols.IEEE Transactions on Software Engineering,1996,22(5):313-328
[53]周典萃,卿斯汉,周展飞.Kailar逻辑的缺陷.软件学报,1999,10(2):1238-1245
[54]冯登国著.密码分析学.北京:清华大学出版社,2000.115-122
[55]S.Brackin.An Interface Specification Language for Automatically Analyzing Cryptographic Protocols.Internet Society Symposium on Network and Distributed System Security.San Diego,CA.1997
[56]卿斯汉.密码学与计算机网络安全.北京:清华大学出版社,2000.127-147
[57]王贵林,卿斯汉,周展飞.认证协议的一些新攻击方法.软件学报,2001,12(6):907-913
[58]J.Zhou,D,Gollmann.A fair Non-repudiation protocol.In:Proceeding of 1996IEEE symposium on security and privacy.Okland,Clifomia,May 1996.55-61
[59]周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具.软件学报,2001,2(9):1318-1328
[60]Feng Bao,Robert H.Deng,and Wenbo Mao.Efficient and Practical Fair Exchange Protocols with Off-Line TTP.In:Proceeding Of The 1998 IEEE symposium on security and privacy.1998.77-85
[61]R.H.Deng,L.Gong,A.A.Lazar.Practical Protocols for Certified Electronic Mail.Journal of network and systems management,1996,4(3):279-297
[62]Woo T.Y.C.and Lam S.S.A lesson on authentication protocol design.Operating Systems Review,1994,24-37
[63]Butyan L.,Staamami S.,and Wilhelm U.A simple logic for authentication protocol design.In 11th IEEE Computer Security Foundations Workshop,1998.153-162
[64] Gong L. and Syverson P. Fail-Stop Protocols: An Approach to Designing Security Protocols. In: R. K. Iyer, M. Morganti, Fuchs W. K, and V. Gligor, editors. Dependable Computing for Critical Applications 5. IEEE Computer Society, 1998, 79-100
[65] Perrig A. and Song D. X. Looking for diamonds in the desert: Extending automatic protocol generation to three-party authentication and key agreement protocols. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, 2000
[66] Perrig A. and Song D. X. On a First Step to the Automatic Generation of Security Protocols. In Network and Distributed System Security Symposium, February 2000
[67] Schneier B. Applied Cryptography. Secoond Edtion. John Wiley&Sons, Inc., 1996
[68] L.Gong, R.Needham, R.Yahalom. Reasoning about Belief in Cryptographic Protocols. In: Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos ,California: IEEE Computer Society Press, 1990: 234-248
[69] N.A.Dargin, J.C.Mitchell. Analysis of Security Protocols. In: M.Broy, R.Steinbruggen editors. Calculational System Design. IOS Press, 1999.369-395
[70] J.Millen. Applications of Term Rewrite to Cryptography Protocol Analysis. In Kokichi Futatsugi editor, the 3rd international Workshop on Rewriting Logic and its Applications, 2000
[71] Ulf Carlsen. Generating Formal Cryptographic Protocol Specifications. In 1994 IEEE Computer society Symposium on Research in Security and Privacy. Oakland, Califonia. 1994. 137-146
[72] Einar Snekkenes. Formal Specification and Analysis of Cryptographic Protocols. [PhD thesis, Faculty of Mathematics and Natural Sciences]. University of Oslo. Norwegian Defence Research Establishment. 1995
[73]C.A.R Hoare.Communicating Sequential Processes.Prentice Hall International Series in Computer Science.London:Prentice Hall,1985
[74]Martin Abadi and Andrew D.Gordon.A Calculus for Cryptographic Protocols:The Spi Calculus.In:Proceedings of the 4th ACM Conference on Computer and Communications Security,1997
[75]Catherine Meadows.Representing partial knowledge in an algebraic security model.Proceedings of the Computer Security Foundation Workshop Ⅱ.1990.23-31
[76]M.Abadi and Z.Manna.Temporal Logic Programming.In:1987 Symposium on Logic Programming.IEEE Computer Society Press,1987.4-16
[77]Z.Manna and A.Pnueli.The Temporal Logic of Reactive and Concurent System Specification.New York:Springer-Verlag,1992
[78]F.Javier Thayer Fabrega,Jonathan C.Herzog and Joshua D.Guttman.Strand Spaces:Why is security protocol corect? In Proceedings of the 1998 IEEE Symposium on Security and Privacy.IEEE Computer Society Press,1998.160-171
[79]F Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Guttman.Strand Spaces:Proving Security Protocols Correct.Journal of Computer Security,1999,7(2-3):191-230
[80]白硕,隋立颖等.安全协议的验证逻辑.软件学报,2000.11(2):213-221
[81]J.Millen.The Interrogator model.In IEEE Symposium on Security and Privacy.IEEE Computer Society,1995.251-260
[82]C.Meadows.Language generation and verification in the NRL protocol analyzer.In:9th IEEE Computer Security Foundations Workshop.IEEE Computer Society,1996.48-61
[83]L.C.Paulson.The Inductive Approach to Verifying Cryptographic Protocols.Journal of Computer Security,1998.6(1-2):85-128
[84] S.H.Brackin. an Interface Specification Language for Automatically Analyzing Cryptographic Protocols. In Symposium on Network and Distributed System Security. 1997.40-51
[85] P. Syverson, C. Meadows, C. Iliano. Dolev-Yao is no better than Machiavelli. in: P. Degano (Ed.), Proc. 1st Workshop on Issues in the Theory of Security-WITS'00. Geneva, Switzerland. 2000. 87-92
[86] Daniel M. Nesset. A Critique of the Burrows, Abadi and Needham Logic. ACM Operating Systems Review. April 1990.24(2): 35-38
[87] C. Bo , W. Mao. On a Limitation of BAN Logic. In Advances in Cryptology-EUROCRYPT93. Volume 765 of Lecture Notes in Computer Science. Springer-Verlag, 1993.240-247
[88] Xu Shouhuai, Zhang Gendu and Zhu Hong. On the Properties of Cryptographic Protocols and the Weaknesses of the BAN-like logics. Operating Systems Review, October 1997: 12-23
[89] Paul C van Oorschot. Extending cryptographic Logics of belief to key agreement protocols. In Proceedings of the First ACM Conference on Computers and Communications security. 1993. 232-243
[90] Volker Kessler and Gabriele Wedel. AUTLOG-An advanced logic of authentication. In Proceedings of the Computer Security Foundations Workshop VII. IEEE Computer Society Press, June 1994. 90-99
[91] C. Meadows. Invariant generation techniques in cryptographic protocol analysis. In PCSFW:Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer Society Press, 2000
[92] C. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, February 1996, 26(2): 113-131
[93] G. Lowe. A hierarchy of authentication speci/cation, in: Proc. 10 Computer Security Foundation Workshop. New York: IEEE Press, 1997:31-43.
[94]Steve Schneider.Verifying authentication protocols in CSR.IEEE Transactions on Software Engineering,1998.24(9):741-758
[95]van der Meyden R,Su Kaile.Symbolic model checking the knowledge of the dining cryptographers.In:Proc of the 17"th IEEE Computer Security Foundation Workshop,2004.280-291
[96]范红,冯登国.一个非否认协议ZG的形式化分析.电子学报,2005,33(1):171-173
[97]G.Lowe.Some new attacks upon security protocols.In:Proceedings of 9th IEEE Computer Security Foundations Workshop.1996.162-169
[98]GBella,F.Massacci,L.C.Paulson.The Verification of an Industrial Payment Protocol:The SET Purchase Phase.In:VAtluri ed.9th ACM Conference on Computer and Comunications Security.ACM Press,2002.12-20
[99]Lawrence C.Paulson.Proving properties of security protocols induction.In:10th IEEE Computer Security Foundations Workshop.IEEE Computer Society Press,1997.70-83
[100]Bart De Decker and Frank Piessens.CryptoLog:A Theorem Prover for Cryptographic Protocols.In DIMACS Workshop on Design and Formal Verification of Security protocols,September 1997
[101]D.Bolignano.An approach for the formal verification of cryptographic protocols.In ACM Conference on Computer and Communications Security.ACM Press,1996.106-118
[102]Blancher B.An efficient cryptographic protocol verifier based on prolog rules.In:Proc of the 14th Computer Security Foundation Workshop(CSFW14).Cape Breton,Nova Scotia,Canada:IEEE Computer Society Press,2001.82-96
[103]B Blanchet.From secrecy to authenticity in security protocols.In:Proc of the 9th Int'I Static Analysis Symposium(SAS'02).LNCS,Vol 2477.Madrid,Spain:Springer-Verlag,2002.242-259
[104]F.Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Gutmian.Honest ideals on strand spaces.In:Proceedings of the 11th IEEE Computer Security Foundations Workshop.IEEE Computer Society Press,June 1998
[105]G.Lowe.Casper:a compiler for the analysis of security protocols.Journal of Computer Security,1998,6(1):53-84
[106]F.Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Guttman.Mixed strand space.Proceedings of the 12~(th) IEEE Computer Security Foundations Workshop.Mordano,Italy:IEEE Computer Society Press,1999.72-82
[107]M.Bellare,PRogaway.Random Oracles are Practical.In:Proceedings of 1st Annual Conference on Computer and Communications Security.ACM Press,1993.154-164
[108]T.Woo and S.Lam.A semantic model for authentication protocols.Proceedings of the 1993 IEEE Computer Society Symposium on Research in Security and Privacy.May 1993.178-194
[109]Paul Syverson and Catherine Meadows.Formal Requirements for Key Distribution Protocols.In A.De Santis.Advances in Cryptology-EUROCRYPT '94.University of Perugia,Italy.Springer-Vedag,1994.325-331
[110]Rohit Chadha,Max Kanovich,Andre Scedrov.Inductive methods and contract signing protocols.In:Proc of the 8th ACM Conference on Computer and Communications Security.Philadelphia,PA:ACM Press,2001.176-185
[11]Catherine Meadows and Paul Syverson.A formal specification of requirements for payment transactions in the SET protocol.In R.Hirschfeld editor.Financial Cryptography,FC'98.Springer-Verlag,LNCS 1465,1998.122-140
[112]周展飞,周典萃,王贵林等.电子商务协议的公平性.电子学报,2000.28(9)
[113]陈庆锋,白硕,王驹.电子商务协议及其非单调动态逻辑验证.软件学报,200111(2):240-250
[114]A.W.Roscoe.Intensional specifications of security protocols.In:J.Guttman ed. Proceedings of 9th IEEE Computer Security Foundations Workshop.Los Alamitos,California:IEEE Computer Society,1996.28-38
[115]A D Gordon,A Jeffrey.Authenticity by typing for security protocols.In:Proc of the 14~(th) Computer Security Foundation Workshop(CSFW14).Cape Breton,Nova Scotia,Canada:IEEE Computer Society Press,2001.145-159
[116]G.Lowe.Hierarchy of Authentication Specifications.In:J.Guttman.10th IEEE Computer Security Foundations Workshop Proceedings.CA:IEEE Computer Society Press,1997.31-43
[117]C.Meadows.Open Issues in Formal Methods for Cryptographic Protocol Analysis.Proceedings of the DISCEX 2000.IEEE Computer Society Press,2000.237-250
[118]Dawn Song,Sergey Berezin,Adrian Perrig.Athena:a New Eficient Automatic Checker for Security Protocol Analysis.In:12th IEEE Computer Security Foundations Workshop.IEEE Computer Society,1999.192-202.
[119]D.E.Denning and G.M.Sacco.Timestamps in key distribution protocols.Communications of the ACM.1981.24(8):533-536
[120]U.Carlsen.Using Logic to Detect Implementation-Dependent Flaws.In:Proceeding of the 9~(th) IEEE Annual Computer Security Applications Conference.IEEE Computer Society Press,1993.64-73
[121]P.Y.A.Ryan,S.Schneider.Process algebra and non-interference.In:Proc.CSFW'99,New York:IEEE Press,1999.214-227
[122]T.Hwang and Yung-Hsiang Chen.On the security of SPLICE/AS:The authentication system in WIDE Internet Information Processing Letters,1995.53:97-101
[123]R.Morris.Password Security:A Case History.Communications of the ACM 1979.22(11):497-594
[124]P.Janson,R.Molva.Security in Open Networks and Distributed Systems. Computer Networks and ISDN System 1991.22(5):323-346
[125]J.Trado and K.Alagappan.SPX:Global authentication using public key certificates.In Proc.14~(th) National Computer Security Conference.NIST/NCSC.Baltimore,1991
[126]L.Gong.Optimal Authentication Protocols Resistant to Password Guessing Attack.In Proceedings of the 1995 IEEE Computer Security Foundationd Workshop Ⅷ.IEEE Computer Society Press,1995.24-29
[127]Michael Burrows and Martin Abadi and Roger Needham.BAN concrete Andrew Secure RPC.Last modified November 14,2002
[128]P.Syverson.A Taxonomy of Reply Attack.In Proceedings of the 1994 IEEE Computer Security Foundations Workshop.IEEE Computer Society Press,1994.187-191
[129]R.C.Neuman and S.G..Stubblebine.A Note on the Use of Timestamps as Nonces.Operating System Review,1993.27(2):10-14
[130]C.Bodei,M.Buchholtz,P Degano,R Nielson etc.Nielson.Automatic Validation of Protocol Narration.In Proceedings of the 16th computer security foundations workshop.IEEE computer society press,2003.126-140
[131]Emina Torlak,Marten van Dijk,Blaise Gassend,etc.Knowledge Flow Analysis for Security Protocols.Computer Science and Artificial Intelligence Laboratory,August 8,2005
[132]Mikael Buchholtz,Hanne Riis Nielson,Flemming Nielson.A Calculus for Control Flow Analysis of Security Protocols.Information Society Technology program of the European Commisssion.2004
[133]卿斯汉,李改成.公平交换协议的一个形式化模型.中国科学(E辑),2005,35(2):161-172
[134]James Heather,Gavin Lowe,and Steve Schneider.How to Prevent Type Flaw Attacks on Security Protocols.In:Proceedings of 13th IEEE Computer Security Foundations Workshop.2000.255-268
[135]James Heather,Gavin Lowe,Steve Schneider.How to prevent type flaw attacks on security protocols.Journal of Computer Security,2003.11(2)
[136]P.J Broadfoot and A.W.Roscoe.Internalising agents in CSP protocol models.Workshop on Issues in the Theory of Security(WITS'02).Protland Oregon,USA.2002
[137]Giampaolo Bella,Fabio Massacci and L.C.Paulson.An overview of the verification of SET.International Journal of Information Security,2005,4:17-28
[138]苏开乐,岳伟亚 等.实例化空间:一种新的安全协议验证逻辑的语义模型.计算机学报,2006,29(9):1657-1665
[139]Scott D.Stoller and Fred B.Schneider.Automated Analysis of Fault-Tolerance in Distributed Systems.Formal Methods in System Design,2005,26(2):183-196
[140]N.Li and J.C.Mitchell.Understanding SPKI/SDSI Using First-Order Logic.IEEE Computer Security Foundations Workshop.Pacific Grove,California,2003.89-103
[141]Joshua D.Guttman,F.Javier Thayer.Protocol Independence through Disjoint Eneryption.In:Proceedings of the 13th IEEE Computer Security Foundations Workshop(CSFW'00).2000.03-05
[142]毛晨晓,罗文坚,王熙法.分析安全协议猜测攻击的模态逻辑方法.计算机学报,2007,30(6):924-933
[143]F Butler,I Cervesato,A Jaggard,and A Scedrov.A formal analysis of some properties of Kerberos V using MSR.In:Proc of the 15~(th) Computer Security Foundations Workshop.IEEE Computer Society Press,2002
[144]B.Blanchet,M.Abadi,C.Fournet.Automated verification of selected equivalences for security protocols.In:20th IEEE Symposium on Logic in Computer Science.June 2005.331-340
[145]侯峻峰,张磊,黄连生.一种新的安全协议形式化验证方法.计算机研究与发 展,2004,41(8):1415-1420
[146]乔海燕.安全协议验证的归纳方法与串空间形式化比较.计算机研究与发展,2008,45:137-142
[147]胡成军,郑援,沈昌祥.密码协议的秘密性证明.计算机学报,2003,26(3):1-6
[148]Durgin N.,Mitchell J.,Pavlovic D.A compositional logic for proving security properties of protocols.Journal of Computer Security,2003,11(4):677-721
[149]Joshua D Guttman.Security Protocol Design Via Authentication Tests.In:Proc of the 15th Computer Security Foundations Workshop.IEEE Computer Society Press,2002
[150]J C Herzog.The Diffie-Hellman Key Agreement Scheme in the Strand Space Model.In:Proc of 16th IEEE Computer Security Foundations Workshop.IEEE CS Press,2003
[151]Boreale M,Buscemi M.Experimenting with STA,a tool for automatic analysis of security protocols.In:Proc of the 2002 ACM Symposium on Applied Computing.Madrid,Spain,2002.281-285
[152]Huanbao Wang,Yousheng Zhang,and Yuan Li.Structural Control Operators for Composing Diagrams of Strand Spaces of Concurrent Cryptographic Protocols.In:Proc of WCICA2006.2006
[153]J.Borgstrom,S.Briais,U.Nestmann.Symbolic Bisimulation in the Spi Calculus.In CONCUR 2004,vol3170 of LNCS,Springer,Aug.2004.161-176
[154]李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述.计算机研究与发展,2004,41(7):1097-1103
[155]薛锐,冯登国.安全协议的形式化分析技术与方法.计算机学报,2006,29(1):1-20
[156]冯登国,陈伟东.基于口令的安全协议的模块化设计与分析.中国科学 E辑:信息科学,2007,37(2):223-237