两个认证密钥协商协议的前向安全性分析
2022-12-28程庆丰马玉千
程庆丰 马玉千
(战略支援部队信息工程大学 郑州 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=
步骤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=
步骤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=
步骤3A截获服务器发送给用户的消息M2=
步骤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通 过安全信道将
(3) 登录和认证阶段。S P通过如下的步骤发起与S Mk的通信，如图1所示。
图1 VSR20协议的登录和认证阶段
步骤1 SP 选择一个随机数d∈Zq，并计算D1=dQ。之后将消息M1=
步骤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=
步骤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=
步骤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软件证明其安全性。
