Needham-Schroeder公钥协议的模型检测分析  

Model Checking Analysis of Needham-Schroeder Public-Key Protocol

作　　者：张玉清[1] 王磊[2] 肖国镇[2] 吴建平[1] 

机构地区：[1]清华大学信息网络工程研究中心,北京100084 [2]西安电子科技大学信息保密研究所,西安710071

出　　处：《软件学报》2000年第10期1348-1352,共5页Journal of Software

基　　金：国家自然科学基金!(No.696730 2 5 )

摘　　要：密码协议安全性的分析是当前网络安全研究领域的一个世界性难题 .提出了运用模型检测工具 SMV( symbolic model verifier)分析密码协议的方法 ,并对著名的 Needham- Schroeder( NS)公钥协议进行了分析 .分析结果表明 ,入侵者可以轻松地对 NS公钥协议进行有效攻击 ,而这个攻击是 BAN逻辑分析所没有发现过的 .同时 ,给出了经 SMV分析过的一个安全的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 .

关 键 词：模型检测 密码协议 网络安全 NS公钥协议 

分 类 号：TN918.1[电子电信—通信与信息系统] TP393.08[电子电信—信息与通信工程]