LONG Shi-gong,WANG Qiao-li,LI Xiang. Promela modeling and analysis for security protocol[J]. Journal of Computer Applications, 2005, 25(07): 1548-1550.
[1]HOLZMANN GJ. Design and Validation of Computer Protocols
[M]. Englewood Cliffs,New JerSey:Prentice-Hall,1991.
[2]PNUELI A. The Temporal Logic of Programs
[A]. Proceedings of 18th IEEE Symposium on Foundations of Computer Science
[C], 1977.46-57.
[3]LOWE G. An attack on the Needham-Schroeder public-key authentication protocol
[J]. Information Processing Letters, 1995,56:131-133, 1995.
[4]LOWE G. Breaking and fixing the Needham-Schroeder public key protocol using FDR
[A]. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), Lecture Notes in Computer Science 1055
[C]. Springer-Verlag, 1996.147-166.
[5]MERZ S. Model Checking: A Tutorial Overview
[EB/OL]. http://spinroot.com/spin/Doc /course/ mc-tutorial.pdf, 2003-10.