密鑰交換協(xié)議前向安全性的自動化分析

顧香++潘進(jìn)++王小明

摘 要： 會話密鑰的安全影響了整個(gè)通信網(wǎng)絡(luò)的安全，前向安全性是密鑰交換協(xié)議中保證會話密鑰安全的一種特殊的安全屬性。首先擴(kuò)展了應(yīng)用PI演算，增加了階段進(jìn)程語法描述協(xié)議的前向安全性；然后提出了一個(gè)基于一階定理證明器ProVerif的前向安全性自動化分析方法；最后運(yùn)用這種方法分析了兩種典型的密鑰交換協(xié)議，STS協(xié)議和MTI協(xié)議的前向安全性，分析結(jié)果表明該方法簡單可靠。

關(guān)鍵詞： 應(yīng)用PI演算； 前向安全性； ProVerif； 自動化分析； STS協(xié)議； MTI協(xié)議

中圖分類號： TN958?34； TP309 文獻(xiàn)標(biāo)識碼： A 文章編號： 1004?373X（2015）22?0021?04

隨著信息時(shí)代的來臨，網(wǎng)絡(luò)已成為人類文明飛速發(fā)展的主要載體[1]。與此同時(shí)，網(wǎng)絡(luò)安全問題也日益突出，這是信息時(shí)代無法回避的關(guān)鍵問題。而安全協(xié)議能夠?yàn)榫W(wǎng)絡(luò)提供有效的安全保障，它可以保證秘密性、認(rèn)證性、完整性、匿名性、公平性等多種安全屬性。根據(jù)協(xié)議安全目的的不同，通常將安全協(xié)議分為認(rèn)證協(xié)議、密鑰交換協(xié)議、認(rèn)證及密鑰交換協(xié)議和電子商務(wù)協(xié)議。其中密鑰交換協(xié)議主要用于建立會話密鑰，在信息系統(tǒng)安全中是極為重要的。

在實(shí)際應(yīng)用中，為了實(shí)現(xiàn)某個(gè)具體目標(biāo)，密鑰交換協(xié)議往往要求達(dá)到某些特殊的安全屬性：已知會話密鑰安全性，前向安全性，不能使用泄露的身份信息冒充其他合法用戶，未知會話密鑰共享，密鑰控制，密鑰的新鮮性[2]。其中前向安全性是一種比較重要的安全屬性，它能夠保證在協(xié)議參與方長期私鑰泄露的情況下不會泄露之前建立的會話密鑰。但是目前，對于前向安全性的分析都僅僅局限于人腦邏輯證明的非形式化分析方法[3?7]，即通過假設(shè)攻擊者在獲取協(xié)議參與方的長期私鑰時(shí)，證明其是否能夠獲取已建的會話密鑰。文獻(xiàn)[6]非形式化地分析了WTLS握手協(xié)議的前向安全性，并提出兩種改進(jìn)的具有前向安全性的協(xié)議方案。而文獻(xiàn)[7]對這兩種方案的前向安全性進(jìn)行分析，提出其中一種方案并不滿足前向安全性。由此可見，非形式化分析方法極易出錯?；趹?yīng)用PI演算對協(xié)議進(jìn)行建模，并用ProVerif、SPVT等工具自動化分析協(xié)議，是一種簡單可靠的協(xié)議分析方法。目前，這種方法能夠自動化分析協(xié)議的秘密性、認(rèn)證性、強(qiáng)秘密性、公平性[8]和抗拒絕服務(wù)攻擊性[9]。由于標(biāo)準(zhǔn)的應(yīng)用PI演算語法不能描述協(xié)議的前向安全性，本文首先對應(yīng)用PI演算進(jìn)行擴(kuò)展，主要是擴(kuò)展了一個(gè)階段進(jìn)程語法，然后提出一個(gè)基于定理證明器ProVerif的前向安全性自動化分析方法，最后應(yīng)用這種方法來分析驗(yàn)證兩種典型密鑰交換協(xié)議的前向安全性。

1 擴(kuò)展的應(yīng)用PI演算

應(yīng)用PI演算[10]是一種進(jìn)程演算，是對PI演算的擴(kuò)展，是SPI演算的一般化形式。應(yīng)用PI演算在PI演算的語法上增加了函數(shù)和等式，使其能夠描述各種密碼操作及精確描述協(xié)議的交互過程。但是現(xiàn)有語法并不足以分析協(xié)議的前向安全性，針對這一缺陷，在應(yīng)用PI演算的現(xiàn)有語法上進(jìn)行擴(kuò)展，擴(kuò)展后的語法如表1所示。

表1 擴(kuò)展的應(yīng)用PI演算語法

表1中，元組項(xiàng)[M1，M2，…，Mn]、進(jìn)程宏[R（M1，M2，…，Mn）]和階段進(jìn)程[phase t.P]是在應(yīng)用PI演算基礎(chǔ)上擴(kuò)展的新語法。 元組[M1，M2，…，Mn]本質(zhì)上也是一個(gè)項(xiàng)，它是具有兩個(gè)以上參數(shù)的項(xiàng)，能夠表示復(fù)雜的消息及操作。進(jìn)程宏[R（M1，M2，…，Mn）]用來表示參與協(xié)議各個(gè)主體的進(jìn)程，其中[M1，M2，…，Mn]表示協(xié)議主體擁有的原始項(xiàng)。進(jìn)程宏的擴(kuò)展可以使協(xié)議的主進(jìn)程用幾個(gè)分進(jìn)程來描述。階段進(jìn)程[phase t.P]表示在t階段執(zhí)行進(jìn)程P，t代表一個(gè)全局時(shí)鐘，并且進(jìn)程[phase t.P]只在t階段是活躍的。帶有階段的進(jìn)程被執(zhí)行如下：首先，執(zhí)行0階段下的所有指令，即不在[i≥1]階段的所有指令；然后，在0階段到1階段的過渡階段，所有沒有達(dá)到[i≥1]階段的所有進(jìn)程被丟棄；然后進(jìn)程執(zhí)行1階段的指令，但不是[i≥2]階段的指令。更一般地，當(dāng)從n階段到n+1階段轉(zhuǎn)換時(shí)，所有沒有達(dá)到n+1階段的進(jìn)程都被丟棄，同時(shí)執(zhí)行n+1階段而不是[i≥n+2]階段的指令。

從上述描述可知，在階段轉(zhuǎn)換之前執(zhí)行一個(gè)特定階段的所有指令是沒有必要的。此外，只有在相同階段的進(jìn)程才能進(jìn)行通信。本文增加階段進(jìn)程用來描述協(xié)議的前向安全性。

2 前向安全性的自動化分析方法

2.1 自動化分析工具ProVerif

Blanchet等人在2002年開發(fā)了自動化分析工具ProVerif[11]，它由3部分組成：協(xié)議輸入部分、系統(tǒng)處理部分和結(jié)果輸出部分，具體結(jié)構(gòu)如圖1所示。其中系統(tǒng)輸入部分可以是Horn邏輯或應(yīng)用pi演算描述的協(xié)議，既要描述協(xié)議的交互過程也要描述所要驗(yàn)證的安全屬性；系統(tǒng)處理部分是基于一階邏輯規(guī)則對安全屬性進(jìn)行推導(dǎo)，該工具能夠解決狀態(tài)空間爆炸問題；結(jié)果輸出部分在協(xié)議不滿足某安全屬性時(shí)能夠給出相應(yīng)的攻擊序列，這是一個(gè)很實(shí)用、可靠的自動化分析工具。目前，該工具已經(jīng)成功分析了很多復(fù)雜協(xié)議，如網(wǎng)絡(luò)投票協(xié)議、JFK協(xié)議、電子商務(wù)協(xié)議等。

2.2 前向安全性的自動化分析

根據(jù)前向安全性的定義[4]，如果協(xié)議參與方中一方的長期私鑰泄露，并不會泄露他們以前建立的會話密鑰，則稱協(xié)議具有前向安全性。如果協(xié)議所有參與方的長期私鑰都泄露，也不會影響之前建立的會話密鑰，則稱協(xié)議具有完美前向安全性。由上述定義可知，協(xié)議具有前向安全性必須滿足兩個(gè)條件：第一階段，運(yùn)行協(xié)議，協(xié)議能夠保證會話密鑰不被攻擊者獲取，即保證會話密鑰的秘密性；第二階段，協(xié)議運(yùn)行結(jié)束后，攻擊者獲取協(xié)議參與方的長期私鑰，但是根據(jù)協(xié)議運(yùn)行時(shí)攻擊者獲取的知識無法計(jì)算出之前建立的會話密鑰。根據(jù)擴(kuò)展的階段進(jìn)程語法[phase t.P]，可以進(jìn)行這兩個(gè)階段的描述。

基于一階定理證明器ProVerif，協(xié)議的秘密性自動化分析方法[12]如定義1。

定義1 秘密性

如果M為協(xié)議的一個(gè)基本項(xiàng)，輸入查詢語句：query attacker（M），其輸出結(jié)果為not attacker（M） is true，則稱協(xié)議保證項(xiàng)M的秘密性。

其中attacker（M）表示攻擊者能夠獲取項(xiàng)M，證明可達(dá)性是ProVerif的最基本功能。工具允許研究查詢攻擊者能夠獲得哪些項(xiàng)，如果攻擊者不能獲取項(xiàng)M，即not attacker（M），那么協(xié)議就保證了項(xiàng)M的秘密性。

根據(jù)前向安全性的定義，基于擴(kuò)展的應(yīng)用pi演算階段進(jìn)程語法及ProVerif工具，定義協(xié)議的前向安全性如下。

定義2 前向安全性

[R1（M1，M2，…，Mn）]、[R2（M1，M2，…，Mk）]為協(xié)議參與方的進(jìn)程宏，k為協(xié)議所建立的會話密鑰。如果運(yùn)行協(xié)議進(jìn)程[！R1（M1，M2，…，Mn）！R2（M1，M2，…，Mn）！phase1；outc，sk]，并輸入查詢語句：query attacker（k）phase 0和query attacker（k）phase 1，其兩個(gè)輸出結(jié)果都為not attacker（k） is true，則稱協(xié)議滿足前向安全性。

其中[phase1；outc，sk]表示1階段在公共信道c上輸出私鑰sk（協(xié)議參與方任意一方的長期私鑰）。ProVerif所有進(jìn)程都默認(rèn)在phase 0下執(zhí)行。由階段進(jìn)程的語法可知，ProVerif會首先執(zhí)行0階段下的所有指令，即[！R1（M1，M2，…，Mn）！R2（M1，M2，…，Mn）！]，這時(shí)就能建立一個(gè)會話密鑰k。然后，在0階段到1階段的過渡階段，所有沒有達(dá)到1階段的進(jìn)程被丟棄，并且進(jìn)程執(zhí)行1階段的指令[outc，sk]，這樣攻擊者就可以獲取協(xié)議參與方的私鑰。查詢會話密鑰k在0階段和1階段是否被泄露，即query attacker（k），就能驗(yàn)證協(xié)議的前向安全性。與秘密性一樣，如果攻擊者不能獲取會話密鑰k，即not attacker（k） is true，則稱協(xié)議具有前向安全性。

引理：[R1（M1，M2，…，Mn）]，[R2（M1，M2，…，Mk）]為協(xié)議參與方的進(jìn)程宏，k為協(xié)議所建立的會話密鑰，s為用會話密鑰k加密傳輸?shù)谋Ｃ苄畔?。如果運(yùn)行進(jìn)程[！R1（M1，M2，…，Mn）！R2（M1，M2，…，Mn）！phase1；outc，sk]，并輸入查詢語句：query attacker（s）phase 0和query attacker（s）phase 1，其輸出結(jié)果都為not attacker（s）is true，則稱協(xié)議滿足前向安全性。

如果s是一條保密的信息，用會話密鑰k加密后傳輸，若攻擊者不能獲取信息s，那么攻擊者必然不知道會話密鑰k，即若輸出結(jié)果為not attacker（s）is true，則協(xié)議滿足前向安全性。

3 兩種典型密鑰協(xié)商協(xié)議前向安全性分析

Diffie?Hellman協(xié)議是最基本的密鑰協(xié)商協(xié)議，它容易遭受中間人攻擊，泄露會話密鑰。STS（端?端）和MTI密鑰協(xié)商協(xié)議是DH協(xié)議的改進(jìn)，能夠抵抗中間人攻擊，建立安全的會話密鑰。

3.1 STS密鑰協(xié)商協(xié)議

STS密鑰協(xié)商協(xié)議[13]由3條消息組成。其中，公開群[G，?]和一個(gè)階為[n]的元素[g∈G]，[ski]和[pki]為用戶[I]的簽名密鑰及其對應(yīng)的公鑰。

[MSG1 A→B： ga，Cert A]

[MSG2 B→A： gb，Cert B，Signb（IDbgbga）]

[MSG3 B→A：Signa（IDagagb）]

協(xié)議消息交互如下：用戶A選取一個(gè)隨機(jī)數(shù)[a]，[0≤a≤n-1]，計(jì)算[ga]，將[ga]和[Cert A]發(fā)送給用戶B；用戶B隨機(jī)選取[b]，[0≤b≤n-1]，計(jì)算[gb]和會話密鑰[k=gab]，并用自己的私鑰[skb]進(jìn)行簽名[Signb（IDbgbga）]，再將[gb]，[Cert B]和[Signb（IDbgbga）]發(fā)送給用戶A；A驗(yàn)證證書及簽名，驗(yàn)證成功后計(jì)算會話密鑰[k=gba]，再用私鑰[ska]進(jìn)行簽名[Signb（IDbgagb）]，并發(fā)送給B；B驗(yàn)證簽名，成功后則完成會話密鑰的協(xié)商。

基于提出的前向安全性自動化分析方法，用擴(kuò)展的應(yīng)用pi演算對STS協(xié)議進(jìn)行建模，然后用ProVerif工具進(jìn)行前向安全性分析。由于篇幅限制，只給出了ProVerif的分析結(jié)果，如圖2所示。

根據(jù)圖2可知，在0階段的查詢結(jié)果為true，表明STS協(xié)議能夠保證會話密鑰的秘密性；在1階段的查詢結(jié)果也為true，表明在用戶A和B的長期私鑰都泄露的情況下，協(xié)議能夠保證之前建立的會話密鑰不被泄露出去，STS協(xié)議具有完美前向安全性。

3.2 MTI密鑰協(xié)商協(xié)議

MTI密鑰協(xié)商協(xié)議[13]由兩條消息組成。其中，公開群[G，?]和一個(gè)階為[n]的元素[g∈G]。每個(gè)用戶[I]擁有一個(gè)私鑰[ski]，其中[0≤xi≤n-1]，對應(yīng)的公鑰為[pki=gski]，被包含在用戶的證書[Cert I]中，且被TA簽名。

[MSG1 A→B：ga，Cert A]

[MSG2 B→A：gb，Cert B]

協(xié)議消息交互如下：用戶A隨機(jī)選取[a]，[0≤a≤n-1]，計(jì)算[ga]，將[ga]和[Cert A]發(fā)送給用戶B；用戶B隨機(jī)選取[b]，[0≤b≤n-1]，計(jì)算[gb]，將[gb]和[Cert B]發(fā)送給用戶A。B通過[Cert A]認(rèn)證A，并獲取A的公鑰[pka]，計(jì)算會話密鑰[k=gabpkaskb]；A通過[Cert B]認(rèn)證B，并獲取B的公鑰[Pb]，計(jì)算會話密鑰[k=gbapkbska]。由于[gabPaxb=gabgskaskb=gbapkbska]，用戶A，B計(jì)算的會話密鑰相等。

同樣，基于提出的方法對MTI協(xié)議進(jìn)行建模及前向安全性分析，分析結(jié)果如圖3和圖4所示。

圖3為只有用戶A的長期私鑰被泄露時(shí)的分析結(jié)果（只泄露用戶B私鑰時(shí)的分析結(jié)果相同）。由圖3可知，兩個(gè)階段的查詢結(jié)果都為true，表明MTI協(xié)議滿足前向安全性。圖4為用戶A和B的私鑰都泄露時(shí)的分析結(jié)果，由圖4可知，1階段的分析結(jié)果為false，表明攻擊者在獲取A和B私鑰時(shí)，能計(jì)算他們之前建立的會話密鑰，則MTI 協(xié)議并不滿足完美前向安全性。

4 結(jié) 語

密鑰交換協(xié)議主要是用來建立會話密鑰的，它的前向安全性能夠保證在協(xié)議參與方長期私鑰泄露的情況下不會泄露會話密鑰。形式化分析方法是一種有效的協(xié)議分析方法。本文擴(kuò)展了應(yīng)用PI演算的階段進(jìn)程語法，并在此基礎(chǔ)上提出了一種基于定理證明器ProVerif的前向安全性自動化分析方法。與人腦邏輯證明分析方法相比，這種能夠?qū)崿F(xiàn)自動化分析，更簡單。這是一種形式化分析方法，不需要依靠人的邏輯思維，更加可靠。但是由于本文考慮的是分析密鑰交換協(xié)議中的前向安全性，這種方法還不足以分析組密鑰協(xié)商協(xié)議的前向安全性，下一步的研究還要繼續(xù)。未來研究工作中，將對應(yīng)用PI演算語法及一階定理證明器ProVerif做進(jìn)一步擴(kuò)展及改進(jìn)，使其能夠分析大型復(fù)雜協(xié)議的多種安全屬性。

參考文獻(xiàn)

[1] 薛銳，雷新鋒.安全協(xié)議：信息安全保障的靈魂：安全協(xié)議分析研究現(xiàn)狀與發(fā)展[J].信息安全，2011，26（3）：287?296.

[2] 馮登國.安全協(xié)議：理論與實(shí)踐[M].北京：清華大學(xué)出版社，2011.

[3] 項(xiàng)順伯，彭志平，柯文德.一種可證安全的兩方口令認(rèn)證密鑰交換協(xié)議[J].計(jì)算機(jī)工程，2013，39（1）：164?167.

[4] 李強(qiáng)，馮登國，張立武，等.標(biāo)準(zhǔn)模型下增強(qiáng)的基于屬性的認(rèn)證密鑰協(xié)商協(xié)議[J].計(jì)算機(jī)學(xué)報(bào)，2013，36（10）：2156?2167.

[5] 陳家琪，馮俊，郝妍.基于無證書密碼學(xué)的可認(rèn)證三方密鑰協(xié)商協(xié)議[J].計(jì)算機(jī)應(yīng)用研究，2010，27（5）：1902?1904.

[6] KWAK D J， HA J， LEE H J C， et al. A WTLS handshake protocol with user anonymity and forward secrecy [J]. Lecture Notes in Computer Science， 2003， 2524： 219?230.

[7] 崔媛媛，周永彬，丁金扣，等.一種具有用戶匿名性和前向安全性的WTLS握手協(xié)議的安全性分析及其改進(jìn)[J].高技術(shù)通訊，2005，15（4）：6?10.

[8] 郭云川，丁麗，周淵，等.基于ProVerif的電子商務(wù)協(xié)議分析[J].通信學(xué)報(bào)，2009，30（3）：125?129.

[9] 孟博，黃偉，王德軍，等.協(xié)議抗拒絕服務(wù)攻擊性自動化證明[J].通信學(xué)報(bào)，2012，33（3）：112?121.

[10] RYAN M D， SMYTH B. Applied Pi calaulus [M]. [S.l.]： IOS Press， 2011.

[11] BLANCHET B. An efficient cryptographic protocol verifier based on prolog rules [C]// Proceedings of 14th IEEE Computer Security Foundations Workshop. Nova Scotia， Canada： IEEE， 2002： 82?96.

[12] BLANCHET B， SMYTH B， CHEVAL V. ProVerif 1.88： automatic cryptographic protocol verifier， user manual and tutorial [M]. [S.l.]： [s.n.]， 2013.

[13] 斯延森.密碼學(xué)原理與實(shí)踐[M].馮登國，譯.3版.北京：電子工業(yè)出版社，2009.