協議組合邏輯安全的WiMAX無線網絡認證協議

馮 濤 張子彬 馬建峰

①(蘭州理工大學計算機與通信學院 蘭州 730050)

②(西安電子科技大學計算機網絡與信息安全教育部重點實驗室 西安 710071)③(福建師范大學網絡安全與密碼技術重點實驗室 福州 350007)

1 引言

寬帶無線接入技術是指以無線傳輸方式向用戶提供接入寬帶固定網絡的接入技術。2005年IEEE 802.16工作組推出了WiMAX無線網絡的國際新標準IEEE 802.16e-2005[1?3]，WiMAX(全球微波接入互操作性)無線網絡基于IEEE 802.16空中接口，是一項新興的無線城域網[4](WMAN)寬帶技術。IEEE 802.16e-2005標準將以前版本中使用的PKM(Privacy and Key Management)安全接入協議升級為PKMv2[5]安全協議。PKMv2安全協議包括安全認證協議和密鑰管理協議兩個子協議，其中PKMv2安全認證協議是整個協議的基礎與核心。

國內外學者針對PKMv2安全認證協議可能存在的安全隱患做了分析與研究，例如， Liu與Lu[6]針對IEEE 802.16e標準中PKMv2安全認證協議在高速移動過程中缺乏保證完整性和不可抵賴性的機制，存在移交攻擊(handover vulnerability)，終端能力限制等問題，提出了使用無線公鑰基礎設施(wireless public key infrastructure)來保證其安全性，并通過仿真證明新方案加解密延遲短，性能更加優越。Sun等[7]基于重認證的需要，提出了一種更加安全快速的重認證機制。Shon與Choi[8]針對IEEE 802.16e標準中PKMv2安全認證協議在其認證初始階段會產生安全內容泄露等問題，提出了使用DH密鑰協商產生會話加密密鑰，并使用該會話加密密鑰來保證認證初始階段的安全性。Xu與Huang[9]針對IEEE 802.16e標準中PKMv2安全認證協議所受到的交錯攻擊，對PKMv2安全認證協議提出了修改意見(這里稱該修改過的協議為SC-PKMv2)，并使用BAN邏輯證明其方案安全性。

本文使用了DDMP組合理論[10?13]對PKMv2安全認證協議進行形式化分析，發現PKMv2安全認證協議存在交錯攻擊。DDMP組合理論包括協議演繹系統(PDS)和協議組合邏輯(PCL)。其理論的核心是協議可組合的安全性證明，該理論以簡單協議模塊的相加性組合與非破壞性組合作為演繹操作的前提，將復雜的組合協議看成是由簡單協議模塊經過一系列演繹操作得到的，這樣復雜協議的模塊化正確性證明就可以通過對簡單協議模塊證明的組合得到。該理論不僅提供了一種全新的分析復雜組合協議的形式化方法，也可以作為協議設計的新方法。本文運用該理論，基于協議組合邏輯(PCL)證明了PKMv2安全認證協議具有密鑰機密性、不具有會話認證性，發現PKMv2安全認證協議存在交錯攻擊，并且在此基礎上運用協議演繹系統(PDS)提出了一種新的WiMAX無線網絡安全認證協議，并使用協議組合邏輯(PCL)給出新協議的模塊化正確性和安全性證明，新協議具有密鑰機密性和會話認證性，相對于PKMv2安全認證協議更加安全。

2 預備知識

2.1 PKMv2安全認證協議

PKMv2安全認證協議的定義如下：

其中Kx表示客戶端X的公鑰，認證密鑰(AK)則是客戶端得到預認證密鑰(PAK)以后，通過計算式AK=MACPAK(NX,NY,XAddr,YAddr,160)[14]計算得出。

2.2 協議演繹系統

協議演繹系統(PDS)由構件集合和操作集合組成。構件是簡單協議的一步或者幾步，基本的構件可用于構造更復雜的協議。操作集合包含3類不同的演繹操作：組合、求精和轉換。本文中主要應用到的演繹操作[10]包括串行組合操作、轉換操作T1以及求精操作R3，R4和R6 (本文將以前相關文獻之HASHK修改為MACK)。

2.3 協議組合邏輯

協議組合邏輯(PCL)是用于證明網絡安全協議安全屬性的證明邏輯，具有精確，易部署，提供信息量豐富等特性。本文中主要應用到的公理與規則[10?13]，具體有協議行為公理AA1，AA4，AN3和ARP，原子謂詞公理REC，時間排序公理FS1和FS2，消息認證碼公理MAC1，MAC3和MAC4(本文將以前相關文獻之HASHK修改為MACK)。

3 PKMv2安全認證協議的形式化分析

3.1 基于PCL的協議模型

PKMv2安全認證協議的參與實體有客戶端(Client)和基站(Server)兩個，用X，Y表示，各自相應的實例用X，Y表示，該協議的客戶端認證程序WiMAX:Client和基站認證程序WiMAX:Server描述如下，其中"client"，"server"分別表示客戶端和基站的身份信息，XAddr,YAddr分別表示客戶端和基站的MAC地址，且根據文獻[5]中所述協議第3條消息中的客戶端MAC地址XAddr包含X的證書，則將XAddr形式化描述為：Kx)。

3.2 前提與恒定量

前提[11,15]是實例執行動作的初始狀態，是協議組合邏輯(PCL)的語法的重要組成部分。恒定量[11,15]則相當于協議運行的操作環境，是協議安全運行的基本保證。PKMv2安全認證協議的前提與恒定量如下所示：

前提θWiMAX描述Client和Server兩個實體共享預認證密鑰(PAK)且不被第3方知曉(只有客戶端才能解開協議第2條消息中用客戶端公鑰加密的預認證密鑰[9])。

恒定量τWiMAX,1描述Client和Server在計算認證密鑰(AK)時，不會泄露給第三方。

恒定量τWiMAX,2描述同一網元不能同時即作為Client又作為Server，同時兼任兩個角色會引起反射攻擊[16]。

3.3 安全屬性及證明

將PKMv2安全認證協議的安全目標形式化描述為兩個安全屬性[11,15]：密鑰機密性(φWiMAX,sec)和會話認證性(φWiMAX,auth)，且只有保障密鑰機密性，才能確保具有會話認證性。這里僅給出Server端的情況，Client端的情況類似，略去。

定理1 (PKMv2安全認證協議具有密鑰機密性) 該協議為Server提供密鑰機密性是指：

即可得出τWiMAX,1∧τWiMAX,2?θWiMAX[WiMAX:Server]YφWiMAX,sec成立。

定理2 (PKMv2安全認證協議不具有會話認證性)該協議為Server提供會話認證性是指：因篇幅原因證明過程略去，經證明τWiMAX,1∧τWiMAX,2?θWiMAX[WiMAX:Server]YφWiMAX,auth不成立，并且根據文獻[17]可知存在交錯攻擊。

4 演繹新的認證協議

本文首先選取兩個單方認證協議，一個是基于簽名的挑戰應答協議P1，一個是基于消息認證碼的挑戰應答協議P2(消息認證碼的密鑰AK由用X公鑰Kx加密的預認證密鑰PAK計算得出，原理同PKMv2安全認證協議)。

對協議P1與P2進行串行組合，用協議P1的輸出代替協議P2的輸入，從而得到協議P3。

對協議P3應用轉換T1，將NY,EKx(PAK)移動到較早的消息中，從而得到協議P4，其主要目的是減少消息數量。

由于應用轉換操作T1后協議第2步使用了客戶端X的公鑰，但是協議第1步并未向基站Y發送X的公鑰證書，根據轉換操作的定義，這里可以應用轉換操作在協議第1步加入IDX，從而得到協議P5。IDX表示客戶端X的公鑰證書，以防止基站Y未持有X的公鑰。

對協議P5應用求精R6得到協議P6，其中IDY表示基站Y的公鑰證書，從而防止客戶端X未持有基站Y的簽名-證明密鑰。

為了防止客戶端X的MAC地址被修改，根據轉換操作的定義，運用轉換操作在第三條消息中加入包含X證書的MAC地址XAddr(根據文獻[11]所述，加入XAddr也是保護認證密鑰AK的一種加鹽操作)，從而得到協議P7。

對協議P7應用求精R4得到協議P8，協議P8擁有協議P7的一切安全屬性，并能有效抵御Lowe’s攻擊[18]。此時，協議已經具備了一定的安全性，但還與PKMv2安全認證協議一樣會受到交錯攻擊。

對協議P8應用求精R3得到協議P9，協議P9擁有協議P8的一切安全屬性，加入求精R2后證明第二條消息是基站Y產生發送的，從而有效的防御交錯攻擊。

到此為止，我們就通過協議演繹系統(PDS)演繹得到了一個新的安全認證協議，命名其為FZMPKMv2安全認證協議，其現實流程圖如下圖1所示。

圖1 FZM-PKMv2安全認證協議現實流程圖

5 FZM-PKMv2協議模塊化正確性和安全性證明

5.1 基于PCL的協議模型

FZM-PKMv2安全認證協議的參與實體也是∧客戶端(Client)和基站(Server)兩個，同樣也分別用X，Y表示，各自相應的實例用X，Y表示，其它信息描述與PKMv2安全認證協議一致。該協議的客戶端認證程序WiMAX':Client 和基站認證程序WiMAX':Server 描述如下：

5.2 前提與恒定量

FZM-PKMv2安全認證協議的前提與恒定量如下所示(同理3.2節)：

5.3 安全屬性及證明

將FZM-PKMv2安全認證協議的安全目標同樣形式化為兩個安全屬性：密鑰機密性和會話認證性這里同樣僅給出Server端的情況，Client端的情況類似，略去。

定理3 (FZM-PKMv2安全認證協議具有密鑰機密性) 該協議為Server提供密鑰機密性是指：其中因證明方法同PKMv2安全認證協議的密鑰機密性證明，故在此略去。

定理4 (FZM-PKMv2安全認證協議具有會話認證性)該協議為Server提供會話認證性是指：因篇幅原因證明過程略去。

FZM- PKMv2與其他PKMv2安全認證協議的安全性比較如下表1所示。

表1 幾類PKMv2安全認證協議的安全性比較

6 結束語

基于協議演繹系統(PDS)本文提出了一種新的WiMAX無線網絡安全認證協議FZMPKMv2，與PKMv2安全認證協議不同的是，它有效地防御了交錯攻擊，并且運用協議組合邏輯(PCL)給出了新協議的模塊化正確性和安全性證明。

本文主要討論了WiMAX無線網絡接入認證的安全問題，以后將用類似方法討論其它類型的網絡安全認證協議。再者，將通過網絡仿真對FZMPKMv2安全認證協議的效率進行分析與優化。

[1] Yarali A and Rahman S. WiMAX broadband wireless access technology: Services, architecture and deployment models [C].Electrical and Computer Engineering, 2008. CCECE 2008,Canada, 2008: 77-82.

[2] IEEE 802.16e-2005. Air interface for fixed broadband wireless access systems, Amendment 2: Physical and medium access control layers for combined fixed and mobile operation in licensed bands[S], NJ, USA, IEEE Press, 2006.

[3] Kim Dongmyoung, Cai Hua, and Na Minsoo, et al..Performance measurement over Mobile WiMAX/IEEE 802.16e network[C], 2008 IEEE International Symposium on A World of Wireless, Mobile and Multimedia Networks,Newport Beach, CA, United states, 2008: 1-8.

[4] Agrawal Dharma P, Gossain Hrishikesh, and Cavalcanti Dave, et al.. Recent advances and evolution of WLAN and WMAN standards[C]. IEEE Wireless Communications, USA,2008: 54-55.

[5] Johnston D and Walker J. Mutual authentication for PKMv2,IEEE C802.16e-04_229rl. 2004.

[6] Liu Fu-qiang and Lu Lei. A WPKI-Based security mechanism for IEEE 802.16e[C]. WiCOM International Conference, Wuhan, 2006: 1-4.

[7] Sun Hung-min, Lin Yue-hsun, and Chen Shuai-min, et al..Secure and fast handover scheme based on pre-authentication method for 802.16/WiMAX infrastructure networks[C]. 2007 IEEE Region 10 Conference, Taipei, 2007: 1-4.

[8] Shon Taeshik and Choi Wook. An analysis of mobile WiMAX security: vulnerabilities and solutions [J]. Lecture Notes in Computer Science, 2007, 4658: 88-97.

[9] Xu Sen and Huang Chin-tser. Attacks on PKM protocols of IEEE 802.16 and its later versions[C]. Proceedings of 3rd International Symposium on Wireless Communication System (ISWCS 2006), Valencia, 2006: 185-189.

[10] Datta A. Security analysis of network protocols:compositional reasoning and complexity-theoretic Foundations[D]. [Ph.D. dissertation], Computer Science Department, Stanford University, 2005.

[11] Datta A, Derek A, and Mitchell J C, et al.. Protocol Composition Logic (PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007, 172: 311-358.

[12] Cremers C. On the protocol composition logic PCL[C].Proceedings of the 2008 ACM symposium on Information,computer and communications security, Tokyo, Japan, 2008:66-76.

[13] Doug K, Ryan M, and Tony B, et al.. A correctness proof of a mesh security architecture[C]. Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, 2008:315-330.

[14] Johnston D and Walker J. Overview of IEEE 802.16 security[J]. IEEE Security & Privacy, 2004, 2: 40-48.

[15] He Chang-hua, Sundararajan M, and Datta A, et al.. A modular correctness proof of IEEE 802.11i and TLS[C],Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS'05), Alexandria, VA, USA,2005: 2-15.

[16] 鐵滿霞, 李建東, 王育民. WAPI密鑰管理協議的PCL證明[J].電子與信息學報, 2009, 31(2): 444-447.Tie Man-xia, Li Jian-dong, and Wang Yu-min. A correctness proof of WAPI key management protocol based on PCL[J].Journal of Electronics & Information Technology, 2009, 31(2):444-447.

[17] Meadows C and Pavlovic D. Deriving, attacking and defending the GDOI protocol[C]. Proceedings of 9th European Symposium On Research in Computer Security,France, 2004: 53-72.

[18] Lowe G. Some new attacks upon security protocols[C].Computer Security Foundations Workshop, 1996,Proceedings, 9th IEEE, Kenmare, Ireland, 1996: 10-12.