摘要
给出用PVS对密码协议进行形式化规范的一种方法.该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统.重要的结构如消息、事件、协议规则等都通过语义编码方式定义.
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.
出处
《中国科学院研究生院学报》
CAS
CSCD
2002年第3期233-239,共7页
Journal of the Graduate School of the Chinese Academy of Sciences
基金
the 973 project(G1999035801)