%0 Journal Article
%T Model Checking Analysis of Needham-Schroeder Public-Key Protocol<br>Needham-Schroeder公钥协议的模型检测分析
%A ZHANG Yu-qing
%A WANG Lei
%A XIAO Guo-zhen
%A WU Jian-ping
%A <br>张玉清
%A 王磊
%A 肖国镇
%A 吴建平
%J 软件学报
%D 2000
%I 
%X 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.
%K Model checking
%K cryptographic protocol
%K formal method<br>模型检测
%K 密码协议
%K 形式方法.
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=7CAE7E50AC820168&yid=9806D0D4EAA9BED3&vid=708DD6B15D2464E8&iid=F3090AE9B60B7ED1&sid=A9974A3EA5885863&eid=B3079604173FE132&journal_id=1000-9825&journal_name=软件学报&referenced_num=27&reference_num=10