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

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

1 引言

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

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

5G AKA 協(xié)議用于實(shí)現(xiàn)用戶和運(yùn)營(yíng)商網(wǎng)絡(luò)之間的身份驗(yàn)證和密鑰協(xié)商, 涉及到的實(shí)體有用戶設(shè)備(user equipment, UE)、用戶在近距離內(nèi)連接的服務(wù)網(wǎng)絡(luò)(serving network, SN) 和與用戶對(duì)應(yīng)的運(yùn)營(yíng)商歸屬網(wǎng)絡(luò)(home network, HN). 服務(wù)網(wǎng)絡(luò)SN 中包括安全錨點(diǎn)功能(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ò)時(shí)代, AKA 協(xié)議的安全性大多是通過使用TLA 和BAN 邏輯[1]手動(dòng)進(jìn)行驗(yàn)證, 這種驗(yàn)證方式只考慮了很簡(jiǎn)單的威脅模型, 也只能提供很弱的安全保證, 并不適用于現(xiàn)在的使用場(chǎng)景. 為了提高協(xié)議的設(shè)計(jì)效率, 研究人員開始使用ProVerif、Scyther、AVISPA、Tamarin 等自動(dòng)化的安全協(xié)議驗(yàn)證工具來對(duì)協(xié)議進(jìn)行形式化分析. 比如, Arapinis 等人[2]用ProVerif 分析了3G 網(wǎng)絡(luò)中的AKA 協(xié)議, 發(fā)現(xiàn)了針對(duì)用戶位置和身份匿名性的攻擊, 并提出了對(duì)應(yīng)的解決方案.

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

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

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

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

1.2 本文貢獻(xiàn)

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

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

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

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

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

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

蜂窩網(wǎng)絡(luò)整體架構(gòu)大致由三個(gè)大的邏輯實(shí)體組成: 用戶設(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 一般是智能手機(jī)或者物聯(lián)網(wǎng)設(shè)備, UE 由移動(dòng)設(shè)備(mobile equipment, ME) 和USIM卡組成, USIM 卡中存有用戶永久身份標(biāo)識(shí)符SUPI、序列號(hào)(sequence number, SQN)、長(zhǎng)期對(duì)稱密鑰K和公共非對(duì)稱密鑰pkHN. SUPI 是一個(gè)唯一且永久的用戶身份標(biāo)識(shí); SQN 是用于驗(yàn)證鑒權(quán)消息新鮮性的計(jì)數(shù)器; 對(duì)稱密鑰K是用戶與其對(duì)應(yīng)歸屬網(wǎng)絡(luò)HN 中的ARPF 之間的共享密鑰; 公共非對(duì)稱密鑰pkHN也對(duì)應(yīng)于歸屬網(wǎng)絡(luò)HN, 用于對(duì)SUPI 進(jìn)行加密得到用戶加密標(biāo)識(shí)符(subscription concealed identifier,SUCI).

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

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

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

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

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

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

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

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

(3) ARPF 通過用戶標(biāo)識(shí)符解密功能SIDF 從SUCI 中解密出SUPI,然后選擇鑒權(quán)方式為5G AKA.ARPF 會(huì)計(jì)算出密鑰KAUSF、參數(shù)XRES* (預(yù)期響應(yīng), expected response), 然后由參數(shù)RAND(一個(gè)隨機(jī)數(shù))、AUTN (認(rèn)證令牌, 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* 計(jì)算出其哈希值HXRES*, 根據(jù)密鑰KAUSF計(jì)算出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 (消息認(rèn)證碼, message authentication code) 和SQN 來驗(yàn)證鑒權(quán)材料的有效性. 若通過驗(yàn)證, 則更新自己的SQN, 計(jì)算出參數(shù)RES* 和密鑰KSEAF, 再把參數(shù)RES* 發(fā)送給SEAF.

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

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

(9) 鑒權(quán)成功后, AUSF 會(huì)發(fā)送密鑰KSEAF和SUPI 給SEAF. 密鑰KSEAF就會(huì)成為安全錨點(diǎn)密鑰, SEAF 會(huì)根據(jù)此密鑰來計(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], 對(duì)鑒權(quán)向量的生成流程和相關(guān)函數(shù)的作用、UE 對(duì)鑒權(quán)材料有效性的驗(yàn)證流程進(jìn)行說明.

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

首先隨機(jī)生成一個(gè)序列號(hào)SQN 和一個(gè)隨機(jī)數(shù)RAND, 再計(jì)算下列各參數(shù):

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

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

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

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

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

3 形式化建模

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.1 驗(yàn)證結(jié)果

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

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

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

4.2 結(jié)果分析

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

(1) 在v0.7.0 版本的5G AKA 協(xié)議中, ARPF 計(jì)算出鑒權(quán)向量并發(fā)送響應(yīng)消息給AUSF. 在這個(gè)消息中并沒有包含SUPI 或SUCI, 如果攻擊者幾乎同時(shí)啟動(dòng)兩個(gè)與服務(wù)網(wǎng)絡(luò)的會(huì)話, AUSF 將無法區(qū)分來自ARPF 的兩個(gè)響應(yīng), 并且可能將錯(cuò)誤的響應(yīng)和錯(cuò)誤的用戶相關(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 的消息中包含了安全錨點(diǎn)密鑰KSEAF. 如果發(fā)生了(1) 中描述的會(huì)話競(jìng)爭(zhēng)情況, 攻擊者就可以獲取到合法用戶的密鑰KSEAF來計(jì)算通信過程中需要的其它密鑰, 從而假冒合法用戶與服務(wù)網(wǎng)絡(luò)進(jìn)行通信.

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

對(duì)于鑒權(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é)議改進(jìn)方法及驗(yàn)證結(jié)果

5.1 SNID 綁定

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

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

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

5.2 會(huì)話綁定

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

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

5.3 密鑰確認(rèn)往返

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

5.4 驗(yàn)證結(jié)果

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

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

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

6 總結(jié)

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

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