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

doi:10.11896/jsjkx.211100111

计算机科学 ›› 2022, Vol. 49 ›› Issue (11A): 211100111-5.doi: 10.11896/jsjkx.211100111

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

陈丽萍^1,2, 徐鹏^1,2, 王丹琛^2,3, 徐扬^1,2

1 西南交通大学数学学院成都 611756
2 系统可信性自动验证国家地方联合工程实验室成都 611756
3 四川省数字经济研究中心成都 610021

出版日期:2022-11-10 发布日期:2022-11-21
通讯作者: 徐鹏(pengxup@swjtu.edu.cn)
作者简介:(1432652087@qq.com)
基金资助:
国家自然科学基金(61976130);四川省科技计划项目(2020YJ0270);中央高校基本科研业务费专项资金(2682021GF012);四川省无线电监测站科研计划([2019]4)

Study on Formal Verification of EAP-TLS Protocol

CHEN Li-ping^1,2, XU Peng^1,2, WANG Dan-chen^2,3, XU Yang^1,2

1 School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China
2 National-local Joint Engineering Lab of System Credibility Automatic Verification,Chengdu 611756,China
3 Sichuan Provinical Digital Economy Research Center,Chengdu 610021,China

Online:2022-11-10 Published:2022-11-21
About author:CHEN Li-ping,born in 1997,postgraduate.Her main research interests include formal verification of security protocols and so on.
XU Peng,born in 1981,Ph.D,lecturer.His main research interests include cyberspace security,formal verification,spectrum and electromagnetic environment management.
Supported by:
National Natural Science Foundation of China(61976130),Sichuan Province Science and Technology Planning Project(2020YJ0270),Fundamental Research Funds for the Central Universities(2682021GF012) and Scientific Research Plan of Sichuan Radio Monitoring Station([2019]4).

摘要/Abstract

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

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

Abstract: EAP-TLS is a security protocol defined under the 5G standard 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.

Key words: Authentication protocol, EAP-TLS, Formal verification, Proverif, Insecure channel

中图分类号:

TN915.04

陈丽萍, 徐鹏, 王丹琛, 徐扬. EAP-TLS协议的形式化验证研究[J]. 计算机科学, 2022, 49(11A): 211100111-5. https://doi.org/10.11896/jsjkx.211100111

CHEN Li-ping, XU Peng, WANG Dan-chen, XU Yang. Study on Formal Verification of EAP-TLS Protocol[J]. Computer Science, 2022, 49(11A): 211100111-5. https://doi.org/10.11896/jsjkx.211100111

参考文献

[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.

相关文章 15

[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(2ⁿ)的形式化研究 Formalization of Finite Field GF(2ⁿ) 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

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

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

Study on Formal Verification of EAP-TLS Protocol

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 0