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

顧香++潘進++王小明

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

關鍵詞： 應用PI演算； 前向安全性； ProVerif； 自動化分析； STS協議； MTI協議

中圖分類號： TN958?34； TP309 文獻標識碼： A 文章編號： 1004?373X（2015）22?0021?04

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

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

1 擴展的應用PI演算

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

表1 擴展的應用PI演算語法

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

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

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

2.1 自動化分析工具ProVerif

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

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

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

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

定義1 秘密性

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

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

根據前向安全性的定義，基于擴展的應用pi演算階段進程語法及ProVerif工具，定義協議的前向安全性如下。

定義2 前向安全性

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

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

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

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

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

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

3.1 STS密鑰協商協議

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

[MSG1 A→B： ga，Cert A]

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

[MSG3 B→A：Signa（IDagagb）]

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

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

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

3.2 MTI密鑰協商協議

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

[MSG1 A→B：ga，Cert A]

[MSG2 B→A：gb，Cert B]

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

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

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

4 結 語

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

參考文獻

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

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

[3] 項順伯，彭志平，柯文德.一種可證安全的兩方口令認證密鑰交換協議[J].計算機工程，2013，39（1）：164?167.

[4] 李強，馮登國，張立武，等.標準模型下增強的基于屬性的認證密鑰協商協議[J].計算機學報，2013，36（10）：2156?2167.

[5] 陳家琪，馮俊，郝妍.基于無證書密碼學的可認證三方密鑰協商協議[J].計算機應用研究，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握手協議的安全性分析及其改進[J].高技術通訊，2005，15（4）：6?10.

[8] 郭云川，丁麗，周淵，等.基于ProVerif的電子商務協議分析[J].通信學報，2009，30（3）：125?129.

[9] 孟博，黃偉，王德軍，等.協議抗拒絕服務攻擊性自動化證明[J].通信學報，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] 斯延森.密碼學原理與實踐[M].馮登國，譯.3版.北京：電子工業出版社，2009.