HB协议的形式规约与验证

摘要：

形式化方法是确保安全协议设计正确性的重要工具,利用形式化方法已经发现了许多安全协议的设计错误.首次利用形式规约语言Z对RFID安全协议HB进行形式规约, 并对HB协议应该满足的安全性质进行形式化描述,使用Z模式推理从协议及其运行环境两个方面验证了协议的关键安全属性,发现了HB协议在设计方面的缺陷,提出了HB协议的一种改进方法.

关键词： 形式规约语言 形式验证 安全协议 HB协议 Z模式推理

作者: 唐静 姬东耀

作者单位: 中国科学院研究生院信息安全国家重点实验室,北京,100049

会议类型: 国内会议

会议名称: 2007全国理论计算机科学学术年会

会议地点: 南宁

会议语种:中文

页码: 113-117

在线出版日期: 2007-11-01（万方平台首次上网日期，不代表论文的发表时间）