協議組合邏輯安全的4G無線網絡接入認證方案

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

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

1 引言

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

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

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

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

2 預備知識

2.1 自證實公鑰系統

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

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

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

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

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

2.2 協議演繹系統和協議組合邏輯

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

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

PCL的基本語法元素是前置斷言—后置斷言表達式，即幾乎所有的安全協議證明步驟都遵循θ[P]Xφ規則，該規則表明協議的執行實例X執行動作序列P以后，狀態由θ轉變為φ。本文用到的部分公理和法則如下[7,11,12]。

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

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

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

Honest(X?)：表示實體X?在當前輪中是誠實的，其執行的所有動作都是協議所規定的。

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

3 4G無線網絡接入認證新方案

3.1 參數描述

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

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

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

3.2 移動終端的首次/切換接入認證協議

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

圖1 首次/切換接入認證過程

此過程說明如下。

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

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

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

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

認證結束后，AN會在數據庫中存儲TIDME和（IDME,YME,KAM）的對應關系，向ME提供服務后可以將作為不可否認憑證發送給ME的歸屬環境HE。其中，bill為計費信息，

3.3 移動終端再次接入認證協議

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

圖2 再次接入認證過程

4 新協議的演繹

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

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

對協議P1 和P2進行串行組合（串行組合操作是通過適當的替代步驟，使前一協議模塊的輸出代替后一協議模塊的輸入來完成協議的組合），用協議P1 的輸出代替P2的輸入，從而得到協議P4。

對協議P4應用轉換操作T1（通過將數據從一個消息移動到另外一個較早的消息中），將cY移動到較早的消息中，從而得到協議P5，其主要目的是減少消息數量。

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

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

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

對協議P8 和P3進行串行組合，用協議P8 輸出代替協議P3的輸入，從而得到協議P9。

對協議P9應用轉換操作T1，將消息RX移動到較早的消息中，從而得到協議P10，其主要目的也是減少消息數量。

由于AN驗證ME時還需要參數TX、X的身份標識IDX以及X的公鑰YX，但協議P10中并未給出，根據轉換操作的定義，這里可以應用轉換操作在協議第3步中加入TX、IDX和YX，從而得到協議P11。

為了保護用戶的身份隱私，首次認證或切換認證之后，用戶再次接入該網絡時是借助一個臨時身份TIDX，但協議P11中并未給出，根據轉換操作的定義，這里可以應用轉換操作在協議第4步中加入TIDX，從而得到協議P12。

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

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

5.1 協議流程表示

PCL標記法表示的協議角色如下。

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

5.2 安全屬性的形式化證明

定理 1 AKEBSP安全認證協議具有會話認證性。

根據協議組合邏輯PCL，需要證明的發起者角色會話認證性的形式化表示為

當上式成立時，AKEBSP協議的發起者角色能夠保證會話認證性。這里僅給出ME端的證明情況，AN端的證明情況類似。

證明

定理2 AKEBSP安全認證協議具有密鑰機密性。

根據協議組合邏輯PCL，需要證明的發起者角色密鑰機密性的形式化表示為

當上式成立時，AKEBSP協議的發起者角色能夠保證密鑰機密性。這里僅給出ME端的證明情況，AN端的證明情況類似。

證明

5.3 新方案的綜合分析

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

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

表1 本方案與相關方案的比較

新方案能提供不可否認服務，整個系統中只有擁有正確私鑰的終端用戶才可以根據cAN構造出合法的TME，一旦終端用戶通過了認證，則不能否認自己的接入。當出現糾紛的時候，AN可以提供RAN、TME和cAN進行驗證，以作為不可否認憑證。

新方案中，ME的身份（IDME/IMSI）是在用戶驗證接入網絡的身份之后發送出去的，沒有以明文形式在空中接口和有線鏈路傳輸，且只有TA知道用戶公鑰和用戶身份的對應關系，攻擊者無法對用戶進行非法跟蹤，提供了身份保護。每次認證后，AN都會動態更換用戶的臨時身份，使得用戶身份的安全性大大增強。

6 結束語

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

[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.