HB协议的形式规约与验证  

Formal Specification and Verification of the HB Protocol

作　　者：唐静[1] 姬东耀[1] 

机构地区：[1]中国科学院研究生院信息安全国家重点实验室,北京100049

出　　处：《计算机研究与发展》2008年第z1期113-117,共5页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(90604010)

摘　　要：形式化方法是确保安全协议设计正确性的重要工具,利用形式化方法已经发现了许多安全协议的设计错误.首次利用形式规约语言Z对RFID安全协议HB进行形式规约,并对HB协议应该满足的安全性质进行形式化描述,使用Z模式推理从协议及其运行环境两个方面验证了协议的关键安全属性,发现了HB协议在设计方面的缺陷,提出了HB协议的一种改进方法.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 focus on the running environment. Some deficiencies of the HB protocol are discovered. Then a method to improve the HB protocol is presented.

关 键 词：形式规约 形式验证 安全协议 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]