安全协议形式化分析中认证测试方法的研究
|
摘要
安全协议是安全共享网络资源的机制和规范，是构建网络安全环境的基石，其安全性对整个网络环境的安全起着至关重要的作用。由于协议安全属性的多样性和微妙性、攻击者模型的不确定性、协议运行环境的复杂性和协议会话的高并发性，安全协议的设计与分析至今仍是一项具有挑战性的工作。形式化方法的出现有助于精确定义安全协议的目标，准确描述安全协议的行为，验证安全协议是否满足预期目标。人们在安全协议的形式化分析上研究探索了近三十年，但这个领域仍然远未成熟。串空间理论的出现将安全协议形式化分析推向了一个新的高度，它以简洁、严谨、高效的特点成为近年来安全协议形式化领域的研究热点。在串空间理论上发展起来的认证测试方法以挑战-应答机制为基础，它充分利用串空间理论中代表事件因果关系的偏序结构，不仅继承了传统串空间模型简单直观、状态空间少的优点，还简化了证明过程，更符合安全协议形式化分析的发展方向。
本文以认证测试方法在协议形式化分析和协议辅助设计中的应用、认证测试理论的扩展和改进，基于认证测试的协议自动化分析算法的设计与实现为主要内容，进行了系统深入的研究，取得了如下创新性成果：
1．从协议分析的角度考虑对协议安全构成威胁的攻击类型和攻击者行为，着重对最为常见的攻击形式——重放攻击进行了分类研究。指出了Syverson重放攻击分类法的不足，按攻击产生的原因将重放攻击分成了五类，针对每个类别列出具体的攻击实例，并提出抵御该类攻击的原则性方法。这种新的重放攻击分类法对于更好地认识各种攻击的原理及寻找有效解决措施具有积极的意义。
2．分别使用串空间最小元素方法、理想诚实方法和认证测试方法对Otway-Rees协议进行分析，总结了这三种方法进行协议分析的过程和特点，指出认证测试方法是前两者的归纳与概括，是理论上的进一步深入，其证明过程更简洁高效。使用认证测试方法对X．509三消息协议进行保密性和认证性分析，指出该协议存在的问题及可能受到的攻击；对协议加以改进，并使用认证测试方法证明了改进协议的正确性。
3．结合协议设计一般原则和J．D．Guttman的协议设计思想，阐述了将认证测试方法用于辅助协议设计的可行性，提出了基于认证测试的通用协议设计思想。将协议设计过程分解为五个步骤，详细讨论了对称密钥体制和不对称密钥体制下构造认证测试的方法。并使用该方法设计了一个新的双向认证密钥协商协议，扩展了认证测试方法的应用范围。
4．将基于认证测试的安全协议形式化分析过程标准化，解决了“认证测试方法的证明过程过于依赖分析人员的主观判断”和“认证测试元素出现位置可能不唯一”的问题，使得认证测试的应用过程更严谨规范，有利于自动化分析工具的实现。使用标准化方法对BAN-Yahalom协议进行分析，找到了针对该协议的一个已知攻击的更普遍形式。
5．分析了认证测试方法中“测试元素不能是任何常规结点消息组成元素的真子项”这一局限性产生的根本原因，指出了Perrig和Song改进方案的漏洞，提出的新认证测试理论有效突破了认证测试定理无法分析多重加密协议的局限性，并通过理论证明和实例分析说明了新认证测试定理的正确性，进一步扩展了认证测试方法的应用范围。
6．针对“认证测试理论不能识别类型缺陷攻击”的不足，结合强制类型检查思想，将消息项的类型和检查机制引入认证测试方法，使得认证测试方法可以根据应用需求检测出不同层次的类型缺陷攻击。并以Otway-Rees、Andrew RPC和Woo-Lam改进协议的分析为例，确认了这一改进的成功。
7．根据认证测试理论的上述三点改进，模拟手工证明过程，设计了一个基于认证测试的协议自动化分析算法ATAPA并进行了初步实现。该算法利用串空间理论和认证测试方法的思想，有效避免了传统自动化分析工具的状态空间爆炸问题，同时能获得较高的分析效率。使用ATAPA算法对NSL协议、Woo-Lam改进协议的认证属性进行分析，得到了与目标一致的结论，一方面证明了协议自动化分析算法的成功，另一方面也验证了改进认证测试理论的正确性。
Security protocols are designed for communication over insecure network. Security protocols work as core components of network security, so their correctness is crucial to network security. The designing and analyzing of security protocols remains a challenge for the subtlety of security goals, the uncertainty of penetrator model, the complexity of the running environment, and the high concurrency of protocol sessions. Formal methods contribute to define security goal of protocols precisely, describe behavior of protocol accurately, and verify whether the protocol meet the target correctly. Through nearly three decades of development, formal analysis of security protocols is immature yet. The emergence of strand space theory sets off a new upsurge of security protocols formal analysis. Strand space theory attracts sights of researchers soon for its compact model, precise definition and efficient proof. Authentication test based upon challenge-response mechanism is a novel method derived from strand space theory. It inherits advantages of strand space, simplifies proving process further, and provides more powerful analysis capabilities on authentication properties.
This thesis makes an in-depth study of authentication test's application in analyzing and designing of security protocols, expands authentication test theory in three aspects, and then designs an automatic protocol verification algorithm based on enhanced authentication test. Related efforts result in following major innovative achievements:
1. Taxonomic study of replay attacks which may do great harm to security of protocols. Proposed a new classification method based on the underlying reasons for success of attacks. For each category, examples of successful attacks are listed and the methods against those attacks in principle are presented.
2. Minimal-element method, ideal-honest method and authentication test method are separately used to verify secrecy and agreement properties of Otway-Rees protocol, followed by summarizing the characteristics of each method through comparison. It shows that authentication test is the most concise and efficient one for protocol analysis. As a case study, secrecy and agreement properties of X.509, an asymmetric key protocol, are verified, then found and amended the flaws in it.
3. Applied authentication test to auxiliary protocol designing. Described the thought and procedure of designing protocols in terms of authentication test from standpoint of protocol analysis. Especially discussed the difference in constructing authentication test under symmetric-key and asymmetric-key cryptography. Designed a new mutual authentication protocol with key negotiation using that approach.
4. Standardized the proving process of protocols' security attributes with authentication test to make it more rigorous, formal and easy to implement in automatic tools. BAN-Yahalom is analyzed with the standardized proving method, and found a normal form of an attack to it.
5. Illustrated the essential cause of limitation of authentication test, that test component cannot occurs as proper subterm of other component. Pointed out the deficiency in Perrig and Song's authentication test version, then proposed the improved authentication test and proved its soundness both in formal and case study.
6. With the idea of forced type checkage, defined different types for terms in messages, designed the inspection rules of authentication test method, so as to detect type-flaw-attacks on different levels according to application requirements. Confirmed the effectiveness of our improvements by analyzing Otway-Rees, Andrew RPC and Woo-Lam protocols.
7. Imitating the manual proving process, designed an automatic protocol verification algorithm ATAPA based on improved authentication test theory mentioned above. With the programming implementation of the algorithm, verified the attributes of NSL and Woo-Lam protocols. Proved the soundness of both the algorithm and the improved authentication test theory.
本文以认证测试方法在协议形式化分析和协议辅助设计中的应用、认证测试理论的扩展和改进，基于认证测试的协议自动化分析算法的设计与实现为主要内容，进行了系统深入的研究，取得了如下创新性成果：
1．从协议分析的角度考虑对协议安全构成威胁的攻击类型和攻击者行为，着重对最为常见的攻击形式——重放攻击进行了分类研究。指出了Syverson重放攻击分类法的不足，按攻击产生的原因将重放攻击分成了五类，针对每个类别列出具体的攻击实例，并提出抵御该类攻击的原则性方法。这种新的重放攻击分类法对于更好地认识各种攻击的原理及寻找有效解决措施具有积极的意义。
2．分别使用串空间最小元素方法、理想诚实方法和认证测试方法对Otway-Rees协议进行分析，总结了这三种方法进行协议分析的过程和特点，指出认证测试方法是前两者的归纳与概括，是理论上的进一步深入，其证明过程更简洁高效。使用认证测试方法对X．509三消息协议进行保密性和认证性分析，指出该协议存在的问题及可能受到的攻击；对协议加以改进，并使用认证测试方法证明了改进协议的正确性。
3．结合协议设计一般原则和J．D．Guttman的协议设计思想，阐述了将认证测试方法用于辅助协议设计的可行性，提出了基于认证测试的通用协议设计思想。将协议设计过程分解为五个步骤，详细讨论了对称密钥体制和不对称密钥体制下构造认证测试的方法。并使用该方法设计了一个新的双向认证密钥协商协议，扩展了认证测试方法的应用范围。
4．将基于认证测试的安全协议形式化分析过程标准化，解决了“认证测试方法的证明过程过于依赖分析人员的主观判断”和“认证测试元素出现位置可能不唯一”的问题，使得认证测试的应用过程更严谨规范，有利于自动化分析工具的实现。使用标准化方法对BAN-Yahalom协议进行分析，找到了针对该协议的一个已知攻击的更普遍形式。
5．分析了认证测试方法中“测试元素不能是任何常规结点消息组成元素的真子项”这一局限性产生的根本原因，指出了Perrig和Song改进方案的漏洞，提出的新认证测试理论有效突破了认证测试定理无法分析多重加密协议的局限性，并通过理论证明和实例分析说明了新认证测试定理的正确性，进一步扩展了认证测试方法的应用范围。
6．针对“认证测试理论不能识别类型缺陷攻击”的不足，结合强制类型检查思想，将消息项的类型和检查机制引入认证测试方法，使得认证测试方法可以根据应用需求检测出不同层次的类型缺陷攻击。并以Otway-Rees、Andrew RPC和Woo-Lam改进协议的分析为例，确认了这一改进的成功。
7．根据认证测试理论的上述三点改进，模拟手工证明过程，设计了一个基于认证测试的协议自动化分析算法ATAPA并进行了初步实现。该算法利用串空间理论和认证测试方法的思想，有效避免了传统自动化分析工具的状态空间爆炸问题，同时能获得较高的分析效率。使用ATAPA算法对NSL协议、Woo-Lam改进协议的认证属性进行分析，得到了与目标一致的结论，一方面证明了协议自动化分析算法的成功，另一方面也验证了改进认证测试理论的正确性。
Security protocols are designed for communication over insecure network. Security protocols work as core components of network security, so their correctness is crucial to network security. The designing and analyzing of security protocols remains a challenge for the subtlety of security goals, the uncertainty of penetrator model, the complexity of the running environment, and the high concurrency of protocol sessions. Formal methods contribute to define security goal of protocols precisely, describe behavior of protocol accurately, and verify whether the protocol meet the target correctly. Through nearly three decades of development, formal analysis of security protocols is immature yet. The emergence of strand space theory sets off a new upsurge of security protocols formal analysis. Strand space theory attracts sights of researchers soon for its compact model, precise definition and efficient proof. Authentication test based upon challenge-response mechanism is a novel method derived from strand space theory. It inherits advantages of strand space, simplifies proving process further, and provides more powerful analysis capabilities on authentication properties.
This thesis makes an in-depth study of authentication test's application in analyzing and designing of security protocols, expands authentication test theory in three aspects, and then designs an automatic protocol verification algorithm based on enhanced authentication test. Related efforts result in following major innovative achievements:
1. Taxonomic study of replay attacks which may do great harm to security of protocols. Proposed a new classification method based on the underlying reasons for success of attacks. For each category, examples of successful attacks are listed and the methods against those attacks in principle are presented.
2. Minimal-element method, ideal-honest method and authentication test method are separately used to verify secrecy and agreement properties of Otway-Rees protocol, followed by summarizing the characteristics of each method through comparison. It shows that authentication test is the most concise and efficient one for protocol analysis. As a case study, secrecy and agreement properties of X.509, an asymmetric key protocol, are verified, then found and amended the flaws in it.
3. Applied authentication test to auxiliary protocol designing. Described the thought and procedure of designing protocols in terms of authentication test from standpoint of protocol analysis. Especially discussed the difference in constructing authentication test under symmetric-key and asymmetric-key cryptography. Designed a new mutual authentication protocol with key negotiation using that approach.
4. Standardized the proving process of protocols' security attributes with authentication test to make it more rigorous, formal and easy to implement in automatic tools. BAN-Yahalom is analyzed with the standardized proving method, and found a normal form of an attack to it.
5. Illustrated the essential cause of limitation of authentication test, that test component cannot occurs as proper subterm of other component. Pointed out the deficiency in Perrig and Song's authentication test version, then proposed the improved authentication test and proved its soundness both in formal and case study.
6. With the idea of forced type checkage, defined different types for terms in messages, designed the inspection rules of authentication test method, so as to detect type-flaw-attacks on different levels according to application requirements. Confirmed the effectiveness of our improvements by analyzing Otway-Rees, Andrew RPC and Woo-Lam protocols.
7. Imitating the manual proving process, designed an automatic protocol verification algorithm ATAPA based on improved authentication test theory mentioned above. With the programming implementation of the algorithm, verified the attributes of NSL and Woo-Lam protocols. Proved the soundness of both the algorithm and the improved authentication test theory.
引文
[1] Needham R, Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM,1978,21 (12): 993-999.
[2] Meadows C. Formal verification of cryptographic protocols: A survey. In: Proc of Advances in Cryptology. Berlin: Springer-Verlag, 1996, 135-150.
[3] Dolev D, Yao A. On the security of public-key protocols. IEEE Transactions on Information Theory, 1983,8(29): 198-208.
[4] Marrero W, Clarke E, Somesh J. A Model Checker for Authentication Protocols. In: Proc of DIMACS Workshop on Cryptographic Protocol Design and Verification, New Jersey: Rutgers Press, 1997, 147-166.
[5] Kailar R. Accountability in Electronic Commerce Protocols. IEEE Transactions on Software Engineering ,1996 ,22 (5) :313-328
[6] Maria F. Reasoning about Knowledge and Belief: A Syntactical Treatment. Logic Journal of the IGPL.2003. 11(2):245-282
[7] Syverson P. Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Computer Security, 1992,1(3): 317-334.
[8] Automated Validation of Internet Security Protocols and Applications. FET Open Project IST-2001-39252[EB/OL]. 2005. http://www.avispa-project.org
[9] Meadows C. The NRL protocol analyzer: An overview. Journal of Logic Programming, 1996,26(2): 113-131.
[10] Meadows C. Analysis of the Internet Key Exchange Protocol using the NRL Protocol Analyzer. In: Proceedings of the 1999 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press,1999:84-89
[11] Hoare C. Communicating sequential processes. New Jersey: Prentice Hall International Series in Computer Science, 1985
[12] Formal Systems(Europe) Ltd. Failure Divergence Refinement Users Manual and Tutorial. 1994
[13] Formal Systems(Europe) Ltd. Failure Divergence Refinement-FDR2 Users Manual. 2005
[14] Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools, 1996,17(3): 93-102
[15] Lowe G. Casper: A Compiler for the Analysis of Security Protocols. In: Proc of 10th IEEE Computer Security Foundations Workshop, Los Alamitos: IEEE Computer Society Press, 1997, 18-30
[16] Millen J, Clark S, Freedman S. The Interrogator: Protocol Security Analysis. IEEE Transactions on Software Engineering, 1987,12(2): 274-288
[17] Burrows M, Abadi M, Needham R. A logic of authentication. Research Report 39, ACM Transactions on Computer Systems,1989,8(1),18-36
[18] Gong L, Needham R, Yahalom R. Reasoning about Belief in Cryptographic Protocols. In: Proc of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos, California : IEEE Computer Society Press, 1990, 234-248
[19] Paul C, Van O. Extending Cryptographic Logics of Belief to Key Agreement Protocols. In: Proc of the 1st ACM Conference on Communications and Computer Security. Virginia: ACM Press, 1993,233-243
[20] Syverson P, Oorschot P. On Unifying Some Cryptographic Protocol Logics. In: Proc of the IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994, 14-28
[21] Abadi M, Tuttle M R. A Semantics for a Logic of Authentication. In: Proc of the Tenth ACM Symposium on Principles of Distributed Computing. Canada: ACM Press, 1991,201-216
[22] Nessett D M. A Critique of the Burrows, Abadi and Needham Logic. ACM Operating Systems Review, 1990,24(2):35-38.
[23] Abadi M, Gordon AD. A Calculus for Cryptographic Protocols: The Spi Calculus. In: Proc of the 4th ACM Conference on Computer and Communications Security. New York: ACM Press 1997,36-47.
[24] Milner R, Parrow J, Walker D. A Calculus of Mobile Processes Part Ⅰ/Ⅱ. Information and Computation, 1992,100(1):1-77.
[25] Amadio R, Prasad S. The Game of the Name in Cryptographic Tables. In: Proc of the Asian Computing Science Conference. Berlin: Springer-Verlag, 1999, 15-26.
[26] Amadio R, Lugiez D. On the reachability problem in cryptographic protocols. In: Proc of the 11th International Conference on Concurrency Theory. Pennsylvania: LNCS Springer, 2000, 380-394.
[27] Abadi M, Blanchet B. Secrecy Types for Asymmetric Communication. In: Proc of Foundations of the Software Science and Computation Structures. Italy: Springer-Verlag, 2001,25-41.
[28] Paulson LC. Proving Properties of Security Protocols by Induction. In: Proc of the 10th IEEE Computer Security Foundations Workshop. Massachusetts: IEEE Computer Society Press, 1997,70-83,
[29] Schneider S. Verifying Authentication Protocols with CSP. In: Proc of the 10th IEEE Computer Security Foundations Work shop. Massachusetts: IEEE Computer Society Press, 1997,3-17
[30] Thayer FJ, Herzog JC, Guttman JD. Strand Space: Why is a Security Protocol Correct. In: Proc of 1998 IEEE Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998,160-171
[31] Thayer FJ, Herzog JC, Guttman JD. Strand Space: Proving Security Protocols Correct. Journal of Computer Security, 1999,7(2-3): 191-230
[32] Maneki A. Honest Functions and Their Application to the Analysis of Cryptographic Protocols. In: Proc of the 12th IEEE Computer Security Foundations Workshop. Mordano, Italy: IEEE Computer Society Press, 1993, 83-89
[33] Song D. Athena: A New Efficient Automatic Checker For Security Protocol Analysis. In: Proc of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999,192-202
[34] Song D, Berezin S, Perrig A. Athena: a Novel Approach to Efficient Automatic Security Protocol Analysis. Journal of Computer Security, 2001,9(1): 47-74
[35] Guttman JD, Thayer FJ. Authentication Tests and the Structure of Bundles. Theoretical Computer Science. 2002,283(2):333-380
[36] Guttman JD. Security Protocol Design via Authentication Tests. In: Proc of the 2002 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 2002, 92-103
[37] Thayer FJ, Herzog JC, Guttman J D. Mixed Strand Spaces. In: Proc of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999, 72-82
[38] Guttman JD, Thayer F J. Protocol Independence through Disjoint Encryption. In: Proc of the 13th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 2000. 24-34
[39] Syverson P. Towards a Strand Semantics for Authentication Logic. Electronic Notes in Theoretical Computer Science,2000,20(1): 62-72
[40]Crazzolara F,Winskel G.Composing Strand Space.BRICS Report Series.UK:University of Cambridge,2002
[41]Robin S,Hansen MR.Timed Traces and Strand Spaces.In:Proc of 2nd International Symposium on Computer Science.Russia:Computer Society Press,2007,373-386
[42]Bond M,Clulow J.Extending Security Protocol Analysis:New Challenges.Electronic Notes in Theoretical Computer Science.2005,125(1):13-24
[43]Perrig A and Song D.A First Step towards the Automatic Generation of Security Protocols.In:Proc of Symposium on Network and Distributed Systems Security,San Diego:Internet Society Press,2000,73-83
[44]Song D,Perrig A,Phan D.AGVI-Automatic Generation,Verification,and Implementation of Security Protocols.In:Proc of 13th Conference on Computer Aided Verification,London,UK:Springer-Verlag,2001,241-245
[45]Perrig A,Song D.Looking for Diamonds in the Desert-Extending Automatic Protocol Generation to Three-party Authentication and Key Agreement Protocols.In:Proc of the 13th IEEE Computer Security Foundations Workshop,Los Alamitos:IEEE Computer Society Press,2000,64-76
[46]Song D.An Automatic Approach for Building Secure Systems.[Doctoral Dissertation].Berkeley:University of California at Berkeley,2002
[47]卿斯汉．密码学与计算机网络安全．北京：清华大学出版社，2000．
[48]卿斯汉．安全协议．北京：清华大学出版社．2005
[49]范红，冯登国．安全协议理论与方法．北京：科学出版社．2003
[50]范红，冯登国．安全协议形式化分析的研究现状及有关问题．网络安全与应用，2001(8)：12-15
[51]范红，冯登国，邹良惠．安全协议形式化分析方法综述之一．网络安全与应用，2003(5)：52-56
[52]范红，冯登国，邹良惠．安全协议形式化分析方法综述之二．网络安全与应用，2003(6)：15-18
[53]卿斯汉．安全协议的设计与逻辑分析．软件学报，2003，14(7)：1300-1309
[54]卿斯汉．认证协议两种形式化分析方法的比较．软件学报，2003，14(12)：2028-2036
[55]冯登国．可证明安全性理论与方法研究．软件学报，2005，16(10)：1743-1756
[56]Ji QG,Qing SH,Zhou YB,Feng DG.Study on strand space model theory.Journal of Computer Science and Technology,2003,18(5):553-570
[57]华东明．安全协议的形式化方法及其应用的研究：[博士论文]．北京：中国科学院计算技术研究所，2005
[58]Li Y J,Jun P.Extending the Strand Space Method to Verify Kerberos V.In:Proc of the Eighth International Conference on Parallel and Distributed Computing,Applications and Technologies.Australia:IEEE Computer Society Press,2007,437-444
[59]李谢华．基于串空间模型的安全协议形式化验证方法的研究：[博士论文]．上海：上海交通大学，2007
[60]刘璟．密码协议的形式化分析方法研究：[博士后研究工作报告]．成都：电子科技大学．2005
[61]信息安全国家重点实验室．安全协议研讨会文集．北京：信息安全国家重点实验室．2007
[62]Schneier B．应用密码学—协议，算法与C源程序，吴世忠译．北京：机械工业出版社，2001
[63]Otway D,Rees O.Efficient and Timely Mutual Authentication.Operating Systems Review.1987,21(1):8-10
[64]Woo TY,Lain SS.A Lesson on Authentication Protocol Design.Operating Systems Review.1994,28(3):24-37
[65]Denning D,Sacco G.Timestamps in Key Distribution Protocols.Communications of the ACM,1981,24(8):523-536
[66]Neuman BC,Stubblebine SG.A Note on the Use of Timestamps as Nonces.Operating Systems Review.1993,27(2):10-14
[67]Gollmann D.What Do We Mean by Entity Authentication.In:Proc of the IEEE Symposium on Security and Privacy.Los Alamitos:IEEE Computer Society Press,1996,46-54.
[68]Lowe G.A Hierarchy of Authentication Specifications.In:Proc of the 10th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,1997,31-43
[69]Gong L.Cryptographic Protocols for Distributed Systems:PHD thesis.Cambridge:Jesus College of University of Cambridge,1990
[70]Thayer FJ,Herzog JC,Guttman JD.Honest Ideals on Strand Spaces.In:Proc of 11th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,1998,66-77
[71]Carlsen U.Cryptographic Protocol Flaws.In:Proc of7th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society,1994,192-200
[72]Gong L,Mark T,Lomas A,et al.Protecting Poorly Chosen Secrets From Guessing Attacks.IEEE Journal on Selected Areas in Communications,1993,11(5):648-656
[73]Xu C,Kedem G,Gong F.Categorizing Attacks on Cryptographic Protocols Based on Intruder's Objectives and Roles.In:Proc of the Workshop on Formal Methods and Computer Security,Chicago:Springer-Verlag,2000,http://www.cs.duke.edu/～chong/papers/fmcs2000.ps
[74]Paul Syverson.A Taxonomy of Replay Attacks.In:Proc of the 7th IEEE Computer Security Foundations Workshop,Los Alamitos:IEEE Computer Society Press,1994,187-191
[75]Abadi M,Needham R.Prudent Engineering Practice for Cryptographic Protocols.IEEE Transactions on Software Engineering,1996,22(1):6-15
[76]Benjamin WL.Formal Verification of Type Flaw Attacks in Security Protocols.In:Proc of the 10th Asia-Pacific Software Engineering Conference,Thailand:IEEE Computer Society Press,2003,415-424
[77]Heather J,Lowe G,Schneider S.How to Prevent Type Flaw Attacks on Security Protocols.In:Proc of the 13th Computer Security Foundations Workshop,Los Alamitos:IEEE Computer Society,2000,255-268.
[78]Meadows C.Identifying Potential Type Confusion in Authenticated Messages.In:Proc of Workshop on Foundation of Computer Security,Denmark:IEEE Computer Society Press,2002,75-84
[79]Meadows C.A Procedure for Verifying Security against Type Confusion Attacks.In:Proc of the 16th IEEE Computer Security Foundations Workshop,Los Alamitos:IEEE Computer Society Press,2003,62-72
[80]王贵林，卿斯汉，周展飞．认证协议的一些新攻击方法．软件学报,2001，12(6)：907-913
[81]林贤金，胡山立．认证协议攻击与非形式化分析．小型微型计算机系统，2003，24(11)：1912-1915
[82]卓继亮，李先贤，李建欣等．安全协议的攻击分类及其安全型评估．计算机研究与发展．2005，42(7)：1100-1107
[83]CCITT.CCITT draft recommendation X.509.The directory-authentication framework,version 7.Gloucester:CCITT,1987
[84]Anson C,Mitchell C.Security Defects in the CCITT Recommendation X.509-The Directory Authentication Framework.Computer Communication Review.1990,20(2):30-34
[85]Lowe G.An Attack on the Needham-Schroeder Public-Key Authentication Protocol.Information Processing Letters.1995,56(3):131-136
[86]John AC,Jeremy J.A Survey of Authentication Protocol Literature:[Technical Report],Heslington York:University of York,1997
[87]Mitchell C.Limitations of Challenge-Response Entity Authentication.Electronic Letters,1989,25(17):1195-1196
[88]Otway D,Rees O.Efficient and Timely Mutual Authentication.ACM Operating Systems Review,1997:21(1):8-10
[89]Lowe G.A Family of Attacks upon Authentication Protocols:[Technical Report],1997,Leicester UK:University of Leicester,1997
[90]Meadow C.Open Issues in Formal Methods for Cryptographic protocol analysis.In:Proc of the 16th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,2003,237-250
[91]Lowe G.Some New Attacks upon Security Protocols.In:Proc of the 9th Computer Security Foundations Workshop.Ireland:IEEE Computer Society Press,1996,162-169
[92]Boyd C,Man Wenbo.On a Limitation of BAN Logic.In:Advances in Cryptology-EUROCRYPT 93,Berlin:Springer-Vedag,1993,240-247
[93]Thayer FJ,Herzog JC,Guttman JD.Mixed Strand Spaces.In:Proc of the 12th IEEE Computer Security Foundations Workshop,Italy:IEEE Computer Society Press,1999,10-14
[94]Kelsey J,Schneier B,Wagner D.Protocol Interactions and the Chosen Protocol Attack.In:Proc of 5th International Workshop on Security Protocols,London:Springer-Verlag,1997,91-104
[95]Guttman JD,Thayer FJ.Protocol Independence through Disjoint Encryption.In:Proc of 13th IEEE Computer Security Foundations Workshop,Washington DC:IEEE Computer Society Press,2000,24-34
[96]Jime AF.Multi-Protocol Attacks and the Public Key Infrastructure.In:Proc of the 21 st National Information System Security Conference,Virginia:National Academy Press,1998,566-576
[97]Aura T.Strategies Against Replay Attacks.In:Proc of the 10th IEEE Computer Society Foundations Workshop,Massachusetts:IEEE Computer Society Press.1997,59-68
[98]蒋睿，李建华，潘理．基于Strand Space模型的X．509协议分析．上海交通大学学报．2004，38(z1)：169-173
[99]Heintze N,Tygar JD.A Model for Secure Protocols and Their Composition.IEEE Transactions on Software Engineering,1996,22(1):16-30.
[103]周永彬．PKI理论与应用技术研究：[博士学位论文]．北京：中国科学院研究生院，2003．
[104]Rui J,Li P,Jianhua L.Further Analysis of Password Authentication Schemes Based on Authentication Tests.Computer & Security,2004,(23):469-477
[105]Xiehua L,Liming H,Shutang Y,et al.Formal Verification of EAP-AKA with Improved Authentication Tests.In:Proc of International Conference on Wireless Communications,Networking and Mobile Computing.Wuhan:IEEE Computer Society Press.2006,1-4
[106]Jiafen L,Mingtian Z.Designing Authentication Protocols via Authentication Test.In:Proc of IEEE Symposium on Computers and Communications,Aveiro Portugal:IEEE Computer Society Press,2007,475-480
[107]蒋睿，胡爱群，李建华．基于Authentication Test方法的高效安全IKE形式化设计研究．计算机学报，2006，29(9)：1692-1699
[108]Doghmi SF,Guttman JD,Thayer FJ.Completeness of the Authentication Test In:Proc of the 12th European Symposium on Research in Computer Security,Washington DC:IEEE Computer Society Press,2007,106-121
[109]杨明，罗军周．基于认证测试的安全协议分析，软件学报．2006，17(1)：148-156
[110]Xiangdong L,Qingxian W.An Improvement of Authentication Test for Security Protocol Analysis.In:Proc of the 20th IEEE International Conference on Micro Electro Mechanical Systems,2007,745-748
[111]Yongjian L,Jun P.Generalized Unsolicited Tests for Authentication Protocol Analysis.In:Proc of the 7th International Conference on Parallel and Distributed Computing,Applications and Technologies,Taipei:IEEE Computer Society Press,2006,509-514
[112]Sigrid G.A Formal Analysis Technique for Authentication Protocols.In:Proceedings of the 5th International Workshop on Security Protocols.London,UK:Springer-Verlag,1997,159-176.
[113]李谢华，杨树堂．基于消息类型检测的认证测试分析方法．上海交通大学学报．2007，41(1)：85-89
[114]Burrows M,Abadi M,Needham R.A logic of authentication.ACM Transaction on Computer Systems,1990,8(1):18-36.
[115]Perrig A,Song D.Looking For Diamonds in the Desert-Extending Automatic Protocol Generation to Three-Party Authentication and Key Agreement.In:Proc of the 13th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,2000,64-76
[116]周宏斌，黄连生，桑田．基于串空间的安全协议形式化验证模型及算法．计算机研究与发展，2003，40(2)：251-257
[117]刘东喜，安全协议的自动化验证技术研究：[学位论文]，上海：上海交通大学，2002
[118] Furqan, Z, Muhammad S,Guha RK. Formal Verification of 802.l 1i Using Strand Space Formalism. In: Proc of International Conference on Systems and International Conference on Mobile Communications and Learning Technologies, Washington DC:IEEE Computer Society Press,2006, 83-86
[119] Parka HS, Leeb HS, Leec DH, et al. Multi-Protocol Authentication for SIP/SS7 Mobile Network, Computer Communications,2008,31(1): 2755-2763
[2] Meadows C. Formal verification of cryptographic protocols: A survey. In: Proc of Advances in Cryptology. Berlin: Springer-Verlag, 1996, 135-150.
[3] Dolev D, Yao A. On the security of public-key protocols. IEEE Transactions on Information Theory, 1983,8(29): 198-208.
[4] Marrero W, Clarke E, Somesh J. A Model Checker for Authentication Protocols. In: Proc of DIMACS Workshop on Cryptographic Protocol Design and Verification, New Jersey: Rutgers Press, 1997, 147-166.
[5] Kailar R. Accountability in Electronic Commerce Protocols. IEEE Transactions on Software Engineering ,1996 ,22 (5) :313-328
[6] Maria F. Reasoning about Knowledge and Belief: A Syntactical Treatment. Logic Journal of the IGPL.2003. 11(2):245-282
[7] Syverson P. Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Computer Security, 1992,1(3): 317-334.
[8] Automated Validation of Internet Security Protocols and Applications. FET Open Project IST-2001-39252[EB/OL]. 2005. http://www.avispa-project.org
[9] Meadows C. The NRL protocol analyzer: An overview. Journal of Logic Programming, 1996,26(2): 113-131.
[10] Meadows C. Analysis of the Internet Key Exchange Protocol using the NRL Protocol Analyzer. In: Proceedings of the 1999 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press,1999:84-89
[11] Hoare C. Communicating sequential processes. New Jersey: Prentice Hall International Series in Computer Science, 1985
[12] Formal Systems(Europe) Ltd. Failure Divergence Refinement Users Manual and Tutorial. 1994
[13] Formal Systems(Europe) Ltd. Failure Divergence Refinement-FDR2 Users Manual. 2005
[14] Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools, 1996,17(3): 93-102
[15] Lowe G. Casper: A Compiler for the Analysis of Security Protocols. In: Proc of 10th IEEE Computer Security Foundations Workshop, Los Alamitos: IEEE Computer Society Press, 1997, 18-30
[16] Millen J, Clark S, Freedman S. The Interrogator: Protocol Security Analysis. IEEE Transactions on Software Engineering, 1987,12(2): 274-288
[17] Burrows M, Abadi M, Needham R. A logic of authentication. Research Report 39, ACM Transactions on Computer Systems,1989,8(1),18-36
[18] Gong L, Needham R, Yahalom R. Reasoning about Belief in Cryptographic Protocols. In: Proc of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos, California : IEEE Computer Society Press, 1990, 234-248
[19] Paul C, Van O. Extending Cryptographic Logics of Belief to Key Agreement Protocols. In: Proc of the 1st ACM Conference on Communications and Computer Security. Virginia: ACM Press, 1993,233-243
[20] Syverson P, Oorschot P. On Unifying Some Cryptographic Protocol Logics. In: Proc of the IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994, 14-28
[21] Abadi M, Tuttle M R. A Semantics for a Logic of Authentication. In: Proc of the Tenth ACM Symposium on Principles of Distributed Computing. Canada: ACM Press, 1991,201-216
[22] Nessett D M. A Critique of the Burrows, Abadi and Needham Logic. ACM Operating Systems Review, 1990,24(2):35-38.
[23] Abadi M, Gordon AD. A Calculus for Cryptographic Protocols: The Spi Calculus. In: Proc of the 4th ACM Conference on Computer and Communications Security. New York: ACM Press 1997,36-47.
[24] Milner R, Parrow J, Walker D. A Calculus of Mobile Processes Part Ⅰ/Ⅱ. Information and Computation, 1992,100(1):1-77.
[25] Amadio R, Prasad S. The Game of the Name in Cryptographic Tables. In: Proc of the Asian Computing Science Conference. Berlin: Springer-Verlag, 1999, 15-26.
[26] Amadio R, Lugiez D. On the reachability problem in cryptographic protocols. In: Proc of the 11th International Conference on Concurrency Theory. Pennsylvania: LNCS Springer, 2000, 380-394.
[27] Abadi M, Blanchet B. Secrecy Types for Asymmetric Communication. In: Proc of Foundations of the Software Science and Computation Structures. Italy: Springer-Verlag, 2001,25-41.
[28] Paulson LC. Proving Properties of Security Protocols by Induction. In: Proc of the 10th IEEE Computer Security Foundations Workshop. Massachusetts: IEEE Computer Society Press, 1997,70-83,
[29] Schneider S. Verifying Authentication Protocols with CSP. In: Proc of the 10th IEEE Computer Security Foundations Work shop. Massachusetts: IEEE Computer Society Press, 1997,3-17
[30] Thayer FJ, Herzog JC, Guttman JD. Strand Space: Why is a Security Protocol Correct. In: Proc of 1998 IEEE Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998,160-171
[31] Thayer FJ, Herzog JC, Guttman JD. Strand Space: Proving Security Protocols Correct. Journal of Computer Security, 1999,7(2-3): 191-230
[32] Maneki A. Honest Functions and Their Application to the Analysis of Cryptographic Protocols. In: Proc of the 12th IEEE Computer Security Foundations Workshop. Mordano, Italy: IEEE Computer Society Press, 1993, 83-89
[33] Song D. Athena: A New Efficient Automatic Checker For Security Protocol Analysis. In: Proc of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999,192-202
[34] Song D, Berezin S, Perrig A. Athena: a Novel Approach to Efficient Automatic Security Protocol Analysis. Journal of Computer Security, 2001,9(1): 47-74
[35] Guttman JD, Thayer FJ. Authentication Tests and the Structure of Bundles. Theoretical Computer Science. 2002,283(2):333-380
[36] Guttman JD. Security Protocol Design via Authentication Tests. In: Proc of the 2002 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 2002, 92-103
[37] Thayer FJ, Herzog JC, Guttman J D. Mixed Strand Spaces. In: Proc of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999, 72-82
[38] Guttman JD, Thayer F J. Protocol Independence through Disjoint Encryption. In: Proc of the 13th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 2000. 24-34
[39] Syverson P. Towards a Strand Semantics for Authentication Logic. Electronic Notes in Theoretical Computer Science,2000,20(1): 62-72
[40]Crazzolara F,Winskel G.Composing Strand Space.BRICS Report Series.UK:University of Cambridge,2002
[41]Robin S,Hansen MR.Timed Traces and Strand Spaces.In:Proc of 2nd International Symposium on Computer Science.Russia:Computer Society Press,2007,373-386
[42]Bond M,Clulow J.Extending Security Protocol Analysis:New Challenges.Electronic Notes in Theoretical Computer Science.2005,125(1):13-24
[43]Perrig A and Song D.A First Step towards the Automatic Generation of Security Protocols.In:Proc of Symposium on Network and Distributed Systems Security,San Diego:Internet Society Press,2000,73-83
[44]Song D,Perrig A,Phan D.AGVI-Automatic Generation,Verification,and Implementation of Security Protocols.In:Proc of 13th Conference on Computer Aided Verification,London,UK:Springer-Verlag,2001,241-245
[45]Perrig A,Song D.Looking for Diamonds in the Desert-Extending Automatic Protocol Generation to Three-party Authentication and Key Agreement Protocols.In:Proc of the 13th IEEE Computer Security Foundations Workshop,Los Alamitos:IEEE Computer Society Press,2000,64-76
[46]Song D.An Automatic Approach for Building Secure Systems.[Doctoral Dissertation].Berkeley:University of California at Berkeley,2002
[47]卿斯汉．密码学与计算机网络安全．北京：清华大学出版社，2000．
[48]卿斯汉．安全协议．北京：清华大学出版社．2005
[49]范红，冯登国．安全协议理论与方法．北京：科学出版社．2003
[50]范红，冯登国．安全协议形式化分析的研究现状及有关问题．网络安全与应用，2001(8)：12-15
[51]范红，冯登国，邹良惠．安全协议形式化分析方法综述之一．网络安全与应用，2003(5)：52-56
[52]范红，冯登国，邹良惠．安全协议形式化分析方法综述之二．网络安全与应用，2003(6)：15-18
[53]卿斯汉．安全协议的设计与逻辑分析．软件学报，2003，14(7)：1300-1309
[54]卿斯汉．认证协议两种形式化分析方法的比较．软件学报，2003，14(12)：2028-2036
[55]冯登国．可证明安全性理论与方法研究．软件学报，2005，16(10)：1743-1756
[56]Ji QG,Qing SH,Zhou YB,Feng DG.Study on strand space model theory.Journal of Computer Science and Technology,2003,18(5):553-570
[57]华东明．安全协议的形式化方法及其应用的研究：[博士论文]．北京：中国科学院计算技术研究所，2005
[58]Li Y J,Jun P.Extending the Strand Space Method to Verify Kerberos V.In:Proc of the Eighth International Conference on Parallel and Distributed Computing,Applications and Technologies.Australia:IEEE Computer Society Press,2007,437-444
[59]李谢华．基于串空间模型的安全协议形式化验证方法的研究：[博士论文]．上海：上海交通大学，2007
[60]刘璟．密码协议的形式化分析方法研究：[博士后研究工作报告]．成都：电子科技大学．2005
[61]信息安全国家重点实验室．安全协议研讨会文集．北京：信息安全国家重点实验室．2007
[62]Schneier B．应用密码学—协议，算法与C源程序，吴世忠译．北京：机械工业出版社，2001
[63]Otway D,Rees O.Efficient and Timely Mutual Authentication.Operating Systems Review.1987,21(1):8-10
[64]Woo TY,Lain SS.A Lesson on Authentication Protocol Design.Operating Systems Review.1994,28(3):24-37
[65]Denning D,Sacco G.Timestamps in Key Distribution Protocols.Communications of the ACM,1981,24(8):523-536
[66]Neuman BC,Stubblebine SG.A Note on the Use of Timestamps as Nonces.Operating Systems Review.1993,27(2):10-14
[67]Gollmann D.What Do We Mean by Entity Authentication.In:Proc of the IEEE Symposium on Security and Privacy.Los Alamitos:IEEE Computer Society Press,1996,46-54.
[68]Lowe G.A Hierarchy of Authentication Specifications.In:Proc of the 10th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,1997,31-43
[69]Gong L.Cryptographic Protocols for Distributed Systems:PHD thesis.Cambridge:Jesus College of University of Cambridge,1990
[70]Thayer FJ,Herzog JC,Guttman JD.Honest Ideals on Strand Spaces.In:Proc of 11th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,1998,66-77
[71]Carlsen U.Cryptographic Protocol Flaws.In:Proc of7th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society,1994,192-200
[72]Gong L,Mark T,Lomas A,et al.Protecting Poorly Chosen Secrets From Guessing Attacks.IEEE Journal on Selected Areas in Communications,1993,11(5):648-656
[73]Xu C,Kedem G,Gong F.Categorizing Attacks on Cryptographic Protocols Based on Intruder's Objectives and Roles.In:Proc of the Workshop on Formal Methods and Computer Security,Chicago:Springer-Verlag,2000,http://www.cs.duke.edu/～chong/papers/fmcs2000.ps
[74]Paul Syverson.A Taxonomy of Replay Attacks.In:Proc of the 7th IEEE Computer Security Foundations Workshop,Los Alamitos:IEEE Computer Society Press,1994,187-191
[75]Abadi M,Needham R.Prudent Engineering Practice for Cryptographic Protocols.IEEE Transactions on Software Engineering,1996,22(1):6-15
[76]Benjamin WL.Formal Verification of Type Flaw Attacks in Security Protocols.In:Proc of the 10th Asia-Pacific Software Engineering Conference,Thailand:IEEE Computer Society Press,2003,415-424
[77]Heather J,Lowe G,Schneider S.How to Prevent Type Flaw Attacks on Security Protocols.In:Proc of the 13th Computer Security Foundations Workshop,Los Alamitos:IEEE Computer Society,2000,255-268.
[78]Meadows C.Identifying Potential Type Confusion in Authenticated Messages.In:Proc of Workshop on Foundation of Computer Security,Denmark:IEEE Computer Society Press,2002,75-84
[79]Meadows C.A Procedure for Verifying Security against Type Confusion Attacks.In:Proc of the 16th IEEE Computer Security Foundations Workshop,Los Alamitos:IEEE Computer Society Press,2003,62-72
[80]王贵林，卿斯汉，周展飞．认证协议的一些新攻击方法．软件学报,2001，12(6)：907-913
[81]林贤金，胡山立．认证协议攻击与非形式化分析．小型微型计算机系统，2003，24(11)：1912-1915
[82]卓继亮，李先贤，李建欣等．安全协议的攻击分类及其安全型评估．计算机研究与发展．2005，42(7)：1100-1107
[83]CCITT.CCITT draft recommendation X.509.The directory-authentication framework,version 7.Gloucester:CCITT,1987
[84]Anson C,Mitchell C.Security Defects in the CCITT Recommendation X.509-The Directory Authentication Framework.Computer Communication Review.1990,20(2):30-34
[85]Lowe G.An Attack on the Needham-Schroeder Public-Key Authentication Protocol.Information Processing Letters.1995,56(3):131-136
[86]John AC,Jeremy J.A Survey of Authentication Protocol Literature:[Technical Report],Heslington York:University of York,1997
[87]Mitchell C.Limitations of Challenge-Response Entity Authentication.Electronic Letters,1989,25(17):1195-1196
[88]Otway D,Rees O.Efficient and Timely Mutual Authentication.ACM Operating Systems Review,1997:21(1):8-10
[89]Lowe G.A Family of Attacks upon Authentication Protocols:[Technical Report],1997,Leicester UK:University of Leicester,1997
[90]Meadow C.Open Issues in Formal Methods for Cryptographic protocol analysis.In:Proc of the 16th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,2003,237-250
[91]Lowe G.Some New Attacks upon Security Protocols.In:Proc of the 9th Computer Security Foundations Workshop.Ireland:IEEE Computer Society Press,1996,162-169
[92]Boyd C,Man Wenbo.On a Limitation of BAN Logic.In:Advances in Cryptology-EUROCRYPT 93,Berlin:Springer-Vedag,1993,240-247
[93]Thayer FJ,Herzog JC,Guttman JD.Mixed Strand Spaces.In:Proc of the 12th IEEE Computer Security Foundations Workshop,Italy:IEEE Computer Society Press,1999,10-14
[94]Kelsey J,Schneier B,Wagner D.Protocol Interactions and the Chosen Protocol Attack.In:Proc of 5th International Workshop on Security Protocols,London:Springer-Verlag,1997,91-104
[95]Guttman JD,Thayer FJ.Protocol Independence through Disjoint Encryption.In:Proc of 13th IEEE Computer Security Foundations Workshop,Washington DC:IEEE Computer Society Press,2000,24-34
[96]Jime AF.Multi-Protocol Attacks and the Public Key Infrastructure.In:Proc of the 21 st National Information System Security Conference,Virginia:National Academy Press,1998,566-576
[97]Aura T.Strategies Against Replay Attacks.In:Proc of the 10th IEEE Computer Society Foundations Workshop,Massachusetts:IEEE Computer Society Press.1997,59-68
[98]蒋睿，李建华，潘理．基于Strand Space模型的X．509协议分析．上海交通大学学报．2004，38(z1)：169-173
[99]Heintze N,Tygar JD.A Model for Secure Protocols and Their Composition.IEEE Transactions on Software Engineering,1996,22(1):16-30.
[103]周永彬．PKI理论与应用技术研究：[博士学位论文]．北京：中国科学院研究生院，2003．
[104]Rui J,Li P,Jianhua L.Further Analysis of Password Authentication Schemes Based on Authentication Tests.Computer & Security,2004,(23):469-477
[105]Xiehua L,Liming H,Shutang Y,et al.Formal Verification of EAP-AKA with Improved Authentication Tests.In:Proc of International Conference on Wireless Communications,Networking and Mobile Computing.Wuhan:IEEE Computer Society Press.2006,1-4
[106]Jiafen L,Mingtian Z.Designing Authentication Protocols via Authentication Test.In:Proc of IEEE Symposium on Computers and Communications,Aveiro Portugal:IEEE Computer Society Press,2007,475-480
[107]蒋睿，胡爱群，李建华．基于Authentication Test方法的高效安全IKE形式化设计研究．计算机学报，2006，29(9)：1692-1699
[108]Doghmi SF,Guttman JD,Thayer FJ.Completeness of the Authentication Test In:Proc of the 12th European Symposium on Research in Computer Security,Washington DC:IEEE Computer Society Press,2007,106-121
[109]杨明，罗军周．基于认证测试的安全协议分析，软件学报．2006，17(1)：148-156
[110]Xiangdong L,Qingxian W.An Improvement of Authentication Test for Security Protocol Analysis.In:Proc of the 20th IEEE International Conference on Micro Electro Mechanical Systems,2007,745-748
[111]Yongjian L,Jun P.Generalized Unsolicited Tests for Authentication Protocol Analysis.In:Proc of the 7th International Conference on Parallel and Distributed Computing,Applications and Technologies,Taipei:IEEE Computer Society Press,2006,509-514
[112]Sigrid G.A Formal Analysis Technique for Authentication Protocols.In:Proceedings of the 5th International Workshop on Security Protocols.London,UK:Springer-Verlag,1997,159-176.
[113]李谢华，杨树堂．基于消息类型检测的认证测试分析方法．上海交通大学学报．2007，41(1)：85-89
[114]Burrows M,Abadi M,Needham R.A logic of authentication.ACM Transaction on Computer Systems,1990,8(1):18-36.
[115]Perrig A,Song D.Looking For Diamonds in the Desert-Extending Automatic Protocol Generation to Three-Party Authentication and Key Agreement.In:Proc of the 13th IEEE Computer Security Foundations Workshop.Los Alamitos:IEEE Computer Society Press,2000,64-76
[116]周宏斌，黄连生，桑田．基于串空间的安全协议形式化验证模型及算法．计算机研究与发展，2003，40(2)：251-257
[117]刘东喜，安全协议的自动化验证技术研究：[学位论文]，上海：上海交通大学，2002
[118] Furqan, Z, Muhammad S,Guha RK. Formal Verification of 802.l 1i Using Strand Space Formalism. In: Proc of International Conference on Systems and International Conference on Mobile Communications and Learning Technologies, Washington DC:IEEE Computer Society Press,2006, 83-86
[119] Parka HS, Leeb HS, Leec DH, et al. Multi-Protocol Authentication for SIP/SS7 Mobile Network, Computer Communications,2008,31(1): 2755-2763