基于时延Petri网的密码协议分析和评估
|
摘要
密码协议安全性分析是网络安全的一个难题，运用形式化方法对密码协议进行分析一直是该领域的研究热点。形式化分析由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径，但是密码协议的形式化分析研究目前还不够深入，本文主要研究了基于时延Petri网的密码协议分析和评估方法。作者所取得的主要研究结果如下：
(1)对四类常见的密码协议形式化分析方法作了一些比较，阐述了各自的特点。
(2)首次提出用时延Petri网作为工具来分析和评估密码协议，并且给出了用它分析和评估密码协议的具体方法和步骤。该方法不但能够反映协议的结构特性和动态特性，而且能够对密码协议进行时间、空间上的性能评估。
(3)给出了时延Petri网的引发规则、时间可达图定义和构造算法，并且介绍了时延Petri网的两个基本分析方法：时间可达图(或可覆盖图)和状态方程。
(4)用时延Petri网对MSR协议、Aziz-Diffle协议和TMN协议进行了具体和详细的分析，给出了这三种协议的发生序列(执行剧情)和攻击者对这三种协议的详细攻击剧情，并且对Aziz-Diffle协议给出了一个改进方案。
(5)本文对这三种密码协议的执行时间、结构特性以及实现分析的软件复杂度给出了客观的评估。
最后，本文建立了实现自动化分析密码协议工具—时延Petri网分析器的结构框架。
It is a hard problem to analyze cryptographic protocol in the area of computer network security. Using formal methods to analyze cryptographic protocol remains the key issue in this field. Because of its compactness, fineness and unambiguity, formal analysis of cryptographic protocol has been an efficient and correct method step by step. The dissertation mainly discusses using formal methods for analysis and evaluation of cryptographic protocols based on timed Petri nets(TPN). The main results that the author obtained are as follows:
(1) The thesis reviews four kinds of formal methods for the analysis of cryptographic protocol and sets forth the merits and disadvantages of each.
(2) The author introduces a new way to describe cryptographic protocol based on timed Petri net, meanwhile, the concrete steps using TPN is expounded. This method not only specifies the structure and dynamic properties but also evaluates the performance of cryptographic protocol (mainly time delay and software complexity).
(3) Firing rules of timed Petri nets and the definition and algorithm of timed reachable graph are given. A fundamental applied methods (mainly timed reachable graph and state equation ) are discussed.
(4) Applying this method to the MSR, Aziz-Diffle and TMN wireless protocol, this thesis verifies the known attacks on them and points out several executive scenarios and attacking scenarios. An improvement on Aziz-Diffle is proposed.
(5) The thesis also objectively evaluates the performance of time delay, structure properties and software complexity of the above three cryptographic protocols.
(6) At last this thesis builds the structure of the automatic tool based on timed Petri nets to analyze cryptographic protocol.
(1)对四类常见的密码协议形式化分析方法作了一些比较，阐述了各自的特点。
(2)首次提出用时延Petri网作为工具来分析和评估密码协议，并且给出了用它分析和评估密码协议的具体方法和步骤。该方法不但能够反映协议的结构特性和动态特性，而且能够对密码协议进行时间、空间上的性能评估。
(3)给出了时延Petri网的引发规则、时间可达图定义和构造算法，并且介绍了时延Petri网的两个基本分析方法：时间可达图(或可覆盖图)和状态方程。
(4)用时延Petri网对MSR协议、Aziz-Diffle协议和TMN协议进行了具体和详细的分析，给出了这三种协议的发生序列(执行剧情)和攻击者对这三种协议的详细攻击剧情，并且对Aziz-Diffle协议给出了一个改进方案。
(5)本文对这三种密码协议的执行时间、结构特性以及实现分析的软件复杂度给出了客观的评估。
最后，本文建立了实现自动化分析密码协议工具—时延Petri网分析器的结构框架。
It is a hard problem to analyze cryptographic protocol in the area of computer network security. Using formal methods to analyze cryptographic protocol remains the key issue in this field. Because of its compactness, fineness and unambiguity, formal analysis of cryptographic protocol has been an efficient and correct method step by step. The dissertation mainly discusses using formal methods for analysis and evaluation of cryptographic protocols based on timed Petri nets(TPN). The main results that the author obtained are as follows:
(1) The thesis reviews four kinds of formal methods for the analysis of cryptographic protocol and sets forth the merits and disadvantages of each.
(2) The author introduces a new way to describe cryptographic protocol based on timed Petri net, meanwhile, the concrete steps using TPN is expounded. This method not only specifies the structure and dynamic properties but also evaluates the performance of cryptographic protocol (mainly time delay and software complexity).
(3) Firing rules of timed Petri nets and the definition and algorithm of timed reachable graph are given. A fundamental applied methods (mainly timed reachable graph and state equation ) are discussed.
(4) Applying this method to the MSR, Aziz-Diffle and TMN wireless protocol, this thesis verifies the known attacks on them and points out several executive scenarios and attacking scenarios. An improvement on Aziz-Diffle is proposed.
(5) The thesis also objectively evaluates the performance of time delay, structure properties and software complexity of the above three cryptographic protocols.
(6) At last this thesis builds the structure of the automatic tool based on timed Petri nets to analyze cryptographic protocol.
引文
1. R. M.Needham,M.D.Schroeder.Using encryption for anthentication in large networks for computers[J],CommunACM,1979, 21(11), 993-999
2. D. E.Denning,G.M.Sacco.Timestamps in key distributeon protocols[J], Common ACM, 1981, 24(8), 533-536
3．冯登国．国内外密码学研究现状及发展趋势[J]，通信学报，2002，23(5)，18-26
4. R.Needham,M. D.Schroeder.Authentication revisited[J],Operating Systems Review,1987, 21(7),
5．李晓东、刑育森、杨义先．Needham-Schroeder密钥分配协议的改进[J]，北京邮电大学学报，1997，20(4)，92—96
6. Neuman and S.G. Stubblebine.A note on the use of timestamps as nonces[J], Operating Systems Review,1993 April,21(2), 10-14
7. Li Gong.A security risk of depending on synchronized clocks[J],Operating Systems Review,1992 January,26(1), 49-53
8．[美]Williman Stallings著 杨明等译．密码编码学与网络安全：原理与实践(第二版)[M]，北京：电子工业出版社，2001年，6-7
9．张玉清．计算机通信网安全协议的分析研究[D]，陕西西安：西安电子科技大学，2000年
10．王育民、柳建伟编著．通信网的安全——理论与技术[M]，陕西西安：西安电子科技大学出版社，1999年第一版
11. D.Dolev, A, Yao. On the security of public key protocols[J],IEEE Transaction on Information Theory,1983,29(2),198-208
12. M.Burrows, M. Abadi,R.Needham.A logic of authentication[C], Proceedings of the Royal Socity of London,1989,A(426), 233-271
13. Li Gong,Needham R,Raphael Yahalom.Reasoning about belief in cryptographic protocols[J],In IEEE Computer Society Symposium in Security and Privacy, IEEE Computer Society Press 1990, 234-248
14. M. Abadi, R. TMark. A semantics for a logic of authentication[A],In Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, ACM Press 1991, 201-216
15. P. Van Oorschot. Extending cryptographic logics ofcryptographic logic of belief to key agreement protocols[A], In Proc of the first ACM conference on Computer and Communications Security, 1993, 232-243
16. Paul Syverson, Paul C, Van Oorschot. On unifying some cryptographic protocol logics[A], In 1994 IEEE Computer Society Symposium in Security and Privacy, IEEE Computer Society, 1994, 14-28
17．肖德琴、周权、张焕国、刘才兴．基于时序逻辑的加密协议分析[J]，计算机学报，2002，25(10)，1083-1089
18. Gavin Lee. Breaking and Fixing the Needham Schroeder public key protocols using FDR[A], In Proc of TACAS, Springer Verlag, 1996, 1055, 147-166
19. SMV. http://www.cs.cmu.edu/～modelcheck/
20．曾小平、孙永强．用Spi演算描述和验证密码学安全协议[J]，计算机工程，1999，25(2)，51-53
21. B. B. Nieh, S.E. Tavares. Modelling and analyzing cryptographic protocols using Petri nets[M]. Advances in Cryptology. 1992, LNCS 718, Springer Verlag, 1992, 275-295
22. Ayda Basyouni. Analysis of wireless cryptographic protocols[D], Master s Thesis ElectricalEngin, Queen s Univ, Kingston, Ontario, Canada
23．郑东、田建波、王育民．关于BAN逻辑扩展的注记[M]，Chinacrypt'98，科学出版社，1998，123-126
24. Mao W. An augmentation of BAN-like Logics[J], Proc of the 1995 IEEE Computer Security Foundation Workshop Ⅷ, 1995, 44-46
25．李益发．密码协议安全性分析中的逻辑化方法—一种新的BAN类逻辑[D]，解放军工程信息大学，2001
26. G. Lower. Towards a completeness result for model checking of security protocols(extended abstract)[J], In Proc of 11th IEEE Computer Security Foundation Workshop, Rockport Massachusetts, June 1998
27. M. Abadi, A. D. Gordon. Reasoning about cryptographic protocols in the Spi calculus[J], in Proc of Concur'97, 1997
28. R. Milner. The polyadic p-Calculus: a tutorials[M], University of Edinburgh, 1991
29．范红、冯登国、郭金庚．安全协议形式化分析的不变式生成技术[J]，中国科学院研究生院学报，2002，19(1)，91-96
30. Kurt Jensen. Coloured Petri nets-Basic concepts[M], Berlin: Spring-verlag, 1996
31. D. M. Stal, S. E. Tavares, H. Meijer. Backward state analysis of cryptographic protocols using coloured Petri nets[A], Workshop on selected Areas in cryptography, SAC'94 Workshop Record, Kingston, Ontario, May 1994, 107-118
32. T. Aura. Modelling the Needham-Schroder authentication protocol woth high level Petri nets[R], Helsinki University of technology digital systems laboratory Series B: Technical Reports No. 14, Sep 1995
33. Lee, G., Lee, J. Petri net based models for specification and analysis of cryptographic protocols[J], J. syst. Software 1997, 37, 141-159
34. M. Tatebayashi, N. Matsuzaki, D. B. Newman. Key distribution protocol for digital mobile communication systems[A], In Proc of Crypto' 89, LNCS vol 435, Berlin: Springer-verlag, 1990, 324-333
35. F. Crazzolara, G. Winskel. Petri nets in cryptographic protocols[A], In Proceedings of the 6th International Workshop on Formal methods for Parallel Programming: Theory and Practice, San Francisco, April 2001. IEEE Press.
36. F. Crazzolara, G. Winskel. Language, Semantics, and Methods for Cryptographic Protocols[R], BRICS Report Series RS-00-18, August 2000
37．刘东喜、赵玉源、李小勇、白英彩．基于对象Petri网的网络认证协议表示及分析[A]，1999信息安全国际会议论文集，1999，159-160
38．袁志祥、蒋昌俊、叶红．基于颜色Petri网的密码协议的分析[J]，安徽工业大学学报，2002，19 (4)，319-324
39．吴哲辉．Petri网的基本概念和基本分析方法，山东科技大学，研究生内部教材
40．J．Peterson，Petri net theory and the modeling ofsystems[M]，吴哲辉译，徐州：中国矿业大学出版社，1989
41. Wolfgang Reisig. Petri Nets-- An Introduction[M], Berlin: Springer Verlag,1982
42. T. Murata. Petri Nets: Properties, Analysis and Applications[A], Proceedings of The IEEE 1989, 541-580
43．袁崇义．Petri网原理[M]，电子工业出版社，1998
44. Wu zhe-hui, T. Murata. Fair Petri nets and weighted synchronic distance[A], In: Procof the 26th Midi west Symposium on CAS, Puebla Mexico, 1983, 129-133
45．吴哲辉．有界Petri网的活性和公平性的分析与实现[J]，计算机学报，1989，12(4)，267-278
46. C. Ramchandani. Analysis of asynchronous concurrent systems by timed Petri nets[R], Massachusetts Inst, Technol, Project MAC, Tech, Rep. 120, 1974
47. W. M. Zuberek. Timed Petri nets and preliminary performance evalution[A], In proc, 7th Annu, Symp. Computer Architecture, May 6-8, 1990, 88-96
48. J. Winkowski. Processes of timed Petri nets[J], Theoretical Computer Science, 2000, Vol. 243, No. 1-2, 1-34.
49．蒋昌俊．离散动态事件系统的PN机理论[M]，北京：中国科学出版社，2000
50．蒋昌俊．Petri网的动态不变性[J]，中国科学(E辑)，1997，Vol．27，No．5，567-573
51．蒋昌俊．同步合成网的完全顺序行为不变性[J]，应用科学学报，2000，Vol．18，No．3，271-275
52. S. M. Shatz, Shengru Tu, T. Murata. An application of Petri net reduction for Ada tasking deadlock analysis[J], IEEE Transaction on Parallel and Distributed Systems, 1996, 7(12), 1307-1322
53. Eric. Y. T. Juan, J. J. P. Tsai, T. Murata, Yi zhou. Reduction methods for real-time systems using delay time Petri nets[J], IEEE Transaction on Software Engineering, 2001, 27(5), 422-448
54. J. Wang. Timed Petri nets: theory and Application[M], Norwell, MA:Kluwer, 1998
55. R. Kemmerer, C. Meadows, J. Millen. Three systems for cryptographic protocol analysis[J], Journal of Cryptology, 1994, 7(2), 79-130
56. C. Meadows. Analysis of the Internet key exchange protocol using the NRL protocol analyzer[A], Proc of the 1999 IEEE symp, on Security and Privacy
57. J. Millen. The Interrogator model[A], In IEEE symp. on security and Privacy, 1995, 251-260
58. C. Ghezzi, et al. Fundamentals of soflware Engineering[M]. Prentice-Hall, N. J., 1991
59. G. Coulouris., et al. Distributed systems concepts and design[M], Addison-Westey, 1996, 477-617
60. RSA Data Security Engineering Report. available at www. rsa. com, 1996
61. M. Beller, L. Chang, Y. Yachobi. Privacy and authentication on a portable communication system[J], IEEE Journal on Selected Areas in Communications, 1993, Vol. 11, No. 6,821-829
62. A. Aziz, W. Diffie. A secure communications protocol to prevent unauthorized acess: Privacy and Authentication for wireless local area networks[J], IEEE Personal Communication, 1994, First Quarter, 25-31
63. CCITT Recommendation X.509. the Directory-Authentication Framework, 1988
64. S. Kent. Privacy Enhancement for Internet Electronic Mail: Part2 ertificate-based key management[M]. RFC 1422, BBN, 1993
65. P. Syverson, C. Meadows. A formal language for cryptographic protocol requirements[J], Designs, Codes and Cryptography, 1996, 7, Jan, 27-59
66. R. Rivest, A. Shamir, L. Adleman. A method for obtaining digital singnatures and public key cryptosystems[J], Commum ACM, 1978, vol(21), No. 2, 120-126
67. R. L. Rivest. The MD5 message digest algorithm, RFC 1321, Apr 1992
68. G. lowe, A. Roscoe. Using CSP to detect errors in the TMN protocol[J], IEEE Trans on Software Engineering, 1997, 23(10), 659-669
69．郑东、王育民．TMN协议的MCJ模型分析[J]，电子学报，1999，27(10)，138-139
70. J. Mitchell, M. Mitchell, U. Stern. Automated analysis of cryptographic protocols using mur[A], Proc of the IEEE symp on Security and Privacy. USA: IEEE Computer Society Press, 1997, 141-151
71．张玉清、王春玲、冯登国．TMN密码协议的SMV分析[J]，计算机研究与发展，2003，40(2)，258-262
72．徐蔚文、陆鑫达．身份认证协议的模型检测分析[J]，计算机学报，2003，26(2)，195-201
2. D. E.Denning,G.M.Sacco.Timestamps in key distributeon protocols[J], Common ACM, 1981, 24(8), 533-536
3．冯登国．国内外密码学研究现状及发展趋势[J]，通信学报，2002，23(5)，18-26
4. R.Needham,M. D.Schroeder.Authentication revisited[J],Operating Systems Review,1987, 21(7),
5．李晓东、刑育森、杨义先．Needham-Schroeder密钥分配协议的改进[J]，北京邮电大学学报，1997，20(4)，92—96
6. Neuman and S.G. Stubblebine.A note on the use of timestamps as nonces[J], Operating Systems Review,1993 April,21(2), 10-14
7. Li Gong.A security risk of depending on synchronized clocks[J],Operating Systems Review,1992 January,26(1), 49-53
8．[美]Williman Stallings著 杨明等译．密码编码学与网络安全：原理与实践(第二版)[M]，北京：电子工业出版社，2001年，6-7
9．张玉清．计算机通信网安全协议的分析研究[D]，陕西西安：西安电子科技大学，2000年
10．王育民、柳建伟编著．通信网的安全——理论与技术[M]，陕西西安：西安电子科技大学出版社，1999年第一版
11. D.Dolev, A, Yao. On the security of public key protocols[J],IEEE Transaction on Information Theory,1983,29(2),198-208
12. M.Burrows, M. Abadi,R.Needham.A logic of authentication[C], Proceedings of the Royal Socity of London,1989,A(426), 233-271
13. Li Gong,Needham R,Raphael Yahalom.Reasoning about belief in cryptographic protocols[J],In IEEE Computer Society Symposium in Security and Privacy, IEEE Computer Society Press 1990, 234-248
14. M. Abadi, R. TMark. A semantics for a logic of authentication[A],In Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, ACM Press 1991, 201-216
15. P. Van Oorschot. Extending cryptographic logics ofcryptographic logic of belief to key agreement protocols[A], In Proc of the first ACM conference on Computer and Communications Security, 1993, 232-243
16. Paul Syverson, Paul C, Van Oorschot. On unifying some cryptographic protocol logics[A], In 1994 IEEE Computer Society Symposium in Security and Privacy, IEEE Computer Society, 1994, 14-28
17．肖德琴、周权、张焕国、刘才兴．基于时序逻辑的加密协议分析[J]，计算机学报，2002，25(10)，1083-1089
18. Gavin Lee. Breaking and Fixing the Needham Schroeder public key protocols using FDR[A], In Proc of TACAS, Springer Verlag, 1996, 1055, 147-166
19. SMV. http://www.cs.cmu.edu/～modelcheck/
20．曾小平、孙永强．用Spi演算描述和验证密码学安全协议[J]，计算机工程，1999，25(2)，51-53
21. B. B. Nieh, S.E. Tavares. Modelling and analyzing cryptographic protocols using Petri nets[M]. Advances in Cryptology. 1992, LNCS 718, Springer Verlag, 1992, 275-295
22. Ayda Basyouni. Analysis of wireless cryptographic protocols[D], Master s Thesis ElectricalEngin, Queen s Univ, Kingston, Ontario, Canada
23．郑东、田建波、王育民．关于BAN逻辑扩展的注记[M]，Chinacrypt'98，科学出版社，1998，123-126
24. Mao W. An augmentation of BAN-like Logics[J], Proc of the 1995 IEEE Computer Security Foundation Workshop Ⅷ, 1995, 44-46
25．李益发．密码协议安全性分析中的逻辑化方法—一种新的BAN类逻辑[D]，解放军工程信息大学，2001
26. G. Lower. Towards a completeness result for model checking of security protocols(extended abstract)[J], In Proc of 11th IEEE Computer Security Foundation Workshop, Rockport Massachusetts, June 1998
27. M. Abadi, A. D. Gordon. Reasoning about cryptographic protocols in the Spi calculus[J], in Proc of Concur'97, 1997
28. R. Milner. The polyadic p-Calculus: a tutorials[M], University of Edinburgh, 1991
29．范红、冯登国、郭金庚．安全协议形式化分析的不变式生成技术[J]，中国科学院研究生院学报，2002，19(1)，91-96
30. Kurt Jensen. Coloured Petri nets-Basic concepts[M], Berlin: Spring-verlag, 1996
31. D. M. Stal, S. E. Tavares, H. Meijer. Backward state analysis of cryptographic protocols using coloured Petri nets[A], Workshop on selected Areas in cryptography, SAC'94 Workshop Record, Kingston, Ontario, May 1994, 107-118
32. T. Aura. Modelling the Needham-Schroder authentication protocol woth high level Petri nets[R], Helsinki University of technology digital systems laboratory Series B: Technical Reports No. 14, Sep 1995
33. Lee, G., Lee, J. Petri net based models for specification and analysis of cryptographic protocols[J], J. syst. Software 1997, 37, 141-159
34. M. Tatebayashi, N. Matsuzaki, D. B. Newman. Key distribution protocol for digital mobile communication systems[A], In Proc of Crypto' 89, LNCS vol 435, Berlin: Springer-verlag, 1990, 324-333
35. F. Crazzolara, G. Winskel. Petri nets in cryptographic protocols[A], In Proceedings of the 6th International Workshop on Formal methods for Parallel Programming: Theory and Practice, San Francisco, April 2001. IEEE Press.
36. F. Crazzolara, G. Winskel. Language, Semantics, and Methods for Cryptographic Protocols[R], BRICS Report Series RS-00-18, August 2000
37．刘东喜、赵玉源、李小勇、白英彩．基于对象Petri网的网络认证协议表示及分析[A]，1999信息安全国际会议论文集，1999，159-160
38．袁志祥、蒋昌俊、叶红．基于颜色Petri网的密码协议的分析[J]，安徽工业大学学报，2002，19 (4)，319-324
39．吴哲辉．Petri网的基本概念和基本分析方法，山东科技大学，研究生内部教材
40．J．Peterson，Petri net theory and the modeling ofsystems[M]，吴哲辉译，徐州：中国矿业大学出版社，1989
41. Wolfgang Reisig. Petri Nets-- An Introduction[M], Berlin: Springer Verlag,1982
42. T. Murata. Petri Nets: Properties, Analysis and Applications[A], Proceedings of The IEEE 1989, 541-580
43．袁崇义．Petri网原理[M]，电子工业出版社，1998
44. Wu zhe-hui, T. Murata. Fair Petri nets and weighted synchronic distance[A], In: Procof the 26th Midi west Symposium on CAS, Puebla Mexico, 1983, 129-133
45．吴哲辉．有界Petri网的活性和公平性的分析与实现[J]，计算机学报，1989，12(4)，267-278
46. C. Ramchandani. Analysis of asynchronous concurrent systems by timed Petri nets[R], Massachusetts Inst, Technol, Project MAC, Tech, Rep. 120, 1974
47. W. M. Zuberek. Timed Petri nets and preliminary performance evalution[A], In proc, 7th Annu, Symp. Computer Architecture, May 6-8, 1990, 88-96
48. J. Winkowski. Processes of timed Petri nets[J], Theoretical Computer Science, 2000, Vol. 243, No. 1-2, 1-34.
49．蒋昌俊．离散动态事件系统的PN机理论[M]，北京：中国科学出版社，2000
50．蒋昌俊．Petri网的动态不变性[J]，中国科学(E辑)，1997，Vol．27，No．5，567-573
51．蒋昌俊．同步合成网的完全顺序行为不变性[J]，应用科学学报，2000，Vol．18，No．3，271-275
52. S. M. Shatz, Shengru Tu, T. Murata. An application of Petri net reduction for Ada tasking deadlock analysis[J], IEEE Transaction on Parallel and Distributed Systems, 1996, 7(12), 1307-1322
53. Eric. Y. T. Juan, J. J. P. Tsai, T. Murata, Yi zhou. Reduction methods for real-time systems using delay time Petri nets[J], IEEE Transaction on Software Engineering, 2001, 27(5), 422-448
54. J. Wang. Timed Petri nets: theory and Application[M], Norwell, MA:Kluwer, 1998
55. R. Kemmerer, C. Meadows, J. Millen. Three systems for cryptographic protocol analysis[J], Journal of Cryptology, 1994, 7(2), 79-130
56. C. Meadows. Analysis of the Internet key exchange protocol using the NRL protocol analyzer[A], Proc of the 1999 IEEE symp, on Security and Privacy
57. J. Millen. The Interrogator model[A], In IEEE symp. on security and Privacy, 1995, 251-260
58. C. Ghezzi, et al. Fundamentals of soflware Engineering[M]. Prentice-Hall, N. J., 1991
59. G. Coulouris., et al. Distributed systems concepts and design[M], Addison-Westey, 1996, 477-617
60. RSA Data Security Engineering Report. available at www. rsa. com, 1996
61. M. Beller, L. Chang, Y. Yachobi. Privacy and authentication on a portable communication system[J], IEEE Journal on Selected Areas in Communications, 1993, Vol. 11, No. 6,821-829
62. A. Aziz, W. Diffie. A secure communications protocol to prevent unauthorized acess: Privacy and Authentication for wireless local area networks[J], IEEE Personal Communication, 1994, First Quarter, 25-31
63. CCITT Recommendation X.509. the Directory-Authentication Framework, 1988
64. S. Kent. Privacy Enhancement for Internet Electronic Mail: Part2 ertificate-based key management[M]. RFC 1422, BBN, 1993
65. P. Syverson, C. Meadows. A formal language for cryptographic protocol requirements[J], Designs, Codes and Cryptography, 1996, 7, Jan, 27-59
66. R. Rivest, A. Shamir, L. Adleman. A method for obtaining digital singnatures and public key cryptosystems[J], Commum ACM, 1978, vol(21), No. 2, 120-126
67. R. L. Rivest. The MD5 message digest algorithm, RFC 1321, Apr 1992
68. G. lowe, A. Roscoe. Using CSP to detect errors in the TMN protocol[J], IEEE Trans on Software Engineering, 1997, 23(10), 659-669
69．郑东、王育民．TMN协议的MCJ模型分析[J]，电子学报，1999，27(10)，138-139
70. J. Mitchell, M. Mitchell, U. Stern. Automated analysis of cryptographic protocols using mur[A], Proc of the IEEE symp on Security and Privacy. USA: IEEE Computer Society Press, 1997, 141-151
71．张玉清、王春玲、冯登国．TMN密码协议的SMV分析[J]，计算机研究与发展，2003，40(2)，258-262
72．徐蔚文、陆鑫达．身份认证协议的模型检测分析[J]，计算机学报，2003，26(2)，195-201