基于Tamarin 的5G AKA 協(xié)議形式化分析及其改進方法*

劉 鏑, 王梓屹, 李大偉, 關(guān)振宇, 孫 鈺, 劉建偉

北京航空航天大學(xué)網(wǎng)絡(luò)空間安全學(xué)院, 北京 100191

1 引言

移動用戶通過全球用戶身份模塊(universal subscriber identity module, USIM) 卡連接到移動網(wǎng)絡(luò),用戶和運營商都希望從所使用的通信協(xié)議中得到安全保證, 比如用戶語音、短信的保密性等. 鑒權(quán)和密鑰協(xié)商協(xié)議(authentication and key agreement, AKA) 能夠?qū)崿F(xiàn)用戶和運營商網(wǎng)絡(luò)之間的相互認證, 并完成協(xié)商會話密鑰的工作, 且能建立一個安全信道來保證后續(xù)通信和數(shù)據(jù)傳輸?shù)陌踩?

攻擊者可能會利用通信協(xié)議存在的安全漏洞來發(fā)起攻擊, 這將嚴重威脅個人隱私、財產(chǎn)安全. 5G 通信的安全嚴重依賴于5G AKA 協(xié)議的安全性, 因此對5G AKA 協(xié)議的安全性分析顯得尤為重要, 但是協(xié)議流程的復(fù)雜性使得很難通過人工的方式去發(fā)現(xiàn)其安全漏洞. 本文利用安全協(xié)議驗證工具Tamarin 對5G AKA 協(xié)議進行形式化分析, 以便更好地發(fā)現(xiàn)其安全漏洞, 從而促進協(xié)議標準的改進和完善, 使得5G AKA 協(xié)議在5G 網(wǎng)絡(luò)全面商用后為用戶和運營商提供更好的安全保證.

5G AKA 協(xié)議用于實現(xiàn)用戶和運營商網(wǎng)絡(luò)之間的身份驗證和密鑰協(xié)商, 涉及到的實體有用戶設(shè)備(user equipment, UE)、用戶在近距離內(nèi)連接的服務(wù)網(wǎng)絡(luò)(serving network, SN) 和與用戶對應(yīng)的運營商歸屬網(wǎng)絡(luò)(home network, HN). 服務(wù)網(wǎng)絡(luò)SN 中包括安全錨點功能(security anchor function, SEAF),歸屬網(wǎng)絡(luò)HN 中包括鑒權(quán)服務(wù)功能(authentication server function, AUSF)、鑒權(quán)證書庫和處理功能(authentication credential repository and processing function, ARPF).

1.1 相關(guān)工作

在3G 網(wǎng)絡(luò)時代, AKA 協(xié)議的安全性大多是通過使用TLA 和BAN 邏輯[1]手動進行驗證, 這種驗證方式只考慮了很簡單的威脅模型, 也只能提供很弱的安全保證, 并不適用于現(xiàn)在的使用場景. 為了提高協(xié)議的設(shè)計效率, 研究人員開始使用ProVerif、Scyther、AVISPA、Tamarin 等自動化的安全協(xié)議驗證工具來對協(xié)議進行形式化分析. 比如, Arapinis 等人[2]用ProVerif 分析了3G 網(wǎng)絡(luò)中的AKA 協(xié)議, 發(fā)現(xiàn)了針對用戶位置和身份匿名性的攻擊, 并提出了對應(yīng)的解決方案.

在4G 網(wǎng)絡(luò)時代, Hussain 等人[3]結(jié)合符號模型檢查和密碼協(xié)議驗證提出一種基于模型的測試化方法, 使用ProVerif 分析了4G 網(wǎng)絡(luò)中的EPS AKA 協(xié)議, 發(fā)現(xiàn)了鑒權(quán)重放攻擊和對用戶位置的欺騙攻擊等, 但是并沒有提出具體的防御措施. 隨著5G 技術(shù)的發(fā)展, 逐漸形成了4G 網(wǎng)絡(luò)和5G 網(wǎng)絡(luò)共存的局面,許多研究者開始對5G AKA 協(xié)議進行分析. Ferrag 等人[4]對4G 和5G 網(wǎng)絡(luò)中的鑒權(quán)和隱私保護方案進行了較為全面的研究, 總結(jié)了相應(yīng)的應(yīng)對策略和形式化及非形式化的安全分析技術(shù), 為未來5G 網(wǎng)絡(luò)安全的研究方向提供了思路.

在5G AKA 協(xié)議的形式化分析方面. Basin 等人[5]使用Tamarin 對5G AKA 協(xié)議進行了形式化分析. 基于3GPP TS 33.501 v15.1.0 版本[6], 針對從5G 安全標準中提取出的安全目標, 提供了第一個5G AKA 協(xié)議形式化模型, 但是作者把AUSF 和ARPF 兩個實體建模為一個大的HN 實體, 并不能準確的刻畫5G AKA 協(xié)議的流程. Cremers 等人[7]基于3GPP TS 33.501 v0.7.0 版本[8], 把HN 中的AUSF和ARPF 分別單獨建模為兩個參與實體, 對5G AKA 協(xié)議進行了分析, 發(fā)現(xiàn)了一種由會話競爭導(dǎo)致的攻擊, 但是他們分析的協(xié)議版本過于老舊, 并且只分析了UE、SN 和HN 之間的部分鑒權(quán)性質(zhì). Edris 等人[9]基于3GPP TS 33.501 v15.5.0 版本, 使用ProVerif 對5G AKA 協(xié)議進行了系統(tǒng)的安全性評估, 但是對于發(fā)現(xiàn)的問題并沒有給出有效的解決方法.

Cao 等人[10]針對5G 網(wǎng)絡(luò)海量設(shè)備并發(fā)連接的場景, 設(shè)計了一種輕量級的安全接入認證協(xié)議, 并使用ProVerif 和Scyther 兩種工具對該協(xié)議進行了形式化分析. 也有研究人員[11,12]使用AVISPA 對5G AKA 協(xié)議的相關(guān)變體協(xié)議進行了形式化分析. 這些工作都對5G AKA 協(xié)議的形式化分析帶來了啟發(fā),但由于ProVerif 中的異或運算是通過用戶自定義方程來實現(xiàn)且其支持驗證的安全性質(zhì)有限, 而Scyther、AVISPA 不能自定義安全性質(zhì)且支持的密碼學(xué)運算較少. 這些工具在協(xié)議的形式化分析上都存在著相應(yīng)的局限性.

目前國內(nèi)外學(xué)者對5G AKA 協(xié)議的形式化分析大多基于3GPP 組織發(fā)布的5G 技術(shù)規(guī)范中的R15標準或者R15 之前的標準, 而在新發(fā)布的R16[13]、R17 標準中對5G AKA 協(xié)議的鑒權(quán)流程進行了幾個大的修改, 這些修改對5G AKA 協(xié)議安全性的影響需要再次被評估. 5G 技術(shù)規(guī)范中最新的R17 標準已于2020 年12 月發(fā)布, 與R16 標準相比, R17 標準中的5G AKA 協(xié)議僅增加了可選的AKMA 功能, 其他并無不同. 因此本文參考R17 標準v17.0.0 版本[14]中的協(xié)議, 選擇內(nèi)置異或等多種運算的Tamarin來綜合評估這些修改對協(xié)議安全性的影響.

1.2 本文貢獻

(1) 本文對新版本5G AKA 協(xié)議和期望其滿足的安全性質(zhì)進行了形式化建模. 搭建的模型[15]可以準確、完整的刻畫5G AKA 協(xié)議的流程, 還可以驗證協(xié)議的相關(guān)安全性質(zhì). 本模型具有很好的擴展性, 可以在本模型的基礎(chǔ)上進行修改來對其他認證和密鑰協(xié)商協(xié)議進行形式化分析.

(2) 本文在Tamarin 中驗證了5G AKA 協(xié)議在安全錨點密鑰KSEAF和長期共享密鑰K上的保密性質(zhì),以及在用戶永久標識符(subscription permanent identifier,SUPI)、服務(wù)網(wǎng)絡(luò)標識符SNID和安全錨點密鑰KSEAF上Lowe 鑒權(quán)性質(zhì)[16]的滿足情況. 發(fā)現(xiàn)在36 條鑒權(quán)性質(zhì)中有23 條沒有得到滿足, 特別是在密鑰KSEAF上的鑒權(quán)性質(zhì)幾乎都沒有滿足, 這表明攻擊者可以發(fā)動針對該密鑰的重放攻擊.

(3) 對于5G AKA 協(xié)議不滿足的鑒權(quán)性質(zhì), 本文參考了Basin[5]和Cremers[7]等人提出的方法, 提出了結(jié)合SNID 綁定、會話綁定、密鑰確認往返三個方面的5G AKA 協(xié)議改進方案. 此方案為未來新版本5G AKA 協(xié)議的設(shè)計和改進提供了新的思路, 并且可以擴展應(yīng)用到EAP-AKA 等協(xié)議的分析上.

(4) 本文根據(jù)提出的綜合改進方案對5G AKA 協(xié)議進行了修改, 并在Tamarin 中重新驗證了改進后的協(xié)議對安全性質(zhì)的滿足情況. 驗證結(jié)果表明, 在改進前的23 條不滿足的鑒權(quán)性質(zhì)中, 有20 條在協(xié)議改進后得到了滿足. 改進后協(xié)議的安全性得到了很大提升.

2 5G AKA 協(xié)議介紹

2.1 蜂窩網(wǎng)絡(luò)架構(gòu)

蜂窩網(wǎng)絡(luò)整體架構(gòu)大致由三個大的邏輯實體組成: 用戶設(shè)備UE、服務(wù)網(wǎng)絡(luò)SN、歸屬網(wǎng)絡(luò)HN. 網(wǎng)絡(luò)架構(gòu)圖如圖1 所示.

圖1 蜂窩網(wǎng)絡(luò)架構(gòu)Figure 1 Cellular network architecture

用戶設(shè)備UE 一般是智能手機或者物聯(lián)網(wǎng)設(shè)備, UE 由移動設(shè)備(mobile equipment, ME) 和USIM卡組成, USIM 卡中存有用戶永久身份標識符SUPI、序列號(sequence number, SQN)、長期對稱密鑰K和公共非對稱密鑰pkHN. SUPI 是一個唯一且永久的用戶身份標識; SQN 是用于驗證鑒權(quán)消息新鮮性的計數(shù)器; 對稱密鑰K是用戶與其對應(yīng)歸屬網(wǎng)絡(luò)HN 中的ARPF 之間的共享密鑰; 公共非對稱密鑰pkHN也對應(yīng)于歸屬網(wǎng)絡(luò)HN, 用于對SUPI 進行加密得到用戶加密標識符(subscription concealed identifier,SUCI).

服務(wù)網(wǎng)絡(luò)SN 主要在漫游場景中和用戶進行通信, 其中的安全錨點功能SEAF 負責(zé)完成對UE 的鑒權(quán)以及協(xié)助UE 和歸屬網(wǎng)絡(luò)HN 之間的鑒權(quán), 在鑒權(quán)成功且與UE 建立安全信道后對UE 提供服務(wù). SN中其它的功能模塊在這里不進行說明.

歸屬網(wǎng)絡(luò)HN 的數(shù)據(jù)庫中也存有序列號SQN、長期共享密鑰K、與公鑰pkHN相對應(yīng)的私鑰等.其中的認證服務(wù)功能AUSF、認證證書庫和處理功能ARPF 負責(zé)向服務(wù)網(wǎng)絡(luò)SN 提供用于認證過程的鑒權(quán)向量, AUSF 會在SEAF 對UE 鑒權(quán)成功后再次鑒權(quán), 用戶標識符解密功能(subscription identifier de-concealing function, SIDF) 負責(zé)將SUCI 解密為SUPI. 因為統(tǒng)一數(shù)據(jù)管理功能(unified data management, UDM) 在鑒權(quán)過程中和ARPF 功能基本一致, 因此本文只對ARPF 進行介紹.

用戶使用配備了USIM 卡的設(shè)備通過不安全的無線信道(在圖1 中用虛線標出) 和SN 中的基站進行通信, SN 和HN 之間以及HN 內(nèi)部的AUSF 和ARPF 之間的通信通過經(jīng)過驗證的有線信道(在圖1 中用實線標出) 進行, 可以認為是安全的.

2.2 5G AKA 協(xié)議的鑒權(quán)流程

5G AKA 協(xié)議使用挑戰(zhàn)-響應(yīng)機制來完成用戶和運營商網(wǎng)絡(luò)之間的身份認證, 同時基于身份認證對通信過程所需的密鑰進行協(xié)商, 是一種雙向的認證機制. 詳細的鑒權(quán)流程如圖2 所示.

圖2 5G AKA 協(xié)議鑒權(quán)流程Figure 2 Authentication procedure for 5G AKA protocol

(1) 當服務(wù)網(wǎng)絡(luò)SN 觸發(fā)和用戶UE 的鑒權(quán), UE 使用其對應(yīng)歸屬網(wǎng)絡(luò)的公鑰pkHN將SUPI 加密為SUCI, 再將SUCI 發(fā)送給SEAF. SEAF 根據(jù)SUCI 中包含的歸屬網(wǎng)絡(luò)標識符選擇用戶對應(yīng)的歸屬網(wǎng)絡(luò)來請求鑒權(quán)材料, 再發(fā)送SUCI 和SNID 給AUSF.

(2) AUSF 將收到的SNID 與預(yù)期的服務(wù)網(wǎng)絡(luò)名稱進行比較. 若一致則會暫時存儲SNID, 再發(fā)送SUCI 和SNID 給ARPF.

(3) ARPF 通過用戶標識符解密功能SIDF 從SUCI 中解密出SUPI,然后選擇鑒權(quán)方式為5G AKA.ARPF 會計算出密鑰KAUSF、參數(shù)XRES* (預(yù)期響應(yīng), expected response), 然后由參數(shù)RAND(一個隨機數(shù))、AUTN (認證令牌, authentication token)、XRES*、KAUSF創(chuàng)建出鑒權(quán)向量5G HE AV (5G home environment authentication vector) 發(fā)送給AUSF.

(4) AUSF 根據(jù)5G HE AV 中的XRES* 計算出其哈希值HXRES*, 根據(jù)密鑰KAUSF計算出KSEAF, 由RAND、AUTN、HXRES*、KSEAF創(chuàng)建出鑒權(quán)向量5G AV (5G authentication vector), 移除密鑰KSEAF得到5G SE AV (5G serving environment authentication vector), 再發(fā)送5G SE AV (RAND、AUTN、HXRES*）給SEAF.

(5) SEAF 接收到AUSF 發(fā)來的5G SE AV 后, 將參數(shù)RAND 和AUTN 發(fā)送給UE.

(6) UE 從AUTN 中提取出MAC (消息認證碼, message authentication code) 和SQN 來驗證鑒權(quán)材料的有效性. 若通過驗證, 則更新自己的SQN, 計算出參數(shù)RES* 和密鑰KSEAF, 再把參數(shù)RES* 發(fā)送給SEAF.

(7) SEAF 計算RES* 的哈希值HRES*, 再比較HRES* 和HXRES* 是否一致. 若不一致則鑒權(quán)失敗, 若一致則從服務(wù)網(wǎng)絡(luò)的角度認為此次鑒權(quán)成功, 再發(fā)送RES* 給AUSF 進行下一步認證.

(8) AUSF 首先驗證鑒權(quán)向量是否過期. 如果過期了, 則AUSF 從歸屬網(wǎng)絡(luò)的角度認為鑒權(quán)失敗; 如果驗證成功, 則AUSF 比較RES* 和XRES* 是否一致. 如果一致, 則AUSF 從歸屬網(wǎng)絡(luò)的角度認為此次鑒權(quán)成功.

(9) 鑒權(quán)成功后, AUSF 會發(fā)送密鑰KSEAF和SUPI 給SEAF. 密鑰KSEAF就會成為安全錨點密鑰, SEAF 會根據(jù)此密鑰來計算后續(xù)通信過程中的其它密鑰.

2.3 相關(guān)參數(shù)的生成流程

5G AKA 協(xié)議的鑒權(quán)流程中涉及到很多的參數(shù)和函數(shù). 下面依據(jù)3GPP 組織發(fā)布的3G 安全結(jié)構(gòu)技術(shù)規(guī)范(TS 33.102) v14.1.0 版本[17], 對鑒權(quán)向量的生成流程和相關(guān)函數(shù)的作用、UE 對鑒權(quán)材料有效性的驗證流程進行說明.

2.3.1 鑒權(quán)向量AV 的生成流程

首先隨機生成一個序列號SQN 和一個隨機數(shù)RAND, 再計算下列各參數(shù):

其中f1、f2 是消息認證函數(shù),f3、f4、f5 是密鑰生成函數(shù),K是與UE 共享的長期對稱密鑰. 計算出上述三個密鑰CK、IK、AK 后, 就可以計算出:

其中KDF 是密鑰派生函數(shù), SHA256 是輸出值長度為256 比特的雜湊函數(shù), 進而可以得到在5G AKA協(xié)議中需要使用的鑒權(quán)向量5G HE AV、5G AV 和5G SE AV:

2.3.2 UE 對鑒權(quán)材料有效性的驗證流程

UE 接收到SEAF 發(fā)來的參數(shù)RAND 和AUTN 之后, 首先通過RAND 計算出匿名密鑰AK, 從AUTN 中提取出序列號SQN 和消息認證碼MAC, 再計算XMAC 和其它參數(shù), 驗證XMAC 和MAC是否相等. 若相等則驗證成功, 再驗證SQN 是否在正確的范圍, 即存儲在UE 處的SQNUE是否小于從AUTN 中提取出的SQN. 具體的計算過程如下:

其中函數(shù)f1-f5 的含義與2.3.1 節(jié)中所述一致. 鑒權(quán)材料有效性驗證成功之后, UE 會計算響應(yīng)RES 發(fā)送給SEAF, 再計算出密鑰KSEAF. 密鑰KSEAF的計算方式與2.3.1 節(jié)中一致.

3 形式化建模

3.1 5G AKA 協(xié)議的建模

Tamarin[18]使用安全協(xié)議理論語言(spthy) 來描述協(xié)議狀態(tài)的轉(zhuǎn)移過程, 用rule 來描述協(xié)議狀態(tài),用lemma 來描述期望驗證的安全性質(zhì). 這二者作為Tamarin 的輸入, 輸出是安全性質(zhì)在所有可能的情況下都成立的結(jié)論或者證明安全性質(zhì)不成立的反例. 在搭建的協(xié)議模型中考慮了4 個參與實體: UE、SEAF、AUSF 和ARPF.

對于存儲在UE 側(cè)的序列號SQN, 將其建模為一個單調(diào)遞增的自然數(shù), 通過一個隨機生成的數(shù)值來初始化SQN, 并假設(shè)攻擊者在協(xié)議運行初始階段不知道SQN 的值, 本文沒有對SQN 失去同步后再重新進行同步的過程進行建模. 在鑒權(quán)初始階段, 服務(wù)網(wǎng)絡(luò)SN 可能會創(chuàng)建一個名為5G-GUPI 的假名來關(guān)聯(lián)用戶標識符SUPI, 以便在后續(xù)會話中識別用戶, 搭建的協(xié)議模型中沒有考慮這一可選機制. 本文也沒有對一些諸如AMF、ABBA 等參數(shù)進行建模, 因為這并不影響協(xié)議分析結(jié)果的準確度, 反而增加了對協(xié)議進行建模的復(fù)雜性.

UE 和SEAF 之間的信道是公共信道, 使用Tamarin 中默認的Dolev-Yao 敵手模型[19]對其進行建模. 攻擊者可以獲取無線公共信道中傳輸?shù)南⒍槐粎f(xié)議參與實體察覺, 在Tamarin 中形式化建模為:[Out(x)]--＞[!KD(x)]. 攻擊者也可以將自己已知的任何消息注入到信道中, 在Tamarin 中形式化建模為: [!KU(x)]--[K(x)]-＞[In(x)].

SEAF 和AUSF 之間以及AUSF 和ARPF 之間的信道認為是安全信道,該信道上傳輸?shù)南⒉荒鼙还粽吒`聽和篡改, 同時攻擊者也不能在該信道上注入自己生成的消息. 使用參數(shù)＜Ch_name,Sender,Receiver＞來標識信道, 分別表示信道名稱、發(fā)送方和接收方[20], 在Tamarin 中形式化建模為:

3.2 安全性質(zhì)的建模

在安全性質(zhì)方面, 本文考慮了保密性質(zhì)和鑒權(quán)性質(zhì). 保密性質(zhì)包括安全錨點密鑰KSEAF和共享密鑰K的保密性; 鑒權(quán)性質(zhì)是基于Lowe 分類法, 包括協(xié)議參與者之間在參數(shù)SUPI、SNID、KSEAF上的非單射一致性, 以及在KSEAF上的單射一致性.

3.2.1 保密性質(zhì)的建模

(1) 安全錨點密鑰KSEAF的保密性質(zhì)

分別從UE、SEAF、AUSF 和ARPF 的角度來考慮密鑰KSEAF的保密性質(zhì). 因為密鑰KSEAF是通過密鑰KAUSF計算出來, 因此攻擊者若獲取了密鑰KAUSF, 就能計算出密鑰KSEAF. 因為密鑰KSEAF是在AUSF 處才計算得到, 在ARPF 處只有密鑰KAUSF, 因此從ARPF 的角度考慮的是密鑰KAUSF的保密性質(zhì).

下面舉例進行說明: 從UE 的角度考慮密鑰KSEAF的保密性質(zhì), 如果UE 聲明會話密鑰是保密的,并且攻擊者沒有危害UE 獲取其密鑰K, 則攻擊者不能夠獲取或者計算出密鑰KSEAF. 在Tamarin 中形式化建模為:

(2) 長期共享密鑰K的保密性質(zhì)

攻擊者一旦獲取了長期共享密鑰K, 就能夠計算出別的參數(shù)和密鑰KSEAF. 可以認為每一個用戶擁有的密鑰K是與用戶標識符SUPI 綁定的, 如果攻擊者不是直接危害UE 獲取到密鑰K, 則攻擊者不能夠獲取到密鑰K. 在Tamarin 中形式化建模為:

3.2.2 鑒權(quán)性質(zhì)的建模

對于協(xié)議參與實體UE、SEAF、AUSF 和ARPF, 本文分別從UE、SEAF 和AUSF 的角度考慮了對其他三個實體在參數(shù)SUPI、SNID 和KSEAF上的鑒權(quán)性質(zhì), 一共有36 種情況. 本文沒有從ARPF 的角度來考慮的原因是AUSF 和ARPF 都屬于歸屬網(wǎng)絡(luò)的一部分, 且ARPF 的作用就是生成鑒權(quán)向量發(fā)送給AUSF, 在這之后并沒有消息再返回給ARPF.

下面舉例進行說明: 從AUSF 的角度, 考慮其和SEAF 在安全錨點密鑰KSEAF上的非單射一致性.AUSF 認為自己和SEAF 完成了一次協(xié)議運行, 協(xié)議涉及到的參與實體是UE、SEAF、AUSF 和ARPF,并且攻擊者沒有獲取UE 的密鑰K, 則至少存在一次SEAF 的協(xié)議運行, SEAF 認為自己和AUSF 在密鑰KSEAF上協(xié)商一致.

4 5G AKA 協(xié)議的驗證分析

4.1 驗證結(jié)果

通過實驗驗證, 本文發(fā)現(xiàn)5G AKA 協(xié)議滿足在安全錨點密鑰KSEAF和長期共享密鑰K上的保密性質(zhì), 5G AKA 協(xié)議對Lowe 鑒權(quán)性質(zhì)的滿足情況驗證結(jié)果如表1 所示.

表1 鑒權(quán)性質(zhì)驗證結(jié)果Table 1 Verification result of authentication properties

表1 中展示了協(xié)議參與實體UE、SEAF、AUSF 和ARPF 之間在參數(shù)SUPI、SNID 和安全錨點密鑰KSEAF上的非單射一致性, 以及在密鑰KSEAF上的單射一致性. 其中符號?代表滿足, 符號× 代表不滿足,KSEAFI代表驗證的是在密鑰KSEAF上的單射一致性.

4.2 結(jié)果分析

對于保密性質(zhì), 并沒有發(fā)現(xiàn)Cremers 等人[7]的論文中描述的一種由會話競爭導(dǎo)致密鑰KSEAF的保密性質(zhì)被違反的攻擊. 本文描述的5G AKA 協(xié)議是TS 33.501 v17.0.0 中的版本, 而該論文參考的是v0.7.0 版本. 相比之下, v17.0.0 版本中5G AKA 協(xié)議的幾個改進之處很好的避免了對密鑰KSEAF保密性質(zhì)的違反, 描述如下:

(1) 在v0.7.0 版本的5G AKA 協(xié)議中, ARPF 計算出鑒權(quán)向量并發(fā)送響應(yīng)消息給AUSF. 在這個消息中并沒有包含SUPI 或SUCI, 如果攻擊者幾乎同時啟動兩個與服務(wù)網(wǎng)絡(luò)的會話, AUSF 將無法區(qū)分來自ARPF 的兩個響應(yīng), 并且可能將錯誤的響應(yīng)和錯誤的用戶相關(guān)聯(lián). 而在v17.0.0 版本中, ARPF 發(fā)送給AUSF 的響應(yīng)消息里包含了SUPI.

(2) 在v0.7.0 版本的5G AKA 協(xié)議中, AUSF 發(fā)送鑒權(quán)向量給SEAF 的消息中包含了安全錨點密鑰KSEAF. 如果發(fā)生了(1) 中描述的會話競爭情況, 攻擊者就可以獲取到合法用戶的密鑰KSEAF來計算通信過程中需要的其它密鑰, 從而假冒合法用戶與服務(wù)網(wǎng)絡(luò)進行通信.

但是在v17.0.0 版本中, AUSF 發(fā)送給SEAF 的鑒權(quán)向量中不包括密鑰KSEAF, 而是在最后對UE鑒權(quán)成功之后才將密鑰KSEAF發(fā)送給SEAF.

對于鑒權(quán)性質(zhì), 從UE 的角度來考慮的大部分鑒權(quán)性質(zhì)都被違反, 而從SEAF 的角度考慮的大部分鑒權(quán)性質(zhì)都得到了滿足. 這跟UE 和SEAF 之間的信道是公共信道有關(guān), 公共信道上的通信更容易受到攻擊. 攻擊者可以在UE 和SEAF 之間的信道上隨意注入SNID, 而UE 并不能分辨其真?zhèn)? 而在派生密鑰KSEAF的過程中需要使用參數(shù)SNID, 導(dǎo)致UE 違反一些鑒權(quán)性質(zhì).

5 協(xié)議改進方法及驗證結(jié)果

5.1 SNID 綁定

通過對Tamarin 輸出的攻擊路徑圖進行分析, 如圖3 所示. 大部分攻擊都發(fā)生在UE 和SEAF 之間的公共信道上, 攻擊者可以截取SEAF 發(fā)送給UE 的消息, 包括RAND 和AUTN, AUTN 的計算需要用到消息認證碼MAC, 但是MAC 并沒有與特定的服務(wù)網(wǎng)絡(luò)標識符SNID 綁定, 攻擊者可以對消息進行篡改再發(fā)送給UE.

圖3 UE 和SEAF 在SNID 上的非單射一致性攻擊路徑Figure 3 Non-injective agreement attack path between UE and SEAF on SNID

通過將SNID 添加到消息認證碼MAC 的計算過程中, 即MAC 的計算方法由原來的MAC =f1(K,(SQN||RAND||AMF)) 修改為MAC =f1(K,(SQN||RAND||SNID||AMF)), 可以使得從UE 的角度考慮的大部分鑒權(quán)性質(zhì)得到滿足. 對協(xié)議進行修改, 再驗證后發(fā)現(xiàn), 只有UE 和SEAF 在參數(shù)SUPI和密鑰KSEAF上的非單射一致性沒有得到滿足. 針對這一情況, 可以通過增加UE 和SEAF 之間的密鑰確認往返過程來解決.

5.2 會話綁定

缺少服務(wù)網(wǎng)絡(luò)和歸屬網(wǎng)絡(luò)之間的會話綁定, 可能導(dǎo)致出現(xiàn)會話競爭情況使得SEAF 和AUSF、ARPF之間的一些鑒權(quán)性質(zhì)被違反. 通過在AUSF 和ARPF 之間以及SEAF 和AUSF 之間的會話中添加一個隨機生成的會話標識符, 來對會話進行綁定, 避免會話沖突, 從而不會出現(xiàn)AUSF 無法區(qū)分來自ARPF 的兩個響應(yīng)消息的情況.

通過增加會話標識符來綁定會話之后, SEAF 和AUSF、AUSF 和ARPF 之間的絕大部分鑒權(quán)性質(zhì)都得到了滿足. 其中, 從SEAF 角度考慮的鑒權(quán)性質(zhì)全部得到滿足, 從AUSF 角度考慮的鑒權(quán)性質(zhì)大部分得到滿足, 但是從AUSF 的角度和SEAF 在密鑰KSEAF上的單射一致性仍然沒有得到滿足. 完整的驗證結(jié)果如表2 所示.

5.3 密鑰確認往返

在增加了SNID 綁定修改之后, 仍然存在UE 和SEAF 在參數(shù)SUPI 和密鑰KSEAF上的非單射一致性沒有得到滿足的情況. 通過在協(xié)議結(jié)束階段SEAF 和AUSF 對UE 鑒權(quán)成功之后增加UE 和SEAF之間的密鑰確認往返過程, 可以解決上述問題. 從UE 的角度來看, SNID 綁定和密鑰確認往返的作用是類似的, 并且可以減少往返次數(shù), 使得密鑰確認往返成為多余的步驟, 鑒權(quán)協(xié)議的效率也更高.

5.4 驗證結(jié)果

通過結(jié)合上述三種協(xié)議改進方法對5G AKA 協(xié)議進行改進后, 協(xié)議對鑒權(quán)性質(zhì)的滿足情況驗證結(jié)果如表2 所示. 表2 中的符號表示含義與表1 中一致. 與表1 中的驗證結(jié)果相比, 絕大部分鑒權(quán)性質(zhì)都已經(jīng)得到了滿足. 表2 中未得到滿足的三種情況分別是: AUSF 對SEAF 在SUPI 上的非單射一致性、AUSF 對SEAF 在密鑰KSEAF上的非單射一致性和單射一致性.

表2 協(xié)議改進后的鑒權(quán)性質(zhì)驗證結(jié)果Table 2 Verification result of authentication properties after the protocol is improved

從AUSF 角度和SEAF 的相關(guān)鑒權(quán)性質(zhì)未被滿足的原因是: AUSF 是在對UE 鑒權(quán)成功之后才將包含密鑰KSEAF和參數(shù)SUPI 的消息發(fā)送給SEAF. SEAF 接收到消息之后, 協(xié)議的鑒權(quán)流程就結(jié)束了, 在這之后SEAF 并沒有再和AUSF 進行交互, AUSF 也并不知道SEAF 是否正確獲取了密鑰KSEAF和參數(shù)SUPI, 從而導(dǎo)致這三條鑒權(quán)性質(zhì)沒有得到滿足.

6 總結(jié)

本文在Tamarin 中完成了對新版本5G AKA 協(xié)議和期望協(xié)議滿足的安全性質(zhì)的形式化建模. 安全性質(zhì)考慮了相關(guān)密鑰的保密性質(zhì)和協(xié)議參與實體之間的Lowe 鑒權(quán)性質(zhì), 驗證分析了5G AKA 協(xié)議在相關(guān)安全性質(zhì)上的滿足情況. 重新評估了新版本5G AKA 協(xié)議在之前舊版本協(xié)議面臨的安全問題上的安全性質(zhì). 針對相關(guān)安全問題, 采用了三種方法來對協(xié)議模型進行改進, 重新驗證了改進后的協(xié)議模型是否滿足了改進前未滿足的安全性質(zhì).

5G AKA 協(xié)議標準目前在持續(xù)的完善過程當中, 在未來可以繼續(xù)對新版本的5G AKA 協(xié)議以及相關(guān)變體協(xié)議進行形式化分析. 本文提出的模型可以作為對后續(xù)新版本協(xié)議進行形式化分析的基礎(chǔ), 也為其他認證和密鑰協(xié)商協(xié)議的形式化分析提供了新思路.