欢迎访问中国科学院大学学报,今天是

中国科学院大学学报 ›› 2002, Vol. 19 ›› Issue (3): 233-239.DOI: 10.7523/j.issn.2095-6134.2002.3.003

• 论文 • 上一篇    下一篇

基于PVS的密码协议形式化规范(英文)

胡成军1,2, 吕述望2, 郑援1, 沈昌祥3   

  1. 1. 中国科学院研究生院信息安全国家重点实验室, 北京 100039;
    2. 海军潜艇学院, 青岛 266071;
    海军计算技术研究所, 北京 100841
  • 收稿日期:2002-05-28 修回日期:2002-06-07 发布日期:2002-05-18
  • 作者简介:HU ChenR-Jun, male, born in May 1972, associate professor
  • 基金资助:

    the 973 project(G1999035801)

Formal Specification of Cryptographic Protocols Using PVS

HU Cheng-Jun1,2, ZHENG Yuan2, LU Shu-Wang1, SHEN Chang-Xiang3   

  1. 1. SKLOIS, Graduate School of the Chinese Academy of Sciences, Beijing 100039;
    2. Navy Submarine Academy, Qingdao 266071;
    3. Institute of Computing Technology, Navy, Beijing 100841
  • Received:2002-05-28 Revised:2002-06-07 Published:2002-05-18

摘要:

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

关键词: 密码协议, 形式化规范, PVS

Abstract:

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.

Key words: cryptographic protocol, formal specification, PVS

中图分类号: