王麗麗，馮濤,2,，馬建峰

(1. 蘭州理工大學(xué) 計算機(jī)與通信學(xué)院, 甘肅 蘭州 730050;2. 福建師范大學(xué) 網(wǎng)絡(luò)安全與密碼技術(shù)重點實驗室, 福建 福州 350007;3. 西安電子科技大學(xué) 計算機(jī)網(wǎng)絡(luò)與信息安全教育部重點實驗室, 陜西 西安 710071)

1 引言

在多種無線通信技術(shù)及異構(gòu)網(wǎng)絡(luò)共存、融合的趨勢下，4G無線網(wǎng)絡(luò)移動終端的安全接入問題變得更加復(fù)雜和重要[1]。2009年，ITU-R確立了兩大4G候選標(biāo)準(zhǔn)：LTE-Advanced和IEEE 802.16m。文獻(xiàn)[2,3] 中介紹了關(guān)于 LTE RAN(radio access network)的安全決策，但沒有給出具體的接入認(rèn)證協(xié)議。文獻(xiàn)[4]中，IEEE 802.16m工作組針對4G網(wǎng)絡(luò)的安全機(jī)制提出了PKMv3(privacy key management version 3)協(xié)議，但也沒有給出具體的接入認(rèn)證過程。

1991年，Girault首次提出自證實公鑰系統(tǒng)[5]。同基于證書的公鑰密碼體制相比，自證實公鑰系統(tǒng)更適用于移動環(huán)境。首先，AN(access network)和ME(mobile equipment)的認(rèn)證參數(shù)中不包含公鑰證書，協(xié)議交互之前，不需要存儲和傳送自己的公鑰證書，不需要驗證彼此公鑰證書的合法性和有效性，節(jié)省了存儲空間和通信帶寬，減輕了網(wǎng)絡(luò)負(fù)載和傳輸時延，減少了移動終端的計算負(fù)擔(dān)；此外，對公鑰的驗證隱藏在簽名驗證或加密過程中，當(dāng)網(wǎng)絡(luò)存在階層關(guān)系時也不需要通過其他網(wǎng)絡(luò)實體轉(zhuǎn)發(fā)認(rèn)證信息，提高了公鑰驗證效率和認(rèn)證效率。

Zheng等人[6]基于自證實公鑰系統(tǒng)提出了一個4G網(wǎng)絡(luò)用戶認(rèn)證方案，但方案還存在不足之處。第一，方案中，網(wǎng)絡(luò)端的公鑰并不是基于自證實公鑰系統(tǒng)構(gòu)建的，對該公鑰的驗證是利用基站聯(lián)合廣播，并在ME中設(shè)立緩沖區(qū)，通過概率統(tǒng)計方法實現(xiàn)的。但是驗證結(jié)果存在風(fēng)險，如局部出現(xiàn)偽基站密度超過合法基站的可能等。而且，方案中沒有明確指出如何確定終端緩沖區(qū)的長度、如何確定偽基站與合法基站的數(shù)量同識別成功的概率之間的關(guān)系。第二，該方案的首次接入認(rèn)證和切換認(rèn)證協(xié)議中，用戶的歸屬環(huán)境和訪問網(wǎng)絡(luò)之間需要交互部分認(rèn)證信息，接入時延會增加，對實時應(yīng)用很不利。第三，Zheng沒有對該方案的安全屬性進(jìn)行形式化分析和證明。

考慮到4G網(wǎng)絡(luò)中ME的安全接入問題，以及ME的移動性和漫游性，本文基于自證實公鑰設(shè)計了一個新的4G無線網(wǎng)絡(luò)終端接入方案，方案包括首次/切換接入認(rèn)證協(xié)議和再次接入認(rèn)證協(xié)議。由于安全協(xié)議的分析和證明對于現(xiàn)代安全網(wǎng)絡(luò)系統(tǒng)至關(guān)重要，通過運用DDMP理論[7]，本文給出新方案的演繹推導(dǎo)，并對其安全屬性進(jìn)行了形式化證明和分析。DDMP理論由A.Datta等人[7]提出，它包括協(xié)議演繹系統(tǒng)PDS和協(xié)議組合邏輯PCL，該理論既可以作為協(xié)議設(shè)計的新方法，又為協(xié)議的安全性證明和分析提供了一種全新的形式化方法。

2 預(yù)備知識

2.1 自證實公鑰系統(tǒng)

TA(trust authority)公開模數(shù)n及其公鑰e，秘密保留私鑰d，用戶的注冊過程如下[5,8]。

1) 用戶選定長度為160bit以上的私鑰x，并計算出V=g-xmodn，n是長度為1 024bit以上的模數(shù)，然后將V和自己身份ID傳給TA。

2) TA計算用戶的公鑰Y，Y=(V-ID)dmodn，并將Y傳給用戶。

3) 用戶驗證V=(Ye+ID)modn，若等式成立，則用戶的公鑰為Y，私鑰為x。

在自證實公鑰系統(tǒng)中，用戶的身份、公鑰和私鑰滿足一種計算上不可偽造的數(shù)學(xué)關(guān)系，在利用密鑰執(zhí)行加解密、簽名驗證、密鑰協(xié)商或其他密碼操作的同時，就可以驗證該數(shù)學(xué)關(guān)系，從而驗證公鑰的合法性和有效性。用戶的私鑰是自己選定的，其安全性基于解離散對數(shù)困難問題，TA無法從傳送過來的數(shù)據(jù)中得到用戶的私鑰，不能冒充用戶偽造他們的簽名，相比于基于身份的公鑰密碼體制，具有更高的安全性，更適合于開放系統(tǒng)環(huán)境中的應(yīng)用。此外，TA無法完全掌握公鑰的產(chǎn)生和驗證，即使TA偽造出相同用戶的另一個公鑰也會被檢測出來。

2.2 協(xié)議演繹系統(tǒng)和協(xié)議組合邏輯

協(xié)議演繹系統(tǒng)(PDS)由構(gòu)件集合和操作集合組成，構(gòu)件是用于構(gòu)造復(fù)雜協(xié)議的簡單協(xié)議，操作集合包含3類不同的演繹操作：組合、求精和轉(zhuǎn)換。組合操作用于2個協(xié)議的組合，包括并行組合和串行組合。求精操作用于一個簡單協(xié)議構(gòu)件上，為協(xié)議添加必要的安全屬性，且不會改變協(xié)議的消息數(shù)或協(xié)議的基礎(chǔ)結(jié)構(gòu)，例如用加密的隨機(jī)數(shù)代替原來沒有加密的隨機(jī)數(shù)。轉(zhuǎn)換操作則是通過移動消息、組合協(xié)議步驟、插入一個或多個協(xié)議步驟等操作完成對協(xié)議的修改，例如將數(shù)據(jù)從一個消息移動到另外一個較早的消息中。本文中主要使用的演繹操作包括串行組合操作、轉(zhuǎn)換操作T1以及求精操作R3、R4和R6(具體含義在本文設(shè)計的安全協(xié)議演繹過程中說明)。

協(xié)議組合邏輯(PCL)可用于安全協(xié)議的形式化證明和分析，同BAN邏輯及其他的邏輯方法相比，PCL支持安全協(xié)議的組合證明；由于包含了協(xié)議的執(zhí)行過程，PCL不需要對協(xié)議進(jìn)行抽象；PCL采用的是標(biāo)準(zhǔn)邏輯概念，而不需要使用“管轄(jurisdiction)”和“信念(belief)”等不清晰規(guī)則。此外，PCL加入了密碼學(xué)原語，并重點刻畫了消息的發(fā)送和接收，這些概念體現(xiàn)了安全協(xié)議的基本要素。目前，PCL已經(jīng)被成功用于形式化證明多個協(xié)議的正確性，如SSL/TLS協(xié)議[7]、IEEE 802.11i協(xié)議[9]、Kerberos V5 協(xié)議[10]等。

PCL的基本語法元素是前置斷言—后置斷言表達(dá)式，即幾乎所有的安全協(xié)議證明步驟都遵循θ[P]Xφ規(guī)則，該規(guī)則表明協(xié)議的執(zhí)行實例X執(zhí)行動作序列P以后，狀態(tài)由θ轉(zhuǎn)變?yōu)棣?。本文用到的部分公理和法則如下[7,11,12]。

Contains(t1,t2)：表示t1包含t2。

Fresh(X,t)：表示在實例X中產(chǎn)生的t是新鮮的。

Has(X,t)：秘密屬性的一種描述，表示實體X?在實例X中擁有信息t。

Honest(X?)：表示實體X?在當(dāng)前輪中是誠實的，其執(zhí)行的所有動作都是協(xié)議所規(guī)定的。

Send(X,t)/New(X,t)/Sign(X,t)/Encrypt(X,t)：分別表示發(fā)生了發(fā)送、生成隨機(jī)數(shù)、簽名和加密動作。

3 4G無線網(wǎng)絡(luò)接入認(rèn)證新方案

3.1 參數(shù)描述

相關(guān)參數(shù)要求[5,8]：|x|表示x的長度，整數(shù)A、B、S滿足其中，|S|表示私鑰長度。TA為ME產(chǎn)生自證實公鑰的過程如下。

1) ME選定私鑰MEx，計算并將IDME、IDHE和VME發(fā)送給TA，其中，IDME是ME的身份標(biāo)識符(IMSI)，IDHE是ME的歸屬環(huán)境HE(home environment)的標(biāo)識符。

同理，AN通過TA獲得公鑰YAN，私鑰ANx。

3.2 移動終端的首次/切換接入認(rèn)證協(xié)議

為了滿足移動網(wǎng)絡(luò)的需求和特性，針對用戶在首次接入、再次接入和漫游切換等不同場景，本文基于自證實公鑰系統(tǒng)提出了首次/切換接入場景下的認(rèn)證與密鑰交換協(xié)議(AKEBSP,authentication and key exchange protocol based on self-certified public key)和再次接入場景下的認(rèn)證協(xié)議，在確保安全接入的前提下，提高了認(rèn)證效率。首次/切換接入場景下的認(rèn)證過程如圖1所示。

圖1 首次/切換接入認(rèn)證過程

此過程說明如下。

1) ME收到AN廣播的IDAN和公鑰YAN后，選擇隨機(jī)數(shù)并將cME、IDAN、IDHE發(fā)送給AN。

2) AN驗證IDAN后，選擇隨機(jī)數(shù)rAN∈[ 0,A]和cAN∈[ 0 ,B]，分別計算TAN=rAN+xANcME和RAN=grANmodn，并將消息cAN、RAN、RAN、SigAN發(fā)送給ME，其中SigAN= {cME,cAN,RAN,TAN}xAN。

3) ME首先驗證SigAN，如果正確，則驗證下面式子是否成立：和TAN∈[0,A+(B-1)(S-1)]。如果成立，則選擇隨機(jī)數(shù)rME∈ [ 0,B]，并計算然后將消息發(fā)送給AN。

5) ME收到消息并解密，獲得了自己的臨時身份TIDME，供再次接入該網(wǎng)絡(luò)使用。

認(rèn)證結(jié)束后，AN會在數(shù)據(jù)庫中存儲TIDME和（IDME,YME,KAM）的對應(yīng)關(guān)系，向ME提供服務(wù)后可以將作為不可否認(rèn)憑證發(fā)送給ME的歸屬環(huán)境HE。其中，bill為計費信息，

3.3 移動終端再次接入認(rèn)證協(xié)議

首次/切換接入認(rèn)證通過后，ME需要再次接入到同一網(wǎng)絡(luò)時，可以利用TIDME代替協(xié)議中的IDME進(jìn)行再次接入認(rèn)證，保護(hù)了ME的身份隱私，其認(rèn)證交互過程如圖2所示。其中，TIDME′是AN為ME生成的新的臨時身份，KAM′是AN生成的新的會話密鑰，作為ME和AN下次交互使用，減少了攻擊者通過已攻陷的會話密鑰同網(wǎng)絡(luò)交互的風(fēng)險。

圖2 再次接入認(rèn)證過程

4 新協(xié)議的演繹

由于篇幅限制，本文僅對首次/切換接入場景下的認(rèn)證與密鑰交換協(xié)議 AKEBSP進(jìn)行演繹推導(dǎo)和形式化證明。在新協(xié)議的演繹過程和步驟中，為了簡潔和清晰，分別用X?和?表示協(xié)議的2個參與方：移動終端ME和接入網(wǎng)絡(luò)AN，其相應(yīng)的實體分別用X和Y表示。此外，AN的公鑰也可用?表示，終端的歸屬環(huán)境標(biāo)識符用IDH表示。

首先，選取3個簡單的基本協(xié)議，一個是基于簽名的挑戰(zhàn)應(yīng)答協(xié)議P1，另外2個是基于加密的挑戰(zhàn)應(yīng)答協(xié)議P2 和P3（其中，?是AN的公鑰，密鑰K是ME通過RY計算得到的）。

對協(xié)議P1 和P2進(jìn)行串行組合（串行組合操作是通過適當(dāng)?shù)奶娲襟E，使前一協(xié)議模塊的輸出代替后一協(xié)議模塊的輸入來完成協(xié)議的組合），用協(xié)議P1 的輸出代替P2的輸入，從而得到協(xié)議P4。

對協(xié)議P4應(yīng)用轉(zhuǎn)換操作T1（通過將數(shù)據(jù)從一個消息移動到另外一個較早的消息中），將cY移動到較早的消息中，從而得到協(xié)議P5，其主要目的是減少消息數(shù)量。

由于ME驗證AN時需要使用2個參數(shù)，分別是由RAN=grANmodn和TAN=rAN+xANcME計算得到的RAN和TAN，但協(xié)議P5中并未給出，根據(jù)轉(zhuǎn)換操作的定義，這里可以應(yīng)用轉(zhuǎn)換操作在協(xié)議第二步中加入RAN和TAN，從而得到協(xié)議P6。

為了讓X確信消息是由Y新鮮生成的，對協(xié)議P6應(yīng)用轉(zhuǎn)換操作T2，得到協(xié)議P7，其主要目的是為了防止重放攻擊。

由于ME要明確接收消息的AN，并需要同歸屬環(huán)境進(jìn)行交互，根據(jù)轉(zhuǎn)換操作的定義，在協(xié)議第一步中加入IDY和TIDH，從而得到協(xié)議P8。

對協(xié)議P8 和P3進(jìn)行串行組合，用協(xié)議P8 輸出代替協(xié)議P3的輸入，從而得到協(xié)議P9。

對協(xié)議P9應(yīng)用轉(zhuǎn)換操作T1，將消息RX移動到較早的消息中，從而得到協(xié)議P10，其主要目的也是減少消息數(shù)量。

由于AN驗證ME時還需要參數(shù)TX、X的身份標(biāo)識IDX以及X的公鑰YX，但協(xié)議P10中并未給出，根據(jù)轉(zhuǎn)換操作的定義，這里可以應(yīng)用轉(zhuǎn)換操作在協(xié)議第3步中加入TX、IDX和YX，從而得到協(xié)議P11。

為了保護(hù)用戶的身份隱私，首次認(rèn)證或切換認(rèn)證之后，用戶再次接入該網(wǎng)絡(luò)時是借助一個臨時身份TIDX，但協(xié)議P11中并未給出，根據(jù)轉(zhuǎn)換操作的定義，這里可以應(yīng)用轉(zhuǎn)換操作在協(xié)議第4步中加入TIDX，從而得到協(xié)議P12。

到此為止，通過協(xié)議演繹系統(tǒng)(PDS)演繹得到了新協(xié)議AKEBSP。

5 新協(xié)議安全性的形式化證明和分析

5.1 協(xié)議流程表示

PCL標(biāo)記法表示的協(xié)議角色如下。

其中，InitAKEBSP是發(fā)起者角色(對應(yīng)于 ME)的動作序列，RespAKEBSP是響應(yīng)者角色(對應(yīng)于AN)的動作序列。

5.2 安全屬性的形式化證明

定理 1 AKEBSP安全認(rèn)證協(xié)議具有會話認(rèn)證性。

根據(jù)協(xié)議組合邏輯PCL，需要證明的發(fā)起者角色會話認(rèn)證性的形式化表示為

當(dāng)上式成立時，AKEBSP協(xié)議的發(fā)起者角色能夠保證會話認(rèn)證性。這里僅給出ME端的證明情況，AN端的證明情況類似。

證明

定理2 AKEBSP安全認(rèn)證協(xié)議具有密鑰機(jī)密性。

根據(jù)協(xié)議組合邏輯PCL，需要證明的發(fā)起者角色密鑰機(jī)密性的形式化表示為

當(dāng)上式成立時，AKEBSP協(xié)議的發(fā)起者角色能夠保證密鑰機(jī)密性。這里僅給出ME端的證明情況，AN端的證明情況類似。

證明

5.3 新方案的綜合分析

從認(rèn)證協(xié)議的可證明安全性、通信效率和計算效率等方面對新方案中的 AKEBSP協(xié)議和文獻(xiàn)[6]提出的SPAKA協(xié)議進(jìn)行比較，結(jié)果如表1所示，其中有關(guān)符號說明如下：|SV|表示一次簽名驗證操作，|SED|表示一次對稱密鑰加解密操作，|PED|表示一次非對稱密鑰加解密操作。

新方案是基于自證實公鑰系統(tǒng)提出的，節(jié)省了存儲空間，減少了ME的計算量和認(rèn)證時延。根據(jù)協(xié)議的演繹過程可知，ME和AN之間傳遞的所有消息均具有新鮮性和不可預(yù)測性，所以新方案能抵御重放攻擊。

表1 本方案與相關(guān)方案的比較

新方案能提供不可否認(rèn)服務(wù)，整個系統(tǒng)中只有擁有正確私鑰的終端用戶才可以根據(jù)cAN構(gòu)造出合法的TME，一旦終端用戶通過了認(rèn)證，則不能否認(rèn)自己的接入。當(dāng)出現(xiàn)糾紛的時候，AN可以提供RAN、TME和cAN進(jìn)行驗證，以作為不可否認(rèn)憑證。

新方案中，ME的身份（IDME/IMSI）是在用戶驗證接入網(wǎng)絡(luò)的身份之后發(fā)送出去的，沒有以明文形式在空中接口和有線鏈路傳輸，且只有TA知道用戶公鑰和用戶身份的對應(yīng)關(guān)系，攻擊者無法對用戶進(jìn)行非法跟蹤，提供了身份保護(hù)。每次認(rèn)證后，AN都會動態(tài)更換用戶的臨時身份，使得用戶身份的安全性大大增強(qiáng)。

6 結(jié)束語

本文分析了4G無線網(wǎng)絡(luò)中移動終端的安全接入認(rèn)證問題，基于自證實公鑰設(shè)計了一個新的終端接入認(rèn)證方案。新方案包括首次/切換接入場景下的認(rèn)證及密鑰交換 AKEBSP協(xié)議和再次接入場景下的認(rèn)證協(xié)議，適應(yīng)了4G無線網(wǎng)絡(luò)的移動和漫游特性。本文應(yīng)用DDMP理論中的協(xié)議演繹系統(tǒng)PDS對新協(xié)議進(jìn)行了演繹推導(dǎo)，用協(xié)議組合邏輯 PCL對協(xié)議進(jìn)行了形式化證明，并綜合分析了協(xié)議的安全性能。結(jié)果表明，新方案具有會話認(rèn)證性和密鑰機(jī)密性，不僅能抵御偽基站攻擊和重放攻擊，還能提供不可否認(rèn)服務(wù)和身份隱私性，同時提高了移動終端的接入效率。

[1] PIYUSH G,PRIYADARSHAN P.4G-A new era in wireless telecommunication[EB/OL]. http://www.idt.mdh.se/kurser/ct3340/ht09/ADMI NISTRATION/IRCSE09-submissions/ircse09_submission_13.pdf, 2009.

[2] AQSACOM S,AQSACOM I. Lawful interception for 3G and 4G networks[EB/OL].http://www.aqsacomna.com/us/articles/Aqsacom_White_paper_4G_LI_v1.pdf,2010.

[3] 3GPP. Technical Specification Group Services and System Aspects;Rationale and Track of Security Decisions in Long Term Evolved(LTE) RAN/3GPP System Architecture Evolution(SAE)(Release 9)[S]. Tech Spec 3GPP TS 33.102 V9.0.0. 2009.

[4] IEEE P802.16m. Part 16:air interface for fixed and mobile broadband wireless access systems[EB/OL].http://lichun.cm.nctu.edu.tw/pa pers/P80216m_D4.pdf,2010.

[5] GIRAULT M. Self-certified public keys[A]. Eurocrypt’91 [C]. Brighton UK,1991.490-497.

[6] HE D K, WANG J,ZHENG Y. User authentication scheme based on self-certified public key for next generation wireless network[A].IEEE International Symposium on Biometrics and Security Technologies [C]. Islamabad, Pakistan, 2008.

[7] DATTA A. Security Analysis of Network Protocol: Compositional Reasoning and Complexity Theoretic Foundations[D]. Computer Science Department, Stanford University, 2005.8-72.

[8] POUPARD C,STERN J. Security analysis of a practical on the fly authentication and signature generation[A]. Eurocrypt’1998[C]. Espoo Finland, 1998. 422-436.

[9] HE C,SUNDARARAJAN M,DATTA A. A modular correctness proof of IEEE 802.11i and TLS[A]. CCS2005-12th ACM Conference on Computer and Communications Security[C].Alexandria,VA, United States,2005.2-15.

[10] ROY A,DATTA A, DEREK A. Secrecy analysis in protocol composition logic[A]. The 11th Asian Computing Science Conference [C].Tokyo,Japan,2006.197-213.

[11] DATTA A, ROY A, MITCHELL J. Protocol composition logic(PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007,172(1): 311-358.

[12] CAS C. On the protocol composition logic PCL[A]. Preceedings of 2008 ACM Symposium on Information, Computer and Communications Security[C].Tokyo, Japan, 2008.18-20.