摘要
密码协议的安全性研究是网络安全研究的主要热点。本论文主要研究了如何应用系统工程思想和形式化方法来分析和设计密码协议,取得的主要研究结果如下:
1.将系统工程思想引入密码协议设计,结合前人的研究成果,提出了10条密码协议工程原则:5条安全需求分析原则,4条详细设计原则以及1条安全性证明原则。将密码协议设计看作密码协议工程,从协议设计的不同阶段给出原则,是帮助研究人员按系统工程思想进行密码协议设计的有益尝试。实例分析表明,这些原则不仅较为完备,而且可操作性强,能帮助研究人员明确协议设计背后的隐含假设,发现和避免协议设计中的漏洞,简化协议设计。
2.首次提出基于信任的新鲜性标识符分析密码协议的安全性,给出了新鲜性原则:对每个通信参与主体而言,密码协议的安全性取决于发送或者接收的、包含自身已相信新鲜的新鲜性标识符的单向变换。该原则找到了一条快捷、有效的密码协议安全性分析方法,论文示例了20多个经典密码协议的分析结果,分析出的针对协议的攻击或者安全隐患有12个是以往没有指出过的。新鲜性原则的特点是:①能有效区分消息是否新鲜,安全性的分析独立于并发运行环境的具体形式化描述,也独立于攻击者能力的具体形式化描述;②基于该原则得到的分析结果能够证明正确协议的安全性,也能够分析出不安全协议存在的安全属性缺失,以及由该缺失直接构造攻击的结构。
3.基于新鲜性原则,提出了基于逻辑推理的信任多集形式化分析方法。以Needham-Schroeder公钥认证协议为例,说明了该分析方法的有效性、严谨性和自动化实现的可能。另外,针对无线网络的开放性和数据包易失的特点,扩展了信任多集方法,能有效用于无线密码协议分析。
4.证明了保证认证协议安全的充分必要条件,这些条件在计算模型下分别满足基于匹配对话和不可区分性的4个可证安全定义。
5.提出了信任多集自动分析工具的总体框架,通过在2种不同开发环境下信任多集自动分析工具初步实现的比较,给出了信任多集自动分析工具的详细设计。正在开发的信任多集自动分析工具已成功实现了对若干密码协议的安全性分析。
6.基于新鲜性原则和因果一致性的分布式逻辑时间,建立了信任多集形式化设计方法。构造了一个公钥认证协议,并证明了该协议达到了消息数和轮数的下限。
The security research of cryptographic protocols is becoming one of the hottest reasearch spots in network security field. This dissertation mainly discusses how to analyze and design cryptographic protocols based on the idea of system engineering and formal methods. The main results that the author obtainted are as follows:
1. Based on the idea of system engineering and the previous presented principles, we present and illustrate 10 cryptographic protocol engineering principles in three groups: 5 cryptographic protocol security requirement analysis principles, 4 detailed protocol design principles and 1 provable security principle. Cryptographic protocol engineering is a new notion introduced in this thesis for cryptographic protocol design, which is derived from software engineering idea. The idea is useful in that it can indicate implicit assumptions behind cryptographic protocol design, and present operational principles on uncovering these subtleties.
2. A novel freshness principle based on trusted freshness component is presented: for each participant of a cryptographic protocol, the security of the protocol depends only on the sent or received one-way transformation of a message, which includes certain trusted freshness component. The freshness principle indicates an efficient and easy method to analyze the security of cryptographic protocols and the analysis results of 20 classical cryptographic protocols are illustrated while 12 possible attacks or flaws are new. The freshness principle has following characteristic: it could efficiently distinguish the freshness of the messages to avoid replay attacks and interleaving attacks etc., and the analysis procedure is independent of the concrete formalization of the protocol concurrent runs and the adversarys' possible behaviors. The security analysis results based on the freshness principle can either establish the correctness of the protocol when it is in fact correct, or identify the absence of the security properties and the structure to construct attacks based on the absence.
3. Based on the freshness principle, a belief multisets formalism is presented. We have shown the efficiency, rigorousness, automation possibility of the belief multisets formalism by illustrating it via the Needham-Schroeder public key protocol. With the open medium transmission and packet loss considerations in mind, we present an extensible belief multisets formalism including DOS-tolerant property and consistency property analysis that is suitable for wireless protocol analysis.
4. Security goals are presented accurately, which are proved not only necessary but also substantial to guarantee the security adequacy of the cryptographic protocols to 4 security definitions under the computational model. These 4 definiitons are presented based on matching conversation definition and indistinguishability security definition.
5. A general model for automation of the belief multisets fomalism is presented. Via the comparison of our two partial implementations of the automation of the belief multisets fomalism under the different development environments, a detail implementation approach is determined. The developing automation of the belief multisets fomalism has successfully analyzed several cryptographic protocols.
6. Based on the freshness principle and the treatment of the distributed logic time causal consistency, a model for designing cryptographic protocols is also proposed. We exemplify the usability of the model via redesigning the Needham-Schroeder public-key protocol, and prove that the reconstructed challenge-response key exchange protocol achieves the lower bounds of three messages and three rounds.
引文
[1]卿斯汉.“安全协议20年研究进展”.软件学报, 14(10): 1740- 1752, 2003.
[2] W. Mao.“Modern Cryptography: Theory and Practice”. English reprint by PEARSON EDUCATION NORTH ASIA LIMITED and Publishing House of Electronic Industry, 2004.
[3] R.A. DeMillo, G.L. Davida, D. P. Dobkin, M.A.Harrison and R.J. Lipton.“Applied Cryptology, Cryptographic Protocols, and Computer Security Models”. Proceedings of symposia in Applied Mathematics, 29: 174, 1983.
[4] A. Menezes, P. van Oorschot and S. Vanstone.“Handbook of Applied Cryptography”. CRC Press, 1996.
[5]沈炜.“用于公平交换的若干协议和规范的研究与应用”.浙江大学,博士论文, 2003.
[6] T.Y.C. Woo and S.S. Lam.“Authentication for Distributed Systems”. Computer, 25(1): 39- 52, 1992.
[7] U.Feige, A.Fiat and A.Shamir.“Zero Knowledge Proofs of Identify”. Proc. of STOC, pp. 210- 219, 1987.
[8] T.Okamoto.“Provably Secure and Practical Identification Schemes and Corresponding Signature Scheme”. Proc. of Crypto'92, Springer- Verlag, pp. 31- 33, 1993.
[9] R.M. Needham and M.D.Schroeder.“Using Encryption for Authentication in Large Network of Computers”. Communication of the ACM, vol. 21(12): 993-999, 1978.
[10] D. Harkins and D. Carrel.“The Internet Key Exchange Protocol (IKE)”. IETF RFC 2409, Available at http://www.ietf.org/rfc/rfc2409.txt, November 1998.
[11] S. P. Miller, B. C. Neuman, J. I. Schiller and J. H. Saltzer.“Kerberos Authentication and Authorization System”. Project Athena Technical Plan Section E.2.1, MIT, 1987.
[12] CCITT.“CCITT Draft Recommendation X.509. The Directory-Authentication Framework”. Version 7, 1987.
[13] C. Kaufman.“Distributed Authentication Security Service”. IETF RFC 1507, Digital Equipment Corporation, Available at http://www.ietf.org/rfc/rfc1507.txt, September 1993.
[14] SET.“Secure Electronic Transaction”. The SET Standard Specification, Available at http://www.setco.org/set-specifications, May 1997.
[15] IBM Zurich Laboratory.“Internet Keyed Payments Protocol (IKP)”. Available at http://www.zurich.ibm.com /Technology/Security/extern/ecommerce/spec, June 30. 1995.
[16]李梦君.“安全协议形式化验证技术的研究与实现”.国防科学技术大学,博士论文, 2005.
[17] G. Lowe.“An Attack on the Needham-Schroeder Public Key Authentication Protocol”. Information Processing Letters, 56(3): 131- 133, 1995.
[18] D.E. Denning and G.M. Sacco.“Timestamps in Key Distribution Protocols”. Communication of the ACM, 24(8): 533- 536, Aug. 1981.
[19] C. Boyd.“Hidden Assumptions in Cryptographic Protocols”. Computers and Digital Techniques, IEE Proceedings, Part E, 137(6): 433- 436, November 1990.
[20] M. Abadi and R. Needham.“Prudent Engineering Practice for Cryptographic Protocols”. IEEE Transactions on Software Engineering, 22(1): 6- 15, January 1996.
[21] J.Clark and J.Jacob.“A Survey of Authentication Protocol Literature: Version 1.0”. Online document, Available at http://www.win.tue.nl/~ecss/downloads/clarkjacob.pdf, November 1997.
[22]卿斯汉.“安全协议的设计与逻辑分析”.软件学报, 14 (7): 1301-1309, 2003.
[23] R. Canetti1 and C. Meadows and P. Syverson.“Environmental Requirements for Authentication Protocols”. ISSS 2002: 339- 355, 2002.
[24] M. Abadi.“Two Facets of Authentication”. SRC Technical Note, 1998– 007, March 18, 1998.
[25] L. Gong.“A security risk of depending on synchronized clocks”. Operating Systems Review, 26(1): 49-54, Jan. 1992.
[26] D.Dolev and A.C.Yao.“On the Security of Public Key Protocols”, IEEE Transactions on Information Theory, 29(2): 198- 208, 1983.
[27] M. Burrows, M. Abadi and R.M. Needham.“A Logic of Authentication”. Proc. Royal Soc. London A, 426: 233- 271, 1989. Also available at http://www.stanford.edu/class/cs259/papers/ ban1990.pdf
[28] L Gong, R.Needham and R.Yahalom.“Reasoning About Belief in Cryptographic Protocols”. The IEEE Symposium on Research in Security and Privacy, Oakland, CA, 1990: 234- 248, 1990.
[29] M. Abadi and M. R. Tuttle.“A Semantics for a Logic of Authentication”. Proc. of the Tenth ACM Symposium on Principles of Distributed Computing, 1991: 201- 216, 1991.
[30] P. F. Syverson and P. C. V. Oorechot.“On unifying some Cryptographic Protocol Logics”. Proc. of the IEEE Computer Society Symp. on Research in Security and Privacy, 1994: 14- 28, 1994.
[31] C. Boyd and W. Mao.“On a Limitations of BAN Logic”. EUROCRYPT1993, LNCS 765: 240- 247, 1993.
[32] W. Mao and C. Boyd.“Towards a Formal Analysis of Security Protocols”. Proc. of the Computer Security Foundations Workshop VI. Washington: IEEE Computer Society Press, 147- 158, 1993.
[33] S. Goldwasser and S. Micali.“Probabilistic Encryption”. Journal of Computer and System Sciences, 28: 270–299, 1984.
[34] M. Bellare and P. Rogaway.“Random Oracles are Practical: a Paradigm for Designing Efficient Protocols”. 1st ACM Conference on Computer and Communications Security, New York: ACM Press, pp. 62- 73, 1993.
[35] M. Bellare and P. Rogaway.“Entity Authentication and Key Distribution”. Proc. of Crypto'93, LNCS 773, pp. 232- 249, 1993.
[36] J. Stern.“Why Provable Security Matters”. EUROCRYPT 2003, LNCS 2656: 449–461, 2003.
[37] G.lowe.“Toward a completeness result for model checking of security protocol”. pp.1- 48, 1999.
[38] G. Lowe.“Breaking and Fixing the Needham-Schroeder Public-key Protocol Using FDR”. Software-Concepts and Tools, 17: 93- 102, 1996.
[39] V. Kessler and G. Wedel.“AUTOLOG- an Advanced Logic of Authentication”. IEEE Proc. of the Computer Security Foundations Workshop, Los Alamitos, pp. 90- 99, 1994.
[40] M. M. J. C. Mitchell and U. Stern.“Automated analysis of cryptographic protocols using murΦ”. Proc. of 1997 IEEE Symposium on Security and Privacy, Oakland, California, pp.141-153, 1997.
[41] C. Meadows.“The NRL Protocol Analyzer: an Overview”. Journal of Logic Programming, 26(2): 113- 131, 1996.
[42] C. Meadows.“A Model of Computation for the NRL Protocol Analyzer”. Proc. of the 1994 Computer Security Foundations Workshop. Franconia, NH, USA, pp. 84- 89, 1994.
[43] C. Meadows.“Analysis of the Internet Key Exchange Protocol using the NRL Protocol Analyzer”. Proc. of the IEEE Symposium on Security and Privacy. Los Alamitos, pp.84- 89, 1999.
[44] L. Paulson.“Proving Properties of Security Protocols by Induction”. IEEE Symp. on Security and Privacy, pp.79-83, 1997.
[45] F.J.T. Fabrega, J.C. Herzog and J.D. Guttman.“Strand Spaces: Why is a Security Protocol Correct?”. Proc. IEEE Symposium on Security and Privacy, 3-6 May 1998, pp. 160- 171, 1998.
[46] F. J. T. Fabrega, J.C. Herzog and J.D. Guttman.“Strand Spaces Pictures”. Proc. of the Workshop on Formal Methods and Security Protocols. Available at http://www.cs.bell-labs.com/who/nch fmsp/ index.html, 1998.
[47] F.J.T. Fabrega, J.C. Herzog and J.D. Guttman.“Honest Ideals on Strand Spaces”. Proc. of the 11th IEEE Computer Security Foundations Workshop, pp. 66- 77, June 1998.
[48] F.J.T. Fabrega, J.C. Herzog and J.D. Guttman.“Mixed Strand Spaces”. Proc. of the 12th IEEE Computer Security Foundations Workshop, 28- 30 June 1999, pp. 72-82, 1999.
[49] J.D. Guttman and F. Thayer.“Authentication Tests”. Proc. of the IEEE Symposium on Security and Privacy, 14-17 May 2000, pp. 96- 109, 2000.
[50] J.D. Guttman.“Security Protocol Design via Authentication Tests”. Proc. of the 15th IEEE Computer Security Foundations Workshop, pp. 92- 103, 2002.
[51] R. Canetti1 and H. Krawczyk.“Analysis of Key-Exchange Protocols and Their Use for Building Secure Channels”. EUROCRYPT 2001, LNCS 2045, pp. 453–474, 2001.
[52] I. Cervesato, N.A. Durgin, P.D. Lincoln, J.C Mitchell and A. Scedrov.“A Meta-notation for Protocol Analysis”. 12th IEEE Computer Security Foundations Workshop, pp. 55- 69, June 1999.
[53] M. Bellare, R. Canetti and H. Krawczyk.“A Modular Approach to the Design and Analysis of Authentication and Key-exchange Protocols”, Proc. of the 30th STOC, pp. 419- 428, 1998.
[54] R. Canetti and H. Krawczyk.“Universally Composable Notions of Key-Exchange and Secure Channels”. Proc. EUROCRYPT 2002, LNCS 2332, pp. 337–351, 2002.
[55] R. Canetti and J. Herzog.“Universally Composable Symbolic Analysis of Mutual Authentication and Key-Exchange Protocols”. Proc. of the TCC 2006, LNCS 3876, pp. 380- 403.
[56] M. Backes, B. Pfitzmann and M. Waidner.“A Composable Cryptographic Library with Nested Operations”. Proc. of the 10th ACM CCS, pp. 220- 230, 2003.
[57] C. K. Wong, M. Gouda, and S. S. Lam.“Digital Signatures for Flows and Multicasts”. IEEE/ACM Transactions on Networking, 7(4): 502- 513, Aug. 1999.
[58] E. Gafni, Jessica. Staddon and Y. L. Yin.“Efficient Methods for Integrating Traceability and Broadcast Encryption”. Proc. CRYPTO1999, LNCS 1666: 372- 387, 1999.
[59] ANSI/IEEE Std 802.11,“Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications”. 1999.
[60] IEEE Std EAP-2004.“Extensible Authentication Protocol (EAP)”. June 2004.
[61] IEEE Std 802.1X.“Port-Based Network Access Control”. 2001.
[62] IEEE Std 802.11i-2004,“Wireless LAN Medium Access Control (MAC ) and Physical Layer (PHY) Specifications: Medium Access Control (MAC) Security Enhancements”. July 2004.
[63] D.W. Carman, P. S. Kruus and B. J. Matt.“Constraints and Approaches for Distributed Sensor Network Security”. NAI Labs Technical Report # 00-010, Sep. 2000.
[64] D. Davis and R. Swick, "Network Security via Private-key Certificates". ACM Operating Systems Review 24(4): 64-67, Oct 1990. Also appeared in Proceedings of USENIX UNIX Security III Symposium, 14- 17 Sep. 1992, 239-242.
[65] A. Perrig, R. Szewczyk, V. Wen, D. Culler and J. D. Tygar.“SPINS: Security Protocols for Sensor Networks”. Wireless Networks. 8(5): 521- 534, 2002.
[66] B. Brown.“802.11: the Security Differences Between b and i”. IEEE Potentials, Oct-Nov 2003, 22(4): 23- 27.
[67] J.C. Chen, M.C. Jiang and Y.W Liu.“Wireless Lan Security and IEEE 802.11i”. IEEE Wireless Communications, 12(1): 27- 36, 2005.
[68] D. Dolev, C. Dwork and M. Naor.“Non-malleable Cryptography”. Proc. of the 23rd STOC, ACM, pp. 542- 552, 1991.
[69] M. Bellare and P. Rogaway.“Optimal Asymmetric Encryption”. Proc. EUROCRYPT’94, LNCS 950, pp. 92- 111, 1995.
[70] R. Cramer and V. Shoup.“A Practical Public Key Cryptosystem Provably Secure Against Chosen Ciphertext Attack”. Proc. CRYPTO’98, LNCS 1462, pp. 13- 25, 1998.
[71] R. Lipton.“How to Cheat at Mental Poker”. Technical Report, Comp. Sci., Dept. Univ. of California, Berkeley, Aug, 1979.
[72] P. A. Fouque, N. Howgrave-Graham, G. Martinet and G.Poupard.“The Insecurity of Esign in Practical Implementations”. ASIACRYPT 2003, LNCS 2894: 492- 506, 2003.
[73] R. Canetti, H. Krawczyk and J.B. Nielsen.“Relaxing Chosen-Ciphertext Security”. CRYPTO 2003, LNCS 2729: 565- 582, 2003.
[74] S. Vaudenay.“Security Flaws Induced by CBC Padding----Application to SSL, IPSEC, WTLS…”. EUROCRYPT 2002, LNCS 2332: 534- 545, 2002.
[75] A.O. Freier, P. Karlton and P. C. Kocher.“The SSL protocol version 3.0”. http://wp.netscape.com/eng/ssl3/draft302.txt, November 18, 1996.
[76] J. C. Mitchell, V. Shmatikov and U. Stern.“Finite State Analysis of SSL 3.0”. Proceedings of the 7th USENIX Security Symposium San Antonio, Texas: 1- 15, 1998.
[77] D.Otway and O.Rees.“Efficient and Timely Mutual Authentication”. Operating Systems Review, 21(1): 8- 10, Jan. 1987.
[78] M. Abadi and P. Rogaway.“Reconciling two views of cryptography (the computational soundness of formal encryption)”. Journal of Cryptology, 15(2): 103- 127, 2002.
[79] R. Bird, I. Gopal, A. Herzberg, P. Janson, S. Kutten, R. Molva and M.Yung.“The KryptoKnight Family of Light-weight Protocols for Authentication and Key Distribution”, IEEE/ACM Trans. On Networking, (3): 31- 41, 1995.
[80] Yahalom.“Yahalom”. http://www.lsv.ens-cachan.fr/spore/yahalom.pdf, 1998.
[81] C. Neumann.“The Kerberos Network Authentication Service (V5)”, RFC 1510, 1993
[82] B. Newman, T. Ts’o.“Kerberos: an Authentication Service for Computer Networks”, IEEE Communications Magazine, 32 (September 1994), 33- 38, 1994.
[83] L. G. and R. B.“Using Csp to Detect Errors in the TMN Protocols”, IEEE Transactions on software engineering, vol. 23, no. 10, 1997.
[84]郑东.“密码协议的逻辑分析与设计”.博士论文,西安电子科技大学, 1999.
[85] ISO/IEC 2nd DIS 11770-3.“Key Management-Part 3: Mechanisms Using Asymmetric Techniques”. International Organization for Standardization, 1997.
[86] G.Horng and C.K.Hsu.“Weakness in the Helsinki Protocol”. Electronics Letters 34(4): 354- 355, 1998.
[87] C.J.Mitchell and C.Y. Yeun.“Fixing a Problem in the Helsinki Protocol”. ACM Operating Systems Review, 32(4): 21- 24, 1998.
[88]张玉清.“计算机通信网密码协议的分析研究”.博士论文,西安电子科技大学, 2000.
[89] GB15629.11-2003《信息技术系统间远程通信和信息交换局域网和城域网特定要求第11部分:无线局域网媒体访问控制和物理层规范》和GB15629.1102-2003《信息技术系统间远程通信和信息交换局域网和城域网特定要求第11部分:无线局域网媒体访问控制和物理层规范:4GHz频段较高速物理层扩展规范》2004.
[90] D. Atkins and Phil Zimmermann.“PGP Message Exchange Formats”. IETF RFC 1991, Available at http://www.ietf.org/rfc/rfc1991.txt, August1996.
[91]李益发.“一种新的BAN类逻辑”.博士论文,解放军信息工程大学, 2001.
[92] J. Zhou and D. Gollmann.“A Fair Non-repudiation Protocol”. Proceedings of 1996 IEEE Symposium on Security and Privacy, Oakland, California, pp. 55- 61, May 1996.
[93] J. Zhou.“Non-repudiation”, PhD Thesis, University of London, December 1996.
[94]邓红素,左益强,赵一鸣,鲍振东.“移动通信中可证安全的双向认证密钥协商协议”.软件学报, 14(8): 1489- 1494, 2003.
[95]周永彬,张振峰,冯登国.“一种认证密钥协商协议的安全分析及改进”.软件学报, 17(4): 868- 875, 2006.
[96] B. C. Neuman and S. G. Stubblebine.“A Note on the Use of Timestamps as Nonces”, Operating Systems Review, 27(2): 10- 14, 1993.
[97] S. T. Andrew.“Computer Networks (Third Edition)”. English reprint by Tsinghua Press: 2000.
[98] L. Buttyan, S. Staamann and U. Wilhelm.“A Simple Logic for Authentication Protocol Design”, 11th IEEE Computer Security Foundations Workshop (CSFW'98), Rockport, MA, USA. June 9-11, 1998.
[99] Li Gong and Paul Syverson.“Fail-stop Protocols: An Approach to Designing Secure Protocols”, IEEE Dependable Computing for Critical Applications, (5): 79- 100, 1998.
[100] A. Datta, A. Derek, J. C. Mitchell and D. Pavlovic.“A Derivation System for Security Protocols and its Logical Foundation”. 16th IEEE Computer Security Foundations Workshop, 2003:109- 125.
[101] A. Datta, A. Derek, J. C. Mitchell and B. Warinschi.“Computationally Sound Compositional Logic for Key Exchange Protocols”. IEEE Computer Security Foundation Symposium, pp. 321- 334, July 2006.
[102] Thomas YC. Woo and Simon S. Lam.“A Lesson on Authentication Protocol Design”. ACM Operating Systems Review. July 1994. 28(3): 24- 37.
[103] W. Diffie, P. van Oorschot and M. Wiener.“Authentication and Authenticated Key Exchanges”. Design, Codes and Cryptography, 2: 107- 125, 1992.
[104] Catherine A. Meadows.“Formal Verification of Cryptographic Protocols: A Survey”, in ASIACRYPY'94, 1995: 135- 150, 1995.
[105] Thomas Y C. Woo and Simon S. Lam.“Design, Verification and Implementation of an Authentication Protocol”. Proceedings International Conference on Network Protocols, Boston, MA, October 1994.
[106] L. Lamport.“Time, Clocks and the Ordering of Events in a Distributed System”. Communication of the ACM, 21(7): 558- 565, 1978.
[107] L. Gong.“Optimal Authentication Protocols Resistant to Password Guessing Attacks”. IEEE Transactions on Software Engineering, pp. 24- 29, 1995.
[108] L.Gong.“Lower Bounds on Messages and Rounds for Network Authentication Protocols”. 1st ACM Conference on Computer and Communications Security, pp. 26- 37, 1993.
[109] L.Gong.“Efficient Network Authentication Protocols: Lower Bounds and Optimal Implementations”. Technical Report SRI-CSL-94-15, Computer Science LaboratorySRI International, 1994.
[110] N. Heintze and J. Tygar.“A Model for Secure Protocols and their Compositions”. IEEE Transactions on Software Engineering, 22(1): 16- 30, Jan. 1996.
[111] E. Saul and A. Hutchison.“Using GYPSIE, GYNGER and visual GNY to analyze cryptographic protocols in SPEAR2”. [EB]: SouthAfrica http://www.cs.uct.ac.za/Research/DNA/microweb/ pearii/ ownloads/ismss2001sh.pdf.
[112] C. A. R. Hoare.“Communicating sequential processes”. Prentice-Hall International, Englewood Cliffs, NJ, Jun 2004.
[113] Sergey Berezin and Alex Groce.“SyMP: The user’s guide. V.0.2-beta”. Computer Science Dept, Carnegie Mellon University. Dec 2000: 25-31.
[114]魏明卿.“安全协议的自动化验证”.学士论文,上海交通大学, 2008.
[115]王恩俊.“安全协议自动化验证工具的研究”.学士论文,上海交通大学, 2008.