EAP-TLS协议的形式化验证研究

摘要：

EAP-TLS是5 G标准定义的在特定物联网环境中提供密钥服务的安全协议,然而EAP-TLS协议无法提供用户设备与网络之间的双向认证,存在设计缺陷的协议在运行时将危害系统安全,因此在协议实施之前分析其安全性,尽可能找到潜在缺陷并将其改进是所有协议必不可少的过程.文中研究了基于Proverif的EAP-TLS协议与安全属性的形式化模型,并验证了用户设备与网络之间的相互认证性、协议中安全锚点密钥KSEAF与用户身份标识SUPI的保密性等安全属性.实验结果表明,在非安全信道下EAP-TLS协议在认证性方面存在安全缺陷,用户设备对网络的认证失败.分析验证结果进一步确定了导致安全缺陷的原因,并给出了相应的攻击路径.最后,基于密码学中的非对称密钥加密与随机数,讨论了安全缺陷改进的可能性.

关键词：认证协议、EAP-TLS、形式化验证、Proverif、非安全信道

所属期刊栏目：49

分类号：TN915.04

资助基金：国家自然科学基金;四川省科技计划项目;中央高校基本科研业务费专项;四川省无线电监测站科研计划

在线出版日期：2023-05-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：673-677