%0 Journal Article
%T 密码协议的promela语言建模及分析
%A 龙士工
%A 王巧丽
%A 李祥
%J 计算机应用
%D 2005
%X ？给出了利用spin模型检测分析密码协议的一般方法。作为一个实例，对needhamschroeder公钥密码协议用promela语言建模，并利用spin进行了分析验证，发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析
%K 密码协议
%K 模型检测
%K spin
%K promela
%U http://www.joca.cn/CN/abstract/abstract13661.shtml