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

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

摘要

为了保证5G专用网络中移动设备的通信安全，第三代合作伙伴计划（3rd generation partnership project， 3GPP）提出了5G可扩展认证协议-传输层安全（extensible authentication protocol-transport layer security， EAP-TLS）。然而，现有的针对于5G EAP-TLS协议的研究工作较少且缺乏系统性。因此，对5G EAP-TLS协议进行详细的描述，并对该协议进行全面的形式化建模。对5G规范中涉及的所有协议实体以及证书分发机制进行建模，同时从5G规约中提取并建模了与5G EAP-TLS协议相关的安全目标。提出证据搜索策略引导符号分析工具Tamarin Prover进行自动化证据搜索，解决了Tamarin Prover在验证复杂模型时验证过程无法终止的问题，实现了5G EAP-TLS安全目标的自动化验证。通过分析验证结果，发现了5G EAP-TLS协议能够满足机密性目标，但难以满足一些认证性目标，同时，揭示了协议存在拒绝服务（denial of service， DoS）攻击和用户通信数据泄露的隐患。针对发现的问题，提出了相应的补丁方案，并通过提出的证据搜索策略引导分析工具Tamarin Prover自动化验证了该补丁方案的有效性。

Abstract

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.

Graphical abstract

关键词

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

Key words

private 5G networks / EAP-TLS / formal analysis / Tamarin Prover / automated verification

0　 引 言

5G专用网络具备布局的灵活性、可靠性、安全性以及对接入设备更好的控制性等，适用于工业、医院等对隐私和安全要求较高的场景^[1]。根据全国移动通讯协会报道，在2025年前，所有的运营商将提供5G专用网络服务^[2]。

为了保障5G网络中通信的机密性和接入设备的真实性，第三代合作伙伴计划（3GPP）提出了一种认证和密钥协商协议(authentication and key agreement, AKA)：5G可扩展认证协议-传输层安全（extensible authentication protocol-transport layer security, EAP-TLS）。AKA协议是一种移动用户和服务运营商之间的身份认证协议，通过认证和协商密钥，他们之间能够建立一个安全通道，从而保障后续的通信安全。5G EAP-TLS是基于公钥证书来识别用户设备的协议，它通过提供集中的证书管理机制来控制访问，适用于专用网络。

分析5G EAP-TLS协议的安全性，对于5G专用网络的普及意义重大。然而，现有的对5G EAP-TLS的研究工作较少且存在局限性。例如，文献[3，4]对5G EAP-TLS协议中的一些字段的建模存在错误，导致他们的分析存在缺陷；Zhang等^[3]将协议涉及的四个实体简化为了两个，陈丽萍等^[5]将四个实体简化为了三个，这类简化了协议实体的建模方法，忽略了建模过程中复杂协议流程和协议实体之间交互存在的安全问题。由于5G EAP-TLS协议流程复杂，涉及的规范众多，并且规约中存在许多描述不清的地方，使得其建模和验证过程较为困难。因此，需要对5G EAP-TLS协议进行进一步研究，对协议涉及的所有实体以及复杂的协议流程进行完整的建模分析，以分析该协议的安全性。

网络认证协议的安全分析，根据分析模型可以分为两类：基于计算模型的分析和基于符号模型的分析^[6]。其中，基于计算模型的分析可以捕捉到细小的威胁行为，但建模和证明过程较为复杂，大部分证明都是由密码学家手工完成^[7]，极易出错；相较于基于计算模型的分析，基于符号模型的分析能够形式化准确描述协议，容易实现自动化。因此，对于复杂协议的分析，如5G EAP-TLS协议，采取基于符号模型的分析方法能够减少建模过程中存在的人为因素导致的错误，提高协议建模的准确性。

基于符号模型实现的自动化分析工具有许多，它们能够通过机器进行安全目标的分析和证明，具有较高的准确性和可靠性。例如，Tamarin Prover^[8]、Scyther^[9]、OFMC^[10]、Proverif^[11]、StatVerif^[12]、Deepsec^[13]、SmartVerif^[14]等。相比其他工具，Tamarin Prover在准确建模具有大规模状态机的复杂协议和安全目标的形式化描述方面表现出色。它考虑了无限会话数量的协议交互过程，更容易发现协议存在的安全漏洞。同时，Tamarin Prover已成功应用于大量复杂协议的分析，例如WPA2接入认证协议^[15]和EMV支付协议^[16]、Yubikey安全密钥协议^[17]。由于5G EAP-TLS协议的复杂协议流程和交互过程，其状态空间非常大，对于验证工具性能要求较高。因此，使用Tamarin Prover来验证该协议可以保证验证结果的可靠性和准确性。

为了弥补5G EAP-TLS研究工作的不足，同时提高建模的准确性，本文通过阅读和分析5G规范、EAP和TLS技术文档，提取和完善了5G EAP-TLS的协议流程，并提供了一个基于符号模型的全面建模分析，通过Tamarin Prover的自动化验证结果发现了协议存在的安全问题，并提出了相应的解决方案。本文的主要贡献如下：

1） 对5G EAP-TLS协议的步骤细节进行了实例化，详细描述了5G标准中未定义的信息元素的内容；从5G规约（超过400页）中提取并解释了5G标准定义的机密性和认证性安全目标；

2） 考虑了协议涉及的所有实体和公钥证书机制，建立了一个系统的5G EAP-TLS的形式化模型；

3） 对5G EAP-TLS协议模型进行了全面的分析，实现了对安全目标的全自动验证，发现了协议存在的安全问题。

1　 5G EAP-TLS协议的形式化建模

1.1　5G专用网络认证架构

如图1所示，5G专用网络认证框架主要包括4个部分：用户设备、基站、认证服务器以及统一数据管理。用户设备和基站之间通过无线信道进行通信，基站与认证服务器、认证服务器与统一数据管理之间通过有线信道进行通信。攻击者可以窃听、拦截并且注入信息到无线信道中；有线信道不是本文考虑的重点，我们假设它是安全的，攻击者无法窃听、注入信息。

用户设备(user equipment, UE)，通常是装有USIM（universal subscriber identity module）卡的移动终端，USIM包含用户永久订阅符（subscription permanent identifier, SUPI）、密钥\mathrm{s}{\mathrm{k}}_{\mathrm{U}\mathrm{E}}及证书信息。UE负责生成密钥材料、加密用户永久订阅符、保护用户数据隐私。

基站(base station, BS)，负责转发用户设备与运营商网络之间的信息，基站的功能由安全锚函数(security anchor function, SEAF)实现。为了简化模型，同时更准确地描述基站的功能，本文中假设每个基站只具有一个安全锚函数，采用安全锚函数的标识符来标记基站。

认证服务器(authentication server, AS)，负责与用户设备进行身份验证、生成密钥材料，认证服务器的功能由认证服务器函数(authentication server function, AUSF)实现。它依赖统一数据管理对用户设备身份验证提供决策，决定用户设备是否通过身份认证。

统一数据管理(unified data management， UDM)，负责为认证服务器选择认证策略，提供数据管理、存储身份验证凭据以及解密用户订阅标识符。

1.2　协议实例的建模

本文从TS 33.501 的17.0.0版本^[18]提取了5G EAP-TLS协议流程，然后根据RFC2716^[19]、RFC5216^[20]、RFC5246^[21]内容对5G EAP-TLS协议步骤内容进行详细的描述。5G EAP-TLS协议主要包括两个阶段：初始化阶段，认证及密钥协商阶段。

1.2.1　初始化阶段

初始化阶段是为了完成统一数据管理、识别用户设备和初始化AKA的任务，如图2所示，图中相关名词解释见表1，具体步骤如下：

步骤① 当用户要访问5G专用网络时，通过用户设备向附近的基站发送连接请求信息，内容为加密的用户永久订阅符SUCI，\{\mathrm{S}\mathrm{U}\mathrm{P}\mathrm{I},R\}\mathrm{p}{\mathrm{k}}_{\mathrm{U}\mathrm{D}\mathrm{M}},\mathrm{i}\mathrm{d}\mathrm{U}\mathrm{D}\mathrm{M}>，其中，\mathrm{a}\mathrm{e}\mathrm{n}\mathrm{c}\{\}\mathrm{p}{\mathrm{k}}_{\mathrm{U}\mathrm{D}\mathrm{M}}表示使用公钥进行非对称加密，\mathrm{p}{\mathrm{k}}_{\mathrm{U}\mathrm{D}\mathrm{M}}表示统一数据管理的公钥，R是随机数，可以防止重放攻击，\mathrm{i}\mathrm{d}\mathrm{U}\mathrm{D}\mathrm{M}表示统一数据管理的身份标识符；基站将SUCI连同其标识符\mathrm{i}\mathrm{d}\mathrm{S}\mathrm{E}\mathrm{A}\mathrm{F}一起传输给认证服务器；认证服务器在检查基站标识符\mathrm{i}\mathrm{d}\mathrm{S}\mathrm{E}\mathrm{A}\mathrm{F}的合法性后，将连接请求信息（包含加密的用户永久订阅符SUCI和基站标识符\mathrm{i}\mathrm{d}\mathrm{S}\mathrm{E}\mathrm{A}\mathrm{F}）转发给统一数据管理。

步骤② 统一数据管理收到连接请求信息后，使用私钥进行解密，提取SUPI，验证SUPI属于合法订阅用户后，从订阅数据库中选择认证方法，如5G EAP-TLS，并将SUPI以及选择的5G EAP-TLS认证方法发送给认证服务器；认证服务器发送\mathrm{T}\mathrm{L}\mathrm{S}\_\mathrm{S}\mathrm{T}\mathrm{A}\mathrm{R}\mathrm{T}至基站，再由基站将\mathrm{T}\mathrm{L}\mathrm{S}\_\mathrm{S}\mathrm{T}\mathrm{A}\mathrm{R}\mathrm{T}发送至用户设备；用户设备接收到\mathrm{T}\mathrm{L}\mathrm{S}\_\mathrm{S}\mathrm{T}\mathrm{A}\mathrm{R}\mathrm{T}后，与认证服务器开始进行认证与密钥协商过程。

5G EAP-TLS协议实例的建模主要包括协议实体初始知识的建模以及相应协议流程的建模。协议实体初始知识包括实体身份标识符、证书、公私钥等信息；协议流程的建模就是对协议实体之间接收到特定的信息进行处理，从一个状态转移到另一个状态的过程。图3展示了统一数据管理在初始化阶段涉及的协议实例的建模。

如图3所示，rule UDM_receive_connect_send_resp指的是统一数据管理处理用户连接请求的过程。其中，Init_UDM状态包含了统一数据管理的初始知识，包括身份标识符（idUDM，SUPI，idAUSF）、私钥信息（\mathrm{s}{\mathrm{k}}_{\mathrm{U}\mathrm{D}\mathrm{M}}）；let-in是一种语法结构，用于将名称与表达式绑定，SUCI与表达式的绑定隐含了对统一数据管理中SUPI值的检查。当统一数据管理从信道接收到连接请求（In_S），并且SUPI检查通过，统一数据管理的状态将由Init_UDM状态转移为St_1_UDM状态，此时的状态除身份标识符和私钥信息外，还包含了检查通过的SUPI信息。之后，统一数据管理将SUPI以及选择的认证方法通过Out_S发送给认证服务器。

1.2.2　认证以及密钥协商阶段

认证以及密钥协商阶段是为了实现5G专网内实体之间的相互认证，并协商生成后续会话密钥。这个阶段包括密钥材料分发过程，握手验证过程以及密钥派生过程，如图4所示，图中相关名词解释见表1。

密钥材料分发过程完成了密钥材料的生成和分发，包括步骤③，④和⑤，具体过程如下：

步骤③ 用户设备生成密钥材料R_{\mathrm{u}\mathrm{e}}，然后将R_{\mathrm{u}\mathrm{e}}以及支持的加密方法\mathrm{M}\mathrm{e}\mathrm{t}\mathrm{h}\mathrm{o}{\mathrm{d}}_{\mathrm{U}\mathrm{E}}共同发送给基站，基站将这些信息转发给认证服务器。

步骤④ 认证服务器接收到基站转发的密钥材料R_{\mathrm{u}\mathrm{e}}以及加密方法\mathrm{M}\mathrm{e}\mathrm{t}\mathrm{h}\mathrm{o}{\mathrm{d}}_{\mathrm{U}\mathrm{E}}后，生成密钥材料R_{\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{f}}，同时将支持的加密方法\mathrm{M}\mathrm{e}\mathrm{t}\mathrm{h}\mathrm{o}{\mathrm{d}}_{\mathrm{A}\mathrm{U}\mathrm{S}\mathrm{F}}以及证书\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{A}\mathrm{U}\mathrm{S}\mathrm{F}}一并发送给基站，由基站转发给用户设备。

步骤⑤ 用户设备接收到基站转发的密钥材料（R_{\mathrm{u}\mathrm{e}}和R_{\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{f}}）以及证书（\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{A}\mathrm{U}\mathrm{S}\mathrm{F}}）等信息后，首先验证证书的合法性，使用证书颁发机构（certificate authority, CA）的公钥，对认证服务器证书\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{A}\mathrm{U}\mathrm{S}\mathrm{F}}中的签名进行校验；验证通过，则生成预主密钥R_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}，该密钥材料是生成会话密钥的关键组成部分，该材料使用认证服务器证书中的公钥\mathrm{p}{\mathrm{k}}_{\mathrm{A}\mathrm{U}\mathrm{S}\mathrm{F}}进行非对称加密发送，即\mathrm{E}\mathrm{n}\mathrm{c}\_{\mathrm{R}}_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}。之后，用户设备使用密钥材料（R_{\mathrm{u}\mathrm{e}}, R_{\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{f}}, R_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}），通过PRF函数（用于推导出临时密钥以及生成验证信息），生成临时密钥k_{\mathrm{s}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}}。然后，构建校验信息\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{y}}\mathrm{和}\mathrm{c}\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{n}{\mathrm{t}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}；其中，\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{y}}是用户设备对H_{\mathrm{1}}散列值的签名，H_{\mathrm{1}}代表先前发送和接收的握手信息（包含步骤③和④中的消息以及R_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}）；\mathrm{c}\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{n}{\mathrm{t}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}是用户设备利用临时密钥k_{\mathrm{s}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}}，生成的关于先前握手信息H_{\mathrm{2}}的证明，H_{\mathrm{2}}包含了H_{\mathrm{1}}以及\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{y}}信息。最后，用户设备将证书\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{U}\mathrm{E}}、\mathrm{E}\mathrm{n}\mathrm{c}\_{\mathrm{R}}_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}、\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{y}}以及\mathrm{c}\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{n}{\mathrm{t}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}发送到基站，由基站转发至认证服务器。

握手验证过程是为了验证协议过程中交换的信息（H_{\mathrm{1}}, H_{\mathrm{2}}, H_{\mathrm{3}}，H_{\mathrm{1}}\subseteq H_{\mathrm{2}}\subseteq H_{\mathrm{3}}）的完整性，防止信息被攻击者伪造或篡改，具体过程如下：

步骤⑥ 认证服务器接收到基站转发的用户设备证书（\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{U}\mathrm{E}}）、密钥材料（\mathrm{E}\mathrm{n}\mathrm{c}\_{\mathrm{R}}_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}）以及校验信息（\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{y}}和\mathrm{c}\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{n}{\mathrm{t}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}）后，使用CA的公钥对用户设备证书签名进行验证。然后，认证服务器使用其私钥对\mathrm{E}\mathrm{n}\mathrm{c}\_{\mathrm{R}}_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}进行解密获取R_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}。接下来，认证服务器基于R_{\mathrm{u}\mathrm{e}}、R_{\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{f}}、R_{\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{k}\mathrm{e}\mathrm{y}}、\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{U}\mathrm{E}}以及\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{A}\mathrm{U}\mathrm{S}\mathrm{F}}构建信息H_{\mathrm{1}}，并使用用户设备证书中的公钥对\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{y}}进行验证；验证通过，则基于三个密钥材料派生临时密钥k_{\mathrm{s}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}}；同时，基于H_{\mathrm{1}}和\mathrm{c}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{y}}构建信息H_{\mathrm{2}}，并利用k_{\mathrm{s}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}}对\mathrm{c}\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{n}{\mathrm{t}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}进行验证；所有验证通过，认证服务器则利用k_{\mathrm{s}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}}构建校验信息\mathrm{s}\mathrm{e}\mathrm{r}\mathrm{v}\mathrm{e}{\mathrm{r}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}，\mathrm{s}\mathrm{e}\mathrm{r}\mathrm{v}\mathrm{e}{\mathrm{r}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}是生成的关于先前握手信息（H_{\mathrm{3}}）的证明。最后，认证服务器将校验信息\mathrm{s}\mathrm{e}\mathrm{r}\mathrm{v}\mathrm{e}{\mathrm{r}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}发送给基站，基站再将其转发给用户设备。

密钥派生过程是为了生成会话密钥k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}，保护用户设备与基站之间的后续通信，包括步骤⑦和⑧，具体过程如下：

步骤⑦ 用户设备接收到认证服务器发送的校验信息\mathrm{s}\mathrm{e}\mathrm{r}\mathrm{v}\mathrm{e}{\mathrm{r}}_{\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{d}}，构建信息H_{\mathrm{3}}并使用k_{\mathrm{s}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}}对该信息进行验证，验证通过，则发送\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{T}\mathrm{L}\mathrm{S}信息至基站，再由基站转发至认证服务器，以通知认证服务器开始派生密钥。

步骤⑧ 当认证服务器收到\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{T}\mathrm{L}\mathrm{S}信息，认证服务器开始进行密钥派生，密钥k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}是通过密钥派生函数\mathrm{K}\mathrm{D}\mathrm{F}，由k_{\mathrm{s}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}}和\mathrm{i}\mathrm{d}\mathrm{S}\mathrm{E}\mathrm{A}\mathrm{F}派生。最后认证服务器将成功信号信息\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}、密钥等信息发送给基站。基站存储密钥k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}，然后将成功信号信息\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}转发给用户设备，准备对用户设备后续通信过程进行加密。用户设备接收到成功信号信息\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}后，进行密钥派生。至此，认证及密钥协商阶段结束。

1.3　证书分发机制的建模

为了建模证书分发机制，本文首先建模了CA这一实体，CA使用自签名证书；然后，CA使用私钥为5G专用网络中的实体签发证书。本文假设证书分发信道是安全的，即攻击者不能干扰证书分发过程。图5展示了CA向UE颁发证书的过程。该过程包括CA注册过程和证书签发过程。

如图5所示，rule CA_register指的是CA注册过程，该过程由CA生成私钥，进行自签名，并将证书广播到5G专用网络；rule CA_sign指的是证书签发过程，该过程先由用户设备通过安全信道向CA发送证书请求，其中包含用户设备的公钥等信息，然后由CA使用私钥对相应信息进行签名并生成证书，通过该信道发送给用户设备。

1.4　安全目标的建模

1.4.1　安全目标解释

5G安全目标涉及终端安全、网络功能虚拟化安全、网络切片安全、接入认证安全等多个方面。本文讨论的是用户设备接入网络所需满足的安全目标，其中包括机密性、认证性和隐私性。隐私性安全目标主要包括用户永久订阅符的机密性、用户位置的安全机密性和用户不可追踪性。由于本文侧重于分析所有协议实体交互过程中是否存在安全漏洞，同时为了简化建模难度，本文对于隐私性的建模仅考虑用户永久订阅符机密性，并将其看作机密性目标。

因此，本文从TS 33.501^[18]规范文档中，提取了5G中5G EAP-TLS协议需要满足的机密性(confidentiality)以及认证性(authentication)安全目标，如表2所示。为了对认证性安全目标进行准确的描述，本文采取Lowe^[22]提出的认证性分类标准，Lowe从一个协议参与方P的角度定义了与另一个协议参与方Q之间的4个级别的身份验证，从低到高分别是：

1） 保活性，P确信Q先前运行过协议，但Q不一定是与P共同运行的；

2） 弱认证性，P确信Q先前与他共同运行了协议，但是不一定认可在运行中协商了相同的数据；

3） 非单射认证性，P确信Q与他共同运行了协议，并且双方都认可在运行中协商了相同的数据；

4） 单射认证性，在非单射认证性的基础上，P确信与Q关于运行过程中协商的数据是唯一的，不存在另一对P1，Q1在协议运行过程中协商了相同的数据，满足该等级的协议，能够防止重放攻击。

1.4.2　安全目标的形式化建模

通过阅读分析5G规范和RFC技术文档，本文对安全目标进行了形式化建模，并从不同的角度（用户设备角度、基站角度、认证服务器角度、统一数据管理角度）进行了安全性分析。

机密性目标C1、C2定义的安全需求，要求网络中掌握隐私信息（SUPI、k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}）的实体对信息进行保密。以C1为例，在协议运行过程中，4个实体都获取了SUPI的信息，因此需要对各自掌握的SUPI进行确认。图6是从用户设备角度建模的机密性引理，该引理用于描述机密性目标C1。

图6中引理的含义是：在任意的时间点i，用户设备确信SUPI是保密的（使用标签Secret_SUPI_UE标记），一定不存在一个时间点j，攻击者可以得知SUPI，除非一个诚实的用户设备将所有隐私信息（SUPI和 \mathrm{s}{\mathrm{k}}_{\mathrm{U}\mathrm{E}}）泄露给攻击者。

认证性目标A1~A6定义的安全需求，要求从认证性目标涉及的所有角度对实体身份标识符等信息（SUPI、idSEAF以及k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}）进行认证。以A1为例，用户设备与基站之间的弱认证目标，需要分别从用户角度、基站角度对另一方的身份进行认证。图7是从用户设备角度与基站建模的认证性引理，该引理用于描述认证性目标A1。

图7中引理的含义是：对于任意的用户设备和基站而言，当用户设备认为与基站关于信息t共同运行了协议（使用标签Commit标记），那么在这之前一定存在基站与用户设备运行了协议会话（使用标签Running标记），但可能是关于另一个信息t₁。

2　 Tamarin Prover证据搜索策略

Tamarin Prover在验证复杂协议模型的安全目标时，容易无法终止证据搜索过程。原因在于Tamarin Prover在寻找协议是否满足安全目标的证据时，模型复杂的状态空间使得其陷入循环，或者搜索过程中状态空间急剧增长使实验平台服务器的计算资源耗尽。5G EAP-TLS协议模型具有庞大的信息流和复杂的状态空间，使得Tamarin Prover在验证其模型的安全目标时无法终止，从而无法完成安全目标的验证。

但是，Tamarin Prover提供了一种手动引导的方式，可以帮助其完成安全目标的验证。这种手动引导的方式可以利用python语言编写引导程序，使得Tamarin Prover可以实现复杂模型下的自动化证据搜索。因此，本文通过对协议安全目标证明过程进行深入分析，提出了相应的证据搜索策略，解决了Tamarin Prover在验证5G EAP-TLS协议模型的安全目标时无法终止的问题，实现了5G EAP-TLS安全目标的自动化验证。

证据搜索策略的编写思路是将Tamarin Prover的安全目标搜索过程分解为多个子目标，并按照优先级进行排序，以此逐步推进证明过程。这种分解和排序的方法可以有效地减少安全目标证明的搜索空间，提高证明效率。

以证明用户设备与统一数据管理关于基站标识符idSEAF的非单射认证性目标证据搜索过程的引导程序为例，如图8所示，可以看出Tamarin Prover验证安全目标时需要解决很多小目标。证据搜索引导策略将这些小目标的解决顺序以数组（rank[]）的形式进行存储，数组序号大代表需优先进行解决。在该认证性目标证明的搜索策略中，使用了re.match函数用来匹配正则表达式对应的目标，并进行排序处理。这样，就可以按照优先级顺序逐个求解问题，既防止状态空间爆炸，又提高了Tamarin Prover的验证效率。

3　 安全分析

3.1　实验环境

本文的实验是在操作系统Ubuntu18.04上完成，处理器为Intel Core i5-8400 2.8 GHz，内存为8 GB，验证工具为Tamarin Prover 1.6.0。

3.2　结果与分析

通过证据搜索策略引导Tamarin Prover对5G EAP-TLS协议模型中的机密性目标C1、C2以及认证性目标A1~A6进行了自动化验证，验证结果如图9。

通过对Tamarin Prover验证的结果进行分析，绘制了表3。

结合表3可知，5G EAP-TLS协议能够满足机密性目标，但是不满足认证性目标。通过Tamarin Prover给出的违反认证目标的攻击路径，本文识别出了该协议存在两种安全问题：

1） 存在拒绝服务（denial of service，DoS）攻击风险。在分析协议不满足认证性目标A6的情况时，从Tamarin Prover给出的攻击路径中识别出了DoS攻击，在AKA阶段，认证服务器与用户设备完成一系列认证和密钥协商，派生密钥并将密钥发送给基站，基站等待用户设备使用密钥进行后续通信，然而，用户设备未进行密钥派生，浪费认证服务器资源。

该攻击有两种实现途径：第一种是攻击者截获用户设备和基站之间的信号信息（\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{T}\mathrm{L}\mathrm{S}或\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}）；在图4的步骤⑦和⑧，如果认证服务器没有收到\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{T}\mathrm{L}\mathrm{S}消息，用户设备没有收到\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}消息，那么认证服务器或用户设备都不能顺利完成认证和密钥协商过程。第二种是攻击者替换用户设备收到的基站的标识符\mathrm{i}\mathrm{d}\mathrm{S}\mathrm{E}\mathrm{A}\mathrm{F}，用户设备将使用错误的基站标识符生成密钥，无法进行后续通信。

2） 可能导致用户通信数据泄露。在分析协议不满足认证性目标A5的情况时，从Tamarin Prover给出的攻击路径中发现了用户设备可能与错误的基站进行后续加密会话通信。如果在初始化过程中传输信息的基站与认证协商过程中传输信息的基站不是同一个基站，并且该基站受攻击者控制，可能导致用户后续通信被窃听，用户通信内容等隐私数据泄露。

该攻击主要通过以下途径实现：在初始化阶段，当监听到正常的用户设备发送接入请求，由基站A进行转发；此时，攻击者发送伪造的接入请求，并且攻击者要将该接入请求通过其控制的基站B转发；当两个并发接入请求连同基站标识符同时转发给认证服务器，经由统一数据管理处理后，认证服务器可能无法识别之后通过哪一个基站与用户设备完成认证和密钥协商过程，从而可能选择与错误的基站进行通信。

通过进一步分析，本文发现5G EAP-TLS协议不满足认证性目标和存在安全问题的原因主要包括以下两点：

1） 用户设备、基站、认证服务器、统一数据管理之间的信息确认过程不完善。由图4可知，当基站收到SUPI和k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}等信息，认证服务器已经完成了其认证流程，认证服务器无法获知后续事件，即用户设备派生密钥，也就无法对用户设备是否生成了正确的密钥进行确认，因此认证服务器不能满足与用户设备关于密钥k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}的单射认证性目标A6；此外，当用户设备收到\mathrm{E}\mathrm{A}\mathrm{P}\_\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}消息派生k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}时，基站已经完成了认证以及密钥协商阶段中的任务，基站不知道后续用户是否会派生出密钥信息，使得基站与用户设备之间也无法达成关于密钥k_{\mathrm{s}\mathrm{e}\mathrm{a}\mathrm{f}}的单射一致性。同理，协议违反了认证目标A4的原因也是如此；以统一数据管理与基站关于SUPI的认证为例，统一数据管理在步骤②将SUPI等信息告知认证服务器，统一数据管理不参与后续过程，无法得知基站是否获得了SUPI，也就无法与基站关于SUPI达成一致。因此，由于实体之间的信息确认过程不完善，使得认证过程无法完成，将导致用户设备无法接入网络。

2） 初始化阶段，统一数据管理与认证服务器缺乏对于基站标识符的验证。导致用户通信数据泄露问题的原因在于，认证服务器向统一数据管理发送的连接请求信息中包含的是SUCI和基站标识符\mathrm{i}\mathrm{d}\mathrm{S}\mathrm{E}\mathrm{A}\mathrm{F}，而统一数据管理接收到连接请求后，向认证服务器发送的却是SUPI和其选择的认证方法。当两个基站同时向认证服务器传输信息时，两个并发请求同时到达认证服务器，根据统一数据管理返回的信息，认证服务器无法确认SUPI与\mathrm{i}\mathrm{d}\mathrm{S}\mathrm{E}\mathrm{A}\mathrm{F}的对应关系，致使与用户设备、认证服务器进行通信的基站和初始化阶段发送连接请求的基站可能不一致，导致用户设备与统一数据管理，认证服务器与统一数据管理之间无法关于基站标识符达成一致，可能导致用户设备、认证服务器与错误的基站完成密钥协商过程，并由该错误的基站负责后续通信。

3.3　安全问题的补丁方案

基于上述分析，为了使5G EAP-TLS协议满足既定的安全目标（包括机密性目标C1、C2，和认证性目标A1~A6），需要在初始化阶段增加统一数据管理向认证服务器发送信息的内容，以及认证服务器向基站发送信息的内容，便于认证服务器对基站以及基站对统一数据管理进行识别，同时，需要在5G EAP-TLS协议的认证和密钥协商阶段后增加密钥和SUPI等信息的确认过程。基于此本文提出了如图10所示的补丁方案。

在初始化阶段，在步骤②统一数据管理向认证服务器发送的信息中，增加了基站标识符idSEAF信息。认证服务器基于基站标识符能够识别出发送SUPI信息的基站，从而避免了用户设备与错误基站通信导致的通信数据泄露问题；同时，在步骤②认证服务器向基站发送的信息中，增加了统一数据管理标识符idUDM，使得基站能够对统一数据管理的身份进行验证。

此外，在认证以及密钥协商阶段之后增加额外的确认过程（即步骤⑨和步骤⑩）。在确认过程中，本文采用了散列密钥及实体类型的方式，增加了认证服务器向统一数据管理发送用户永久订阅符SUPI和基站标识符idSEAF，以实现密钥确认、统一数据管理对用户设备以及基站的认证。由于基站需要分别向用户设备和认证服务器进行密钥确认，为了防止攻击者获取到一次散列值从而推出二次散列值，本文采取了先二次散列再一次散列的方式。通过以上方式，用户设备、基站、认证服务器以及统一数据管理之间可以实现相互认证，用户设备、基站与认证服务器之间可以关于密钥达成一致。

最后，通过提出的证据搜索策略引导Tamarin Prover工具对该补丁方案的有效性进行了验证，验证结果表明该方案能够满足既定的安全目标。

4　 结 语

本文对5G EAP-TLS协议进行了详细的描述和全面的形式化建模，对5G规范中涉及的所有协议实体及证书分发机制进行了建模，并从5G规约中提取和建模了协议相关的安全目标，对符号分析工具Tamarin Prover的证据搜索过程进行了优化，提出了引导Tamarin Prover自动化验证的证据搜索策略。在此基础上，利用Tamarin Prover对安全目标进行了自动化验证。

通过对验证结果的分析，从违反安全目标的攻击路径中识别出了DoS攻击。攻击者可以在用户设备和基站之间的公共信道中拦截信号数据包，使得用户设备无法与基站及认证服务器完成认证以及密钥协商阶段，这意味着随后的通信无法得到有效保护。此外，还发现5G EAP-TLS协议在初始化阶段缺少对于基站标识符的验证，可能导致用户设备与错误的基站通信，进而导致用户通信数据泄露。针对5G EAP-TLS协议存在的安全问题，提出了相应的补丁方案，在初始化阶段的认证以及密钥协商阶段之后增加额外的验证和确认过程，并通过证据搜索策略引导符号分析工具Tamarin Prover自动化验证了该补丁方案的有效性。

分析5G EAP-TLS在安全通道被破坏的强大威胁模型下是否能满足相应的安全目标是我们未来需要做的工作。

参考文献

[1] AIJAZ A. Private 5G： The future of industrial wireless［J］. IEEE Industrial Electronics Magazine， 2020， 14（4）： 136-145. DOI： 10.1109/MIE.2020.3004975 .

[2] KECHICHE S. Securing Private Networks in the 5G Era ［EB/OL］. ［2021-06-01］.

[3] ZHANG J 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）. New York： IEEE Press， 2019： 503-509. DOI： 10.1109/DSC.2019.00082 .

[4] 王跃东， 熊焰， 黄文超， 等. 一种面向5G专网鉴权协议的形式化分析方案［J］. 信息网络安全， 2021， 21（9）：1-7. DOI：10.3969/j.issn.1671-1122.2021.09.001 .

[5] WANG Y D， XIONG Y， HUANG W C， et al. A formal analysis scheme for 5G private network authentication protocol［J］. Netinfo Security， 2021， 21（9）：1-7. DOI：10.3969/j.issn.1671-1122.2021.09.001（Ch ）.

[6] 陈丽萍， 徐鹏， 王丹琛，等. EAP-TLS协议的形式化验证研究［J］. 计算机科学， 2022， 49（11A）： 211100111-5. DOI： 10.11896/jsjkx.211100111 .

[7] CHEN L P， XU P， WANG D C， et al. Study on Formal Verification of EAP-TLS Protocol［J］. Computer Science， 2022， 49（11A）：211100111-5. DOI：10.11896/jsjkx.211100111 .

[8] CORTIER V， KREMER S， WARINSCHI B. A survey of symbolic methods in computational analysis of cryptographic systems［J］. Journal of Automated Reasoning， 2011， 46（3）： 225-259. DOI： 10.1007/s10817-010-9187-9 .

[9] BLANCHET B. Security protocol verification： Symbolic and computational models［C］//International Conference on Principles of Security and Trust. Berlin： Springer， 2012： 3-29. DOI：10.1007/978-3-642-28641-4_2 .

[10] MEIER S， SCHMIDT B， CREMERS C， et al. The TAMARIN prover for the symbolic analysis of security protocols［C］//International Conference on Computer Aided Verification. Berlin： Springer， 2013： 696-701. DOI： 10.1007/978-3-642-39799-8_48 .

[11] CREMERS C J F. The scyther tool： Verification， falsification， and analysis of security protocols［C］//International Conference on Computer Aided Verification. Berlin： Springer， 2008： 414-418. DOI： 10.1007/978-3-540-70545-1_38 .

[12] BASIN D， MÖDERSHEIM S， VIGANÒ L. OFMC： A symbolic model checker for security protocols［J］. International Journal of Information Security， 2005， 4（3）： 181-208. DOI： 10.1007/s10207-004-0055-7 .

[13] BLANCHET B. Modeling and verifying security protocols with the applied pi calculus and ProVerif［J］. Foundations and Trends® in Privacy and Security， 2016， 1（1/2）： 1-135. DOI： 10.1561/3300000004 .

[14] ARAPINIS M， RITTER E， RYAN M D. StatVerif： verification of stateful processes［C］//2011 IEEE 24th Computer Security Foundations Symposium. New York： IEEE Press， 2011： 33-47. DOI： 10.1109/CSF.2011.10 .

[15] LING X， JI S L， ZOU J X， et al. DEEPSEC： A uniform platform for security analysis of deep learning model［C］//2019 IEEE Symposium on Security and Privacy （SP）. New York： IEEE Press， 2019： 673-690. DOI： 10.1109/SP.2019.00023 .

[16] XIONG Y， SU C， HUANG W C， et al. Smartverif： Push the limit of automation capability of verifying security protocols by dynamic strategies［EB/OL］. ［2020-08-12］. DOI: 10.3390/rs12030450 .

[17] CREMERS C， KIESL B， MEDINGER N. A formal analysis of IEEE 802.11’s wpa2： Countering the kracks caused by cracking the counters ［C］// Proceedings of the 29th USENIX Security Symposium. Berkeley： USENIX Association， 2020：1-17.

[18] BASIN D， SASSE R， TORO-POZO J. The EMV standard： Break， fix， verify［C］//2021 IEEE Symposium on Security and Privacy （SP）. New York： IEEE Press， 2021： 1766-1781. DOI： 10.1109/SP40001.2021.00037 .

[19] KÜNNEMANN R， STEEL G. YubiSecure？ formal security analysis results for the Yubikey and YubiHSM［C］//International Workshop on Security and Trust Management. Berlin： Springer， 2013： 257-272. DOI： 10.1007/978-3-642-38004-4_17 .

[20] ETSI. TS 33.501： Security architecture and procedures for 5G system（V17.0.0） ［S/OL］. ［2020-12-16］.

[21] ABOBA B， SIMON D. PPP EAP TLS authentication protocol［EB/OL］. ［2021-06-19］. DOI: 10.17487/rfc2716 .

[22] SIMON D， HURST R， ABOBA B. The EAP-TLS Authentication Protocol［EB/OL］. ［2021-07-26］. DOI: 10.17487/rfc5216 .

[23] DIERKS T， RESCORLA E. RFC 5246 - The transport layer security （TLS） protocol version 1.2［EB/OL］. ［2021-08-06］. DOI: 10.17487/rfc5246 .

[24] LOWE G. A hierarchy of authentication specifications［C］//Proceedings 10th Computer Security Foundations Workshop. New York： IEEE Press， 2002： 31-43. DOI： 10.1109/CSFW.1997.596782 .

基金资助

国家重点研发计划(2021YFB2700200)

国家自然科学基金(61772383)

国家自然科学基金(U1836202)

国家自然科学基金(62076187)

国家自然科学基金(62172303)