密码协议的promela语言建模及分析

？给出了利用spin模型检测分析密码协议的一般方法。作为一个实例，对needhamschroeder公钥密码协议用promela语言建模，并利用spin进行了分析验证，发现了其安全漏洞。该方法很容易推广到有多个主体参与的密码协议的分析