身份认证协议的模型检测分析
Model Checking of Authentication Protocols作者机构:上海交通大学计算机科学与工程系上海200030
出 版 物:《计算机学报》 (Chinese Journal of Computers)
年 卷 期:2003年第26卷第2期
页 面:195-201页
核心收录:
学科分类:0810[工学-信息与通信工程] 0808[工学-电气工程] 0839[工学-网络空间安全] 08[工学] 0835[工学-软件工程] 081001[工学-通信与信息系统] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术(可授工学、理学学位)]
摘 要:提出一个直观、易用的模型来模拟和验证身份认证协议 ,并给出基于Spin(模型检测工具 )的实现 ,它不仅可以模拟多对参与者同时进行会话 ,而且还有效缩减了状态空间 ,从而避免了以前文献中提到的状态爆炸现象 .同时该文用Needham Schroeder公钥协议和TMN协议来说明如何应用该模型 .