计算机科学 ›› 2022, Vol. 49 ›› Issue (11A): 211100111-5.doi: 10.11896/jsjkx.211100111
陈丽萍1,2, 徐鹏1,2, 王丹琛2,3, 徐扬1,2
CHEN Li-ping1,2, XU Peng1,2, WANG Dan-chen2,3, XU Yang1,2
摘要: EAP-TLS是5G标准定义的在特定物联网环境中提供密钥服务的安全协议,然而EAP-TLS协议无法提供用户设备与网络之间的双向认证,存在设计缺陷的协议在运行时将危害系统安全,因此在协议实施之前分析其安全性,尽可能找到潜在缺陷并将其改进是所有协议必不可少的过程。文中研究了基于Proverif的EAP-TLS协议与安全属性的形式化模型,并验证了用户设备与网络之间的相互认证性、协议中安全锚点密钥KSEAF与用户身份标识SUPI的保密性等安全属性。实验结果表明,在非安全信道下EAP-TLS协议在认证性方面存在安全缺陷,用户设备对网络的认证失败。分析验证结果进一步确定了导致安全缺陷的原因,并给出了相应的攻击路径。最后,基于密码学中的非对称密钥加密与随机数,讨论了安全缺陷改进的可能性。
中图分类号:
[1]HUANG Z W.5G network security practice [M].Beijing:Posts &Telecom Press,2020:116-119. [2]3GPP.3GPP TS 33.501 Security architecture and proceduresfor 5G system(Release 16)[S].Nice:3GPP,2020. [3]SHOJAIE B,SABERI I,SALLEH M.Enhancing EAP-TLS authentication protocol for IEEE 802.11i[J].Wireless Networks,2017,23(5):1491-1508. [4]ZHAO Y H,QIAN Q.Research on Security Analysis and Improvement of EAP-TLS Protocol[J].Software Guide,2017,16(8):174-178. [5]ZHANG J,WANG Q,YANG L,et al.Formal Verification of 5G-EAP-TLS Authentication Protocol[C]//2019 IEEE Fourth International Conference on Data Science in Cyberspace(DSC).Hangzhou:IEEE,2019:503-509. [6]ZHANG J,YANG L,CAO W,et al.Formal Analysis of 5G EAP-TLS Authentication Protocol Using Proverif[J].IEEE Access,2020,8:23674-23688. [7]TIAN J.Formal Verification[M].Wiley-IEEE Press,2005:251-266. [8]BLANCHET B.Modeling and Verifying Security Protocols with the Applied Pi Calculus and Proverif[M].Now Foundations and Trends,2016:1-135. [9]DIERKS T,RESCORLA E.The Transport Layer Security(TLS) Protocol Version 1.2 [EB/OL].[2020-01-21].https://datatracker.ietf.org/doc/rfc5246/. [10]YANG Z Q,SU L,YANG B,et al.5G Security Technology and Standards[M].Beijing:Posts & Telecom Press,2020:275-289. [11]HUANG Z W.5G network security practice [M].Beijing:Posts &Telecom Press,2020:331-332. [12]RYAN M D,SMYTH B.Applied pi calculus[EB/OL].[2021-11-08].https://www.cs.bham.ac.uk/~mdr/research/papers/pdf/11-applied-pi.extended.pdf. [13]DOLEV D,YAO A.On the security of public key protocols[J].IEEE Transactions on Information Theory,1983,29(2):198-208. [14]FENG D G,XU J,LAN X.5G mobile communication network security research[J].Journal of Software,2018,29(6):1813-1825. [15]QIANG Q,WU G,HUANG K Z,et al.Progress in 5G security technology research and standards[J].Scientia Sinica(Informationis),2021,51(3):347-366. |
[1] | 蹇奇芮, 陈泽茂, 武晓康. 面向无人机通信的认证和密钥协商协议 Authentication and Key Agreement Protocol for UAV Communication 计算机科学, 2022, 49(8): 306-313. https://doi.org/10.11896/jsjkx.220200098 |
[2] | 杨萍, 王生原. CompCert编译器目标代码生成机制分析 Analysis of Target Code Generation Mechanism of CompCert Compiler 计算机科学, 2020, 47(9): 17-23. https://doi.org/10.11896/jsjkx.200400018 |
[3] | 李凌, 李璜华, 王生原. 在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程 Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design 计算机科学, 2020, 47(6): 8-15. https://doi.org/10.11896/jsjkx.191000173 |
[4] | 范永乾, 陈钢, 崔敏. 基于COQ的有限域GF(2n)的形式化研究 Formalization of Finite Field GF(2n) Based on COQ 计算机科学, 2020, 47(12): 311-318. https://doi.org/10.11896/jsjkx.190900197 |
[5] | 刘静, 赖英旭, 杨胜志, Lina Xu. 一种面向WSN的双向身份认证协议及串空间模型 Bilateral Authentication Protocol for WSN and Certification by Strand Space Model 计算机科学, 2019, 46(9): 169-175. https://doi.org/10.11896/j.issn.1002-137X.2019.09.024 |
[6] | 夏奴奴, 杨晋吉, 赵淦森, 莫晓珊. 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证 Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model 计算机科学, 2019, 46(8): 206-211. https://doi.org/10.11896/j.issn.1002-137X.2019.08.034 |
[7] | 马振威,陈钢. 基于Coq记录的矩阵形式化方法 Matrix Formalization Based on Coq Record 计算机科学, 2019, 46(7): 139-145. https://doi.org/10.11896/j.issn.1002-137X.2019.07.022 |
[8] | 陈昊,罗蕾,李允,陈丽蓉. 安全虚拟机监视器的形式化验证研究 Study on Formal Verification of Secure Virtual Machine Monitor 计算机科学, 2019, 46(3): 170-179. https://doi.org/10.11896/j.issn.1002-137X.2019.03.026 |
[9] | 李璐璐, 董庆宽, 陈萌萌. 基于云的轻量级RFID群组标签认证协议 Cloud-based Lightweight RFID Group Tag Authentication Protocol 计算机科学, 2019, 46(1): 182-189. https://doi.org/10.11896/j.issn.1002-137X.2019.01.028 |
[10] | 徐扬,苑津莎,高会生,赵振兵. 基于二次剩余理论的智能电表安全认证协议 Authentication Protocol for Smart Meter Based on Quadratic Residues 计算机科学, 2018, 45(7): 158-161. https://doi.org/10.11896/j.issn.1002-137X.2018.07.027 |
[11] | 徐扬,苑津莎,高会生,胡晓宇,赵振兵. 基于伪ID的RFID认证协议及串空间证明 RFID Authentication Protocol Based on Pseudo ID and Certification by Strand Space Model 计算机科学, 2017, 44(10): 142-146. https://doi.org/10.11896/j.issn.1002-137X.2017.10.027 |
[12] | 陈红松,王钢,傅忠传. 基于分段模型检测的云服务跨域认证协议的形式化分析与验证 Cloud Services Cross-domain Authentication Protocol Formal Analysis and Verification Based on Fragment Model Check 计算机科学, 2016, 43(4): 140-144. https://doi.org/10.11896/j.issn.1002-137X.2016.04.028 |
[13] | 李艳春,李晓娟,关永,王瑞,张杰,魏洪兴. 基于xMAS模型的SpaceWire信誉逻辑的形式化验证 xMAS-based Formal Verification of SpaceWire Credit Logic 计算机科学, 2016, 43(2): 113-117. https://doi.org/10.11896/j.issn.1002-137X.2016.02.026 |
[14] | 杨秀梅,关永,施智平,吴爱轩,张倩颖,张杰. 函数矩阵及其微积分的高阶逻辑形式化 Higher-order Logic Formalization of Function Matrix and its Calculus 计算机科学, 2016, 43(11): 24-29. https://doi.org/10.11896/j.issn.1002-137X.2016.11.005 |
[15] | 任超群,徐明. 基于簇的水声传感器网络的安全认证协议 Security Authentication Protocol Based on Cluster for Underwater Acoustic Sensor Networks 计算机科学, 2016, 43(10): 166-171. https://doi.org/10.11896/j.issn.1002-137X.2016.10.031 |
|