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

Study on Formal Verification of EAP-TLS Protocol

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

EAP-TLS is a security protocol defined under the 5Gstandard that provides key services in a specific IoT environment.However,the EAP-TLS protocol cannot provide mutual authentication between user equipment and the network.A protocol with design flaws will endanger the security of the system during operation.Therefore,it is a very necessary process to analyze its security before the implementation of the protocol,try to find potential flaws and improve them.This paper studies theformal model of EAP-TLS protocol and security properties based on Proverif,and verifies the security properties such as the mutual authentication between user equipment and network,confidentiality between KSEAF(security anchor key)and subscriber permanent identity(SUPI).Verification results find that there are some security flaws in the EAP-TLS protocol in terms of authentication under insecure channels,and the user equipment fails to authenticate the network.Analytical results further confirm the reasons of security flaws,and the corresponding attacks are also given.Finally,the possibility of improving security flaws is discussed based on asymmetric key encryption and random numbers in cryptography.