收稿日期: 2002-05-28
修回日期: 2002-06-07
网络出版日期: 2002-05-18
基金资助
the 973 project（G1999035801）
Formal Specification of Cryptographic Protocols Using PVS
Received date: 2002-05-28
Revised date: 2002-06-07
Online published: 2002-05-18
胡成军 , 吕述望 , 郑援 , 沈昌祥 . 基于PVS的密码协议形式化规范(英文)[J]. 中国科学院大学学报, 2002 , 19(3) : 233 -239 . DOI: 10.7523/j.issn.2095-6134.2002.3.003
A specification method using PVS is presented. Higher order logic is chosen as the specification language. Strong spy and ideal encryption are assumed, and trace model is used to define protocols' behaviors. Moreover, useful structures such as message, event, protocol rule, etc. are semantically encoded.
Key words： cryptographic protocol; formal specification; PVS
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
/
| 〈 |
|
〉 |
