| 1. Lowe G. Breaking and Fixing the Needham-Schroedet Public-key Protocol using FDR. In: Margaria, Steffen(Eds.):Tools and Algo-rithms for the Construction and Analysis of Systems. LNCS 1055, 1996. 147^-1662. Gurevich Y. Sequential Abstract State Machines Capture Sequential Algorithms. ACM Tansactions on Computational logic, 2000, 1(1):77一1113. Gurevich Y. Evolving Algebra 1993: Lipari Guide. Specification and Validation Methods. Oxford University Press, 1995. 9一364. Gurevich Y. May 1997 Draft of the ASM Guide. Technical Report CSE-TR-336-97. University of Michigin, EECS Department. 19975. G Bella, E Riccobene. A Realistic Environment for Crypto-Protocol Analyses by ASMs. In: Germany U Glasser ed. Proc of INFOR-MATIK'98, 5th International Workshop on Abstract State Machines. Ma列eburg,1998.127^}1386. ISO/IEC 2nd DIS 1177-3. Key management-Part 3: Mechanisms using asymmetric techniques. International Orgnization for Standardi-nation, 19977. Horng G, Hsu C K. Weakness in the Helsinki Protocol. Electronic Letters, 1998, 34(4) :354一3558. G Bella, L C Paulson. Mechanising BAN Kerberos by the Inductive Method. In: A 7 Hu, M Y Vardi eds. Proc of CAV'98, 10th Confer-ence on Computer Aided Verification. Vancouver:Springer-Verlag, 1998.416^4279. G Bella, E Riccobene. Formal Analysis of the Kerberos Authentication System. Jorunal of Universal Computer Science, 1997, 3(12):1337——1381 |
