needham-schroeder公钥协议的模型检测分析

密码协议安全性的分析是当前网络安全研究领域的一个世界性难题.提出了运用模型检测工具smv(symbolicmodelverifier)分析密码协议的方法,并对著名的needham-schroeder(ns)公钥协议进行了分析.分析结果表明,入侵者可以轻松地对ns公钥协议进行有效攻击,而这个攻击是ban逻辑分析所没有发现过的.同时,给出了经smv分析过的一个安全的ns公钥协议的改进版本.