|
|||||
|
|
| Needham-Schroeder公钥协议的模型检测分析 | |
| 引用本文： | 张玉清,王磊,肖国镇,吴建平.Needham-Schroeder公钥协议的模型检测分析[J].软件学报,2000,11(10):1348-1352. |
| 作者姓名： | 张玉清 王磊 肖国镇 吴建平 |
| 作者单位： | 1. 清华大学信息网络工程研究中心,北京,100084;西安电子科技大学信息保密研究所,西安,710071 2. 西安电子科技大学信息保密研究所,西安,710071 3. 清华大学信息网络工程研究中心,北京,100084 |
| 基金项目： | 本文研究得到国家自然科学基金(No.69673025)资助. |
| 摘 要： | 密码协议安全性的分析是当前网络安全研究领域的一个世界性难题.提出了运用模型检测工 具SMV(symbolic model verifier)分析密码协议的方法,并对著名的Needham-Schroeder(NS )公钥协议进行了分析.分析结果表明,入侵者可以轻松地对NS公钥协议进行有效攻击,而这个 攻击是BAN逻辑分析所没有发现过的.同时,给出了经SMV分析过的一个安全的NS公钥协议 的改进版本. |
| 关 键 词： | 模型检测 密码协议 形式方法. |
| 收稿时间： | 1999/1/22 0:00:00 |
| 修稿时间： | 9/7/1999 12:00:00 AM |
Model Checking Analysis of Needham-Schroeder Public-Key Protocol |
|
| ZHANG Yu-qing,WANG Lei,XIAO Guo-zhen and WU Jian-ping.Model Checking Analysis of Needham-Schroeder Public-Key Protocol[J].Journal of Software,2000,11(10):1348-1352. | |
| Authors: | ZHANG Yu-qing WANG Lei XIAO Guo-zhen and WU Jian-ping |
| Abstract: | It is an important and hard problem in the area of computer network security to analyze cryptographic protocols. A methodology is presented using a model checke r of formal methods, SMV (symbolic model verifier), to analyze the well known Ne edham-Schroeder Public-Key Protocol. The SMV is used to discover an attack upo n the protocol, which has never been discovered by BAN logic. Finally, the proto col is adapted, and then the SMV is used to show that the new protocol is secure. |
| Keywords: | Model checking cryptographic protocol formal method |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
| 点击此处可从《软件学报》浏览原始摘要信息 | |
| 点击此处可从《软件学报》下载全文 | |