兩個認證密鑰協商協議的前向安全性分析

程慶豐 馬玉千

(戰略支援部隊信息工程大學 鄭州 450001)

(數學工程與先進計算國家重點實驗室 鄭州 450001)

1 引言

1989年，Günther[1]首次提出了前向安全性的概念，同時提出了一個基于身份的AKA協議，并在文中證明了該協議滿足前向安全性。隨后，前向安全性受到越來越多的學者關注，具有前向安全特性的AKA協議也相繼被提出，例如Matsumoto等人[2]提出了能夠滿足弱前向安全性質的密鑰協商協議，Jeong等人[3]提出了能夠滿足強前向安全性質的一輪密鑰協商協議。2005年，Krawczyk[4]指出，一輪AKA協議最多只能達到弱前向安全性。事實上，2010年，Boyd等人[5]指出該結論是不正確的，并給出了用于改進協議的通用模板，該模板能夠在敵手不能夠進行臨時密鑰泄露問詢的情況下，使得一輪AKA協議達成強前向安全性。在現實生活應用中，前向安全性也正在逐步成為各方的研究熱點。2014年，曹晨磊等人[6]為保證分屬于不同層級的云實體能夠進行安全的通信，提出了一個基于層級化身份的AKA協議，并在eCK模型下證明該協議能夠滿足前向安全性、已知密鑰安全性等多種安全屬性。2015年，楊孝鵬等人[7]利用格上判定帶誤差學習問題困難假設構造了一個AKA協議，同時證明了該協議在CK模型下是可證明安全的，能夠達成弱前向安全性。2017年，熊婧和王建明[8]針對RFID技術在信息傳遞過程中的弱點提出了一個基于哈希函數的雙向認證協議，并聲明該協議具有一定程度上的防竊聽、前向安全性、防位置追蹤等屬性。2020年，Li等人[9]面向無線醫療傳感器網絡系統提出了一個三方用戶認證協議，并聲稱該協議能夠滿足前向安全性。然而一年后，Saleem等人[10]分析得出Li等人的協議不能夠抵抗傳感器節點的偽裝攻擊，并且不能夠提供匿名性。連接至物聯網中的設備計算能力、存儲能力參差不齊，而它們需要滿足的安全性質并沒有減弱，許多學者面向物聯網的不同應用環境提出了滿足前向安全性的多個協議[11–16]。再以目前網絡中廣泛應用的傳輸層協議TLS為例，現在最新版本的TLS 1.3版本[17]僅允許使用滿足前向安全的密鑰交換方案。2021年，Boyd等人[18]將協議下的前向安全性擴展到其他密碼原語中，并總結給出了為在不同密碼原語中達到前向安全性的方法。更進一步的，Boyd等人通過將前向安全性進行分類、提出了能力更強的敵手，并聲稱該能力在之前的安全模型中并未包含。

另外，在前向安全性提出之后，研究者還將該性質添加至了安全模型中，從而使得AKA協議的前向安全性分析更加有說服力。2007年，結合前向安全性這個概念，LaMacchia等人[19]在原有CK模型[20]中添加了包含前向安全性在內的其他性質，提出了eCK模型，進一步完善了AKA協議的安全模型。目前，前向安全性經過30多年的蓬勃發展，可以根據敵手能力的不同分為以下幾類：

(1) 前向安全性(Forward Security)。稱一個協議具有前向安全性是指，當協議參與方中一方或多方的長期密鑰泄露，協議之前達成的會話密鑰仍是安全的。

(2) 部分前向安全性(Partial Forward Security)。稱一個協議具有部分前向安全性是指，當協議參與方中指定一方或多方的長期私鑰泄露，協議之前達成的會話密鑰仍是安全的。

(3) 弱前向安全性(Weak Forward Security)。稱一個協議具有弱前向安全性是指，在敵手為被動敵手的情況下，當協議參與方中一方或多方的長期私鑰泄露，協議之前達成的會話密鑰仍是安全的。

(4) 強前向安全性(Strong Forward Security)稱一個協議具有強前向安全性是指，在敵手為主動敵手的情況下，當協議參與方中一方或多方的長期私鑰泄露，協議之前達成的會話密鑰仍是安全的。

在上述研究的基礎上，本文首先分析了MZK20和VSR20兩個AKA協議，首先利用BAN邏輯分析了MZK20協議不具有弱前向安全性；其次利用啟發式分析和Scyther形式化證明工具證明了VSR20協議不具備前向安全性。進一步，本文在分析VSR20協議設計缺陷的基礎上提出了改進方案，并在eCK模型下證明了改進后協議的安全性；并且，結合Scyther軟件證明了改進VSR20協議與VSR20協議相比明顯提高了安全性。

2 基礎知識

2.1 數學困難問題

本節介紹分析和改進協議時用到的數學困難問題[21]。

定義1 橢圓曲線上的離散對數問題(Discrete Logarithm Problem over Elliptic Curve, ECDLP)。設E是定義在有限域Zq上的橢圓曲線，P,Q是E上的任意兩點，則求解滿足等式kP=Q成立的唯一整數k是困難的。

定義2 橢圓曲線上的計算性Diffie-Hellman問題(Computational Diffie-Hellman Problem over Elliptic Curve, ECCDH)。設E是定義在有限域Zq上的橢圓曲線，G是與E對應的有限循環群，給定P,aP,bP ∈G，則求解abP ∈G是困難的。

2.2 形式化分析工具

本文主要用到了BAN邏輯和Scyther軟件兩種形式化工具方法，下面分別簡要介紹這兩種工具。

(1) BAN邏輯。BAN邏輯是Burrows等人于1990年提出的[22]，BAN邏輯因其簡潔直觀的證明過程、方便易學的規則而引起了研究者的普遍關注。BAN邏輯的提出為解決安全協議分析問題做出了很大的貢獻，它成功地對Needham-Schroeder,Kerberos等幾個著名的協議進行了分析，找到了其中已知和未知的漏洞。

(2) Scyther形式化分析工具。Scyther軟件[23]是由牛津和蘇黎世聯邦理工學院的研究學者聯合研發的一個形式化分析工具，該軟件首次發行于2008年左右。目前，Scyther軟件已經被廣泛地應用于協議分析領域，例如，該軟件已經用于分析被大家所熟知的HMQV協議、KEA+協議、NAXOS協議等。

2.3 安全模型

本節介紹分析改進協議時所基于的eCK安全模型。eCK模型是LaMacchia等人[19]在2007年提出的，該模型賦予了敵手更加貼近現實環境的攻擊能力。

(1) 長期私鑰暴露問詢S taticKeyReveal(Pi)：通過該問詢，A可以獲得用戶Pi的長期密鑰；

(2) 臨時私鑰暴露問詢EphemeralKeyReveal(Pi)： 通過該問詢，A可 以獲得用戶Pi的臨時密鑰；

(3) 會話密鑰暴露問詢 SessionKeyReveal(Pi)：通過該問詢，A可以獲得會話s id的會話密鑰；

(4) 發送消息問詢 S end(sid,m)：通過該問詢，A可以向會話s id發 送消息m并根據協議規范獲得相應的回復消息；

(5) 測試問詢T est(sid)：A選 定新鮮會話s id進行該問詢，模擬算法S隨機投擲硬幣，根據結果b ∈{0,1}來 回答該問詢。如果b=1，預言機返回該會話的正確會話密鑰；如果b=0，則返回一個與正確密鑰同分布的隨機值。

在eCK模型中，模擬算法S通過測試游戲來模擬敵手A的攻擊。在測試游戲中某一個時刻，敵手A選定一個已經結束的會話s id作為測試會話，進行問詢，具體步驟如下：

(1)A任意進行S taticKeyReveal(Pi)問詢、EphemeralKeyReveal(Pi)問 詢、SessionKeyReveal(Pi)問詢和S end(sid,m)問詢；

(2) 在某個時刻，A選定一個標識為s id的新鮮會話進行1次T est(sid)問詢；

(3)A根據需要繼續進行S taticKeyReveal(Pi)問詢、E phemeralKeyReveal(Pi)問 詢、SessionKeyReveal(Pi)問 詢和 Send(sid,m)問詢；

(4)A輸出猜測結果。

(1) 匹配會話能夠得到相同的會話密鑰；

(2) 不存在敵手能夠以不可忽略的優勢贏得測試游戲。

3 兩個協議的前向安全性分析

3.1 MZK20協議安全性分析

2020年，Akram等人[24]提出了一個用于多方服務器情況的AKA協議(以下簡稱MZK20協議)，并聲稱該協議具有匿名性，能夠抵抗重放攻擊、偽裝攻擊、口令猜測攻擊等。本小節將指出該協議不具備弱前向安全性和匿名性。

3.1.1 MZK20協議描述

MZK20協議共由服務器注冊階段、用戶注冊階段、登錄和認證階段、口令更換階段、重新注冊階段5個部分組成，其中完成1次通信只需服務器注冊、用戶注冊、登錄和認證3個階段，下面主要介紹完成通信的這3個階段。

(1) 服務器注冊階段

服務器通過如下的步驟在 RC處注冊成為合法服務器Sj：

步驟1 服務器通過安全信道向 RC發送自己的身份標識I Dj；

步驟2 在收到I Dj之 后，R C計 算s=h(IDj||x)，pkSj=sP，pkRC=xP，其中x是 R C的私鑰；

步驟3 最后， RC 將s,pkSj,pkRC發送給服務器，服務器Sj完成注冊。

(2) 用戶注冊階段

用戶通過如下的步驟在 RC處注冊成為網絡中的合法用戶Uu：

步驟1 用戶選擇自己的身份標識 I Du、口令PWu和 生物特征Bu， 并產生一個隨機數a。之后，用戶計算M=H(IDu||Bu)， T W=h(a ⊕H(Bu||PWu))。最后，用戶將I Du,M,TW發 送給 RC；

步驟2 RC 在收到用戶消息后，計算Xu=h(IDu||pkRC)，Yu=Xu ⊕h(M||TW)，Fu=h(h(IDu||TW)) 。 之后，R C將h(),Yu,Fu存儲在智能卡S Cu中發送給用戶；

步驟3 用戶在智能卡信息中增添隨機數a，最后，用戶Uu的 智能卡信息為{h(),Yu,Fu,a}。

(3) 登錄和認證階段

步驟1 Uu輸 入I Du, P Wu和Bu。 智能卡計算TW=h(a ⊕H(Bu||PWu))并 檢驗Fu=h(h(IDu||TW))的正確性。如果正確，則智能卡計算M=H(IDu||Bu)，Uu選 擇一個隨機數Cu并 計算Op=CupkSj=CusP，之 后 依 次 計 算 PIDu=CuP ⊕IDu,Xu′=Yu ⊕h(M||TW) 和DIDu=h(IDu||Xu′||CuP)。 最 后，Uu發送消息M1= 給Sj；

步驟2 在收到M1后 ，Sj用 私鑰s計算s?1Op=CuP，IDu=CuP ⊕PIDu，Xu=h(IDu||pkRC)。利用這3個結果驗證等式D IDu=h(IDu||Xu||CuP)是否成立。如果成立，Sj首 先選擇隨機數Dj，然后依次計 算Tu=h(IDu||Xu),Vj=Dj ⊕Xu和Quj=h(IDu||Tu||CuP||Dj||Xu||IDj)。 最后，Sj將M2=發送給Uu；

步驟3 在收到M2后，Uu計算Dj=Vj ⊕Xu，并驗證等式h(IDu||h(IDu||Xu′)||CuP||Dj||Xu′||IDj)=Quj的正確性；

步驟4 如果等式正確則 Uu進一步計算會話密鑰SKuj=h(IDu||CuP||Dj||Xu′||IDj) 以 及Zuj=h(SKuj||IDu||Dj||Xu′||IDj) 。最 后，Uu將M3=Zuj發送給Sj；

步驟5 在收到M3后，Sj首先按照SKuj=h(IDu||CuP||Dj||Xu||IDj)計算會話密鑰，其次驗證等式h(SKuj||IDu||CuP||Xu||IDj)=Zuj的正確性。

3.1.2 MZK20協議分析

(1) 啟發式分析方法。當服務器的長期私鑰s泄露時，指出該協議不具備弱前向安全性和匿名性。具體攻擊步驟如下(假設敵手為A)：

步驟1 敵手A通過長期私鑰泄露問詢獲知服務器Sj的長期私鑰s；

步驟2A截獲用戶發送給服務器的消息M1=，從而獲知如下信息：(a)根據Op=CusP=sCuP可得CuP；(b)根據P IDu=CuP ⊕IDu可 得I Du；(c)根據Xu=h(IDu||pkRC)可 得Xu；

步驟3A截獲服務器發送給用戶的消息M2=， 從而可以根據Vj=Dj ⊕Xu可 得Dj；

步驟4A根據獲知的信息CuP, I Du和Dj，可得會話密鑰S Kuj=h(IDu||CuP||Dj||Xu||IDj)。

通過上述步驟，敵手A在通信中只進行了竊聽，通過計算就可獲得用戶的身份標識和計算得到最終的會話密鑰。

(2) 利用BAN邏輯分析MZK20協議。下面用BAN邏輯對MZK20協議進行分析。首先給出BAN邏輯中的規定[20]，其中A ,B表 示用戶，X ,Y表示某一陳述，K表示密鑰：

(a) A belives X ：用戶 A 相 信陳述 X；

(b) A sees X： 用戶 A 收 到了陳述 X；

(c) A said X ：用戶 A曾給某一協議參與方發送了陳述 X；

(h) A?XB ： 用戶A ,B之 間共享秘密 X；

(i){X}K：由密鑰K加 密的陳述 X；

(j) < X>Y： 秘密陳述 Y 與陳述 X進行捆綁。

由于消息M1,M2,M3中，D IDu,Quj,M3都是用于驗證雙方身份的，所以將Sj和Uu之間的通信消息進行簡化表述。最終用BAN邏輯分析MZK20協議的過程如表1所示。

表1 BAN邏輯分析MZK20協議

由此， Uu并不能保證相信該會話密鑰，即并不能滿足協議目標G4，因此利用BAN邏輯分析得出該協議存在安全性質上的不足。

3.2 VSR20協議安全性分析

2020年，Sureshkumar等人[25]面向智能電網環境，提出了一個雙向AKA協議(以下簡稱該協議為VSR20協議)，并聲稱該協議具有匿名性、前向安全性、不可追蹤性等多種安全屬性。本小節將指出VSR20協議不具備弱前向安全性，且不能夠抵抗臨時私鑰泄露攻擊。

3.2.1 VSR20協議描述

VSR20協議共由系統建立階段、注冊階段、登錄和認證階段、密鑰建立階段4個部分組成，下面具體介紹每個階段的步驟。

(1) 系統建立階段。服務器(以下簡稱 SP)通過如下的步驟生成系統參數：

步驟1 S P在 域Zq上 建立一個橢圓曲線E(a,b):y2=x3+ax+b，其中q是大素數。G是橢圓曲線上的加法阿貝爾群，Q是群G的生成元。

步驟2 S P選 擇一個哈希函數h:{0,1}?→{0,1}160。

(2) 注冊階。 SP 執 行如下的步驟完成第k個用戶(以下簡稱S Mk)的注冊：

步驟1 S P在 域Zq上 選擇兩個隨機數s和xk，用s作為自己的私鑰，用xk作為S Mk的秘密參數。并計算自己的公鑰S=sQ。

步驟2 S P為 S Mk選擇一個160 bit的身份標識IDk，并將I Dk和xk存儲在數據庫中。

步驟3 S P通 過安全信道將發送給S Mi,i=1,2,...,k,...,n。

(3) 登錄和認證階段。S P通過如下的步驟發起與S Mk的通信，如圖1所示。

圖1 VSR20協議的登錄和認證階段

步驟1 SP 選擇一個隨機數d∈Zq，并計算D1=dQ。之后將消息M1=進行廣播，其中T S1是S P此刻的時間戳。

步驟2 在收到M1后 ，S Mk選擇一個隨機數r ∈Zq，并計算R=rQ,D2=rS=rsQ,D3=h(D1||D2||R||TS2) ,D4=IDk ⊕D3和D5=h(IDk||R||xk) 。S Mk將登錄消息M2=發送給S P ，其中 T S2是此刻的時間戳。

步驟3 在收到M2后，S P 驗 證時間戳T S2的有效 性。如果 驗 證通 過，則 SP 計 算R′=s?1D2,D3′=h(D1||D2||R′||TS2) , I D′k=D4⊕D3′。之 后，SP在 數據庫查找I D’k，若該身份標識存在，則通過數據 庫 獲知與 ID’k相 對 應的xk，并 計算D5′=h(ID′kk||R′||xk)， S P 驗證等式D5′=D5是否成立，如果成立，則認證完成，S P執行步驟4。

步 驟4 SP 計 算D6=h(ID’k||R′||TS3)將消息M3= 發送給 S Mk。

步驟5 在收到M3后，S Mk驗證時間戳T S3的有效性。如果驗證通過，則S Mk計 算D6?=h(IDk||R||TS3) ，S Mk驗證等式D6′=D6是否 成立，如果成立，則認證完成。

(4) 密鑰建立階段。 SP與 S Mk之間的相互認證完成后，雙方就可以分別計算會話密鑰SK=h(R||D3||TS1)。

3.2.2 VSR20協議安全分析

本小節分別通過啟發式分析的方法和Scyther形式化工具方法[23]，指出了VSR20協議在安全性上的不足，具體分析如下。首先通過啟發式的分析指出該協議不具備弱前向安全性，并且不能抵抗臨時私鑰泄露攻擊。其次用Scyther軟件證明了啟發式分析方法的正確性。

(1) 啟發式分析方法。

(a)弱前向安全性。當 SP的 長期私鑰s泄露時，指出該協議不具備匿名性和弱前向安全性。具體攻擊步驟如下(假設敵手為A)：

步驟1 敵手A通過長期私鑰泄露問詢獲知服務器S P的 長期私鑰s；

步驟2A截獲服務器發送給用戶的消息M1=；

步驟3A截獲用戶發送給服務器的消息M2=，從而獲知如下信息：

① 根據D2可 得R；

② 根據R,D1,D2和T S2，可計算得D3=h(D1||D2||R||TS2)；

步驟4A根據獲知的信息R,D3,D4和T S1，從而獲知如下信息：

① 可計算得會話密鑰S K=h(R||D3||TS1)；

② 可計算得用戶的身份標識 IDk=D4⊕D3。

通過上述步驟，敵手A僅通過竊聽就能夠同步獲得用戶與服務器之間的會話密鑰，因此該協議不具有弱前向安全性。并且敵手A可以恢復出用戶的身份標識I Dk，因此該協議同時不能具有匿名性。

(b) 臨時私鑰泄露攻擊。當 S Mk的臨時私鑰泄露時，指出該協議不能夠抵抗臨時私鑰泄露攻擊。具體攻擊步驟如下(假設敵手為A)：

步驟1A通過臨時私鑰泄露問詢獲知用戶SMk的臨時私鑰r；

步驟2A截獲服務器發送給用戶的消息M1=；

步驟3A截獲用戶發送給服務器的消息M2=；

步驟4A根據獲知的信息r、D1、D2、T S1和TS2，從而獲知如下信息：

①可計算得D3=h(D1||D2||R||TS2)=h(D1||D2||rQ||TS2)；

②可計算得會話密鑰SK=h(R||D3||TS1)=h(rQ||D3||TS1)。

通過上述步驟，敵手A在獲知用戶臨時私鑰r的情況下能夠同步恢復出會話密鑰S K，因此該協議不能夠抵抗臨時私鑰泄露攻擊。

(2) 利用Scyther軟件進行分析。利用形式化分析工具Scyther分析VSR20協議，Scyther分析結果如圖2所示，給出的具體攻擊路徑如圖2(b)所示。根據圖2可得，該協議不具備完全的安全性質，存在至少一種攻擊方法，即如圖2(b)所示，該協議不能夠抵抗用戶臨時私鑰泄露攻擊。

圖2 Scyther軟件分析VSR20協議

3.3 VSR20協議的改進與分析

總結并分析上述兩個協議的安全性不足，在MZK20協議中，用戶采用服務器的長期公鑰與自己的臨時密鑰進行捆綁，但忽略了服務器長期私鑰泄露的情況；同樣地，在VSR20協議中，當敵手獲取服務器的長期私鑰時，敵手即可從消息中恢復用戶的臨時密鑰。當敵手恢復出用戶的臨時密鑰時，敵手就可以利用臨時密鑰對之后的消息進行解密。并且協議最后計算會話密鑰時，兩個協議沒有將雙方的臨時密鑰進行捆綁，只采用了一方的臨時密鑰，在這種情況下，當該方的臨時密鑰泄露時就很容易計算出最終的會話密鑰。因此，在安全的AKA協議中計算會話密鑰時應該既考慮長期私鑰又考慮臨時私鑰。

(1) 改進VSR20協議描述。根據3.2.2節的分析，針對VSR20協議登錄和認證階段的不足，給出了如下的改進方案，在最后的計算會話密鑰階段將用戶的臨時密鑰和服務器的臨時密鑰進行捆綁，用戶的長期密鑰和服務器的長期密鑰進行捆綁(如圖3所示)，提高協議的抗攻擊能力。對于 SP，會話密鑰為 S KSP=h(sR||dxQ||D3||TS1) ； 對于S Mk，會話密鑰為S Kk=h(rS||xD1||D3||TS1)。

圖3 改進VSR20協議

(2) 改進VSR20協議的安全性分析。首先證明匹配會話在協議結束后會得到相同的會話密鑰。因為

所以 SP 和S Mk計算的會話密鑰相同，即SKSP=SKk。

其次證明不存在多項式時間敵手能夠以不可忽略的優勢贏得測試游戲。

定理1 若h是隨機預言且ECCDH假設在群G中成立，那么改進后的VSR20協議在eCK模型中是安全的。

證明 設敵手A在系統安全參數為τ的情況下，最多能夠激活n個誠實用戶和s個會話。如果A能夠獲得生成會話密鑰的非平凡信息，則有可能以不可忽略的優勢成功贏得測試游戲。由于h是隨機預言，因此A在進行完測試游戲后只能夠以下列的方式區分正確的會話密鑰和與正確會話密鑰同分布的隨機值：

事件1 猜測攻擊：A通過猜測的方式獲得正確的會話密鑰；

事件2 會話密鑰復制攻擊：A通過某種方式建立一個與測試會話不匹配的會話 sid’，但是能夠與測試會話生成相同的會話密鑰，此時，A通過查詢 sid’就可以獲得測試會話的會話密鑰，贏得測試游戲；

事件3 偽造攻擊：A在某個時刻對隨機預言h進行了與測試會話的會話密鑰相同的查詢。

對于事件2，這種情況下相當于對h進行碰撞攻擊，而h是一個隨機預言，對其實施碰撞攻擊成功的概率為O(s2/2τ)，這個概率也是可以忽略的，因此事件2的情況也可以不予考慮。

對于事件3，可以將會話分為以下兩種情形：

情形1 測試會話存在匹配會話，而且匹配會話的擁有者是誠實用戶；

情形2 測試會話不存在匹配會話，或者匹配會話的擁有者不是誠實用戶。

下面針對這兩種情形，分別進行分析。證明的思路是如果存在敵手能夠以不可忽略的優勢贏得測試游戲，那么可以以該敵手為子算法構造能夠以不可忽略優勢解決ECCDH問題的算法。

情形1A主要通過如下4種方式對測試會話發起攻擊：

(a) StaticKeyReveal(C) 問詢：如果用戶C是SMk或 者S P ， 則S放棄本次模擬運行；否則，S提供用戶C的長期私鑰作為應答，其中長期私鑰是S在模擬初始階段生成的；

(b) EphemeralKeyReveal(C,sid) 問詢：S提供用戶C在會話s id中的臨時私鑰作為應答；

(c) S essionKeyReveal(sid) 問 詢：S以 如 下 方 式提供會話密鑰作為本次問詢的應答：設會話標識為sid=(A,C,D1,D2,D3,D4,D5,D6,TS1,TS2,TS3)，則相應的會話密鑰是 S K=h(σ)，其中隨機預言的輸入為

σ=(ECCDH(pkSP,epkk)||ECCDH(xQ,epkSP)||D3||TS1)。

S查詢隨機預言h輸入是否已經被問詢過，如果未被問詢過，則輸出一個與會話密鑰同分布的隨機值；如果已經被問詢過，則輸出正確的會話密鑰。

(a) StaticKeyReveal(C) 問詢：如果用戶C是SP 或 者S Mk，則S放棄本次模擬運行；否則，S提供用戶C的長期私鑰作為應答，其中長期私鑰是S在模擬初始階段生成的；

(b) EphemeralKeyReveal(C,sid) 問詢：S提供用戶在會話s id中的臨時私鑰作為應答；

(c) S essionKeyReveal(sid) 問 詢：S以如下方式提供會話密鑰作為本次問詢的應答：設會話標識為

sid=(A,C,D1,D2,D3,D4,D5,D6,TS1,TS2,TS3)，則相應的會話密鑰是 S K=h(σ)，其中隨機預言的輸入為σ=(ECCDH(pkSP,epkk)||ECCDH(xQ,epkSP)||D3||TS1)。

其中，P2(τ,t)表 示情形1.2發生且A成功的概率。

情形1.3A對 測試會話進行長期密鑰暴露查詢，對測試會話的匹配會話進行臨時密鑰暴露查詢。給定ECCDH實例aQ,bQ ∈G， 下面構造模擬算法S能夠以不可忽略的優勢解決ECCDH問題。S可以以至少 1/sn概率猜測A選擇會話s id’作為測試會話，且測試會話的擁有者為 SP，測試會話的匹配會話的擁有者為用戶 SMk。將SP的臨時公鑰設置為aQ，SM_k的長期公鑰設置為bQ，剩余用戶正常分配公私鑰對。然后，模擬一個協議運行環境，保證不能以不可忽略概率區分這個模擬環境與現實環境。情形1.3中各種查詢的模擬與情形1.1相似，則情形1.3中成功解決ECCDH問題的優勢估計為

其中，P4(τ,t)表 示情形1.4發生且A成功的概率。

情形2 在這種情況下，測試會話不存在匹配會話。A主要通過以下兩種方式對測試會話進行攻擊：

情形2.1A對測試會話進行臨時密鑰暴露問詢，由于測試會話不存在匹配會話，因此當A獲得測試會話擁有者的臨時密鑰時，A相當于也獲得了測試會話預通信方的臨時密鑰。這種情形下，與情形1.1類似。根據情形1.1的分析，如果A成功贏得測試游戲，則S能夠以不可忽略的優勢解決ECCDH問題。

情形2.2A對測試會話進行長期密鑰暴露問詢，由于測試會話不存在匹配會話，因此當A獲得測試會話擁有者的長期密鑰時，A相當于也獲得了測試會話預通信方的臨時密鑰。這種情形下，與情形1.4類似。根據情形1.4的分析，如果A成功贏得測試游戲，則S能夠以不可忽略的優勢解決ECCDH問題。

綜合上述分析，情形1和情形2情況下都有，如果A能夠成功贏得測試游戲，那么S都能夠以不可忽略的優勢解決ECCDH問題，這與ECCDH在群G中時困難的相矛盾。 證畢

利用Scyther軟件形式化分析改進后的VSR20協議，具體結果如圖4所示。通過Scyther軟件分析可以直觀地看到改進后的VSR20協議彌補了VSR20協議的不足，抗攻擊能力提高，改進后VSR20協議能夠保證雙方長期密鑰和臨時密鑰的安全性，同時會話密鑰的安全性也有所加強。

圖4 Scyther軟件分析改進后VSR20協議

4 結束語

前向安全性能夠為使用者提供重要的安全保障，使得協議在用戶的長期私鑰泄露的情況下仍然能夠保證會話密鑰的安全性。目前，分析AKA協議是否具有前向安全性、怎樣使得AKA協議能夠滿足前向安全性已經成為協議研究的重要方面。本文通過給出協議的有效攻擊方法，分析了MZK20和VSR20兩個AKA協議。文中采用了不同的分析方法分別研究這兩個協議，首先利用BAN邏輯分析了MZK20協議不具有弱前向安全性；其次利用啟發式分析和Scyther工具證明了VSR20協議不具備前向安全性，并且該協議不能夠抵抗臨時密鑰泄露攻擊。文中簡要分析了產生這類安全缺陷的原因，并給出了針對VSR20協議不足的改進方案，改進后的VSR20協議不但是可證明安全的，并且能夠利用Scyther軟件證明其安全性。