安全协议的形式化规范

作者：胡成军; 郑援; 吕述望; 沈昌祥

来源：电子与信息学报, 2004, (04): 556-561.

• 安全协议
• 形式化规范
• PVS Security protocol
• Formal specification
• Prototype Verification System (PVS)

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

• 单位
  海军潜艇学院; 中国科学院研究生院; 信息安全国家重点实验室