摘要
计算机网络正以惊人的速度向各个领域渗透,其中的安全问题也变得越来越突出和复杂,解决安全问题对许多网络应用来说已是头等大事。从目前解决安全问题的方式来看,安全协议是解决网络安全问题最有效的手段之一。如何保证安全协议的安全性是安全协议研究领域的一个关键问题。为了保证和验证安全协议的安全性,研究人员提出了形式化的方法。经过二十多年的发展,安全协议的形式化方法得到了快速的发展和广泛的应用,已经成为公认的,在安全协议验证和设计领域最为合理、有效的方法。形式化方法通过建立科学的理论模型,对安全协议进行严格的数学和逻辑推导,以此来证明安全协议的安全性或指出安全协议中存在的安全缺陷;同时,形式化方法还可用来指导安全协议的设计。
虽然形式化方法已经成功地发现了许多安全协议的漏洞和攻击,但是,这些方法仍然存在很多问题。通过综合分析这些方法,我们发现,现有分析方法中有两个固有缺陷:一是没有明确的形式化的方法来统一描述多种安全属性;二是缺乏一般化的形式语言模型作为分析安全协议的统一框架。
针对上述两个固有缺陷,我们从三个层面逐步深入地进行了研究:首先,我们深入研究了三类典型且重要的形式化分析方法:类BAN逻辑、串空间、SPI演算,分析了他们的固有缺陷,有效地改进了他们的部分缺陷。其次,我们提出了一种用有向图来描述协议运行的分析方法,该方法部分解决了目前协议分析方法共性问题中的第二个固有缺陷。最后,我们提出了一个安全协议的统一分析框架,在更高的抽象层次上对安全协议运行和安全属性及其验证方法进行形式化建模,并在这个框架指导下,基于符号迹的方法设计了一种新的协议分析方法,实例分析表明该方法是有效的。我们提出的安全协议统一分析框架是解决目前安全协议分析方法两个固有缺陷的一次有意义的尝试,取得了一定的科研成果。
本文的主要创新点如下:
(1)改进类BAN逻辑在“理想化协议”步骤和单调性信任关系方面的缺陷,提出了基于消息唯一起源的动态逻辑方法。通过消息唯一起源的概念,解决了“相信事情的发生”和“相信事情的真实性”两种不同信任的区别,在此基础上建立了动态逻辑方法。
(2)定义了新的类BAN逻辑语义模型,分析了类BAN逻辑的本质缺陷。该模型定义了“可能世界”及“可达关系”的概念。在这种模态逻辑框架下,我们给出了类BAN逻辑的真值赋值函数。从理论上证明了类BAN逻辑的逻辑语义缺陷是不可逾越的。
(3)提出了安全属性的统一形式化描述方法,尝试用匹配关系来描述安全属性。在研究过程中,我们对此做了进一步的改进,安全属性被最终定义为:实体的时序消息与属性消息之间的推导关系。该定义脱离具体协议,是对安全属性的抽象建模,因此,更具有普适性。
(4)将进程演算与实体消息推理结合起来,采用匹配关系来描述安全属性,提出了组合分析方法。该方法一方面弥补了进程演算缺乏数据结构来表示实体知识的缺陷,另一方面明确指出了在符号迹的分析过程中,如何及何时进行带符号的消息推理。由于采用了与协议无关的安全属性形式化描述方法,该方法扩展性很强。
(5)提出了安全协议有向图分析法,部分解决了当前分析方法在协议运行的形式化建模方面的缺陷。该方法将协议规范中的每个协议步骤分解为有序动作序列,给出协议的有向图生成规则以及能够准确地跟踪协议消息的多种构造途径的消息构造逆向搜索算法。
(6)提出“安全属性建模+协议运行建模”模式的统一分析框架。在统一框架的基础上,采用时序消息的推导关系来描述安全属性,为符号迹方法增加时间概念和基于时间的消息推理规则,从而有效地构造了基于符号迹的安全协议分析方法。这种统一分析框架对于安全协议的设计和分析方法的设计具有十分重要的意义。
The computer network is penetrating into all kinds of realm, this makes the security problem becomes more and more outstanding and complicated. Addressing security problems for many network applications is already the major event. Judging from the current solution to security problems, the security protocol is one of the most effective means to resolve the network security problems. How to analyze the security protocols to ensure their safety and validity is one of the key problems should be solved by formal methods for security protocols. After developing for more than twenty years, the formal method of security protocols has been rapid development and wide application, and accepted as the most effective and reasonable method in the field of security protocol verification. The formal method builds up the scientific theory model to carry out the strict mathematics and logic on security protocols to verify their security or point out their security flaws. Meanwhile, the formal method can be used to guide the design of security protocols.
Although the formal methods have been succeeded in finding flaws and attacks of many security protocols, they still suffer from lots of problems. By comprehensive analysis of these methods, we have found two inherence drawbacks: do not unite the description of the security property with a clear formal method; lack of a more generalized formal language used as the unified framework to analyze security protocols.
Aiming at the above-mentioned two inherent drawbacks, we gradually carry out the study from three levels: first of all, we in-depth study three kinds of typical and important formal methods: BAN-like logic, strand space, SPI calculus, analyze their inherent drawbacks, and effectively improve their partial drawbacks. Secondly, we present a method based on directed graph. This method partially solved the second inherent drawback. Finally, we put forward a unified framework to analyze the security protocol. This method models the protocol run, the security property and its verification at a high-level logic abstraction. Guided by this framework, we also design a new analysis method based on symbolic trace method. Examples show that this method is effective.
The unified framework we presented in this dissertation is a significative attempt to solve the two inherent drawbacks of current security protocols. The main innovations are as follows:
1. In order to overcome the flows of BAN-like logics in their“idealization protocol”step and monotony trust relationship, we present a dynamic logic based on the concept of MUO (Message Unique Origin). The concept of MUO resolves the difference between“believe the occurrence of the event”and“believe the truth of the event”, based on this, a dynamic logic is built up.
2. Proposing a new semantic model to analyze the syntax flow of BAN-like logics. This model defines the possible worlds and their relationships of BAN-like logic, and under this modal logic frame, evaluation function is presented. We theoretically prove that the logic semantic flow of BAN-like logic is insurmountable.
3. Proposing the unified formal method to description the security property, we attempt to use match relationship to depict the security property. But in the research process, we have made the improvement regarding this, and then the security property is finally defined as the deduction relationship between the messages based on time and the property messages. This definition is separated from the concrete protocol, therefore, has the universality.
4. Proposing a combined analysis model which uses the matching relationship to depict security properties. This model combines the process calculus and the message deduction relationship. On the one hand, the method makes up the lack of the data structure in process calculus; on the other hand, the method makes it clear that how and when to carry out the symbolic message deduction.
5. Proposing a directed-graph-based method to analyze security protocols, this preliminarily solves the flows in formally modeling the security protocol. This method decomposes each protocol step into the sequence of actions, and then defines the rules to generate the directed graph, as well as the converse-searching algorithm which can accurately tracks the ways to construct the protocol messages.
6. Proposing a unified framework based on the pattern of“security property modeling + protocol run modeling”. We use time-based message deduction relationship to depict the security properties, and add time concept and time-based message reasoning rules to symbolic trace method, thus we effectively construct the symbolic-trace-based method to analyze security protocols. The unified framework is of great significance for the design of security protocols, as well as the design of the analysis method.
引文
[1] Needham R.M, Schroeder M.D. Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM, 1978, 12(12), pp:993-999.
[2]王郁武,詹佑邦.零知识证明的量子身份认证协议.物理学报, 2009, 58(11):7668-7671.
[3] IEEE 802.11e-2005 IEEE Standard for Information technology.
[4] K?ien G M. An introduction to access security in UMTS. IEEE Wireless Communication, 2004, 3(1), pp:8-18.
[5] Rose G, K?ien G M. Access security in CDMA2000, including a comparison with UMTS, access security. IEEE Wireless Communications, 2004, 11(1), pp:19-25.
[6] S.Venkatramulu, S.Veena. Secure Communication Using Two Party Authenticated Quantum key Distribution Protocols. International Journal of Computer Science and Network Security, 2010, 10(8), pp:233-238.
[7] T. Dierks, E. Rescorla. The Transport Layer Security (TLS) Protocol Version 1.1. IETF RFC 4346, April, 2006.
[8] Kent S., Atkinson R., IP Encapsulating Security Payload. IETF RFC 2406, Nov.1998.
[9] Y. Kawatsura. Secure Electronic Transaction (SET) Supplement for the v1.0 Internet. IETF RFC 3538. June, 2003.
[10] Nitish Dalal, Jenny Shah, Khushboo Hisaria, Devesh Jinwala. A Comparative Analysis of Tools for Verfication of Security Protocols. Int. J. Communications, Network and System Science, 2010, 3, pp:779-787.
[11] Juan Carlos López Pimentel and Raúl Monroy. Formal Support to Security Protocol Development: A Survey. Computación y Sistemas ISSN (Versión impresa): 1405-5546, 2008, 12(1), pp:89-108.
[12] Burrows M., Abadi M., Needham R. A logic of authentication. Technical Report 39, Digital Systems Research Center, 1989.
[13] Dolev D, Yao A. On the security of public-key protocols. IEEE Transactions on Information Theory, 1983, 8(29), pp:198-208.
[14]沈海峰,薛锐,黄河燕.用串空间分析公平交换协议.小型微型计算机系统, 2006, 27(1):62-68.
[15] Abadi M., Tuttle M. A semantics for a logic of authentication. In Proceedings of the 10th ACM Symposium on Principles of Distributed Computing, 1991, pp:201-216.
[16] Syverson P. F., van Oorschot P.C. On unifying some cryptographic protocol logics. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, 1994, pp:14-28.
[17] Gong Li, Needham R., Yahalom R. Reasoning about belief in cryptographic protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, 1990, pp:234-248.
[18] Joint Workshop, ARSPA-WITS 2010, Paphos, Cyprus, March 27-28, 2010, Revised Selected Papers. Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security. Springer, ISBN: 3642160735.
[19]薛锐,冯登国.安全协议的形式化分析技术与方法.计算机学报, 2006, 29 (01): 1-20.
[20] van Oorschot P.C. Extending Cryptographic Logics of Belief to Key Agreement Protocols. In Proceedings of the 1st ACM Conference on Communications and Computer Security. 1993, pp:233-243.
[21] Bieber P. A Logic of Communication in a Hostile Environment. In Proceedings of the Computer Security Foundations Workshop III, 1990, pp:14-22.
[22] Syverson P. Formal semantics for logics of cryptographic protocols. In: Proceedings of the Computer Security Foundations Workshop III, 1990, pp:32-41.
[23] Kindred D. Theory generation for security protocols [Ph.D. Thesis]. Pittsburgh: Computer Science Department, Carnegie Mellon University, 1999.
[24] Meadows C. The NRL protocol analyzer: An overview. Journal of Logic Programming, 1996, 26(2), pp:113-131.
[25] Datta A., Derek A., Mitchell J. C., Roy A. Protocol Composition Logic (PCL). Electronic Notes in Theoretical Computer Science (ENTCS), 2007, pp:311-358.
[26] Hoare C. Communicating sequential processes. New Jersey: Prentice Hall International Series in Computer Science, 1985.
[27] Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools, 1996, 17(3), pp:93-102.
[28] Kemmerer R., Meadows C., Millen J. Three systems for cryptographic protocol analysis. Journal of Cryptology, 1994, 7(2), pp:251-260.
[29] Paulson LC. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998, pp:85-128.
[30] C.J.Cremer, P.Lafourcade and P.Nadean. Comparing Strand Spaces in Automatic Security protocol Analysis. Formal to Practical Security: Papers Issured from the 2005-2008 French-Japanese Collaboration, Springer-Verlag, 2009, pp:70-94.
[31] Song D, Berezin S, Perrig A. Athena: a Novel Approach to Efficient Automatic Security Protocol Analysis. Journal of Computer Security, 2001, 9(1), pp:47-74.
[32] Guttman JD, Thayer FJ. Authentication Tests and the Structure of Bundles. Theoretical Computer Science, 2002, 283(2), pp:333-380.
[33] Schneider S. Verifying Authentication Protocols with CSP. In Procedings of the 10th IEEE Computer Security Foundations Workshop, 1997, pp:3-17.
[34] Millen J, Clark S, Freedman S. The Interrogator: Protocol Security Analysis. IEEE Transactions on Software Engineering, 1987, 13(2), pp:274-288.
[35] Nessett D.M. A critique of the Burrows, Abadi, and Needham logic. Operating Systems Review, 1990, 24(2), pp:38-35.
[36] Mao W. An augmentation of of BAN-like logics. In Procedings of the 8th IEEE Computer Security Foundations Workshop, 1995, pp: 44-55.
[37] Louise E. Moser. A logic of knowledge and belief for reasoning about computer security. In Proceedings of the Computer security Foundation Workshop II, 1989, pp:57-63.
[38] Rubin A. D., Honeyman P. Nonmonotonic Cryptographic Protocols. In Proceedings of 7th IEEE Computer Security Foundations Workshop VII, 1994, pp:100-116.
[39]陆汝钤,人工智能.科学出版社, 1996.
[40] Denning D., Saeeo G.. Timestamps in key distribution protocols. Communieations of the ACM, 1981, 24(8), pp:553-536.
[41] Syverson P. A Taxonomy of Relay Attacks. In proceedings of the 7th IEEE Computer Security Foundations Workshop, 1994, pp:131-136.
[42] Woo T, Lam S S. A Semantic Model for Authentication Protocols. In Proceedings of IEEE Symposium on Security and Privacy, 1993, pp:178-194.
[43] Mitchell J, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Murphi. In Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy, 1997, pp:141-151.
[44] David Basin, Sebastian Moedersheim, and Luca Viganò. OFMC: A symbolic model checker for security protocols. In International Journal of Information Security, 2005, 4 (3), pp:181-208..
[45] Clarke E M, Jha S, Marrero W. Partial Order Reductions for Security Protocol Verification. In Tools and Algorithms for the Construction and Analysis of Systmes, 2000.
[46] Sigrid Gürgens. SG Logic-A Formal Analysis Technique for Authentication Protocols. In Proceedings of the 5th International Workshop on Security Protocols, 1997, pp:159-176.
[47] Kailar R. Accountability in Electronic Commerce Protocols. IEEE Transactions on Software Engineering, 1996, 22(5), pp:313-328.
[48] Longley D, Rigby S. An Automatic Search for Security Flaw in Key Management Schemes. Computers and Security, 1992, 11(1), pp:75-90.
[49] Xinming Ye, Jing Liu, Jun Zhang. Security and performance joint analysis method for authentication protocol based on CPN models. International Conference on Computer Application and System Modeling, 2010, pp:505-511.
[50] Maneki AP. Honest functions and their application to the analysis of cryptographic protocols. In Proceedings of the Computer Security Foundations Workshop VI, 1993. pp:147-158.
[51] Doghmi S.F., Guttman J.D., Thayer F.J. Skeletons, Homomorphisms, and Shapes: Characterizing Protocol Executions. ENTCS’2007, 2007, pp:85-102.
[52] Crazzolara F., Winskel G. Composing Strand Spaces. In Proceedings of the 22nd Conference Kanpur on Foundations of Software Technology and Theoretical Computer Science, 2002, pp:97-108.
[53] Halpern J. Y., Pucella R. On the relationship between strand spaces and multi-agent systems. ACM Transactions on Information and System Security, 2003, pp:43-70.
[54] Cervesato I., Durgin N.A., Lincoln P.H., Mitchell J.C., Scedrov A. Relating strands and multiset rewriting for security protocol analysis. In Proceedings of 13th IEEE Computer Security Foundations Workshop, 2000, pp:35-51.
[55] Heather J. Strand Spaces and Rank Functions: More Than Distant Cousins. In Proceedings of the 15th IEEE Computer Security Foundations Workshop, 2002, pp:98-110.
[56] Guttman J. D., Thayer F. J., Carlson J. A., Herzog J. C., Ransdell J. D., Sniffen B. T. Trust Management in Strand Spaces: A Rely-Guarantee Method. 13th European Symposium on Programming, 2004, pp:325-339.
[57] Herzog J. C. The Diffie-Hellman Key-Agreement Scheme in the Strand-Space Model. In Proceedings of the 16th Computer Security Foundations Workshop, 2003, pp:234-247.
[58] Mukhamedov A., Kremer S., Ritter E. Analysis of a Multi-Party Fair Exchange Protocol and Formal Proof of Correctness in the Strand Space Model. In the 9th International Conference on Financial Cryptography and Data Security, 2005, pp:255-269.
[59] A. Al-Tameem, M. Zairi, M. Kamala. Critical factors of information security implementation. In 2009 1st International Conference on Networked Digital Technologies, 2009, pp:379–385.
[60] Yun Jiang, Xifa Liu. Formal Analysis for Cryptographic Protocols on a Trace Semantics. International Conference on Advanced Computer Theory and Engineering, 2008, pp:957-960..
[61] 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.
[62]李谢华.基于串空间模型的安全协议形式化验证方法的研究. [博士论文],上海:上海交通大学, 2007.
[63]邓珍荣,李陶深.串空间模型中认证性测试方法的缺陷.计算机科学, 2006, 33(2):103-105.
[64] Li YJ, Jun P. Extending the Strand Space Method to Verify Kerberos V. In Procedings of the 8th International Conference on Parallel and Distributed Computing, Applications and Technologies, 2007, pp:437-444.
[65]刘义春,张焕国.电子商务协议的串空间分析.计算机科学, 2008, 35(2):109-114.
[66]沈海峰,薛锐,黄河燕,陈肇雄串空间理论扩展.软件学报, 2006, 27(1):62-68.
[67]周宏斌,黄连生,桑田.基于串空间的安全协议形式化验证模型及算法.计算机研究与发展, 2003, 40(2):251-257.
[68]刘东喜,白英彩.基于Strand空间的认证协议证明方法研究.软件学报, 2002, 13(7): 1313-1317..
[69]王焕宝,张佑生,李援.安全协议的串空间图表示.计算机研究与发展, 2006, 43(12):2062-2068.
[70]杨明,罗军舟.基于认证测试的安全协议分析.软件学报, 2006, 17(1):148-156.
[71] Abadi M, Gordon AD. A Calculus for Cryptographic Protocols: The Spi Calculus. In: Proc of the 4th ACM Conference on Computer and Communications Security, 1997, pp:36-47.
[72] Milner R, Parrow J, Walker D. A Calculus of Mobile Processes Part I/II. Information and Computation, 1992, 100(1), pp:1-77.
[73] Haack C., Jeffrey A. Timed Spi-calculus with Types for Secrecy and Authenticity. CONCUR 2005 - Concurrency Theory, 2005, pp:202-216.
[74] Haack C., Jeffrey A. Pattern-matching Spi-calculus. Information and Computation, 2006, 204(8), pp:1195-1263.
[75] Backes M., Cortesi A., Focardi R., Maffei M. A Calculus of Challenges and Responses. In Proceedings of the 2007 ACM workshop on Formal methods in security engineering, 2007, pp:51-60.
[76] Bugliesi M., Focardi R., Maffei M. Compositional analysis of authentication protocols. In Proceedings of European Symposium on Programming, 2004, pp:140-154.
[77]徐东红,齐勇,候迪. SPI演算规范的建模、实现验证研究.计算机科学, 2007, 34(10):80-83.
[78] Gu Yonggen, Fu Yuxi. A Simple Process Calculus for the analysis of Security Protocols. In Procedings of the 6th International Conference on Parallel and Distributed Computing, Applications and Technologies, 2005, pp:110-114.
[79]李国强,顾永跟.基于SPI演算的Kerberos认证协议形式化研究.计算机科学, 2004, 31(11):7-10.
[80] Sumii E, Pierce B C. A bisimulation for type abstraction and recursion. ACM SIGPLAN Notices, 2005, 40(1), pp:63-74
[81]赵宇,王亚弟.基于SPI演算的SSL3.0协议安全性分析.计算机应用, 2005 25(11): 2515-2520
[82]顾永跟.基于类PI演算的电子支付协议安全性形式化分析研究.计算机应用研究, 2006 23(3):22-24.
[83]顾永跟,傅育熙.基于进程演算和知识推理的安全协议形式化分析方法.计算机研究与发展, 2006, 43(5):953-958.
[84]李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述.计算机研究与发展, 2004, 41(7):1097-1103.
[85] Boreale M. Symbolic trace analysis of cryptographic protocols. In Proceedings of the 28th ICALP’01, 2001, pp:667-681.
[86] Micali S. Simple and Fast Optimistic Protocols for Fair Electronic Exchange. In Proceedings of 22nd annual symposium on Principles of distributed computing, 2003, pp:12-19.
[87] Clarke E.M., Jha S., Marrero W. Verifying Security Protocols with Brutus. ACM Transactions on Software Engineering and Methodology, 2000, 9(4), pp:443-487.
[88] Woo T. Y. C., Lam S. S. Authentication for distributed systems. Computer, 1992, 25(1), pp: 39-52.
[89] Bolignano D. Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols, CAV'98, 1998, pp:77-87.
[90] Huima A. Efficient Infinite-State Analysis of Security Protocols. In Proceedings FLOC Workshop on Formal Methods of Security Protocols, 1999.
[91] Laifeng Lu, Jianfeng Ma. Formal analysis model of security protocol based on PCL. International Conference on Computer Application and System Modeling, 2010, pp:658-660.
[92] Bruno Blanchet. Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security, 2009, 17(4):363-434.
[93] Schneider S. Formal analysis of a non-repudiation protocol. In Proceedings of CSFW'98, 1998, pp:54-65.
[94] Pfitzmann A., K?ohntopp M. Anonymity, Unobservability, and Pseudonymity - A Proposal for Terminology. In Proceedings of Workshop on Design Issues in Anonymity and Unobservability, 2000, pp:1-9.
[95] Bugliesi M., Focardi R., Maffei M. Compositional Analysis of Authentication Protocols. in proceedings of 13th European Symposium on Programming, 2004, pp:140-154.
[96]贾国梁,杨树堂,诸鸿文,李谢华. BAN逻辑与串空间相结合的安全协议分析方法.信息安全与通信保密, 2005, 03:147-149.
[97] Ferrari G., Montanari U., Tuosto E. Model Checking for Nominal Calculi. In Foundations of Software Science and Computational Structures 8th International Conference, 2005, pp:1-24.
[98] A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In Proceedings of TACAS 2006, Vol. 3920, Springer Verlag, 2006, pp: 450–454.
[99] Sebastian M?dersheim, Luca Viganò. The open-source fixed-point model checker for symbolic analysis of security protocols. IN: FOSAD 2007–2008–2009, LNCS 5705, 2009, pp:166-194.
[100] K?hler D., Küsters R., Truderung T. Infinite State AMC-Model Checking for Cryptographic Protocols. In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, 2007, pp:181-192.
[101] Armando A., Carbone R., Compagna L. LTL Model Checking for Security Protocols. In Proceedings of the 20th IEEE Computer Security Foundations Symposiu, 2007, pp:385-396.
[102] Armando A.,Compagna L. SAT-based model-checking for security protocols analysis. International Journal of Information Security, 2008, 7(1), pp:3-32.
[103] Kadhi N. E., Hazem E.G. Advanced method for cryptographic protocol verification. Journal of Computational Methods in Sciences and Engineering, 2006, pp:109-119.
[104] Boreale M., Buscemi M.G. A Method for Symbolic Analysis of Security Protocols. Theoretical Computer Science, 2005, 338(1-3), pp:393-425.
[105] Lafrance S. Symbolic Approach to the Analysis of Security Protocols. Journal of universal computer science, 2004, 10(9), pp:1156-1199.
[106] Li Guoqiang, Liu Bochao, Xin Li, Ogawa M. Type-directed Trace Analysis of Security Protocols in Process Calculus. The 22nd Conference of Japan Society for Software Science and Technology, 2005, pp:399-407.
[107] Delaune S., Lafourcade P., Lugiez D., Treinen R. Symbolic protocol analysis for monoidal equational theories. Information and Computation, 2008, 206(2-4), pp:312-351。
[108]张玉清,李继红,肖国镇,密码协议分析工具--BAN逻辑及其缺陷.西安电子科技大学学报, 1999, 26(3):376-378
[109]陈更力,张青.类BAN逻辑的进一步研究.微计算机信息, 2006, 22(6-3):84-86.
[110] Hunter A., Delgrande J. P. Belief Change and Cryptographic Protocol Verification. Proceedings of the 22nd AAAI Conference on Artificial Intelligence, 2007, pp:427-433.
[111] Bruno Blanchet and Avik Chaudhuri. Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. In IEEE Symposium on Security and Privacy, 2008, pp:417-431.
[112]王继志,王英龙.基于改进的串空间分析Ad Hoc路由协议安全性.软件学报, 2006, 17(增刊):256-261.
[113]周清雷,王峰,赵东明.基于认证测试的一种安全协议一致性分析方法.计算机科学, 2007, 34(10):98-102.
[114] Boreale M., Gorla D. On Compositional Reasoning in the Spi-calculus. Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, 2002, pp:67-81.
[115] Fiore M., Abadi M. Computing Symbolic Models for Verifying Cryptographic Protocols. In Proceedings of the 14th IEEE workshop on Computer Security Foundations, 2001, pp:160-173.
[116] Bugliesi M., Focardi R., Maffei M. Principles for entity authentication. In Proceedings of 5th International Conference Perspectives of System Informatics, 2003, pp:294-307.
[117] S. Basagiannis, P. Katsaros, and A. Pombortsis. An intruder model with message inspection for model checking security protocols. Computers and Security, 2010, 29(1):16–34.
[118] T.Y.C.Woo, S.S.Lam. A lesson on authentication protocol design. In Operation Systems Review, 1994, pp:24-37.