基于Tamarin 的5G AKA 协议形式化分析及其改进方法*

刘 镝, 王梓屹, 李大伟, 关振宇, 孙 钰, 刘建伟

北京航空航天大学网络空间安全学院, 北京 100191

1 引言

移动用户通过全球用户身份模块(universal subscriber identity module, USIM) 卡连接到移动网络,用户和运营商都希望从所使用的通信协议中得到安全保证, 比如用户语音、短信的保密性等. 鉴权和密钥协商协议(authentication and key agreement, AKA) 能够实现用户和运营商网络之间的相互认证, 并完成协商会话密钥的工作, 且能建立一个安全信道来保证后续通信和数据传输的安全.

攻击者可能会利用通信协议存在的安全漏洞来发起攻击, 这将严重威胁个人隐私、财产安全. 5G 通信的安全严重依赖于5G AKA 协议的安全性, 因此对5G AKA 协议的安全性分析显得尤为重要, 但是协议流程的复杂性使得很难通过人工的方式去发现其安全漏洞. 本文利用安全协议验证工具Tamarin 对5G AKA 协议进行形式化分析, 以便更好地发现其安全漏洞, 从而促进协议标准的改进和完善, 使得5G AKA 协议在5G 网络全面商用后为用户和运营商提供更好的安全保证.

5G AKA 协议用于实现用户和运营商网络之间的身份验证和密钥协商, 涉及到的实体有用户设备(user equipment, UE)、用户在近距离内连接的服务网络(serving network, SN) 和与用户对应的运营商归属网络(home network, HN). 服务网络SN 中包括安全锚点功能(security anchor function, SEAF),归属网络HN 中包括鉴权服务功能(authentication server function, AUSF)、鉴权证书库和处理功能(authentication credential repository and processing function, ARPF).

1.1 相关工作

在3G 网络时代, AKA 协议的安全性大多是通过使用TLA 和BAN 逻辑[1]手动进行验证, 这种验证方式只考虑了很简单的威胁模型, 也只能提供很弱的安全保证, 并不适用于现在的使用场景. 为了提高协议的设计效率, 研究人员开始使用ProVerif、Scyther、AVISPA、Tamarin 等自动化的安全协议验证工具来对协议进行形式化分析. 比如, Arapinis 等人[2]用ProVerif 分析了3G 网络中的AKA 协议, 发现了针对用户位置和身份匿名性的攻击, 并提出了对应的解决方案.

在4G 网络时代, Hussain 等人[3]结合符号模型检查和密码协议验证提出一种基于模型的测试化方法, 使用ProVerif 分析了4G 网络中的EPS AKA 协议, 发现了鉴权重放攻击和对用户位置的欺骗攻击等, 但是并没有提出具体的防御措施. 随着5G 技术的发展, 逐渐形成了4G 网络和5G 网络共存的局面,许多研究者开始对5G AKA 协议进行分析. Ferrag 等人[4]对4G 和5G 网络中的鉴权和隐私保护方案进行了较为全面的研究, 总结了相应的应对策略和形式化及非形式化的安全分析技术, 为未来5G 网络安全的研究方向提供了思路.

在5G AKA 协议的形式化分析方面. Basin 等人[5]使用Tamarin 对5G AKA 协议进行了形式化分析. 基于3GPP TS 33.501 v15.1.0 版本[6], 针对从5G 安全标准中提取出的安全目标, 提供了第一个5G AKA 协议形式化模型, 但是作者把AUSF 和ARPF 两个实体建模为一个大的HN 实体, 并不能准确的刻画5G AKA 协议的流程. Cremers 等人[7]基于3GPP TS 33.501 v0.7.0 版本[8], 把HN 中的AUSF和ARPF 分别单独建模为两个参与实体, 对5G AKA 协议进行了分析, 发现了一种由会话竞争导致的攻击, 但是他们分析的协议版本过于老旧, 并且只分析了UE、SN 和HN 之间的部分鉴权性质. Edris 等人[9]基于3GPP TS 33.501 v15.5.0 版本, 使用ProVerif 对5G AKA 协议进行了系统的安全性评估, 但是对于发现的问题并没有给出有效的解决方法.

Cao 等人[10]针对5G 网络海量设备并发连接的场景, 设计了一种轻量级的安全接入认证协议, 并使用ProVerif 和Scyther 两种工具对该协议进行了形式化分析. 也有研究人员[11,12]使用AVISPA 对5G AKA 协议的相关变体协议进行了形式化分析. 这些工作都对5G AKA 协议的形式化分析带来了启发,但由于ProVerif 中的异或运算是通过用户自定义方程来实现且其支持验证的安全性质有限, 而Scyther、AVISPA 不能自定义安全性质且支持的密码学运算较少. 这些工具在协议的形式化分析上都存在着相应的局限性.

目前国内外学者对5G AKA 协议的形式化分析大多基于3GPP 组织发布的5G 技术规范中的R15标准或者R15 之前的标准, 而在新发布的R16[13]、R17 标准中对5G AKA 协议的鉴权流程进行了几个大的修改, 这些修改对5G AKA 协议安全性的影响需要再次被评估. 5G 技术规范中最新的R17 标准已于2020 年12 月发布, 与R16 标准相比, R17 标准中的5G AKA 协议仅增加了可选的AKMA 功能, 其他并无不同. 因此本文参考R17 标准v17.0.0 版本[14]中的协议, 选择内置异或等多种运算的Tamarin来综合评估这些修改对协议安全性的影响.

1.2 本文贡献

(1) 本文对新版本5G AKA 协议和期望其满足的安全性质进行了形式化建模. 搭建的模型[15]可以准确、完整的刻画5G AKA 协议的流程, 还可以验证协议的相关安全性质. 本模型具有很好的扩展性, 可以在本模型的基础上进行修改来对其他认证和密钥协商协议进行形式化分析.

(2) 本文在Tamarin 中验证了5G AKA 协议在安全锚点密钥KSEAF和长期共享密钥K上的保密性质,以及在用户永久标识符(subscription permanent identifier,SUPI)、服务网络标识符SNID和安全锚点密钥KSEAF上Lowe 鉴权性质[16]的满足情况. 发现在36 条鉴权性质中有23 条没有得到满足, 特别是在密钥KSEAF上的鉴权性质几乎都没有满足, 这表明攻击者可以发动针对该密钥的重放攻击.

(3) 对于5G AKA 协议不满足的鉴权性质, 本文参考了Basin[5]和Cremers[7]等人提出的方法, 提出了结合SNID 绑定、会话绑定、密钥确认往返三个方面的5G AKA 协议改进方案. 此方案为未来新版本5G AKA 协议的设计和改进提供了新的思路, 并且可以扩展应用到EAP-AKA 等协议的分析上.

(4) 本文根据提出的综合改进方案对5G AKA 协议进行了修改, 并在Tamarin 中重新验证了改进后的协议对安全性质的满足情况. 验证结果表明, 在改进前的23 条不满足的鉴权性质中, 有20 条在协议改进后得到了满足. 改进后协议的安全性得到了很大提升.

2 5G AKA 协议介绍

2.1 蜂窝网络架构

蜂窝网络整体架构大致由三个大的逻辑实体组成: 用户设备UE、服务网络SN、归属网络HN. 网络架构图如图1 所示.

图1 蜂窝网络架构Figure 1 Cellular network architecture

用户设备UE 一般是智能手机或者物联网设备, UE 由移动设备(mobile equipment, ME) 和USIM卡组成, USIM 卡中存有用户永久身份标识符SUPI、序列号(sequence number, SQN)、长期对称密钥K和公共非对称密钥pkHN. SUPI 是一个唯一且永久的用户身份标识; SQN 是用于验证鉴权消息新鲜性的计数器; 对称密钥K是用户与其对应归属网络HN 中的ARPF 之间的共享密钥; 公共非对称密钥pkHN也对应于归属网络HN, 用于对SUPI 进行加密得到用户加密标识符(subscription concealed identifier,SUCI).

服务网络SN 主要在漫游场景中和用户进行通信, 其中的安全锚点功能SEAF 负责完成对UE 的鉴权以及协助UE 和归属网络HN 之间的鉴权, 在鉴权成功且与UE 建立安全信道后对UE 提供服务. SN中其它的功能模块在这里不进行说明.

归属网络HN 的数据库中也存有序列号SQN、长期共享密钥K、与公钥pkHN相对应的私钥等.其中的认证服务功能AUSF、认证证书库和处理功能ARPF 负责向服务网络SN 提供用于认证过程的鉴权向量, AUSF 会在SEAF 对UE 鉴权成功后再次鉴权, 用户标识符解密功能(subscription identifier de-concealing function, SIDF) 负责将SUCI 解密为SUPI. 因为统一数据管理功能(unified data management, UDM) 在鉴权过程中和ARPF 功能基本一致, 因此本文只对ARPF 进行介绍.

用户使用配备了USIM 卡的设备通过不安全的无线信道(在图1 中用虚线标出) 和SN 中的基站进行通信, SN 和HN 之间以及HN 内部的AUSF 和ARPF 之间的通信通过经过验证的有线信道(在图1 中用实线标出) 进行, 可以认为是安全的.

2.2 5G AKA 协议的鉴权流程

5G AKA 协议使用挑战-响应机制来完成用户和运营商网络之间的身份认证, 同时基于身份认证对通信过程所需的密钥进行协商, 是一种双向的认证机制. 详细的鉴权流程如图2 所示.

图2 5G AKA 协议鉴权流程Figure 2 Authentication procedure for 5G AKA protocol

(1) 当服务网络SN 触发和用户UE 的鉴权, UE 使用其对应归属网络的公钥pkHN将SUPI 加密为SUCI, 再将SUCI 发送给SEAF. SEAF 根据SUCI 中包含的归属网络标识符选择用户对应的归属网络来请求鉴权材料, 再发送SUCI 和SNID 给AUSF.

(2) AUSF 将收到的SNID 与预期的服务网络名称进行比较. 若一致则会暂时存储SNID, 再发送SUCI 和SNID 给ARPF.

(3) ARPF 通过用户标识符解密功能SIDF 从SUCI 中解密出SUPI,然后选择鉴权方式为5G AKA.ARPF 会计算出密钥KAUSF、参数XRES* (预期响应, expected response), 然后由参数RAND(一个随机数)、AUTN (认证令牌, authentication token)、XRES*、KAUSF创建出鉴权向量5G HE AV (5G home environment authentication vector) 发送给AUSF.

(4) AUSF 根据5G HE AV 中的XRES* 计算出其哈希值HXRES*, 根据密钥KAUSF计算出KSEAF, 由RAND、AUTN、HXRES*、KSEAF创建出鉴权向量5G AV (5G authentication vector), 移除密钥KSEAF得到5G SE AV (5G serving environment authentication vector), 再发送5G SE AV (RAND、AUTN、HXRES*）给SEAF.

(5) SEAF 接收到AUSF 发来的5G SE AV 后, 将参数RAND 和AUTN 发送给UE.

(6) UE 从AUTN 中提取出MAC (消息认证码, message authentication code) 和SQN 来验证鉴权材料的有效性. 若通过验证, 则更新自己的SQN, 计算出参数RES* 和密钥KSEAF, 再把参数RES* 发送给SEAF.

(7) SEAF 计算RES* 的哈希值HRES*, 再比较HRES* 和HXRES* 是否一致. 若不一致则鉴权失败, 若一致则从服务网络的角度认为此次鉴权成功, 再发送RES* 给AUSF 进行下一步认证.

(8) AUSF 首先验证鉴权向量是否过期. 如果过期了, 则AUSF 从归属网络的角度认为鉴权失败; 如果验证成功, 则AUSF 比较RES* 和XRES* 是否一致. 如果一致, 则AUSF 从归属网络的角度认为此次鉴权成功.

(9) 鉴权成功后, AUSF 会发送密钥KSEAF和SUPI 给SEAF. 密钥KSEAF就会成为安全锚点密钥, SEAF 会根据此密钥来计算后续通信过程中的其它密钥.

2.3 相关参数的生成流程

5G AKA 协议的鉴权流程中涉及到很多的参数和函数. 下面依据3GPP 组织发布的3G 安全结构技术规范(TS 33.102) v14.1.0 版本[17], 对鉴权向量的生成流程和相关函数的作用、UE 对鉴权材料有效性的验证流程进行说明.

2.3.1 鉴权向量AV 的生成流程

首先随机生成一个序列号SQN 和一个随机数RAND, 再计算下列各参数:

其中f1、f2 是消息认证函数,f3、f4、f5 是密钥生成函数,K是与UE 共享的长期对称密钥. 计算出上述三个密钥CK、IK、AK 后, 就可以计算出:

其中KDF 是密钥派生函数, SHA256 是输出值长度为256 比特的杂凑函数, 进而可以得到在5G AKA协议中需要使用的鉴权向量5G HE AV、5G AV 和5G SE AV:

2.3.2 UE 对鉴权材料有效性的验证流程

UE 接收到SEAF 发来的参数RAND 和AUTN 之后, 首先通过RAND 计算出匿名密钥AK, 从AUTN 中提取出序列号SQN 和消息认证码MAC, 再计算XMAC 和其它参数, 验证XMAC 和MAC是否相等. 若相等则验证成功, 再验证SQN 是否在正确的范围, 即存储在UE 处的SQNUE是否小于从AUTN 中提取出的SQN. 具体的计算过程如下:

其中函数f1-f5 的含义与2.3.1 节中所述一致. 鉴权材料有效性验证成功之后, UE 会计算响应RES 发送给SEAF, 再计算出密钥KSEAF. 密钥KSEAF的计算方式与2.3.1 节中一致.

3 形式化建模

3.1 5G AKA 协议的建模

Tamarin[18]使用安全协议理论语言(spthy) 来描述协议状态的转移过程, 用rule 来描述协议状态,用lemma 来描述期望验证的安全性质. 这二者作为Tamarin 的输入, 输出是安全性质在所有可能的情况下都成立的结论或者证明安全性质不成立的反例. 在搭建的协议模型中考虑了4 个参与实体: UE、SEAF、AUSF 和ARPF.

对于存储在UE 侧的序列号SQN, 将其建模为一个单调递增的自然数, 通过一个随机生成的数值来初始化SQN, 并假设攻击者在协议运行初始阶段不知道SQN 的值, 本文没有对SQN 失去同步后再重新进行同步的过程进行建模. 在鉴权初始阶段, 服务网络SN 可能会创建一个名为5G-GUPI 的假名来关联用户标识符SUPI, 以便在后续会话中识别用户, 搭建的协议模型中没有考虑这一可选机制. 本文也没有对一些诸如AMF、ABBA 等参数进行建模, 因为这并不影响协议分析结果的准确度, 反而增加了对协议进行建模的复杂性.

UE 和SEAF 之间的信道是公共信道, 使用Tamarin 中默认的Dolev-Yao 敌手模型[19]对其进行建模. 攻击者可以获取无线公共信道中传输的消息而不被协议参与实体察觉, 在Tamarin 中形式化建模为:[Out(x)]--＞[!KD(x)]. 攻击者也可以将自己已知的任何消息注入到信道中, 在Tamarin 中形式化建模为: [!KU(x)]--[K(x)]-＞[In(x)].

SEAF 和AUSF 之间以及AUSF 和ARPF 之间的信道认为是安全信道,该信道上传输的消息不能被攻击者窃听和篡改, 同时攻击者也不能在该信道上注入自己生成的消息. 使用参数＜Ch_name,Sender,Receiver＞来标识信道, 分别表示信道名称、发送方和接收方[20], 在Tamarin 中形式化建模为:

3.2 安全性质的建模

在安全性质方面, 本文考虑了保密性质和鉴权性质. 保密性质包括安全锚点密钥KSEAF和共享密钥K的保密性; 鉴权性质是基于Lowe 分类法, 包括协议参与者之间在参数SUPI、SNID、KSEAF上的非单射一致性, 以及在KSEAF上的单射一致性.

3.2.1 保密性质的建模

(1) 安全锚点密钥KSEAF的保密性质

分别从UE、SEAF、AUSF 和ARPF 的角度来考虑密钥KSEAF的保密性质. 因为密钥KSEAF是通过密钥KAUSF计算出来, 因此攻击者若获取了密钥KAUSF, 就能计算出密钥KSEAF. 因为密钥KSEAF是在AUSF 处才计算得到, 在ARPF 处只有密钥KAUSF, 因此从ARPF 的角度考虑的是密钥KAUSF的保密性质.

下面举例进行说明: 从UE 的角度考虑密钥KSEAF的保密性质, 如果UE 声明会话密钥是保密的,并且攻击者没有危害UE 获取其密钥K, 则攻击者不能够获取或者计算出密钥KSEAF. 在Tamarin 中形式化建模为:

(2) 长期共享密钥K的保密性质

攻击者一旦获取了长期共享密钥K, 就能够计算出别的参数和密钥KSEAF. 可以认为每一个用户拥有的密钥K是与用户标识符SUPI 绑定的, 如果攻击者不是直接危害UE 获取到密钥K, 则攻击者不能够获取到密钥K. 在Tamarin 中形式化建模为:

3.2.2 鉴权性质的建模

对于协议参与实体UE、SEAF、AUSF 和ARPF, 本文分别从UE、SEAF 和AUSF 的角度考虑了对其他三个实体在参数SUPI、SNID 和KSEAF上的鉴权性质, 一共有36 种情况. 本文没有从ARPF 的角度来考虑的原因是AUSF 和ARPF 都属于归属网络的一部分, 且ARPF 的作用就是生成鉴权向量发送给AUSF, 在这之后并没有消息再返回给ARPF.

下面举例进行说明: 从AUSF 的角度, 考虑其和SEAF 在安全锚点密钥KSEAF上的非单射一致性.AUSF 认为自己和SEAF 完成了一次协议运行, 协议涉及到的参与实体是UE、SEAF、AUSF 和ARPF,并且攻击者没有获取UE 的密钥K, 则至少存在一次SEAF 的协议运行, SEAF 认为自己和AUSF 在密钥KSEAF上协商一致.

4 5G AKA 协议的验证分析

4.1 验证结果

通过实验验证, 本文发现5G AKA 协议满足在安全锚点密钥KSEAF和长期共享密钥K上的保密性质, 5G AKA 协议对Lowe 鉴权性质的满足情况验证结果如表1 所示.

表1 鉴权性质验证结果Table 1 Verification result of authentication properties

表1 中展示了协议参与实体UE、SEAF、AUSF 和ARPF 之间在参数SUPI、SNID 和安全锚点密钥KSEAF上的非单射一致性, 以及在密钥KSEAF上的单射一致性. 其中符号✓代表满足, 符号× 代表不满足,KSEAFI代表验证的是在密钥KSEAF上的单射一致性.

4.2 结果分析

对于保密性质, 并没有发现Cremers 等人[7]的论文中描述的一种由会话竞争导致密钥KSEAF的保密性质被违反的攻击. 本文描述的5G AKA 协议是TS 33.501 v17.0.0 中的版本, 而该论文参考的是v0.7.0 版本. 相比之下, v17.0.0 版本中5G AKA 协议的几个改进之处很好的避免了对密钥KSEAF保密性质的违反, 描述如下:

(1) 在v0.7.0 版本的5G AKA 协议中, ARPF 计算出鉴权向量并发送响应消息给AUSF. 在这个消息中并没有包含SUPI 或SUCI, 如果攻击者几乎同时启动两个与服务网络的会话, AUSF 将无法区分来自ARPF 的两个响应, 并且可能将错误的响应和错误的用户相关联. 而在v17.0.0 版本中, ARPF 发送给AUSF 的响应消息里包含了SUPI.

(2) 在v0.7.0 版本的5G AKA 协议中, AUSF 发送鉴权向量给SEAF 的消息中包含了安全锚点密钥KSEAF. 如果发生了(1) 中描述的会话竞争情况, 攻击者就可以获取到合法用户的密钥KSEAF来计算通信过程中需要的其它密钥, 从而假冒合法用户与服务网络进行通信.

但是在v17.0.0 版本中, AUSF 发送给SEAF 的鉴权向量中不包括密钥KSEAF, 而是在最后对UE鉴权成功之后才将密钥KSEAF发送给SEAF.

对于鉴权性质, 从UE 的角度来考虑的大部分鉴权性质都被违反, 而从SEAF 的角度考虑的大部分鉴权性质都得到了满足. 这跟UE 和SEAF 之间的信道是公共信道有关, 公共信道上的通信更容易受到攻击. 攻击者可以在UE 和SEAF 之间的信道上随意注入SNID, 而UE 并不能分辨其真伪, 而在派生密钥KSEAF的过程中需要使用参数SNID, 导致UE 违反一些鉴权性质.

5 协议改进方法及验证结果

5.1 SNID 绑定

通过对Tamarin 输出的攻击路径图进行分析, 如图3 所示. 大部分攻击都发生在UE 和SEAF 之间的公共信道上, 攻击者可以截取SEAF 发送给UE 的消息, 包括RAND 和AUTN, AUTN 的计算需要用到消息认证码MAC, 但是MAC 并没有与特定的服务网络标识符SNID 绑定, 攻击者可以对消息进行篡改再发送给UE.

图3 UE 和SEAF 在SNID 上的非单射一致性攻击路径Figure 3 Non-injective agreement attack path between UE and SEAF on SNID

通过将SNID 添加到消息认证码MAC 的计算过程中, 即MAC 的计算方法由原来的MAC =f1(K,(SQN||RAND||AMF)) 修改为MAC =f1(K,(SQN||RAND||SNID||AMF)), 可以使得从UE 的角度考虑的大部分鉴权性质得到满足. 对协议进行修改, 再验证后发现, 只有UE 和SEAF 在参数SUPI和密钥KSEAF上的非单射一致性没有得到满足. 针对这一情况, 可以通过增加UE 和SEAF 之间的密钥确认往返过程来解决.

5.2 会话绑定

缺少服务网络和归属网络之间的会话绑定, 可能导致出现会话竞争情况使得SEAF 和AUSF、ARPF之间的一些鉴权性质被违反. 通过在AUSF 和ARPF 之间以及SEAF 和AUSF 之间的会话中添加一个随机生成的会话标识符, 来对会话进行绑定, 避免会话冲突, 从而不会出现AUSF 无法区分来自ARPF 的两个响应消息的情况.

通过增加会话标识符来绑定会话之后, SEAF 和AUSF、AUSF 和ARPF 之间的绝大部分鉴权性质都得到了满足. 其中, 从SEAF 角度考虑的鉴权性质全部得到满足, 从AUSF 角度考虑的鉴权性质大部分得到满足, 但是从AUSF 的角度和SEAF 在密钥KSEAF上的单射一致性仍然没有得到满足. 完整的验证结果如表2 所示.

5.3 密钥确认往返

在增加了SNID 绑定修改之后, 仍然存在UE 和SEAF 在参数SUPI 和密钥KSEAF上的非单射一致性没有得到满足的情况. 通过在协议结束阶段SEAF 和AUSF 对UE 鉴权成功之后增加UE 和SEAF之间的密钥确认往返过程, 可以解决上述问题. 从UE 的角度来看, SNID 绑定和密钥确认往返的作用是类似的, 并且可以减少往返次数, 使得密钥确认往返成为多余的步骤, 鉴权协议的效率也更高.

5.4 验证结果

通过结合上述三种协议改进方法对5G AKA 协议进行改进后, 协议对鉴权性质的满足情况验证结果如表2 所示. 表2 中的符号表示含义与表1 中一致. 与表1 中的验证结果相比, 绝大部分鉴权性质都已经得到了满足. 表2 中未得到满足的三种情况分别是: AUSF 对SEAF 在SUPI 上的非单射一致性、AUSF 对SEAF 在密钥KSEAF上的非单射一致性和单射一致性.

表2 协议改进后的鉴权性质验证结果Table 2 Verification result of authentication properties after the protocol is improved

从AUSF 角度和SEAF 的相关鉴权性质未被满足的原因是: AUSF 是在对UE 鉴权成功之后才将包含密钥KSEAF和参数SUPI 的消息发送给SEAF. SEAF 接收到消息之后, 协议的鉴权流程就结束了, 在这之后SEAF 并没有再和AUSF 进行交互, AUSF 也并不知道SEAF 是否正确获取了密钥KSEAF和参数SUPI, 从而导致这三条鉴权性质没有得到满足.

6 总结

本文在Tamarin 中完成了对新版本5G AKA 协议和期望协议满足的安全性质的形式化建模. 安全性质考虑了相关密钥的保密性质和协议参与实体之间的Lowe 鉴权性质, 验证分析了5G AKA 协议在相关安全性质上的满足情况. 重新评估了新版本5G AKA 协议在之前旧版本协议面临的安全问题上的安全性质. 针对相关安全问题, 采用了三种方法来对协议模型进行改进, 重新验证了改进后的协议模型是否满足了改进前未满足的安全性质.

5G AKA 协议标准目前在持续的完善过程当中, 在未来可以继续对新版本的5G AKA 协议以及相关变体协议进行形式化分析. 本文提出的模型可以作为对后续新版本协议进行形式化分析的基础, 也为其他认证和密钥协商协议的形式化分析提供了新思路.