SPIN在无线网络安全认证协议建模中的应用

作者：周莉; 陆萍; 董虎胜; 谭方勇模型检测认证协议协议验证可扩展认证协议传输层安全

摘要：为确保无线网络安全认证，应用模型检查工具SPIN对EAP－TLS认证协议进行建模，根据SPIN给出攻击轨迹，指出EAP－TLS可能存在双向认证失败的安全隐患，从抵抗攻击和协议改进提出了基于隧道的认证方法。使用SPINPROMELA语言对通信各方建模，用线性时态逻辑LTL表示安全属性，提出了将SPIN应用于认证协议的验证方法。

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社