HU Cheng-Jun , ZHENG Yuan , LU Shu-Wang , SHEN Chang-Xiang . Formal Specification of Cryptographic Protocols Using PVS[J]. Journal of University of Chinese Academy of Sciences, 2002 , 19(3) : 233 -239 . DOI: 10.7523/j.issn.2095-6134.2002.3.003

1. R Bird, I Gopal, A Herzberg, P Janson, S Kutten, R Molva, M Yung. Systematic design of a family of attack-resistant authenticationprotocols. IEEE J Selected Areas in Communications, 1993, 11 (5) :679一693

2. D Denning, G Sacco. Timestamps in key distribution protocols. Commun ACM, 1981，24(8) :533^536

3. W Diffie, P porschot, M Wiener. Authentication and authehticated key exchanges. Design, Codes and Cryptography. Kluwer Academic Publishers:1992.2,107一125

4. ISO CD 9798-2, Information Technology-Security techniques-Entity authentication mechahisms, Part 2:Entity authentication using symmetric techniques,June 1990

5. R M Needham, M D Schroeder. Using encryption for authentication in large networks of computers. Commun ACM, 1978, 21(12) :993^999

6. ISO 9798-2(2nd edition)，Information Technology-Security technigues-Entity authentication mechanisms, Part 2:Entity authentication using symmetric techniques, 1999

7. R Molva, G Tsudik, E V Herreweghen, S Zatti. KryptoKnight authentication and key distribution system. In: Proceedings of ESO-RICS'92,1992

8. M Bellare, P Rogaway. Entity authentication and key distribution. In: Advances in Cryptology-CRYPTO'93 Proceedings, Springer-

9. ISO CD 10202-S,Financial Transaction Cards-Security architecture of financial systems using integrated circuit cards:Part 5:Use of Algorithms, June 1993