基于重寫邏輯的PKMv3協(xié)議形式化建模與驗證

佘 葭 張 民

(華東師范大學計算機科學與軟件工程學院 上海 200062)

基于重寫邏輯的PKMv3協(xié)議形式化建模與驗證

佘 葭 張 民

(華東師范大學計算機科學與軟件工程學院 上海 200062)

IEEE802.16m標準在MAC安全子層定義了密鑰管理PKMv3協(xié)議，用于認證和授權信息的傳輸以及密鑰的交換。由于寬帶無線網(wǎng)絡具有易遭受攻擊的特性，引入入侵者模型分析密鑰管理協(xié)議的安全機制。利用一種基于重寫邏輯的形式化建模語言Maude，實現(xiàn)對PKMv3網(wǎng)絡環(huán)境中的通信主體以及系統(tǒng)狀態(tài)的建模，并利用其自帶的模型檢測工具驗證協(xié)議的安全特性。驗證結果表明，PKMv3協(xié)議能保證密鑰的機密性以及認證的可靠性，但仍有可能遭遇到中間人攻擊破壞消息傳輸?shù)耐暾浴?/p>

IEEE802.16m標準 PKMv3協(xié)議 密鑰管理 重寫邏輯 Maude語言 形式化驗證

0 引 言

IEEE802.16m[1]是全球微波互聯(lián)技術WiMAX[2]的新一代標準。WiMAX是一種支持無線數(shù)據(jù)長距離高速傳輸?shù)碾娮油ㄐ偶夹g，正逐步實現(xiàn)寬帶業(yè)務的移動化。IEEE802.16m在MAC安全子層中定義了WiMAX的安全規(guī)范，其中包括對數(shù)據(jù)包進行加密的封裝協(xié)議和提供密鑰分發(fā)和安全訪問控制的PKMv3協(xié)議。PKMv3協(xié)議在前兩代密鑰管理協(xié)議的基礎上進行改進[3]，增加對消息的分級保護，采用更安全的AES加密算法，并支持基于EAP (Extensible Authentication Protocol)的認證方式和CMAC(Cipher-based Message Authentication)消息驗證，減少了遭受攻擊的可能性。

由于移動WiMAX網(wǎng)絡比傳統(tǒng)無線網(wǎng)絡面臨更多的威脅，針對密鑰管理PKM協(xié)議安全性已有學者做了大量的研究工作。文獻[4]利用BAN邏輯實現(xiàn)了對前兩代密鑰管理協(xié)議的分析，指出PKMv1協(xié)議中單向認證的缺陷和PKMv2協(xié)議中遭遇到的穿插攻擊。文獻[5]使用自動化協(xié)議檢測工具Scyther實現(xiàn)對PKMv2協(xié)議的形式化分析，驗證出協(xié)議中機密性、認證性和完整性的缺陷。文獻[6]通過Casper協(xié)議建模工具對PKMv2協(xié)議進行描述，并用FDR工具分析進程通信的輸出結果，發(fā)現(xiàn)入侵者可以截獲消息進行重放攻擊。文獻[7]通過文件綜述的方式，論述WiMAX中認證和授權的安全問題，如可能遭遇到的DoS攻擊，存在認證缺陷和密鑰空間不足等問題。文獻[8]使用CasperFDR工具對PKMv3協(xié)議中基站、手機站和中繼站間傳遞明文消息的過程進行建模，分析輸出結果得到竊取密鑰的攻擊方式。文獻[9]利用PROMELA語言對PKMv3協(xié)議密鑰生命周期的時間特性進行建模，并用DT-Spin工具實現(xiàn)對協(xié)議活躍性、連續(xù)性和消息一致性的模型檢測。針對歷代密鑰管理協(xié)議中存在的缺陷，學者們也提出不少改進方案。文獻[10]提出一種改進的安全網(wǎng)絡認證協(xié)議ISNAP，在認證消息中同時使用隨機值和時間戳來防御網(wǎng)絡中的重放攻擊和DoS攻擊。文獻[11]針對網(wǎng)絡中的非法訂閱者發(fā)送大量請求消息造成基站計算負擔的問題，采用可視秘密共享技術以防御DoS攻擊。文獻[12]提出了基于消息驗證碼的共享認證消息技術，預防網(wǎng)絡中的DDoS攻擊。文獻[13]探討了利用標簽ticket實現(xiàn)目標基站間快速切換的機制，減少了重認證的時間開銷。

隨著目前WiMAX技術的廣泛應用，針對IEEE802.16m標準中經(jīng)過改進的第三代密鑰管理協(xié)議的研究卻仍然較少，因此對PKMv3協(xié)議安全特性的研究十分必要。本文采用基于重寫邏輯[14]的建模語言Maude[15]，并引入了入侵者模型，實現(xiàn)對PKMv3協(xié)議安全特性的形式化的分析和驗證。Maude建模語言能夠用簡潔的語義準確描述網(wǎng)絡安全協(xié)議的安全性質，建立協(xié)議分析的形式化模型，并提供用于模型檢測的命令工具發(fā)現(xiàn)協(xié)議設計中的安全漏洞或者證明協(xié)議的正確性[16]。

1 PKMv3協(xié)議

PKMv3協(xié)議是定義在IEEE802.16m安全子層的密鑰管理協(xié)議，它提供了從基站到終端的密鑰數(shù)據(jù)的安全分發(fā)機制。通過該協(xié)議的執(zhí)行，基站與終端間實現(xiàn)了雙向認證與授權、安全組件的協(xié)商，以及密鑰交換。在IEEE802.16m的AAI(Advanced Air Interface)網(wǎng)絡中，BS(Base Station)作為認證端，同時SS(Subscriber Station)被描述為終端。AAI網(wǎng)絡的安全功能模塊通過提供BS與SS間協(xié)議數(shù)據(jù)的加密傳輸，為雙方保障了隱私性、認證性和機密性。

1.1 雙向認證過程

PKMv3協(xié)議支持基于EAP認證的方式，EAP是一種提供多種驗證方法的通用框架，用于在請求方和服務器間傳遞身份驗證消息。SS和BS的雙向認證過程如圖1所示，SS首先向BS發(fā)送認證請求消息作為EAP會話的開始，發(fā)送的消息中包括SS的X.509數(shù)字證書Cert(SS)，SS生成的隨機值NS以及其支持的認證和加密算法Capabilities，并將該消息用SS的私鑰加密實現(xiàn)數(shù)字簽名以抵抗攻擊者的篡改。其中，X.509證書由CA認證中心發(fā)放，包括使用者的標識號，公鑰信息以及MAC地址等。隨機值則用于幫助網(wǎng)絡中的通信主體識別連續(xù)的請求，從而辨別出攻擊者的重放消息并抵抗DoS攻擊。

圖1 雙向認證過程

BS將SS發(fā)送的認證請求消息用SS的公鑰解密，若解密消息得到的數(shù)字證書的主體與SS一致，則BS向SS發(fā)送認證應答消息作為響應，并用BS的私鑰對消息進行數(shù)字簽名作為防篡改保護。消息中包括BS的X.509證書Cert(BS)，接收到的SS隨機數(shù)NS，BS生成的隨機數(shù)NB，使用SS公鑰加密保護的主密鑰PMK(Pairwise Master Key)，以及PMK的序列號PMK_SN。同樣，SS對接收到的BS發(fā)送的消息用BS的公鑰解密，認證BS數(shù)字證書的合法性，及前兩條消息中隨機數(shù)NS的值是否一致。

至此，SS和BS間完成了相互認證，SS向BS發(fā)送認證成功消息作為整個EAP認證階段的結束。消息中包含接收到的BS生成的隨機數(shù)NB以及SS的地址信息，并附上校驗和以確保該消息的完整性。授權密鑰AK(Authorization Key)由主密鑰PMK，SS的地址和BS標識號生成，并用于演化出后續(xù)所需的其他密鑰材料，這種密鑰分層機制允許在不增加額外計算復雜度的同時，加密密鑰的頻繁刷新。

1.2 安全組件的交換

認證過程完成后，SS和BS通過安全信息的交換均生成授權密鑰AK，同時還要為每個AK維護同步計數(shù)器AK_COUNT，該計數(shù)器在SS由空閑模式重新進入網(wǎng)絡，安全位置更新等情況下依次遞增。雙方通過AK和AK_COUNT生成CMAC-TEK prekey，從而計算出用于生成CMAC消息摘要的CMAC key。其次，SS與BS間通過三次握手過程實現(xiàn)對安全組件SA(Security Association)的協(xié)商，以確定之后消息傳輸?shù)募用芊绞揭约捌渌璋踩珔?shù)。安全性協(xié)商參數(shù)具體包括包序列號PN的長度以及完整性檢驗值ICV的長度。雙方所協(xié)商成功的SA用SAID標識，用于識別消息無保護、支持機密性、完整保護、只支持機密性保護三種不同的分級保護策略。在安全組件協(xié)商的過程中，SS和BS間傳輸?shù)娜挝帐窒⒍际墙?jīng)過CMAC保護的，將CMAC key與明文消息生成的CMAC摘要附在消息末尾，用以保證消息的認證性和完整性。

1.3 加密密鑰的傳輸

在基站和終端共同維護的合法安全組件下，SS向BS請生成加密傳輸密鑰TEK(Traffic Encryption Key)的關鍵材料。SS向BS發(fā)送包含SAID的密鑰請求消息以及CMAC消息摘要，BS通過檢測消息驗證碼以及SAID的正確性，決定給SS發(fā)送請求確認消息還是請求無效消息。若請求成功，BS給SS發(fā)送用于生成TEK的計數(shù)值Counter_TEK以及用于區(qū)分連續(xù)TEK的序列號EKS。若請求失敗，BS則向SS發(fā)送相應的錯誤代碼及錯誤原因，通知SS需要重新發(fā)送密鑰請求消息。

如圖2所示的密鑰分級結構顯示了出現(xiàn)在PKMv3安全協(xié)議中的所有密鑰和對應密鑰通過Dot16KDF算法的計算方式。經(jīng)過了完整的AK授權，SA連接，TEK交換的過程，BS與SS間已經(jīng)建立了安全機制，即可對雙方正常通信的內容通過密鑰TEK進行加密保護，從而開始消息會話的傳輸過程。

圖2 密鑰層次結構

2 Maude與重寫邏輯

Maude是一種基于重寫邏輯的形式化建模語言和工具。該建模語言主要具有以下三個方面的特點：首先是語言的簡潔性，Maude是一種純函數(shù)式語言，語法結構簡單；其次是表達能力強，其底層邏輯為重寫邏輯，可用于描述軟件系統(tǒng)及邏輯推理系統(tǒng)；同時它的計算性能高，在具體實施過程中，運行速度可與其他高效的編程系統(tǒng)相競爭。因此，Maude在編寫應用程序、描述可執(zhí)行規(guī)范、建立系統(tǒng)模型等方面有著廣泛的應用。

重寫邏輯是一種通用的并發(fā)處理的邏輯框架。它基于代數(shù)語義和重寫語義，可由四元組(Σ,E∪A,φ,R)表示。其中(Σ,E)是重寫邏輯繼承于關系等式邏輯的部分，Σ表示成員關系等式邏輯的簽名，用于表示數(shù)據(jù)的類型，E表示成員關系等式集合，集合中包括等式的定義以及成員關系的聲明，A表示等式屬性的集合。φ表示邏輯簽名Σ中操作符的參數(shù)，R代表重寫規(guī)則的集合，定義了系統(tǒng)狀態(tài)的轉化。

Maude語言用關鍵字sort定義數(shù)據(jù)類型，用關鍵字op實現(xiàn)函數(shù)申明。如以下自然數(shù)操作，構造函數(shù)定義0為單位元，操作s用于描述下一個自然數(shù)，操作+實現(xiàn) 加法算法，同時滿足結合律和交換律。

sort Nat .

op 0 : -> Nat [ctor].

op s_ : Nat -> Nat .

op _+_ : Nat Nat -> Nat [assoc comm] .

通過關鍵字var(vars)生成自然數(shù)類型的變量，以及用eq關鍵字實現(xiàn)具體加法操作的等式定義。

vars X Y : Nat .

eq 0 + X = X .

eq s X + Y = s (X + Y) .

同時，Maude支持通過關鍵字rl或crl定義的重寫規(guī)則或基于條件的重寫規(guī)則，從而描述系統(tǒng)狀態(tài)間的轉換。如下標簽為add的重寫規(guī)則表示某一自然數(shù)執(zhí)行該規(guī)則后轉變?yōu)樗南乱粋€自然數(shù)。

rl[add] : X => s (X) .

此外，Maude還提供rewrite命令用于仿真系統(tǒng)從初始狀態(tài)的一次執(zhí)行，以及search命令用于從一個給定的初始狀態(tài)搜索系統(tǒng)所有可達的狀態(tài)，得以驗證模型的屬性。

3 PKMv3協(xié)議的形式化建模

本文將PKMv3安全協(xié)議及其所處的環(huán)境視為一個系統(tǒng)。在這個系統(tǒng)中，包括發(fā)送和接收消息的誠實主體和其他攻擊者，以及消息發(fā)送和接收的規(guī)則。通過Maude建模語言將系統(tǒng)中的各種對象，狀態(tài)和關系等進行邏輯抽象，并將針對協(xié)議安全性質的討論放在與密碼算法數(shù)學細節(jié)無關的層次上進行。由該協(xié)議中的密鑰結構可知，認證密鑰AK用于生成三次握手與密鑰交換階段的其他所有密鑰，AK的機密性和認證的可靠性保障了后續(xù)加密密鑰TEK的正確生成。因此為了簡化模型，本文通過對認證階段的建模從而檢驗PKMv3協(xié)議的安全性質。

3.1 對通信主體的建模

3.1.1 站點建模

首先，定義Station數(shù)據(jù)類代表網(wǎng)絡中出現(xiàn)的所有站點，并定義Ss和Bs子類分別代表手機站和基站。Ss與Bs類型的數(shù)據(jù)可由String預定義類型的數(shù)據(jù)通過構造函數(shù)ss與bs生成。

sorts Station Ss Bs .

subsorts Ss Bs < Station .

op ss : String -> Ss [ctor].

op bs : String -> Bs [ctor].

主體擁有生成隨機數(shù)的能力，將SS和BS各自的初始隨機值用構造函數(shù)seed和seed1表示，數(shù)據(jù)類型為Rand。next操作用于生成隨機數(shù)序列，例如seed，next(seed)，next(next(seed))。為了區(qū)分網(wǎng)絡中各主體發(fā)送的隨機值，將隨機值Nonce建模為以下構造函數(shù)，箭頭左側的三個變量分別代表發(fā)送、接收消息的主體以及本次消息所用到的隨機數(shù)。

op nonce : Station Station Rand -> Nonce [ctor].

協(xié)議中的每個主體都擁有屬于自己的一對公鑰和私鑰，公鑰被網(wǎng)絡中的所有成員熟知，私鑰只有主體自身持有。定義密鑰類型Key代表協(xié)議中出現(xiàn)的所有的密鑰，并定義其子類型Pubkey和Prikey代表公鑰和私鑰。以下構造函數(shù)生成了各主體的公鑰與私鑰。

op pubkey : Station -> Pubkey [ctor] .

op prikey : Station -> Prikey [ctor] .

另外定義數(shù)據(jù)類MacAddr代表主體的MAC地址，并用操作數(shù)macaddr構造，從而CA簽發(fā)給各主體的X.509證書可表示為以下構造函數(shù)，由主體名、主體的MAC地址和公鑰生成Cert類型的數(shù)字證書。

op cert : Station MacAddr Pubkey -> Cert .

當網(wǎng)絡中的主體接收到其他主體的證書時，必須能從該證書中提取出相應的信息，因此定義以下操作分別從證書中獲得證書擁有者的MAC地址和公鑰。

op getaddr : Cert -> MacAddr .

op getpub : Cert -> Pubkey .

var S : Station .

eq getaddr(cert(S,macaddr(S),pubkey(S))) = macaddr(S) .

eq getpub(cert(S,macaddr(S),pubkey(S))) = pubkey(S).

3.1.2 密鑰信息建模

將協(xié)議中采用的密碼算法用構造函數(shù)進行抽象。用構造函數(shù)capa代表主體支持的加密算法，并用操作符algo代表生成密鑰時使用的數(shù)學算法。

op capa : Station -> Capa [ctor] .

op algo : -> Algo [ctor].

因此，認證過程中生成的主密鑰PMK可表示為以下構造函數(shù)，分別代表參與會話的SS和BS的標識符，各自在認證階段發(fā)送的隨機值以及加密算法。同時，序列號PMK_SN可由PMK生成。

op pmk : Ss Bs Nonce Nonce Algo -> Pmk [ctor ] .

op pmksn: Pmk -> Pmksn [ctor].

認證密鑰AK由PMK衍生而成，相應的構造函數(shù)如下所示，其中Ssaddr代表SS的地址，該類型的數(shù)據(jù)用操作符ssaddr生成。

op ak : Pmk Bs Ssaddr Algo -> Ak [ctor].

3.1.3 消息內容建模

為了便于管理，將網(wǎng)絡中出現(xiàn)的主體類型Station，密鑰類型Key，證書類型Cert，隨機值類型Rand等劃分為Content類型的子類。Content類型的數(shù)據(jù)滿足交換律和結合律，并且將內容集合Contents類型定義為它的父類，集合中各內容間用“,”隔開。為了判斷內容集合中是否存在特定內容，定義布爾操作inc，若符號左邊的內容屬于其右邊內容的集合，則返回true，反之為false。

op contnil : -> Contents [ctor] .

op _,_ : Contents Contents -> Contents [assoc comm] .

op _inc_ : Content Contents -> Bool .

在認證階段中，存在對信息的加密處理以保證機密性。利用主體的公鑰通過操作encrypt將Contents類型的信息集加密為Cipher類型的密文，并用相同主體的私鑰通過操作decrypt進行解密。

op encrypt : Contents Pubkey -> Cipher .

op decrypt : Cipher Prikey -> Ncipher .

消息中對信息的數(shù)字簽名操作保障了信息的完整性來源的可靠性。定義sencrypt操作用主體自身的私鑰對消息進行數(shù)字簽名，反之，用其公鑰將簽名信息恢復為明文。簽名過程中的操作如下所示。

op sencrypt : Contents Prikey -> Content .

op sdecrypt : Contents Pubkey -> Content .

消息的完整性校驗和通過校驗和算法checksum與初始算子iv得出，數(shù)據(jù)類型為Contents的信息從而被加工成Checksum類型的校驗和附在原明文消息后。

op checksum : Contents Iv -> Checksum [ctor] .

op iv : -> Iv [ctor] .

最后，將雙向認證過程SS與BS互相發(fā)送的認證請求，認證響應和認證確認消息內容依次定義為AuthRequest，AuthResponse，AuthConfirm類型，并根據(jù)圖1中的消息元素分別描述他們的構造函數(shù)。

sorts AuthRequest AuthResponse AuthConfirm .

subsorts AuthRequest AuthResponse AuthConfirm < Content .

op authrequest :Cert Nonce Capa->AuthRequest[ctor] .

op authresponse : Cert Nonce Nonce Cipher Pmksn -> AuthResponse [ctor] .

op authconfirm : Nonce Ssaddr -> AuthConfirm [ctor] .

3.2 對網(wǎng)絡環(huán)境的建模

3.2.1 系統(tǒng)狀態(tài)的形式化定義

網(wǎng)絡環(huán)境中包括各主體節(jié)點以及在主體間消息傳遞的行為。將網(wǎng)絡中的主體節(jié)點定義為Node類型，構造函數(shù)中用橫線代表變量的位置，分別表示節(jié)點的主體名和主體已生成或已得到的信息集。

op node[_]:_ : Station Contents -> Node [ctor].

網(wǎng)絡中傳播的消息為Message類型，網(wǎng)絡中的空消息用msgnil表示，發(fā)送消息構造函數(shù)中的變量分別代表發(fā)送方，接收方以及消息的內容。

op msgnil : -> Message [ctor] .

op from_to_send_ : Station Station Contents -> Message [ctor] .

網(wǎng)絡節(jié)點中的信息的集合以及傳遞的消息的集合構成了網(wǎng)絡的當前狀態(tài)。定義網(wǎng)絡的狀態(tài)為State類型，滿足交換律和結合律，它的子類為Node類型和Message類型。操作ina用于表示某一狀態(tài)是否為狀態(tài)集的子集，如果成立則返回true。

sort State .

subsorts Message Contents Node < State .

op __ : State State -> State [assoc comm] .

op _ina_ : State State -> Bool .

3.2.2 系統(tǒng)行為的形式化定義

為了描述協(xié)議中主體通信的動態(tài)過程，采用重寫規(guī)則定義雙向認證中各消息的發(fā)送和接收，實現(xiàn)PKMv3網(wǎng)絡系統(tǒng)的狀態(tài)轉換。圖3所示的重寫規(guī)則描述了誠實主體通信的部分過程，并用下劃線標示出規(guī)則執(zhí)行前后狀態(tài)改變的部分。表1顯示了重寫規(guī)則中出現(xiàn)的各變量的類型以及具體含義。

圖3 描述誠實主體行為的重寫規(guī)則

變量類型描述A,B,CStation手機站,基站,侵入者R1,R2,R0Rand各主體的初始隨機數(shù)NC_X(X=A,B,C)Nonce主體X發(fā)送的隨機值CERT_X(X=A,B,C)Cert主體X的數(shù)字證書PRI1,PRI2Prikey各主體的私鑰PMKPmk主密鑰PMK_SNPmksn主密鑰的序列號MSG1AuthRequest認證請求消息MSG2AuthResponse認證響應消息MSG3AuthConfirm認證確認消息CIPHER,NCIPHERCipher,Ncipher加密,解密后的內容CHECKSUMChecksum消息校驗和

SS向BS發(fā)送認證請求消息作為通信的開始，這一過程用標簽為SendAuthRequestMsg的重寫規(guī)則描述。在消息發(fā)送前，SS和BS的消息集中擁有自身的隨機數(shù)R0和R1，以及X.509數(shù)字證書，并且此時網(wǎng)絡中消息為空。SS生成隨機值NS并向BS發(fā)送認證請求消息，該消息用SS的私鑰加密作為簽名保護。消息發(fā)送后，BS的信息集暫時保持不變。

通過帶條件的重寫規(guī)則RecvAuthRequestMsg模擬BS收到請求認證消息并分析消息元素的過程。getcert1和getnon1操作分別代表提取出請求認證消息MSG1中SS的數(shù)字證書和隨機值。規(guī)則中的if條件語句表示恢復數(shù)字簽名為明文后，若從證書中取得的主體公鑰與用于解密的公鑰一致，則認為該條消息由誠實主體發(fā)送。經(jīng)過本次重寫，網(wǎng)絡中的本條消息被BS所消耗，BS的消息集中添加了SS的數(shù)字證書和SS生成的隨機值。

BS驗證SS的身份后，生成主密鑰PMK和序列號PMK_SN，并向SS發(fā)送經(jīng)過數(shù)字簽名保護的認證響應消息，傳遞PMK相關信息。SS檢測從認證響應消息中獲得BS的數(shù)字證書和隨機值的正確性。若滿足認證條件，SS獲得PKM_SN，并將接收到的PMK加密內容用自己的私鑰進行解密。描述認證響應過程的重寫規(guī)則與認證請求階段類似。

規(guī)則SendAuthConfirmMsg描述了認證確認消息的發(fā)送過程。SS從認證響應消息中成功獲得主密鑰PMK及PMK_SN后，利用自己的地址ssaddr(A)作為參數(shù)生成認證密鑰AK，并向BS發(fā)送認證確認消息，包括BS的隨機值NB以及SS的地址，同時在消息末附上認證確認消息的校驗和。

BS接收到認證確認消息，具體過程如規(guī)則RecvAuthConfirmMsg所示，其中if語句代表如果確認消息MSG3計算出的校驗和結果與接收到的校驗和CHECKSUM一致，且接收到的隨機值NB與自己生成的隨機值相等，則用函數(shù)getssaddr從消息中提取出SS的地址，結合PMK相關信息生成AK。

4 入侵者模型

入侵者屬于網(wǎng)絡環(huán)境中的一部分，它可以參與到正常的協(xié)議過程中去，擁有誠實主體的一切行為能力。此外，入侵者對網(wǎng)絡具有完全的控制力，可竊聽攔截系統(tǒng)中的任何消息，并利用該消息為自己增加新知識，同時還具有重放已知消息或者篡改消息內容的能力。本文將網(wǎng)絡中可能遭遇的攻擊模擬為一個入侵者的行為。

定義Intruder類，并指定它為Station的子類，使其繼承普通站點的所有能力。通過函數(shù)intru生成Intruder類，seed0代表其初始隨機數(shù)。

sort Intruder .

subsort Intruder < Station .

op intru : String -> Intruder [ctor] .

op seed0 : -> Rand [ctor].

同樣，可用重寫規(guī)則描述入侵者以中間人的身份參與到SS與BS間認證會話的行為。重寫規(guī)則中的各變量的定義也如表1所示，將描述誠實主體和入侵者行為的重寫規(guī)則放在同一個系統(tǒng)模塊中，則可共享預定義變量。圖4中的重寫規(guī)則分別表示侵入者進行消息攔截、消息重放和篡改消息的過程。

圖4 描述入侵者行為的重寫規(guī)則

入侵者攔截網(wǎng)絡中通信消息的行為，用規(guī)則RecvAuthResponseMsgFake為例描述。當入侵者攔截到BS發(fā)送給SS的認證響應消息后，利用BS的公鑰對消息的數(shù)字簽名進行解密。若確認了BS證書的合法性和隨機值NB的準確性，則從響應消息MSG2中通過函數(shù)getcert2提取出BS的數(shù)字證書，getnon22提取出隨機值NB，以及getpmksn2提取出PMK_SN，并嘗試解密通過SS公鑰加密的PMK內容。此時SS無法接收到BS發(fā)送的認證響應消息。

竊取到網(wǎng)絡中的消息后，入侵者可選擇將消息原文重放，從而以中間人的身份參與到消息的傳輸中。以入侵者假冒BS將請求響應消息轉發(fā)給SS為例，可用重寫規(guī)則SendAuthResponseMsgFake表示，其中主體C信息集中的變量NCIPHER代表入侵者通過自己的私鑰嘗試解PMK加密信息后得到的內容，其發(fā)送的消息內容是未經(jīng)修改的響應消息。

除了將截獲的原文消息重放，入侵者還可以偽裝為誠實主體將消息內容篡改后再轉發(fā)，從而破壞認證消息的完整性。以入侵者假冒SS向BS發(fā)送認證確認消息為例，具體可描述為重寫規(guī)則SendAuthConfirmMsgChange。箭頭左邊表示入侵者截獲并消耗掉認證確認消息，并從中取得隨機值NB以及SS的地址。箭頭右邊表示入侵者將原消息中SS的地址篡改成自己的地址，并生成新的消息校驗和附在消息后發(fā)送給BS。

對于認證階段消息的每一次收發(fā)過程，入侵者均可以選擇實施類似以上截取，重放和篡改的操作，參與到SS與BS的正常會話中，得以不斷收集和分析新的信息，并阻礙雙方的認證過程。

5 驗證與分析

本文采用基于模型檢測的協(xié)議分析方法，基于已定義的網(wǎng)絡環(huán)境的狀態(tài)模型以及狀態(tài)遷移的重寫規(guī)則，可通過窮盡搜索狀態(tài)空間從而判斷某些特定狀態(tài)的可達性，檢驗出協(xié)議的安全性質。使用Maude中的search指令實現(xiàn)協(xié)議模型的安全性檢測，search指令能遍歷系統(tǒng)的全部重寫行為，并找出所有與規(guī)定的模式相匹配的狀態(tài)。

通過init操作指定PKMv3協(xié)議所處的網(wǎng)絡環(huán)境的初始狀態(tài)。并假設在初始狀態(tài)中，存在名為a的手機站，名為b的基站以及名為c的入侵者，它們擁有各自的數(shù)字證書和初始隨機數(shù)，并且此時網(wǎng)絡中的消息為空。

op init : -> State [ctor] .

eq init = (node[ss(″a″)]: seed,cert(ss(″a″),macaddr(

ss(″a″)),pubkey(ss(″a″)))) (node[bs(″b″)]: seed1,

cert(bs(″b″), macaddr(bs(″b″)),pubkey(bs(″b″))))

(node[intru(″c″)]: seed0, cert(intru(″c″),macaddr(

intru(″c″)),pubkey(intru(″c″)))) (msgnil) .

本文利用Maude檢測工具從以下幾個方面驗證了PKMv3協(xié)議模型的安全性質：

1) 機密性 協(xié)議的機密性表現(xiàn)為在誠實主體的通信過程中，入侵者無法獲取EAP傳輸中的主密鑰PMK，從而即使其竊取到生成AK的其他信息，如SS的地址，BSID 等，也無法最終生成認證密鑰AK以完成后續(xù)的通信。使用如下search指令以初始狀態(tài)為起點，檢測所有可達的最終狀態(tài)，查找侵入者的消息集中存在PMK的可達路徑。

Maude> search init =>! (S:State) (node[intru(″c″)]: C:Contents) such that pmk(ss(″a″),bs(″b″),nonce(ss(″a″),bs(″b″),seed), nonce(bs(″b″),ss(″a″),seed1),

algo) inc C:Contents .

No solution.

states: 26 rewrites: 347 in 4ms cpu (2ms real) (86750 rewrites/second)

執(zhí)行該指令返回結果為不存在解決方案，表明侵入者在任意可達狀態(tài)下都不可能竊取到明文狀態(tài)的主密鑰PMK。因此，該協(xié)議可滿足密鑰的機密性。

2) 認證性 認證性是協(xié)議最重要的安全性質，該協(xié)議的認證性體現(xiàn)在即使有入侵者的參與，SS和BS間仍能相互間確認真實身份。執(zhí)行search語句搜尋SS成功接收BS傳輸?shù)闹髅荑€PMK的最終狀態(tài)。

Maude> search init =>! (S:State) (node[ss(″a″)]: C:Contents) such that pmk(ss(″a″),bs(″b″),nonce(ss(″a″),bs(″b″),seed), nonce(bs(″b″),ss(″a″),seed1),algo) inc C:Contents .

Solution 1 (state 13)

states: 17 rewrites: 173 in 0ms cpu (1ms real) (～ rewrites/second)

C:Contents -->…pmk(ss(″a″),bs(″b″),nonce(ss(″a″), bs(″b″),seed),nonce(bs(″b″),ss(″a″),seed1),algo) …

Solution 5 (state 25)

…

No more solutions.

states: 26 rewrites: 347 in 4ms cpu (4ms real) (86750 rewrites/second)

執(zhí)行結果顯示共有四種可達路徑。使用show path labels[state]語句，打印出各方案所執(zhí)行的重寫規(guī)則序列，分析得出四條路徑分別為SS和BS間無入侵者干擾的認證過程，以及入侵者以中間人的身份依次加入到雙方認證請求，認證響應和認證確認消息的傳輸中的過程中。實驗結果表明，SS和BS總是能實現(xiàn)身份認證并成功交換主密鑰PMK。

3) 完整性 協(xié)議的完整性保證是指誠實主體間傳遞的消息不能被誤傳和篡改，或至少能夠檢測出錯誤的消息數(shù)據(jù)。在消息的請求和響應階段均使用了數(shù)字簽名保障完整性和認證性，因此主要檢測確認消息的完整性，使用search語句檢測BS收到錯誤的SS地址，從而生成與BS不一致AK的可能性。

Maude> search init =>* (S:State) (node[bs(″b″)]: (C:Contents),(A:Ssaddr),(K:Ak)) such that A:Ssaddr =/= ssaddr(ss(″a″)) .

Solution 1 (state 25)

states: 26 rewrites: 345 in 4ms cpu (3ms real) (86250 rewrites/second)

S:State --> …

A:Ssaddr --> ssaddr(intru(″c″))

K:Ak --> ak(pmk(ss(″a″), bs(″b″), nonce(ss(″a″), bs(″b″), seed), nonce(bs(″b″),ss(″a″), seed1), algo),bs(″b″), ssaddr(intru(″c″)), algo)

No more solutions.

states: 26 rewrites: 345 in 8ms cpu (5ms real) (43125 rewrites/second)

執(zhí)行結果返回一條重寫路徑，表明BS接收到入侵者篡改過后的SS地址ssaddr(intru(“c”))，利用其生成無效的認證密鑰AK，使得消息的完整性遭到破壞。并且SS雖然與BS實現(xiàn)了相互認證，仍存在因無效AK無法進行后續(xù)通信的可能。這是由于認證確認消息采用了通用校驗和算法，入侵者可以將截獲的消息篡改后，自行生成對應的校驗和。BS只能確認收到的消息沒有被網(wǎng)絡誤傳，并無法驗證其是否被攻擊者惡意篡改。

針對以上出現(xiàn)的無法保障協(xié)議完整性的安全漏洞，存在一種可行的改進方案：通過使用認證密鑰AK計算出認證確認消息的校驗和。BS先利用接收到的SS地址生成AK，再對比AK與明文消息的計算結果和校驗和是否一致。由于入侵者始終無法獲得明文PMK，從而無法生成AK并得出正確的校驗和，用AK作為算子生成校驗和保障了消息不會被非法用戶篡改。修改過后的認證確認消息可表示為：

SS -> BS : NB| SS_Address | AK(NB| SS_Address)

將建模過程中校驗和操作checksum中的初始算子iv改為AK的值，再重新執(zhí)行該search語句。返回結果為No Solution，表明改進過后的認證過程可保障消息傳輸?shù)耐暾浴?/p>

6 結 語

本文對IEEE802.16m中的密鑰管理PKMv3協(xié)議進行了詳細的分析和研究，并利用基于重寫邏輯的Maude語言對協(xié)議的認證階段實現(xiàn)形式化建模，從而驗證了該協(xié)議的安全特性。驗證結果表明，PKMv3協(xié)議能保證密鑰的機密性，參與協(xié)議主體雙方的認證性。但采用傳統(tǒng)校驗和方式的驗證確認消息會遭遇中間人攻擊，使得消息的完整性和生成AK的正確性都無法保證，而利用AK計算確認消息校驗和的方式則可解決這一問題。下一步工作將繼續(xù)對協(xié)議中的三次握手以及密鑰交換階段進行建模，并引入時間機制探討密鑰的生命周期。

[1] Ieee B E.802.16m-2011 - IEEE Standard for Local and metropolitan area networks Part 16:Air Interface for Broadband Wireless Access Systems Amendment 3:Advanced Air Interface[S].2011:1-1112.

[2] Andrews J G,Ghosh A,Muhamed R.Fundamentals of WiMAX:Understanding Broadband Wireless Networking[J].Prentice Hall Communications Engineering & Emerging Technologies,2007.

[3] 楊玖宏,王玉柱,何定養(yǎng).IEEE802.16m中PKMv3協(xié)議的安全分析及改進[J].中國儲運,2012(8):126-129.

[4] Xu S,Huang C T.Attacks on PKM Protocols of IEEE 802.16 and Its Later Versions[C]//International Symposium on Wireless Communication Systems,2006:185-189.

[5] Kahya N,Ghoualmi N,Lafourcade P.Formal analysis of PKM using scyther tool[C]//International Conference on Information Technology and E-Services.IEEE,2012:1-6.

[6] Xu S,Huang C T,Matthews M M.Modeling and analysis of IEEE 802.16 PKM Protocols using CasperFDR[C]//IEEE International Symposium on Wireless Communication Systems.IEEE,2008:653-657.

[7] Sikkens B.Security issues and proposed solutions concerning authentication and authorization for WiMAX (IEEE 802.16 e)[C]//Proc.of 8th Conference on IT Enschede University of Twente.2008.

[8] Raju K V K,Kumari V V,Varma N S,et al.Formal Verification of IEEE802.16m PKMv3 Protocol Using CasperFDR[C]//Information and Communication Technologies-International Conference,ICT 2010,Kochi,Kerala,India,September 7-9,2010.Proceedings,2010:590-595.

[9] Zhu X,Xu Y,Guo J,et al.Formal Verification of PKMv3 Protocol Using DT-Spin[C]//International Symposium on Theoretical Aspects of Software Engineering.IEEE,2015:71-78.

[10] Hashmi R M,Siddiqui A M,Jabeen M,et al.Improved Secure Network Authentication Protocol (ISNAP) for IEEE 802.16[C]//International Conference on Information and Communication Technologies.IEEE Xplore,2009:101-105.

[11] Altaf A,Sirhindi R,Ahmed A.A Novel Approach against DoS Attacks in WiMAX Authentication Using Visual Cryptography[C]//International Conference on Emerging Security Information,Systems and Technologies,2008.Securware.IEEE Xplore,2008:238-242.

[12] Kim Y,Lim H K,Bahk S.Shared Authentication Information for Preventing DDoS attacks in Mobile WiMAX Networks[C]//Consumer Communications and NETWORKING Conference,2008.Ccnc.IEEE,2008:765-769.

[13] Fu A,Zhang Y,Zhu Z,et al.A Fast Handover Authentication Mechanism Based on Ticket for IEEE 802.16m[J].Communications Letters IEEE,2010,14(12):1134-1136.

[14] 尹劍飛,王學斌.模型轉換的重寫邏輯構架研究[J].計算機工程與應用,2006,42(2):14-16.

[15] Clavel M,Durán F,Eker S,et al.Maude Manual (Version 2.4)[M].University of Illinois,2008.

[16] Pita I,Riesco A.Specifying and Analyzing the Kademlia Protocol in Maude[C]//International Colloquium on Theoretical Aspects of Computing-ICTAC. Springer-Verlag New York,Inc,2015.

FORMALMODELINGANDVERIFICATIONOFPKMV3PROTOCOLBASEDONREWRITINGLOGIC

She Jia Zhang Min

(InstituteofComputerScienceandSoftwareEngineering,EastChinaNormalUniversity,Shanghai200062,China)

IEEE802.16m standard defines PKMv3 (Privacy and Key management) protocol in MAC security sub-layer to realize the transmission of authentication information and exchange of secret key. Because of the vulnerability of broadband wireless network, intruder model is introduced to analyze the security mechanism of this key management protocol. Using a formal modeling language Maude which based on rewriting logic, we achieved the modeling of communication agent and system state in PKMv3 network environment. And Maude utilized formal verification tools to verify the security feature of this protocol. Verification result showed that PKMv3 protocol can guarantee the confidentiality of secret key and the reliability of authentication. However, it also showed that the protocol cannot prevent Man-in-the-Middle attack and the integrity of message transmission may be destroyed.

IEEE 802.16m standard PKMv3 protocol Key management Rewriting logic Maude language Formal verification

2017-02-04。國家自然科學基金青年基金項目(61502171)。佘葭，碩士生，主研領域：高可信計算理論與技術。張民，副教授。

TP311.5

A

10.3969/j.issn.1000-386x.2017.11.050