适用于电力5G终端的二次认证方法及其形式化分析

马媛媛，李尼格，邵志鹏，徐子超

（1.国网智能电网研究院有限公司，南京 210003；2.国家电网公司信息网络安全实验室，南京 210003；3.国网浙江省电力有限公司信息通信分公司，杭州 310007）

随着5G 的到来，电力物联网的发展有了新的前景和机遇。另一方面，设备安全接入挑战更加严峻。为满足垂直行业的高安全要求，5G 网络提出了二次认证架构[1]，采用可扩展身份认证协议（EAP）实现用户终端与数据网络之间的二次认证，满足不同业务的安全要求。在海量接入场景下，连接到物联网的设备具有性质迥异、数量庞大的特点，需要对每个终端逐一认证，带来了认证成本高、效率低的问题。

通过聚合签密技术，每台物联网设备都可以对采集到的数据进行签密[2]，并将签密后的密文发送到指定设备。设备通过聚合算法将接收到的有符号加密密文进行聚合，得到长度非常小的密文发送到处理中心。最后，处理中心对已签名加密的密文进行验证和解密，同时实现设备的身份认证和发送数据的可靠性检验。

在以往的移动通信系统中，针对认证和密钥协议的攻击层出不穷。随着协议本身复杂性的不断增加，以及攻击者攻击能力（如转发、篡改、伪造等）的不断提高，协议中存在的安全漏洞难以人工识别[3]。过去已经开发了许多安全协议的模型检查器，例如ProVerif，TAMARIN 和Scyther。

本文提出了一种适用于电力5G 终端的二次认证方法，该方法在电力5G 终端二次认证的流程引入无证书聚合签密技术，相比传统的公钥密码体制，在保证安全性的同时具有计算和存储空间消耗少和运行效率高的特点，同时避免了传统公钥密码体制中的证书管理问题和基于身份的公钥密码体制中的密钥托管问题。对于适用于电力物联网鉴权和密钥协商采用的5G EAP-TLS 协议，借助ProVerif 工具进行形式化验证，找出潜在的漏洞并提出修正方案。

1 二次认证方案

为了克服现有技术中认证成本高、效率低的缺陷，提出了一种适用于电力5G 终端二次认证的基于聚合签密的二次认证方法，流程如图1所示。该方法包括：

图1 基于聚合签密的二次认证方法流程Fig.1 Flow chart of secondary authentication method based on aggregated signcryption

采用标准模型下高效的基于口令认证密钥协商协议[4]，建立密钥传输的安全通道。二次认证触发模块接收到特定的事件触发后，检查主认证是否已通过。在5G 和电力通信网混合组网架构中，企业专有5G 设备与Internet 服务器之间没有本地流量路径，因此流量必须到达运营商边缘云中的UPF，然后通过专线回到企业内部，与企业局域网设备进行通信。为企业中的5G 设备提供5G 应用服务的MEC位于移动运营商边缘云中。因此，认证请求报文通过接入网和承载网进入运营商核心网的UPF 进行流量卸载，然后送入企业内网的DN-AAA 服务器。

DN-AAA 服务器响应报文，生成基于随机数和时间戳的挑战码，采用基于椭圆曲线有限域的无证书签密方案签密，将签密消息发送到电力5G 终端。电力5G 终端的二次认证模块解签密得到挑战码，判断所述DN-AAA 服务器的网络身份认证是否通过。身份认证通过后，电力5G 终端对挑战码和电力5G 终端的身份认证码采用基于椭圆曲线有限域的无证书签密方案进行签密。

签密消息通过接入网和承载网进入本地厂站端UPF 进行流量卸载，然后送入MEC 设备进行聚合处理。根据不同的业务类型，形成不同的业务流向。互联网大区业务及管理大区低带宽非实时的业务经由部署在核心网的MEC/UPF 处理后，经5G 网络EAP 通道返回给AAA 服务器。生产控制大区以及管理信息大区高带宽低延时高可靠的业务经由部署在电网厂站端的MEC/UPF 处理后，通过正反向隔离装置，经5G 网络EAP 通道返回给AAA 服务器。

DN-AAA 服务器进行聚合解签密，判断所述电力5G 终端的身份认证是否通过。身份认证通过后，DN-AAA 服务器发送身份认证成功声明到所述电力5G 终端，成功建立电力5G 终端建立到数据网络的连接。

为增强二次认证过程中密钥生成中心KGC、电力5G 终端、认证服务器之间密钥传输的安全性，采用标准模型下高效的基于口令认证密钥协商协议，建立密钥传输的安全通道。在带外方式分配简单口令给KGC、5G 终端、认证服务器后，利用口令认证密钥交换（PAKE）协议使得共享低熵口令的用户通过不安全的公共信道安全地生成共享的高熵会话密钥，从而建立密钥传输的安全通道。KGC 和5G 终端通过该密钥协商协议进行密钥交换的步骤包括：

1）5G 终端选取一个随机数，利用公开参数计算消息发送给KGC；

2）KGC 收到5G 终端的消息后，选取一个随机数，利用公开参数计算消息和认证信息发送给5G终端；

3）5G 终端收到消息和认证信息后，利用公开参数对认证信息进行验证，对5G 终端收到的消息利用公开参数计算，将得到的值与认证信息相比较，一致则通过验证。验证通过后计算出确认消息和高熵会话密钥sk，将该密钥作为和KGC 共享的会话密钥，并将确认消息发送给KGC；

4）KGC 收到确认消息后，利用前面的计算结果验证确认消息。代入公开参数计算，将得到的值与确认消息相比较，一致则通过验证。验证通过后，利用公开参数计算出高熵会话密钥sk；

5）利用高熵会话密钥sk，KGC 和5G 终端之间可以建立安全通道传输密钥。

聚合签密采用基于椭圆曲线有限域的无证书签密方案。聚合签密由多个签名者、一个签密聚合者和一个验证者组成，这里的参与者分别为电力5G终端、MEC 上的聚合中心、DN-AAA 服务器。

聚合签密阶段步骤包括：

1）密钥生成中心KGC 进行系统初始化。KGC选取随机数作为主密钥，并计算主公钥；

2）KGC 广播选取参与运算的公开参数；

3）电力5G 终端、聚合中心、DN-AAA 服务器选取随机数作为长期私钥，根据公开参数计算出对应公钥，得到公私钥对，并将公钥通过已建立的安全通道发送给KGC，进行注册；

4）KGC 根据公开参数计算出电力5G 终端的部分私钥，通过已建立的安全通道发送给对应终端。同样，KGC 计算出聚合中心、DN-AAA 服务器的部分私钥，并通过安全通道发送到终端；

5）电力5G 终端对挑战码和身份认证码进行签密；

6）签密消息聚合处理；

7）DN-AAA 服务器对5G 电力终端返回的应答解签密。

该方法在电力5G 终端二次认证的流程引入无证书聚合签密技术，相比传统的公钥密码体制，在保证安全性的同时具有计算和存储空间消耗少和运行效率高的特点，同时又避免了传统公钥密码体制中的证书管理问题以及基于身份的公钥密码体制中的密钥托管问题。

2 形式化分析

本文基于TS 33.501 文档构建5G EAP-TLS 协议模型，采用ProVerif 验证工具验证协议的安全属性并修正。

2.1 协议描述

TS33.501 文档中描述了3 个不同的鉴权协议，分别是5G AKA 协议、5G EAP-AKA’ 协议及5G EAP-TLS 协议。其中，5G EAP-TLS 协议主要用于5G 专网或IoT 场景下的鉴权和密钥协商。该协议以TLS 协议为基础，包含多种密钥协商模式[5]。5G EAPTLS 协议有4 个参与方：

1）UE（用户设备），存储HN（本地网络）公钥pk、用户的身份SUPI 以及共享长期密钥，主要构成为USIM。

2）SEAF（安全锚功能），SN（服务网络）的主要参与实体。

3）AUSF（身份认证服务器），本地网络的参与实体，负责判断SEAF 实体的授权与否、生成锚定密钥KSEAF 以及验证来自UE 的认证响应的正确性。

4）ARPF（身份认证凭证存储和处理），本地网络的参与实体，负责存储保密信息、授权SUPI 以及生成认证向量，保存本地网络私钥sk，解析SUCI 获取SUPI。

TS33.501 提出的5G EAP-TLS 认证协议的详细步骤如图2所示。

图2 5G EAP-TLS 认证协议Fig.2 5G EAP-TLS authentication protocol

2.2 形式化模型

使用形式化分析工具分析安全协议，可以更有效地发现协议设计缺陷[6]。本文使用形式化分析工具ProVerif 对5G EAP-TLS 过程进行建模和分析。

ProVerif 主要用于与密码学相关的安全协议的自动验证。其基础是函数约简的等价理论、项目和过程的定义、扩展过程之间的结构等价、内部约简等规则[7]。ProVerif 现在已经成功地验证和分析了许多复杂的安全协议。

ProVerif 使用Applied Pi 演算描述来建模分布式系统及其交互，经过处理模块转换成Horn 子句。ProVerif 的整体结构由协议输入、分析验证和结果输出3 部分组成，如图3所示。

图3 ProVerif 工具整体结构Fig.3 Overall structure of the ProVerif tool

ProVerif 可以输出网页展示结果。如果协议是安全的，则不需要证明，直接输出结果。如果验证表明某个安全属性不满足，并且该属性是目标可达的，则ProVerif 将攻击重构。

ProVerif 中对5G EAP-TLS 协议形式化建模，需要建模协议的交互过程，以及需要验证的属性描述。

根据5G EAP-TLS 的协议流程[8]，对信道建模：c1 代表UE 和SEAF 之间通信的公共信道，c2 代表SEAF 和AUSF 之间的私密信道，c3 代表AUSF 和ARPF 之间的私密信道。

分别对UE，SN，HN 流程进行建模。首先生成用于非对称加密和签名的私钥，并在通道c1，c2 和c3上输出相应的公钥。SEAFN 是用于派生锚密钥的服务网络名称。它也在公共频道上广播，攻击者可以访问。然后，协议过程是UE，SEF，AUSF 和UDM 过程无限复制的并行组合。

基于3GPP 描述的一些安全要求，通过对协议流程和安全要求的分析，对以下安全属性建模[9]：

认证属性：

A1：家庭网络和用户应就预主密钥Rprekey 达成一致。

A2：家庭网络和用户应就彼此的身份达成一致。

保密属性：

S1：攻击者无法获得诚实用户的预主密钥Rprekey。

S2：攻击者无法获得诚实用户的会话密钥Ksession。

S3：攻击者无法获取诚实用户的身份SUPI。

认证属性由通信断言捕获，它可以以“如果协议中执行了某个事件，那么之前执行过另一个事件”的形式表示事件之间的关系。在ProVerif 中，事件的形式是event e（M1，…，Mn），对应断言的查询是：

query x1：t1，...，xn：tn；event（e（M1，...，Mj））==＞

event（e’（N1，...，Nk））.

考虑以下通信断言来证明认证属性：

query x：bitstring；inj-event（endAUSF（x））

==＞inj-event（acceptUE（x））.

query x：bitstring；inj-event（endUE（x））

==＞inj-event（acceptAUSF（x））.

query x：key；inj-event（acceptPrek（x））

==＞inj-event（sendPrek（x））.

为了证明M 项的保密性，ProVerif 本质上解决了一个可达性问题，即攻击者是否能达到M 项可用的状态。ProVerif 在协议模型中进行以下查询，以检查预主密钥Rprekey、会话密钥Ksession 和用户身份SUPI 的保密性：

query attacker（Rprekey）

query attacker（Ksession）

query attacker（SUPI）

2.3 实验结果分析

程序运行结果如图4所示。

图4 运行结果Fig.4 Operation result

结果表明，所有的保密属性（即S1，S2 和S3）都满足，而认证属性（即A1 和A2）则被违反。

输出结果还包含了违反认证属性的推导过程，如图5所示。

图5 违反认证属性过程Fig.5 Process of violation of authentication attribute

A1 属性要求成功终止后，家庭网络和用户应就预主密钥Rprekey 达成一致。攻击者可以采用中间人攻击，在用户和家庭网络之间拦截和转发消息[10]。当用户认为已经与家庭网络建立了预主密钥Rprekey，此时家庭网络认为预主密钥正在建立，因此违反了该属性。

A2 属性要求成功终止后，家庭网络和用户应就彼此的身份达成一致。但是在当前的5G EAP-TLS协议中，攻击者能够轻松伪造用户和家庭网络之间的明文握手消息，模拟家庭网络并与用户建立连接。用户无法验证家庭网络的身份，因此违反了该属性。

针对攻击者的可能攻击路径，提出了一种可能的修复方案，将用户和家庭网络之间用于验证的消息进行加密处理，避免攻击者拦截并伪造消息，模拟家庭网络并与用户建立连接。同时在家庭网络和用户建立预主密钥Rprekey 的过程中增加挑战－应答机制，避免中间人攻击的发生。

3 结语

二次认证是3GPP 为满足垂直行业的高安全需求提出的新的架构，如何进一步提高5G 业务的安全性和可用性，是一项亟待解决的问题。本文提出了一种适用于电力5G 终端的二次认证方法，该方法在电力5G 终端二次认证的流程引入无证书聚合签密技术，相比传统的公钥密码体制，在保证安全性的同时具有计算和存储空间消耗少和运行效率高的特点，同时又避免了传统公钥密码体制中的证书管理问题以及基于身份的公钥密码体制中的密钥托管问题。对于适用于电力物联网鉴权和密钥协商采用的5G EAP-TLS 协议，借助ProVerif 工具进行形式化验证，找出潜在的漏洞并提出修复方案。