安全协议的形式化规范  

Formal Specification of Security Protocols

作　　者：胡成军[1] 郑援[1] 吕述望[2] 沈昌祥[3] 

机构地区：[1]海军潜艇学院信息研究所,青岛266071 [2]中国科学院研究生院信息安全国家重点实验室,北京100039 [3]海军计算技术研究所,北京100841

出　　处：《电子与信息学报》2004年第4期556-561,共6页Journal of Electronics & Information Technology

基　　金：973项目(G1999035801);总装技术基础项目资助课题

摘　　要：该文给出用PVS(Prototype Verification System)对安全协议进行形式化规范的一种方 法。该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想 加密系统。重要的结构如消息、事件、协议规则等都通过语义编码方式定义.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.

关 键 词：安全协议 形式化规范 PVS 高阶逻辑 trace模型 语义编码 

分 类 号：TN918[电子电信—通信与信息系统]