| 摘要: |
| 密码协议安全性的分析是当前网络安全研究领域的一个世界性难题.提出了运用模型检测工 具SMV(symbolic model verifier)分析密码协议的方法,并对著名的Needham-Schroeder(NS )公钥协议进行了分析.分析结果表明,入侵者可以轻松地对NS公钥协议进行有效攻击,而这个 攻击是BAN逻辑分析所没有发现过的.同时,给出了经SMV分析过的一个安全的NS公钥协议 的改进版本. |
| 关键词: 模型检测,密码协议,形式方法. |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金(No.69673025)资助. |
|
| Model Checking Analysis of Needham-Schroeder Public-Key Protocol |
|
ZHANG Yu-qing,WANG Lei,XIAO Guo-zhen,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. |
| Key words: Model checking, cryptographic protocol, formal method. |
