基于Tamarin Prover的5G EAP-TLS协议的形式化分析  

Formal Analysis of 5G EAP-TLS Protocol Based on Tamarin Prover

作　　者：马壮壮 杜瑞颖[1,2] 陈晶 何琨[1] MA Zhuangzhuang;DU Ruiying;†;CHEN Jing;HE Kun(Key Laboratory of Aerospace Information Security and Trusted Computing,Ministry of Education,School of Cyber Science and Engineering,Wuhan University,Wuhan 430072,Hubei,China;Collaborative Innovation Center of Geospatial Technology,Wuhan 430079,Hubei,China;Rizhao Institute of Information Technology,Wuhan University,Rizhao 276800,Shandong,China)

机构地区：[1]空天信息安全与可信计算教育部重点实验室,武汉大学国家网络安全学院,湖北武汉430072 [2]地球空间信息技术协同创新中心,湖北武汉430079 [3]武汉大学日照信息技术研究院,山东日照276800

出　　处：《武汉大学学报（理学版）》2023年第5期653-664,共12页Journal of Wuhan University:Natural Science Edition

基　　金：国家重点研发计划(2021YFB2700200);国家自然科学基金(61772383,U1836202,62076187,62172303)。

摘　　要：为了保证5G专用网络中移动设备的通信安全,第三代合作伙伴计划(3rd generation partnership project,3GPP)提出了5G可扩展认证协议-传输层安全(extensible authentication protocol-transport layer security,EAP-TLS)。然而,现有的针对于5G EAP-TLS协议的研究工作较少且缺乏系统性。因此,对5G EAP-TLS协议进行详细的描述,并对该协议进行全面的形式化建模。对5G规范中涉及的所有协议实体以及证书分发机制进行建模,同时从5G规约中提取并建模了与5G EAPTLS协议相关的安全目标。提出证据搜索策略引导符号分析工具Tamarin Prover进行自动化证据搜索,解决了Tamarin Prover在验证复杂模型时验证过程无法终止的问题,实现了5G EAP-TLS安全目标的自动化验证。通过分析验证结果,发现了5G EAP-TLS协议能够满足机密性目标,但难以满足一些认证性目标,同时,揭示了协议存在拒绝服务(denial of service,DoS)攻击和用户通信数据泄露的隐患。针对发现的问题,提出了相应的补丁方案,并通过提出的证据搜索策略引导分析工具Tamarin Prover自动化验证了该补丁方案的有效性。To guarantee the communication security of mobile devices in 5G private networks,the 3rd generation partnership project(3GPP)has proposed the 5G EAP-TLS.However,the existing research work on the 5G EAP-TLS protocol is limited and unsystematic.Therefore,a detailed description of the 5G EAP-TLS protocol and a comprehensive formal modelling of the protocol are provided.All protocol entities involved in the 5G specification are modeled,as well as the certificate distribution mechanism,while the security goals related to the 5G EAP-TLS protocol are extracted and modeled from the 5G specification.A proof search strategy is proposed to guide Tamarin Prover,a symbolic analysis tool,to perform an automated evidence search,thus the problem of Tamarin Prover being unable to terminate the verification process when verifying complex models has been solved,achieving automatic verification of 5G security goals.By analyzing the verification results,it is found that the 5G EAP-TLS protocol can meet confidentiality goals,but it is difficult to meet some authentication goals,revealing that the protocol suffers from denial of service(DoS)attack and has potential threat of user communication data leakage.Finally,a corresponding patch solution is proposed to fix the problems,and the effectiveness of the patch is automatically verified using the Tamarin Prover analysis tool by the proposed proof search strategy.

关 键 词：5G专用网络 EAP-TLS协议 形式化分析 Tamarin Prover 自动化验证 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]