|
|
|
| Formal Specification of Security Protocols |
| 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.
|
|
Received: 28 November 2002
|
|
|
|
|
|
|
|
|
2004, Vol. 26 
