Welcome to Journal of University of Chinese Academy of Sciences,Today is

›› 2002, Vol. 19 ›› Issue (3): 233-239.DOI: 10.7523/j.issn.2095-6134.2002.3.003

Previous Articles     Next Articles

Formal Specification of Cryptographic Protocols Using PVS

HU Cheng-Jun1,2, ZHENG Yuan2, LU Shu-Wang1, SHEN Chang-Xiang3   

  1. 1. SKLOIS, Graduate School of the Chinese Academy of Sciences, Beijing 100039;
    2. Navy Submarine Academy, Qingdao 266071;
    3. Institute of Computing Technology, Navy, Beijing 100841
  • Received:2002-05-28 Revised:2002-06-07 Online:2002-05-18

Abstract:

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

CLC Number: