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

A Formal Analysis Scheme for 5G Private Network Authentication Protocol

作　　者：王跃东 熊焰[1] 黄文超[1] 武建双 WANG Yuedong;XIONG Yan;HUANG Wenchao;WU Jianshuang(School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China;Hefei Tianwei Information Security Technology Co.,Ltd.,Hefei 230000,China)

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

出　　处：《信息网络安全》2021年第9期1-7,共7页Netinfo Security

基　　金：国家自然科学基金[61972369];国家重点研发计划[2018YFB2100301]。

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

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

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