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

佘 葭 張 民

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

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

佘 葭 張 民

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

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

IEEE802.16m標(biāo)準(zhǔn) PKMv3協(xié)議 密鑰管理 重寫(xiě)邏輯 Maude語(yǔ)言 形式化驗(yàn)證

0 引 言

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

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

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

1 PKMv3協(xié)議

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

1.1 雙向認(rèn)證過(guò)程

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

圖1 雙向認(rèn)證過(guò)程

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

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

1.2 安全組件的交換

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

1.3 加密密鑰的傳輸

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

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

圖2 密鑰層次結(jié)構(gòu)

2 Maude與重寫(xiě)邏輯

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

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

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

sort Nat .

op 0 : -> Nat [ctor].

op s_ : Nat -> Nat .

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

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

vars X Y : Nat .

eq 0 + X = X .

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

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

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

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

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

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

3.1 對(duì)通信主體的建模

3.1.1 站點(diǎn)建模

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

sorts Station Ss Bs .

subsorts Ss Bs < Station .

op ss : String -> Ss [ctor].

op bs : String -> Bs [ctor].

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

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

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

op pubkey : Station -> Pubkey [ctor] .

op prikey : Station -> Prikey [ctor] .

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

op cert : Station MacAddr Pubkey -> Cert .

當(dāng)網(wǎng)絡(luò)中的主體接收到其他主體的證書(shū)時(shí)，必須能從該證書(shū)中提取出相應(yīng)的信息，因此定義以下操作分別從證書(shū)中獲得證書(shū)擁有者的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é)議中采用的密碼算法用構(gòu)造函數(shù)進(jìn)行抽象。用構(gòu)造函數(shù)capa代表主體支持的加密算法，并用操作符algo代表生成密鑰時(shí)使用的數(shù)學(xué)算法。

op capa : Station -> Capa [ctor] .

op algo : -> Algo [ctor].

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

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

op pmksn: Pmk -> Pmksn [ctor].

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

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

3.1.3 消息內(nèi)容建模

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

op contnil : -> Contents [ctor] .

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

op _inc_ : Content Contents -> Bool .

在認(rèn)證階段中，存在對(duì)信息的加密處理以保證機(jī)密性。利用主體的公鑰通過(guò)操作encrypt將Contents類(lèi)型的信息集加密為Cipher類(lèi)型的密文，并用相同主體的私鑰通過(guò)操作decrypt進(jìn)行解密。

op encrypt : Contents Pubkey -> Cipher .

op decrypt : Cipher Prikey -> Ncipher .

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

op sencrypt : Contents Prikey -> Content .

op sdecrypt : Contents Pubkey -> Content .

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

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

op iv : -> Iv [ctor] .

最后，將雙向認(rèn)證過(guò)程SS與BS互相發(fā)送的認(rèn)證請(qǐng)求，認(rèn)證響應(yīng)和認(rèn)證確認(rèn)消息內(nèi)容依次定義為AuthRequest，AuthResponse，AuthConfirm類(lèi)型，并根據(jù)圖1中的消息元素分別描述他們的構(gòu)造函數(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 對(duì)網(wǎng)絡(luò)環(huán)境的建模

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

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

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

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

op msgnil : -> Message [ctor] .

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

網(wǎng)絡(luò)節(jié)點(diǎn)中的信息的集合以及傳遞的消息的集合構(gòu)成了網(wǎng)絡(luò)的當(dāng)前狀態(tài)。定義網(wǎng)絡(luò)的狀態(tài)為State類(lèi)型，滿(mǎn)足交換律和結(jié)合律，它的子類(lèi)為Node類(lèi)型和Message類(lèi)型。操作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é)議中主體通信的動(dòng)態(tài)過(guò)程，采用重寫(xiě)規(guī)則定義雙向認(rèn)證中各消息的發(fā)送和接收，實(shí)現(xiàn)PKMv3網(wǎng)絡(luò)系統(tǒng)的狀態(tài)轉(zhuǎn)換。圖3所示的重寫(xiě)規(guī)則描述了誠(chéng)實(shí)主體通信的部分過(guò)程，并用下劃線(xiàn)標(biāo)示出規(guī)則執(zhí)行前后狀態(tài)改變的部分。表1顯示了重寫(xiě)規(guī)則中出現(xiàn)的各變量的類(lèi)型以及具體含義。

圖3 描述誠(chéng)實(shí)主體行為的重寫(xiě)規(guī)則

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

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

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

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

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

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

4 入侵者模型

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

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

sort Intruder .

subsort Intruder < Station .

op intru : String -> Intruder [ctor] .

op seed0 : -> Rand [ctor].

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

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

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

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

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

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

5 驗(yàn)證與分析

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

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

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檢測(cè)工具從以下幾個(gè)方面驗(yàn)證了PKMv3協(xié)議模型的安全性質(zhì)：

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

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í)行該指令返回結(jié)果為不存在解決方案，表明侵入者在任意可達(dá)狀態(tài)下都不可能竊取到明文狀態(tài)的主密鑰PMK。因此，該協(xié)議可滿(mǎn)足密鑰的機(jī)密性。

2) 認(rèn)證性 認(rèn)證性是協(xié)議最重要的安全性質(zhì)，該協(xié)議的認(rèn)證性體現(xiàn)在即使有入侵者的參與，SS和BS間仍能相互間確認(rèn)真實(shí)身份。執(zhí)行search語(yǔ)句搜尋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í)行結(jié)果顯示共有四種可達(dá)路徑。使用show path labels[state]語(yǔ)句，打印出各方案所執(zhí)行的重寫(xiě)規(guī)則序列，分析得出四條路徑分別為SS和BS間無(wú)入侵者干擾的認(rèn)證過(guò)程，以及入侵者以中間人的身份依次加入到雙方認(rèn)證請(qǐng)求，認(rèn)證響應(yīng)和認(rèn)證確認(rèn)消息的傳輸中的過(guò)程中。實(shí)驗(yàn)結(jié)果表明，SS和BS總是能實(shí)現(xiàn)身份認(rèn)證并成功交換主密鑰PMK。

3) 完整性 協(xié)議的完整性保證是指誠(chéng)實(shí)主體間傳遞的消息不能被誤傳和篡改，或至少能夠檢測(cè)出錯(cuò)誤的消息數(shù)據(jù)。在消息的請(qǐng)求和響應(yīng)階段均使用了數(shù)字簽名保障完整性和認(rèn)證性，因此主要檢測(cè)確認(rèn)消息的完整性，使用search語(yǔ)句檢測(cè)BS收到錯(cuò)誤的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í)行結(jié)果返回一條重寫(xiě)路徑，表明BS接收到入侵者篡改過(guò)后的SS地址ssaddr(intru(“c”))，利用其生成無(wú)效的認(rèn)證密鑰AK，使得消息的完整性遭到破壞。并且SS雖然與BS實(shí)現(xiàn)了相互認(rèn)證，仍存在因無(wú)效AK無(wú)法進(jìn)行后續(xù)通信的可能。這是由于認(rèn)證確認(rèn)消息采用了通用校驗(yàn)和算法，入侵者可以將截獲的消息篡改后，自行生成對(duì)應(yīng)的校驗(yàn)和。BS只能確認(rèn)收到的消息沒(méi)有被網(wǎng)絡(luò)誤傳，并無(wú)法驗(yàn)證其是否被攻擊者惡意篡改。

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

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

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

6 結(jié) 語(yǔ)

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

[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ìn)[J].中國(guó)儲(chǔ)運(yùn),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] 尹劍飛,王學(xué)斌.模型轉(zhuǎn)換的重寫(xiě)邏輯構(gòu)架研究[J].計(jì)算機(jī)工程與應(yīng)用,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。國(guó)家自然科學(xué)基金青年基金項(xiàng)目(61502171)。佘葭，碩士生，主研領(lǐng)域：高可信計(jì)算理論與技術(shù)。張民，副教授。

TP311.5

A

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