Hu Cheng-jun①②; Zheng Yuan①; Lǚ Shu-wang②; Shen Chang-xiang③
①Inst. of Info.,Navy Submarine Academy Qingdao 266071 China;②SKLOIS Graduate School of the Chinese Academy of Sciences Beijing 100039 China;③Institute of Computing Technology Navy Beijing 100841
Abstract：In this paper, 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.
2004, Vol. 26 
