| HB协议的形式规约与验证 |
| |
| 引用本文： | 唐静,姬东耀.HB协议的形式规约与验证[J].计算机研究与发展,2008,45(Z1):113-117. |
| |
| 作者姓名： | 唐静 姬东耀 |
| |
| 作者单位： | 中国科学院研究生院信息安全国家重点实验室,北京,100049 |
| |
| 摘 要： | 形式化方法是确保安全协议设计正确性的重要工具,利用形式化方法已经发现了许多安全协议的设计错误.首次利用形式规约语言Z对RFID安全协议HB进行形式规约, 并对HB协议应该满足的安全性质进行形式化描述,使用Z模式推理从协议及其运行环境两个方面验证了协议的关键安全属性,发现了HB协议在设计方面的缺陷,提出了HB协议的一种改进方法.
|
| 关 键 词： | 形式规约 形式验证 安全协议 |
| 修稿时间： | 2007年7月10日 |
Formal Specification and Verification of the HB Protocol |
| |
| Tang Jing,Ji Dongyao.Formal Specification and Verification of the HB Protocol[J].Journal of Computer Research and Development,2008,45(Z1):113-117. |
| |
| Authors: | Tang Jing Ji Dongyao |
| |
| Affiliation: | Tang Jing , Ji Dongyao(State Key Laboratory of Information Security,Graduate University of Chinese Academy of Sciences,Beijing 100049) |
| |
| Abstract: | Formal method is an important tool for assuring the validity of security protocol. By making use of formal method, the design errors of some security protocols have been discovered. As an important part of pervasive computing environment, many RFID security protocols have been brought forward recently, which have no formal specifications and analyses. Using formal specification language Z, a formal specification of HB protocol is presented making it possible to verify the security of RFID protocols, with a ... |
| |
| Keywords: | formal specifications formal verification security protocol |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
