一種改進的IKEv2協(xié)議及其形式化驗證

摘 要:針對IKEv2協(xié)議在系統(tǒng)開銷和發(fā)起方身份保護方面的不足，提出了一種改進協(xié)議的方案。新的協(xié)議采用基于超橢圓曲線的Weil對技術(shù)進行數(shù)字簽名認(rèn)證，并且首先認(rèn)證響應(yīng)方身份。通過該方案，改進后的協(xié)議降低了系統(tǒng)開銷，實現(xiàn)了對發(fā)起方身份的主動保護。最后，基于應(yīng)用pi演算的方法對協(xié)議進行了建模，并定義和分析了協(xié)議的安全屬性。結(jié)果表明，改進后的協(xié)議具有更好的安全性和實用性。

關(guān)鍵詞:IKEv2協(xié)議; 身份保護; Weil對; 應(yīng)用pi演算

中圖分類號:TP393.08

文獻(xiàn)標(biāo)志碼:A

文章編號:1001-3695(2010)02-0707-05

doi:10.3969/j.issn.1001-3695.2010.02.084

Improved IKEv2 protocol and its formal verification

HAN Ming-kui， PAN Jin， LI Bo

(Xi’an Communications Institute， Xi’an 710106， China)

Abstract:IKEv2 protocol had some flaw in protecting initiator’s identity and system requirement， so this paper presented an improved protocol. In the new protocol， used Weil pairing technology， based on hyperelliptic curves， in digital signature authentication， and first authenticated the responder. By those means， the protocol had reduced the system cost and actively protected the initiator’s identity. At last， formally analyzed the improved protocol’s security property based on applied pi calculus. Analysis result shows that the protocol has a better performance in secure and application.

Key words:IKEv2 protocol; identity protection; Weil pairing; applied pi calculus

由于Internet密鑰交換協(xié)議IKEv1[1]標(biāo)準(zhǔn)過于復(fù)雜、協(xié)商效率低、容易受到DoS攻擊和中間人攻擊[2]，IETF工作組推出了IKEv2[3]協(xié)議用于替代IKEv1。新版本的協(xié)議提供了兩種認(rèn)證方式，即預(yù)共享密鑰認(rèn)證和數(shù)字簽名認(rèn)證。但這兩種認(rèn)證方式都存在問題。文獻(xiàn)[4]指出預(yù)共享密鑰認(rèn)證方式存在無法大規(guī)模應(yīng)用、暴力字典破解等問題。文獻(xiàn)[5]通過頻繁更換預(yù)共享密鑰的方法抵御離線字典攻擊。文獻(xiàn)[6]通過修改密鑰生成算法解決預(yù)共享密鑰認(rèn)證的中間人攻擊問題。文獻(xiàn)[7]指出數(shù)字簽名認(rèn)證依賴于公鑰基礎(chǔ)設(shè)施PKI，并且傳輸、維護、保存、驗證證書等造成的巨大開銷使該方式不適于實時和低帶寬等情況。同時，兩種認(rèn)證方式都不能保護相對重要的發(fā)起方的身份[8]。作為互聯(lián)網(wǎng)關(guān)鍵的安全技術(shù)之一，對IKEv2協(xié)議進行分析和改進有著非常重要的意義。

文獻(xiàn)[9，10]提出了一些保護發(fā)起方身份的方案，但不夠理想。本文通過基于身份認(rèn)證的公鑰密碼體制提出了一個新的改進方案。基于身份認(rèn)證的公鑰密碼體制思想最早由文獻(xiàn)[11]提出，在該體制中公鑰由用戶的身份信息獲得，私鑰由可信第三方生成。基于該思想，相繼提出了多個實現(xiàn)方案，但實用性均不強。2001年，文獻(xiàn)[12]提出的基于超橢圓曲線的Weil對技術(shù)是第一個公認(rèn)有效的方案。本文基于Weil對技術(shù)改進了IKEv2協(xié)議，并且基于應(yīng)用pi演算[13~15]的方法對改進后協(xié)議的安全屬性進行了證明。分析結(jié)果表明，在無須部署PKI的情況下，新的協(xié)議是安全的，并且能夠保護發(fā)起方的身份。

1 IKEv 2協(xié)議及其分析

1.1 IKEv 2協(xié)議介紹

首先對標(biāo)志符進行說明。I和R分別代表發(fā)起方和響應(yīng)方;HDR為IKE消息頭部，用于標(biāo)志當(dāng)前會話;SA為安全關(guān)聯(lián)，用來協(xié)商安全參數(shù);KE為用于進行DH(Diffie- Hellman)交換的公共參數(shù);N為隨機數(shù)nonce，保證密鑰和消息的新鮮性;ID為協(xié)議參與方的身份;AUTH為認(rèn)證載荷，用于身份認(rèn)證和消息完整性保護;CERT/ CERTREQ為證書/證書請求;TS為流量選擇載荷;sk{}表示對內(nèi)容進行加密和完整性保護。

IKEv2初始交換協(xié)議由四條消息組成，前兩條消息被稱做IKE_SA_INIT交換，主要進行密鑰算法的協(xié)商、nonce以及DH交換，從而生成用于加密和驗證后續(xù)交換的密鑰材料。后兩條消息被稱做IKE_AUTH交換，實現(xiàn)對前兩條消息的驗證，同時交換身份和證書信息，并建立第一個IPSec SA，除消息頭外，IKE_AUTH交換中的消息都用前面生成的密鑰材料進行了加密和完整性保護。當(dāng)檢測到DoS攻擊時，增加兩條包含cookie的消息。協(xié)議描述如下:

1 I→R: HDR， SAi1， KEi， Ni

2 R→I: HDR， SAr1， KEr， Nr，[CERTREQ]

3 I→R: HDR， sk{IDi，[CERT]，[CERTREQ]， AUTH， SAi2， TSi， TSr}

4 R→I: HDR， sk{IDr，[CERT]，AUTH， SAr2， TSi，TSr}

1.2 協(xié)議分析

文獻(xiàn)[8]指出Internet用戶(特別是移動IP用戶)的身份及位置信息的保密性尤為重要，所以協(xié)議應(yīng)當(dāng)對發(fā)起方提供主動身份保護，然而協(xié)議對發(fā)起方只提供了被動身份保護。本文采用應(yīng)用pi演算與協(xié)議分析工具ProVerif[16]相結(jié)合的方法驗證了文獻(xiàn)[9，10]指出的問題。下面過程給出了ProVerif輸出的攻擊者P得到發(fā)起方I身份的過程:I向R發(fā)送第一條消息請求建立SA，攻擊者P截獲消息并冒充R與I進行交互。P(R)表示攻擊者冒充響應(yīng)方R，a1、a2、a3是攻擊者生成的符合載荷格式的數(shù)據(jù)。攻擊步驟4是指P得到包含I身份的消息3后不再響應(yīng)或認(rèn)證失敗等導(dǎo)致的協(xié)商中斷。由于P和I建立了共享密鑰，可以解密消息3，得到I的身份IDi。

1 I→R: HDR，SAi1，KEi，Ni

2 I→P(R):HDR，SAi1，KEi，Ni

3 P(R)→I: HDR， a1，a2，a3

4 I→P(R):HDR，sk{IDi， AUTH， SAi2，TSi，TSr}

5 交換中斷

此外，協(xié)議在應(yīng)用方面存在問題。在IKEv2協(xié)議的預(yù)共享密鑰認(rèn)證方式中，任何兩個通信實體之間都要共享一個密鑰的要求導(dǎo)致密鑰數(shù)量會隨著通信實體的增加而劇增(如n個通信實體需要n×(n-1)/2個密鑰)。數(shù)字簽名認(rèn)證的前提是部署公鑰基礎(chǔ)設(shè)施PKI，認(rèn)證中心CA不僅要為通信實體簽發(fā)證書，還要在網(wǎng)絡(luò)中維護PKI;通信實體間證書的傳遞會導(dǎo)致帶寬需求增大，存儲對方的證書則需要較大存儲空間[17]。因此，提供一種低開銷的數(shù)字簽名認(rèn)證方案具有很好的應(yīng)用價值。

2 基于Weil對改進的IKEv 2協(xié)議設(shè)計

2.1 Weil對技術(shù)

設(shè)G1、G2分別是階為q的加法循環(huán)群和乘法循環(huán)群。其中q是大素數(shù)，且在G1、G2中離散對數(shù)問題都是難解的。設(shè)e∧是G1×G1→G2的雙線性映射，滿足如下性質(zhì):

a)雙線性。對任意P，Q∈G1，所有a，b∈Z+，滿足e∧(aP，bQ)=e∧(P，Q)ab;同時，對任意P1，P2，Q∈G1，有e∧(P1+P2，Q)=e∧(P1，Q)×e∧(P2，Q)。

b)非退化性。若P是G1的生成元，則e∧(P，P)∈G2是G2的生成元。

c)可計算性。存在一個高效的算法計算e∧(P，Q)，P，Q∈G1。

通常G1取為有限域Fe上的橢圓曲線有理點群的一個加法子群，G2取為這個有限域的擴域上的一個乘法子群，雙線性映射e∧由橢圓曲線上的Weil配對派生得到。H1、H2是公開的加密用哈希函數(shù)，H1:{0，1}→G1，H2:{0，1}×G2→Fq。

構(gòu)建可信第三方:私鑰生成中心(private key generator，PKG)，PKG隨機選擇一個生成元P∈G1和一個整數(shù)s∈Fp。計算Qta=sP，公開(P，Qta)，保密s作為系統(tǒng)主密鑰。對任一客戶端C，PKG在驗證了用戶的身份后計算并安全分發(fā)用戶的私鑰。設(shè)C的身份由字符串ID給出，則C的公鑰Qc=H1(ID)，私鑰Sc=sQc，密鑰對為(Qc，Sc)。

2.2 基于Weil對改進的IKEv 2協(xié)議

針對1.2節(jié)中指出的問題，本文改進了協(xié)議的初始交換部分。一方面，由于Weil對技術(shù)實現(xiàn)了基于身份的公鑰密碼體制，可以把Weil對技術(shù)用于IKEv2協(xié)議的數(shù)字簽名認(rèn)證。I、R在獲得對方身份ID之后即可計算其公鑰并對簽名進行認(rèn)證，無須在協(xié)議信息中請求和發(fā)送證書，也就不必部署PKI。另一方面，為了保證協(xié)議的靈活性，改進后的IKEv2協(xié)議保留了預(yù)共享密鑰認(rèn)證方式，協(xié)議雙方可以在SA提議中指出具體的認(rèn)證方式。改進后協(xié)議的框架、載荷類型、標(biāo)志符等與RFC4306中定義保持一致，如下所示:

1′ I→R:HDR，SAi1，KEi，Ni

2′ R→I:HDR，SAr1，KEr，Nr，sk{IDr，AUTHr}

3′ I→R:HDR，sk{IDi，IDr，AUTHi，SAi2，TSi，TSr}

4′ R→I:HDR，sk{IDi，IDr，SAr2，TSi，TSr}

改進后的IKEv2初始交換協(xié)議由四條消息組成，為了區(qū)別于原有消息記為消息i′。當(dāng)檢測到DoS攻擊時，采用cookie機制增加兩條消息。

消息1′:發(fā)起方I發(fā)起建立連接的請求，向響應(yīng)方R發(fā)送安全關(guān)聯(lián)SA提議、DH交換值、保證密鑰新鮮性和防重放攻擊的隨機值Ni。

消息2′:響應(yīng)方R選擇一個SA提議，并將自己的DH交換值、隨機值Nr以及加密后的身份信息IDr和認(rèn)證載荷AUTH一起發(fā)送給發(fā)起方I。

消息3′:在驗證了響應(yīng)方的認(rèn)證載荷之后，I向R發(fā)送用于IPSec SA的提議，同時包括自己的身份信息和證明、對方的身份信息以及流量選擇符。

消息4′:R選擇一個提議，并響應(yīng)I的認(rèn)證消息，完成初始交互。

采用數(shù)字簽名認(rèn)證方式時，公鑰由用戶的身份信息ID確定，私鑰由PKG生成。密鑰衍生和認(rèn)證載荷的計算分別滿足式(1)～(4)。S{}表示使用私鑰對內(nèi)容進行簽名。

數(shù)字簽名方式的密鑰衍生滿足如下公式:

SKEYSEED=prf(Ni|Nr，g^ir)(1)

{SK_d|SK_ai|SK_ar|SK_ei|SK_er|SK_pi

|SK_pr}=prf+(SKEYSEED，Ni|Nr|SPIi|SPIr)

(2)

數(shù)字簽名方式認(rèn)證載荷的計算滿足如下式:

AUTHr=S{HDR，SAr1，KEr，Nr，Ni，prf(SK_pr，IDr)}(3)

AUTHi=S{HDR，SAi1，KEi，Ni，Nr，prf(SK_pi，IDi)}(4)

采用預(yù)共享密鑰認(rèn)證方式時，將預(yù)共享密鑰值散列后參與種子密鑰的衍生，可以抵御中間人攻擊、提供發(fā)起方身份的主動保護。該認(rèn)證方式下的密鑰衍生和認(rèn)證載荷的計算滿足式(2)和(5)～(7)。

預(yù)共享密鑰方式的密鑰衍生滿足下式:

SKEYSEED=prf(Ni|Nr|prf(shared secred，

\"Key Pad for IDEv2\")，g^ir)(5)

預(yù)共享密鑰方式認(rèn)證載荷的計算滿足下式:

AUTHr=prf(prf(shared secret，\"Key Pad for IKEv2\")，

(HDR，SAr1，KEr，Nr，Ni，prf(SK_pr，IDr)))

(6)

AUTHi=prf(prf(shared secret，\"Key Pad for IKEv2\")，

(HDR，SAi1，KEi，Ni，Nr，prf(SK_pi，IDi)))

(7)

3 基于應(yīng)用pi演算的安全協(xié)議證明

基于應(yīng)用pi演算分析協(xié)議的安全屬性是一種新的形式化方法。應(yīng)用pi演算是交互、并發(fā)系統(tǒng)的理論模型，提供了相關(guān)的概念框架和數(shù)學(xué)工具，用于建模、描述系統(tǒng)，并推導(dǎo)系統(tǒng)的安全性質(zhì)。基于應(yīng)用pi演算的形式化分析方法適合分析并發(fā)、分布式的協(xié)議，具有簡潔高效的特點[18，19]。

3.1 應(yīng)用pi演算

3.1.1 應(yīng)用pi演算的語法語義

定義Σ為一有限函數(shù)集合，給定一個Σ，應(yīng)用pi演算的項定義如下:

L，M，N::=n|x|f(M1，M2，…，Ml) f∈Σ

其中:n表示名，x表示變量，f(M1，M2，…，Ml)表示函數(shù)項，l是函數(shù)f的項數(shù)。

應(yīng)用pi演算的普通進程定義如下:

P，Q，R::=0|P|Q|!P|(vn).P|if M=N then P

else Q|c(x)c-〈M〉.P

其中:0表示空進程，P|Q表示并發(fā)復(fù)合，!P表示復(fù)制，(vn).P表示范圍受限，if M=N then P else Q表示條件，c(x).P表示輸入，c-〈M〉.P表示輸出。

普通進程增加主動替換(active substitution)原語，可以被擴展為擴展進程。定義如下:

A，B，C::=P|A|B|(vn).A|(vx).A|{M/x}

其中:P表示普通進程，A|B表示并發(fā)復(fù)合，(vn).A表示名受限，(vx).A表示變量受限，{M/x}表示主動替換。

應(yīng)用pi演算的語義包括用于函數(shù)約簡的等式理論，以及擴展進程間的結(jié)構(gòu)等價、內(nèi)部約簡關(guān)系等。等式理論是符號集合Σ中項集合上的等價關(guān)系，且其在主動替換的條件下封閉;結(jié)構(gòu)等價“≡”在名、變量的α轉(zhuǎn)換以及評價上下文下封閉;內(nèi)部約簡用“→”表示，是封閉擴展進程集合上最小關(guān)系，并在結(jié)構(gòu)等價，評價上下文下封閉;標(biāo)記操作語義用于進程和與其交互的環(huán)境行為的推理。

3.1.2 應(yīng)用pi演算的等價關(guān)系

應(yīng)用pi演算使用上下文代表主動攻擊者，上下文不能區(qū)分的兩個進程滿足觀察等價，表示攻擊者不能區(qū)分進程內(nèi)容的不同。這一節(jié)主要介紹應(yīng)用pi演算的觀察等價、框架的靜態(tài)等價、標(biāo)記等價，并說明標(biāo)記等價與觀察等價的一致性，從而得到證明進程等價的簡便方法。

在定義觀察等價之前，需要定義表示進程在通道上可觀察的謂詞。若擴展進程A能夠在通道a上發(fā)送消息則稱擴展進程A在通道a上可觀察，記做Aa，即對不限制a的上下文有:A→C[a-〈m〉.P]。

定義1 觀察等價≈。

觀察等價是具有相同域(domain)的擴展進程間最大的對稱關(guān)系，且A R B滿足:

1)若Aa，則Ba;

2)若A→A′，則B→B′，且對B′，A′ R B′成立;

3)對所有封閉的評價上下文C[_]，有C[A] R C[B]。

靜態(tài)等價(≈s)表示兩個進程的任何框架不能被任何其他進程所區(qū)分。下面給出框架、框架相等的定義，以便形式化地描述靜態(tài)等價。框架是一個由0和形式如{M/x}的主動替換通過并發(fā)組合或/和限制算子構(gòu)成的擴展進程，用φ或ψ表示;框架的導(dǎo)出變量是框架在主動置換{M/x}中而不在限制算子中的變量x;dom(φ)是框架φ的域，是框架φ導(dǎo)出變量的集合。

定義2 項在框架中的相等。

項M和N在框架φ中相等，記做(M=N)φ，當(dāng)且僅當(dāng)φ≡vn-.σ，有Mσ=Nσ成立，且對名n-和替換σ有{n-}∩(fn(M)∪fn(N))=。

定義3 框架靜態(tài)等價。

稱封閉框架φ和ψ靜態(tài)等價，記做φ≈sψ，若

1)dom(φ)=dom(ψ);

2)對所有的項M和N有(M=N)φ(M=N)ψ。

若擴展進程A，B的框架滿足靜態(tài)等價，則它們滿足靜態(tài)等價，記做A≈sB。

定義4 標(biāo)記互模擬 (labeled bisimulation)。

標(biāo)記互模擬≈l是封閉擴展進程集合上最大的對稱關(guān)系R，A R B蘊涵:

1)A≈sB;

2)若A→A′則有B→B′，且A′ R B′;

3)A a A′，其中:fv(a)dom(A)，bn(a)∩fn(B)=);則有B′滿足B→ a →B′，且A′R B′。

標(biāo)記互模擬滿足下面的性質(zhì):

定理1 觀察等價是(is)標(biāo)記互模擬，即≈=≈l。

≈l在封閉的評價上下文下封閉，同時由于≈l的證明中不包括關(guān)于上下文的條件，標(biāo)記互模擬的證明比觀察等價的證明簡單。進程的觀察等價一般通過標(biāo)記互模擬來證明。

3.2 基于應(yīng)用pi演算的協(xié)議模型

在協(xié)議的形式化描述中，需要定義它的項如表1所示。

表1 協(xié)議的項

M，T，U，V::=項

I，R，x1，x2，…變量

Ni，Nr，sa，TS，c…名

f(U1，U2，…，Ul)函數(shù)f∈Σ

其中:函數(shù)集Σ包括了以下三種類型的函數(shù):

a)密碼相關(guān)的函數(shù)。H1(x1)表示公鑰生成函數(shù);H2(x1，x2)表示私鑰生成函數(shù);H{K}(x)表示含密鑰的單向散列函數(shù);pk(x)表示公鑰;sk(x)表示私鑰;E{K}(x)表示共享密鑰加密;D{K}(x)表示共享密鑰解密;S{sk}(x)表示私鑰簽名;checksign{pk}(x1，x2)表示使用公鑰驗證簽名。

b)消息構(gòu)造函數(shù)。IKEv2的消息載荷有固定的格式，四條消息可以定義為cons1(x1，x2，x3，x4)、cons2(x1，x2，x3，x4，x5，x6)、cons3(x1，x2，x3)、cons4(x1，x2，x3)。

c)投影函數(shù)。該函數(shù)就是選擇構(gòu)造消息函數(shù)中的第j個消息。包括cons1.j(cons1(x1，x2，x3，x4))、cons2.j(cons2(x1，x2，x3，x4，x5，x6))、cons3.j(cons3(x1，x2，x3))、cons4.j(cons4(x1，x2，x3)) 。

由上述函數(shù)，本文定義如下項的代數(shù)相等關(guān)系:

D{k}(E{k}(x))=x

checksign{pk(k)}(S{sk(k)}(x)，x)=true

Tuple.j(Tuple(x1，…，xi))=xj for j

在以上定義的項和函數(shù)相等關(guān)系的基礎(chǔ)上，建立如下協(xié)議模型。I代表發(fā)起方進程，R代表響應(yīng)方進程，I、R共同構(gòu)成系統(tǒng)進程S。

I=!init(sai1，sai2).keyi(ski).v di.v Ni，c-〈cons1(HDR，sai1，KEi，Ni)〉.c(cons2(HDR，sar1，KEr，Nr，er1，hr1)).let KI in if hr1=H{Kar}(r，er1) then let{IDr，AUTHr}=D{Ker}(er1)in let IDr′=H{Kpr}(IDr)in let PKr=H1(IDr) in if checksign{PKr}(AUTHr，(HDR，sar1，KEr，Nr，Ni，IDr′))=true then let IDi′=H{Kpi}(IDi)in let AUTHi=S{ski}(HDR，sai1，KEi，Ni，Nr，IDi′)in let ei=E{Kei}(IDi，IDr，sai2，AUTHi，TSi，TSr)in let hi=H{Kai}(i，ei)in c-〈cons3(HDR，ei，hi)〉.c(cons4(HDR，er2，hr2)). if hr2=H{Kar}(r，er2) then let(=IDi，=IDr，sar2，TSi，TSr)=D{Ker}(er2) in connect(IDi，IDr，sai2，sar2，Kd)

R=keyr(skr).c(cons1(HDR，sai1，KEi，Ni)).v dr.v Nr.v sar1.let KR in let IDr′=H{Kpr}(IDr) in let AUTHr=S{skr}(HDR，sar1，KEr，Nr，Ni，IDi′)in let er1=E{Ker}(IDr，AUTHr)in let hr1=H{Kar}(r，er1)in c-〈cons2(HDR，sar1，KEr，Nr，er1，hr1)〉.c(cons3(HDR，ei，hi). if H{Kai}(i，ei)=hi then let(IDi，=IDr，sai2，AUTHi，TSi，TSr)=D{Kei}(ei)in let IDi′=H{Kpi}(IDi)in let PKi=H1(IDi) in if checksign{PKi}(ei，(HDR，sai1，KEi，Ni，Nr，IDi′))=true then v sar2.accept〈IDi，IDr，sai2，sar2，Kd〉.let er2=E{Ker}(IDi，IDr，sar2，TSi，TSr) in let hr2=H{Kar}(r，er2) in c-〈cons4(HDR，er2，hr2)〉

S=(v IDi)(v IDr)(v s.let pk_i=H1(IDi) in let pk(i)=pk_i in let sk_i=H2(s，pk_i) in let sk(i)=sk_i in keyi〈sk_i〉.let pk_r=H1(IDr) in let pk(r)=pk_r in let sk_r=H2(s，pk_r) in let sk(r)=sk_r in keyr〈sk_r〉)|I|R)

其中，發(fā)起方的密鑰值為

KI=∏u=Kai，Kei，Kpi，Kar，Ker，Kpr，Kd{Ku=H{KEr^di}(Ni，Nr，u)}

響應(yīng)方的密鑰值為

KR=∏u=Kai，Kei，Kpi，Kar，Ker，Kpr，Kd{Ku=H{KEi^dr}(Ni，Nr，u)}

通道init、connect、accept代表協(xié)議與主機交互的隱藏信道，環(huán)境無法與這些信道進行交互。通道keyi、keyr是用來建模私鑰生成中心PKG與客戶端之間傳遞私鑰的安全信道，攻擊者不能得到通道內(nèi)的內(nèi)容。

3.3 安全屬性的形式化驗證

本文采用觀察等價[20]和對應(yīng)性斷言[21]等方法形式化地證明了協(xié)議的私密性、認(rèn)證性和身份保護。部分形式化分析工作是在ProVerif的輔助下完成[22]。

首先考慮私密性。IKEv2協(xié)議用于為IPSec協(xié)商安全關(guān)聯(lián)、建立共享密鑰等參數(shù)，當(dāng)環(huán)境無法區(qū)分IKEv2協(xié)商出的不同參數(shù)時，說明協(xié)議實現(xiàn)了對內(nèi)容的保護，即滿足私密性。因此，有如下定理:

定理2 協(xié)議的私密性。對于攻擊者，如果有

S(IDi，IDr，sai2，sar2，Kd)≈S(IDi，IDr，sai2，sar2，Kd)

則說明協(xié)議滿足私密性。記R為這兩個進程間的最大對稱關(guān)系。

證明 由協(xié)議模型可以定義如下框架:

定義φ(S(IDi，IDr，sai2，sar2，Kd))為

{x1=(HDR，sai1，KEi，Ni)

|x2=(HDR，sar1，KEr，Nr，E{Ker}(IDr，S{skr}(HDR，sar1，KEr，Nr，Ni，IDr′))，hr1)

|x3=(HDR，E{Kei}(IDi，IDr，sai2，S{ski}(HDR，sai1，KEi，Ni，Nr，IDi′)，TSi，TSr)，hi)

|x4=(HDR，E{Ker}(IDi，IDr，sar2，TSi，TSr)，hr2)}

定義ψ(S(IDi，IDr，sai2，sar2，Kd))為

{x1=(HDR，sar1，KEi，Ni)

|x2=(HDR，sar1，KEr，Nr，E{Ker}(IDr，S{skr}(HDR，sar1，KEr，Nr，Ni，IDr′))，hr1)

|x3=(HDR，E{Kei}(IDi，IDr，sai2，S{ski}(HDR，sai1，KEi，Ni，Nr，IDi′)，TSi，TSr)，hi)

|x4=(HDR，E{Ker}(IDi，IDr，sar2，TSi，TSr)，hr2)}

1)很顯然，dom(φ)=dom(ψ)在假設(shè)DH交換安全的前提下，受密鑰保護的安全參數(shù)對攻擊者而言是不可觀察的。根據(jù)定義3可知:φ≈sψ，S(IDi，IDr，sai2，sar2，Kd)≈sS(IDi，IDr，sai2，sar2，Kd)，則R≈s。

2)兩個進程具有相同的模型，則對于進程S(IDi，IDr，sai2，sar2，Kd)的任意內(nèi)部動作τ和外部動作α，進程S(IDi，IDr，sai2，sar2，Kd)能夠做相同的動作，并保持一致的結(jié)果。

以上分析表明，進程S(IDi，IDr，sai2，sar2，Kd)、S(IDi，IDr，sai2，sar2，Kd)滿足定義4，即S(IDi，IDr，sai2，sar2，Kd)≈l S(IDi，IDr，sai2，sar2，Kd)。由定理1可得兩個進程滿足觀察等價，即R≈。表示發(fā)起方和響應(yīng)方之間協(xié)商的信息能夠受到有效的保護，攻擊者無法獲得安全參數(shù)。

采用同樣的方法可以證明S(IDi，IDr，sai2，sar2，Kd)≈S(IDi，IDr，sai2，sar2，Kd)，表示攻擊者不能區(qū)分不同的發(fā)起方與同一響應(yīng)方建立的不同的安全參數(shù)。當(dāng)攻擊者采用中間人攻擊的方法時，由于獲得了響應(yīng)方身份IDr，則S(IDi，IDr，sai2，sar2，Kd)S(IDi，IDr，sai2，sar2，Kd)。但是，中間人攻擊所偽造的消息由于無法通過驗證而導(dǎo)致協(xié)商失敗，雙方不建立任何安全參數(shù)，不會對系統(tǒng)安全造成影響。改進后的協(xié)議具有私密性，能夠?qū)崿F(xiàn)對安全信息的保護。

發(fā)起方I和響應(yīng)方R的身份是以密文的形式在信道中傳遞，因此身份保護是協(xié)議私密性的拓展。對身份保護的驗證可被建模為安全屬性查詢:攻擊者能否獲得加密后消息中的內(nèi)容IDi和IDr。該驗證是在自動化工具ProVerif的輔助下完成，查詢以下事實是否成立。輸出結(jié)果表明，改進后的協(xié)議能夠?qū)崿F(xiàn)對發(fā)起方的身份的主動保護;實現(xiàn)對響應(yīng)方身份的被動保護。

query attacker:IDi

query attacker:IDr

定理3 協(xié)議的認(rèn)證性。對任意跡S η S′，η滿足條件:

a)R對I的認(rèn)證性。如果在η中存在

accept〈IDi，IDr，sai2，sar2，Kd〉

則在此項之前，η中必定存在

init(sai1，sai2) and

checksign{PKi}(ei，(HDR，sai1，KEi，Ni，Nr，IDi′))=true

b)I對R的認(rèn)證性。如果在η中存在

connect〈IDi，IDr，sai2，sar2，Kd〉

則在此項之前，η中必定存在

accept〈IDi，IDr，sai2，sar2，Kd〉 and

checksign{PKr}(AUTHr，(HDR，sar1，KEr，Nr，Ni，IDr′))=true

證明 可以用對應(yīng)性斷言(correspondence assertion)解釋和證明這個定理。R對I的認(rèn)證性:如果響應(yīng)方接收了協(xié)商出的安全參數(shù)，則發(fā)起方必定發(fā)起了該協(xié)商，并且所聲稱的身份是真實的;I對R的認(rèn)證性:如果發(fā)起方基于協(xié)商出的安全參數(shù)建立了安全連接，則響應(yīng)方已接收協(xié)商出的安全參數(shù)，并且所聲稱的身份是真實的。

該定理的證明通過自動化工具ProVerif完成。在完成協(xié)議模型腳本代碼的基礎(chǔ)上，查詢(query)模型是否滿足以下對應(yīng)性斷言。輸出結(jié)果表明協(xié)議滿足認(rèn)證性。

ev:accept〈X1，X2，X3，X4，X5〉(ev:RchecksignI(true)ev:init(X1，X2))

ev:connect〈X1，X2，X3，X4，X5〉(ev:accept〈X1，X2，X3，X4，X5〉ev:IchecksignR(true))

4 結(jié)束語

針對IKEv2協(xié)議的不足，本文將基于身份認(rèn)證的公鑰密碼體制，即Weil對技術(shù)用于數(shù)字簽名認(rèn)證并改進了初始交換協(xié)議。改進后的協(xié)議降低了系統(tǒng)開銷，能夠更好地滿足實時性和低帶寬等條件下的應(yīng)用。同時，基于應(yīng)用pi演算的方法形式化地驗證了新協(xié)議的安全屬性。結(jié)果表明改進后的協(xié)議滿足私密性和認(rèn)證性，并能夠?qū)崿F(xiàn)對發(fā)起方身份的主動保護。因此改進后的協(xié)議具有更好的安全性和實用性。

參考文獻(xiàn):

[1]HARKINS D， CARREL D. RFC 2409， The Internet key exchange (IKE) [S]. United States: RFC Editor， 1998.

[2]HANDLY M， GREENHALGH A. Steps towards a DoS resistant Internet architecture[C]//Proc of ACM SIFCOMM Workshop on future Directions in Network Architecture. Portland: ACM Press， 2004: 49-56.

[3]KAUFMAN C. RFC 4306， Internet key exchange (IKEv2) protocol [S]. Washington: IETF， 2005.

[4]STEVEN M， BELLOVIN， MICHAEL M. Encrypted key exchange: password -based protocols secure against dictionary attacks[C]//Proc of IEEE Symposium on Research in Security and Privacy. Oakland: IEEE Computer Society， 1992:72-84.

[5]RAED B H. Enhancing the IKE pre-shared key authentication method [D].Missouri: Graduate School， University of Missouri-Columbia， 2006.

[6]張朝東，徐明偉.密鑰交換協(xié)議IKEv2的分析與改進[J].清華大學(xué)學(xué)報:自然科學(xué)版，2006，46(7):1274-1277.

[7]劉文紅.下一代互聯(lián)網(wǎng)服務(wù)保證關(guān)鍵技術(shù)研究[D].北京:北京交通大學(xué)，2007.

[8]曹春杰，張帆，馬建峰.可證安全的Internet密鑰交換協(xié)議[J].武漢大學(xué)學(xué)報:理學(xué)版，2006，52(5):545-549.

[9]沈海峰，薛銳，黃河燕.IKEv2協(xié)議的安全性分析[J].計算機科學(xué)，2005，32(11): 59-63.

[10]吳昌，肖美華.基于SPIN的IKEv2協(xié)議高效模型檢測[J].計算機工程與應(yīng)用，2008，44(5):158-161.

[11]SHAMIR A. Identity-based cryptosystems and signature schemes[C]//Advances in Cryptology- Crytpo’84， LNCS 196.1985. Berlin: Springer-Verlag， 1985: 47-53.

[12]BONEH D， FRANKLIN M. Identity based encryption from the Weil pairings[C]//Advances in Cryptology- Crypto 2001， LNCS 2139. Berlin: Springer-Verlag， 2001:213-229.

[13]ABADI M， FOURNET C. Mobile values， new names and secure communication[C]//Proc of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’01). London: ACM， 2001:104-115.

[14]MICHAEL B， CATALIN H， MATTEO M. Automated verification of remote electronic voting protocols in the applied Pi-calculus[C]//Proc of the 21st IEEE Computer Security Foundations Symposium (CSF). Pittsburgh: IEEE Press， 2008:195-209.

[15]ABADI M， BLANCHET B. Just fast keying in the pi calculus[J]. ACM Trans on Information and System Security (TISSEC)，2007，10(3):1-59.

[16]ABADI M， BLANCHET B. Analyzing security protocols with secrecy types and logic programs[J]. Journal of the ACM (JACM)，2005，52(1):102-146.

[17]拾以娟.基于身份的公鑰密碼學(xué)關(guān)鍵問題研究[D].上海:上海交通大學(xué)，2007.

[18]廖軍，潭浩，劉錦德.基于Pi-演算的Web服務(wù)組合的描述和驗證[J].計算機學(xué)報，2005，28(4):635-643.

[19]袁祿來，曾國蓀，王偉.基于Pi-演算的信任網(wǎng)絡(luò)形式化建模[J].系統(tǒng)仿真學(xué)報，2008，20(1):57-61.

[20]BLANCHET B，ABADI M， FOURNET C. Automatic verification of selected equivalences for security protocols[J]. Journal of Logic and Algebraic Programming，2008，75(1):3-51.

[21]BLANCHET B， FOURNET C. Automatic verification of correspondences for security protocols[C]//Proc of the 20th Annual IEEE Symposium on Logic in Computer Science. Washington: IEEE Computer Society， 2005:331-340.

[22]顧永跟，傅育熙，朱涵.基于可達(dá)關(guān)系的安全協(xié)議保密性分析[J].計算機學(xué)報，2007，30(2):255-261.