適用于電力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 工具進行形式化驗證，找出潛在的漏洞并提出修復方案。