一种面向5G专网鉴权协议的形式化分析方案

doi:10.3969/j.issn.1671-1122.2021.09.001

信息网络安全 ›› 2021, Vol. 21 ›› Issue (9): 1-7.doi: 10.3969/j.issn.1671-1122.2021.09.001

一种面向5G专网鉴权协议的形式化分析方案

王跃东¹(), 熊焰¹, 黄文超¹, 武建双²

1.中国科学技术大学计算机科学与技术学院,合肥 230026
2.合肥天帷信息安全技术有限公司,合肥 230000

收稿日期:2021-04-11 出版日期:2021-09-10 发布日期:2021-09-22
通讯作者: 王跃东 E-mail:ustcwyd@mail.ustc.edu.cn
作者简介:王跃东（1996—）,男,山东,硕士研究生,主要研究方向为协议形式化验证|熊焰（1960—）,男,安徽,教授,博士,主要研究方向为网络安全、漏洞挖掘、形式化建模|黄文超（1982—）,男,湖北,副教授,博士,主要研究方向为网络安全、漏洞挖掘、形式化建模|武建双（1984—）,男,山西,硕士,主要研究方向为网络安全等级保护
基金资助:
国家自然科学基金(61972369);国家重点研发计划(2018YFB2100301)

A Formal Analysis Scheme for 5G Private Network Authentication Protocol

WANG Yuedong¹(), XIONG Yan¹, HUANG Wenchao¹, WU Jianshuang²

1. School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China
2. Hefei Tianwei Information Security Technology Co., Ltd., Hefei 230000, China

Received:2021-04-11 Online:2021-09-10 Published:2021-09-22
Contact: WANG Yuedong E-mail:ustcwyd@mail.ustc.edu.cn

摘要/Abstract

摘要：

文章提出一种面向5G专网鉴权协议EAP-TLS的细粒度形式化建模与验证方案。方案以TS 33.501文档为依据,首先构建基于Diffie-Hellman模式的协议交互模型;然后扩展Dolev-Yao攻击者模型,提出了两种参与方受控场景和混合信道模型;最后使用验证工具SmartVerif验证保密性、认证性、隐私性3类安全属性。实验结果表明,协议在保密性和认证性方面存在3类安全隐患。文章分析了出现安全隐患的根本原因并提出了修订方案,修订后的协议可以满足文章定义的全部安全属性。

关键词: 5G专网, EAP-TLS认证协议, Dolev-Yao攻击者模型, 形式化方法

Abstract:

This paper proposed a fine-grained formal modeling and verification scheme for the 5G EAP-TLS protocol. According to the TS 33.501 document, the scheme first constructed a protocol interaction model based on the Diffie-Hellman mode. Then the scheme expanded the Dolev-Yao model by introducing two participant compromised scenarios and mixed channel model. Finally, the verification tool SmartVerif was used to verify three types of security properties including confidentiality properties, authentication properties, and privacy properties. Experimental results show that the protocol exist safety flaws in terms of confidentiality properties and authentication properties. This paper analyzes the root causes of safety flaws and proposes a revised protocol. The revised protocol can meet all the security properties defined in the paper.

Key words: 5G private network, EAP-TLS authentication protocol, Dolev-Yao attacker model, formal method

中图分类号:

TP309

王跃东, 熊焰, 黄文超, 武建双. 一种面向5G专网鉴权协议的形式化分析方案[J]. 信息网络安全, 2021, 21(9): 1-7.

WANG Yuedong, XIONG Yan, HUANG Wenchao, WU Jianshuang. A Formal Analysis Scheme for 5G Private Network Authentication Protocol[J]. Netinfo Security, 2021, 21(9): 1-7.

图/表 11

图1

图2

图3

表1

表2

表3

表4

表5

表6

表7

图4

参考文献 13

[1]	BROEK F V D, VERDULT R, DE RUITER J. Defeating IMSI Catchers [C]//ACM. 22nd ACM SIGSAC Conference on Computer and Communications Security, October 12-16, 2015, Denver, CO, USA. New York: ACM, 2015: 340-351.
[2]	BLANCHET B. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules [C]//IEEE. 2001 IEEE Computer Security Foundations Symposium, June 11-13, 2001, Cape Breton, Nova Scotia, Canada. New Jersey: IEEE, 2001: 82-96.
[3]	CHEVAL V, KREMER S, RAKOTONIRINA I. DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice [C]//IEEE. 2018 IEEE Symposium on Security and Privacy(SP), May 21-23, 2018, San Francisco, California, USA. New Jersey: IEEE, 2018: 529-546.
[4]	BASIN D, DREIER J, HIRSCHI L, et al. A Formal Analysis of 5G [C]//ACM. 2018 ACM SIGSAC Conference on Computer and Communications Security, October 15-19, 2018, Toronto, ON, Canada. New York: ACM, 2018: 1383-1396.
[5]	MEIER S, SCHMIDT B, CREMERS C, et al. The TAMARIN Prover for the Symbolic Analysis of Security Protocols [C]//Springer. International Conference on Computer Aided Verification, July 13-19, 2013, Saint Petersburg, Russia. Heidelberg: Springer, 2013: 696-701.
[6]	CREMERS C, DEHNEL-WILD M. Component-based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion [C]//ISOC. Network and Distributed Systems Security(NDSS) Symposium, February 24-27, 2019, San Diego, California, USA. Rosten: ISOC, 2019: 1245-1260.
[7]	ZHANG Jiajing, WANG Qiang, YANG Lin, et al. Formal Verification of 5G-EAP-TLS Authentication Protocol [C]//IEEE. IEEE 4th International Conference on Data Science in Cyberspace(DSC), June 23-25, 2019, Hangzhou, China. New Jersey: IEEE, 2019: 503-509.
[8]	ZHANG Jiajing, WANG Qiang, YANG Lin, et al. Formal Analysis of 5G EAP-TLS Authentication Protocol Using ProVerif[EB/OL]. https://www.researchgate.net/publication/338985300_Formal_Analysis_of_5G_EAP-TLS_Authentication_Protocol_Using_Proverif, 2020-12-22.
[9]	CREMERS C. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols [C]//Springer. International Conference on Computer Aided Verification, July 7-14, 2008, Princeton, NJ, USA. Heidelberg: Springer, 2008: 414-418.
[10]	XIONG Yan, SU Cheng, HUANG Wenchao, et al. Smartverif: Push the Limit of Automation Capability of Verifying Security Protocols by Dynamic Strategies[EB/OL]. https://www.usenix.org/conference/usenixsecurity20/presentation/xiong, 2020-08-12.
[11]	DOLEV D, YAO Qizhi. On the Security of Public Key Protocols[J]. IEEE Transactions on Information Theory, 1983, 29(2): 198-208. doi: 10.1109/TIT.1983.1056650 URL
[12]	LOWE G. A Hierarchy of Authentication Specifications [C]//IEEE. 10th Computer Security Foundations Workshop, June 10-12, 1997, Rockport, MA, USA. New Jersey: IEEE, 1997: 31-43.
[13]	ARAPINIS M, MANCINI L, RITTER E, et al. New Privacy Issues in Mobile Telephony: Fix and Verification [C]//ACM. 2012 ACM Conference on Computer and Communications Security, October 16-18, 2012, Raleigh, NC, USA. New York: ACM, 2012: 205-216.

消息	形式化描述
Client/Server_Key_Exchange	g^c/g^s
R_PREKEY	g^cs
Certificate_UE/AUSF	sign(<SUPI, pkUE/pkAUSF>,ltkCA)
Client_Certificate_Verif	sign(hash(Previous),ltkUE)
Finished	senc(hash(Previous), K_SEAF)

等式	描述
(x^y)^z=x^yz	变量x的y次方的z次方等于x的yz次方
x¹=x	变量x的1次方等于x本身
xy=yx	等式满足交换律
(xy)z=x(yz)	等式满足结合律
xinv(x)=1	变量x与其逆相乘结果为1

信道	信道描述	建模假设
UE↔SEAF	无线空口链路,可能存在主动攻击者	公开信道
SEAF↔AUSF/ AUSF↔ARPF	有线链路,可提供保密、完整、重播保护	私密信道
UE↔CA/ ARPF↔CA	可信机构通过私密信道为参与方颁发证书	私密信道

设备	型号
CPU	Intel Broadwell E5-2620 v4 @2.10 GHz
内存容量	128 GB
操作系统	Ubuntu16.04 LTS
GPU	GeForce RTX 1080Ti（GPU显存11.0 GB）
底层验证工具	Tamarin-prover 1.5.1

密钥保密性	诚实参与方场景	UE受控场景	SEAF受控场景
S₁	√	-	√
S₂	√	-	√
S₃	√	-	×

一种面向5G专网鉴权协议的形式化分析方案

A Formal Analysis Scheme for 5G Private Network Authentication Protocol

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 11

参考文献 13

相关文章 3

编辑推荐

Metrics

本文评价

相互认证性	诚实参与方场景	UE受控场景	SEAF受控场景
A₁	√	√	√
A₂	×	×	×
A₃	√	√	√
A₄	√	√	√
A₅	√	√	√
A₆	×	×	×
A₇	×	×	×

[1]	易辉凡, 万良, 黄娜娜, 王鹍鹏. 基于SPIN的安全协议的攻击者建模方法研究[J]. 信息网络安全, 2018, 18(2): 61-70.
[2]	章玥;郭建;朱晓冉. 基于模型的开发方法在多应用智能卡中的应用[J]. , 2013, 13(12): 0-0.
[3]	李改成. 安全应用系统的形式化规范与求精过程研究[J]. , 2009, 9(5): 0-0.