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

关键词：安全协议 形式化规范 pvs 高阶逻辑 trace模型 

单位：海军潜艇学院信息研究所; 青岛; 266071; 中国科学院研究生院信息安全国家重点实验室; 北京; 100039; 海军潜艇学院信息研究所; 青岛; 266071; 中国科学院研究生院信息安全国家重点实验室; 北京; 100039; 海军计算技术研究所; 北京; 100841