1 引　言

随着通信技术的发展, 移动设备已经广泛普及, 比如手机、智能手表等. 据统计, 目前已有50亿人都是移动通信用户, 这是一个庞大的群体^[1]. 他们通过多种多样的设备来享受移动网络提供的丰富服务, 并被国际移动电信组织(3rd generation partnership projec, 3GPP)制定的安全机制所保护. 在漫长的发展历程中, 移动通信技术已经走过了最初的2G、惊喜的3G和成熟的4G时代, 今天正处于5G时代, 即第5代移动网络.

每一代移动网络的发展都离不开安全这一主题, 都会形成一系列的安全机制, 而其中一个极其重要的机制是用户设备(user equipment, UE)和归属网(home network, HN)之间的双向认证. 事实上, 3G已经存在较为稳定的认证方法, 即认证与密钥协商机制(authentication and key agreement, AKA). 到了4G, AKA方法得到进一步发展, 演变为更加成熟和安全的EPS-AKA和EAP-AKA协议. 现如今, 经3GPP在前人基础上长达数年的研究, 5G的鉴权与认证协议最终形成^[2]. 该协议的目标是在包含通用用户身份模块(universal subscriber identity module, USIM)的设备和归属网络之间提供一个双向鉴权机制, 以使双方在信息读取、网络接入等权限问题上达成一致. 在确保隐私安全的情况下, 用户可以正常的享用移动通信服务. 为了实现这一目标, AKA协议会在认证成功之后, 赋予UE和HN一个共享会话密钥以保障后续双方的信息通信. 经过3GPP组织反复的商榷, 最终确立的5G鉴权协议有两种, 即5G-AKA和EPS-AKA'. 事实上, 它们的设计目标是一致的, 而其中的差异也只关乎法律因素^[3]. 因此, 就本文聚焦的隐私安全来说, 它们没有不同, 在此, 本文主要选取5G-AKA协议展开研究和讨论.

近些年, 针对认证协议的研究取得了巨大的进展, 业界已经发现了一些关于5G-AKA协议的脆弱性, 如: 不同类型的失败消息的可区分性可能会使鉴权结果泄露、序列号的不完善加密可能会导致其被破解以及SUPI的非对称加密可能会带来较高计算复杂度. 同时, 协议分析逐渐大量采用形式化分析方法^[4-6]. 一些研究者通过形式化手段分析5G-AKA, 发现了协议中的一些缺陷, 如SUPI在UE侧的不可靠存储、会话密钥的弱私密性等^{[7, 8]}. 针对当前5G认证协议存在的缺陷, 一些安全研究人员提出了改进方案. Koutsos等人^[9]提出了具有两阶段子协议的AKA⁺方案, 其最大的特色是设计了两个子协议相互补充的机制, 其总体运行模式如图1. 它采用新颖的交替运行实现了认证协议所有的功能, 两个子协议互为补充, 分别应对不同的情况, 是一个较为优秀的改进方案. AKA⁺协议会依据V-GUTI的值来决定选用哪个子模块, 而鉴权的结果, 即成功或者失败, 又会反过来影响V-GUTI的值. 作者还证明了该协议不仅可以很好地抵抗现有攻击, 还取得了较高的平均认证效率.

通过分析AKA⁺方案独特的工作模式, 如图1, 我们发现了其存在一个脆弱点. 在该协议中, 用户永久身份标识(subscription permanent identifier, SUPI)和全局唯一临时标识(globally unique temporary identity, GUTI)子协议传输的消息结构和组成不同, 因而, 我们在实际观测中可以识别认证网正在运行何种子协议. 据此, 我们设计了一种连接性攻击, 总体过程如图2. 具体来说, 当需要判断一个隐式UE_x与目标UE₀的关系时, 攻击者首先监测UE_x和UE₀一次成功的AKA⁺认证. 根据协议规定, UE₀和UE_x的GUTI标识符(V-GUTI)都会被设置为True. 接下来, 攻击者让UE₀再进行一次AKA⁺认证, 并通过消息截断的方式使其认证失败, 此时UE₀的GUTI会被消耗, 即V-GUTI变为False. 最后, UE₀和UE_x再进行一次AKA⁺认证. 通过观察传输的消息类型, 攻击者能够判断是哪个子协议在运行. 作为结果, 有两种情况.

● 如果UE_x运行的是SUPI子协议, 则有UE₀=UE_x, 即未知的UE_x即是目标UE₀.

● 如果UE_x运行的是GUTI子协议, 则有UE₀≠UE_x, 即未知的UE_x不是目标UE₀.

因此, 攻击者可以推断出UE_x和目标UE₀之间的关系, 这违背了协议的无连接性要求, 即攻击者通过对协议的攻击, 能够探知多个隐式目标之间的关系, 如判断两次跟踪的未知UE是否为同一UE等.

不可否认的是, AKA⁺协议的工作模式是新颖的, 在运行效率上具有很大的优势. 其总是倾向于采用速度更快的GUTI子协议, 而SUPI子协议也在为使用高效的GUTI模块服务. 受此启发, 也鉴于上述指出的脆弱点, 我们提出了具有两阶段平行子模块的SM-AKA协议. 该协议与AKA⁺有类似的工作模式, 即包含一个SUPI子模块和一个GUTI子模块. 不同的是, 我们令两个子模块的鉴权变量具有相同的组成和结构, 从而确保子协议不可区分. 该协议包含3个认证阶段, 分别是: UE向HN发送身份消息, 开启鉴权流程; HN向UE发送结果, 同时更新用于后续认证的变量; UE完成最后的信息检验, 决定是否更新GUTI. 此外, 我们对提出的SM-AKA协议实施了全面的形式化分析, 并得出较有价值的结论. 本文中我们做了如下贡献.

(1) 提出一个改进的认证方案, 即SM-AKA. 它不仅可以提供稳定可靠的交互认证, 还可以有效阻止所有已知的针对5G-AKA及其一些修正版本的攻击.

(2) 在认证协议中仅用到一个随机数和两次消息传输, 并通过新颖的交替运行模式更多的选用轻便的子模块, 这给协议带来了较高的运行效率.

(3) 对SM-AKA协议开展一次精细的形式化分析, 完成了对其各项属性的评估. 同时, 完整的分析证明过程也给形式化验证的发展提供一个经典示范.

本文第2、3节描述了5G-AKA的协议细节及当前研究进展. 第4节介绍SM-AKA协议的鉴权流程. 第5节对提出的改进方案展开了形式化验证和讨论. 最后, 在第6节中给出结论.

2 相关工作

随着5G时代的到来, 研究人员在5G鉴权协议上投入了大量的精力, 取得了可观的进展. 在此, 我们主要从脆弱性挖掘、协议改进和形式化分析3个方面阐述相关研究.

目前, 业界已经发现了鉴权协议的一些脆弱点. Arapinis等人^[10]利用变量的结构缺陷, 提出了一种连接性攻击, 尽管这种攻击的设计初衷是针对4G通信的, 但其对5G-AKA依然适用^[9]. 具体来说, 由于协议在认证失败后, 会产生两种错误消息, 这两种消息的长度和组成不同, 因而易于区分. 攻击者利用这一缺陷能够判断两个未知UE之间的关系, 从而打破协议的无连接性. 攻击能够顺利实现的另一个原因是消息通过空口传输, 攻击者很容易在空气中捕捉到它. 在鉴权中, 空口传输是不可避免的, 因而只能通过改进消息设计阻止可能的攻击. 聚焦于序列号的加密机制, Borgaonkar等人^[11]利用变量的不完备加密, 巧妙地设计了一种信息破译攻击. 攻击者主要通过收集大量鉴权失败响应发挥破译算法的作用. 具体来说, 攻击者首先令UE和HN之间反复进行鉴权, 并通过信息截断等手段, 让鉴权结果交替出现成功和失败. 而在每次获取失败响应时, 攻击者都会通过重放过时的消息以确保结果是重同步类型的, 所谓“重放”是指把同一消息重复发送超过两次. 经过大量的重复操作, 攻击者可以收集到多条重新步类型的失败响应. 然后依据异或计算的特点, 攻击者采用迭代的方式逐位计算出序列号的二进制编码. 最后攻击者可以根据破译的编码在一段时间内的变化推断出用户的隐私, 如通信活动、地理位置等.

Arapinis等人^[10]提出了Fixed-AKA协议, 以应对可能发生的针对消息类型的攻击. 该协议通过公钥加密的方式令两种失败消息具有相同的外部组成, 从而使攻击者无法仅通过观测消息的长度和结构就获悉消息的类型, 故可以阻断攻击行为的进行. 通过研究, Fouque等人^[12]发现上述协议在变量的新鲜度维持上存在缺陷(新鲜度是指消息的唯一性、时效性、不可重用性, 即确保消息是唯一生成, 同时融入时效信息且不能被重用), 以致其容易遭受一种重放攻击. 于是, 新的改进协议PRIV-AKA被提出. 该协议通过使服务侧的序列号只有在收到用户侧的确认消息后才会增加. 这维持了鉴权变量的新鲜性, 避免消息重放. 同时, PRIV-AKA吸收Fixed-AKA的优势, 使鉴权失败消息的类型不可区分. 然而, Koutsos等人^[9]发现, PRIV-AKA无法满足协议的无连接性要求, 攻击者能够轻松的区分目标用户和未知用户之间的关系. 于是, 他们提出了AKA⁺协议, 通过对SUPI和GUTI的交叉运用, 以及对子协议优先级的设定, 很好地满足了UE和HN之间双向认证需求. 同时, AKA⁺每成功运行一次都会为下一次的鉴权生成GUTI, 这使得相对高效的GUTI子协议可以被更多的使用. 此外, Braeken等人^[13]提出了一个两阶段鉴权协议. 它设计了一个身份注册阶段, 通过把SUPI和私钥整合为动态的身份变量来实现信息的加密传输. 并且, 该协议仅使用了2次空口传输, 具有很高的认证效率. 该协议着重于满足协议在效率和安全方面的需求, 是一个较为优秀的改进方案. 聚焦于提升鉴权效率, Gharsallah等人^[14]提出了SEL-AKA协议. 协议去除了认证对全局公钥体系的依赖, 取而代之的是, 用一个新提出的参数发挥相应的作用. 通过其在用户端和服务端的共享, 该参数完成了信息在双端的交换. 分析表明, SEL-AKA很大程度上简化了流程和计算, 满足了鉴权在功能和效率方面的要求. 另外, Braeken等人^[15]在空口消息中, 创新的使用随机数来取代序列号, 以减少协议所需的通信步骤的数量. 而Han等人^[16]则采用了一种新的模式, 把移动边缘计算用于鉴权, 大大丰富了用于变量检验的算力, 可以明显降低认证延迟.

形式化分析作为一种强有力的属性验证方法, 出现在大量5G鉴权协议的研究工作中, 用于评估其安全有效性. 具体来说, Basin等人^[7]使用Tamarin证明器^[17]展开协议的安全属性验证, 其把参与鉴权的终端归为3个实体, 即UE、服务网络和HN, 然后通过Tamarin的规则描述协议内容, 通过引理给出隐私目标. 最终, 分析结果显示, 5G-AKA无法满足无连接性要求以及可能遭受一些特定情况下的攻击. 类似的, Cremers等人^[8]也使用Tamarin对5G-AKA展开分析, 并得到了很有价值的结论. 不同的是, 后者进一步细化协议的参与者, 引入分别执行用户管理和认证管理的单元, 使协议分析更加精细. 当然, 定义的规则和引理也更加复杂. 另外, Edris等人^[18]采用ProVerif工具^[19]对5G-AKA展开形式化验证. 除此之外, 也有一些针对5G-AKA协议变种的分析案例. 如Gharsallah等人^[14]结合AVISPA^[20]和SPAN^[21]对其提出的SEL-AKA协议展开安全属性评估, 并得到一些很有价值的结论. Braeken等人^[13]使用RUBIN逻辑^[22]检验其提出的协议, 验证了协议拥有的优良特性. Koutsos等人^[9]使用BANA-COMON逻辑^[23]评估其提出的AKA⁺协议, 有力地证明了协议能够满足其声明的若干要求.

在本文, 我们针对5G-AKA和AKA⁺协议的缺陷, 提出改进方案. 相较于现有研究, 该方案采取一种交替运行的模式, 不仅可以抵御已知的攻击, 还能够大大提高鉴权的平均效率. 同时, 改进方案减少通信步骤, 降低资源消耗. 而通过形式化验证, 我们证明了该方案可以满足协议的包括无连接性在内的诸多要求, 具有很强的安全特性. 此外, 由于认证过程中使用较多的异或操作, 为了更真实的建模SM-AKA协议, 我们选用功能强大且支持异或操作的Tamarin形式化工具.

3 预知识

本节将阐述我们聚焦的5G-AKA协议, 同时介绍参与认证的实体.

3.1 实体描述

认证协议主要涉及3个实体: UE、服务网络(service network, SN)和归属网络(home network, HN), 其中:

(1) UE是指获取通信服务的载体, 例如移动电话. 每个UE都包含一张USIM卡, 它存储一组用于鉴权的变量: 用户永久身份标识(SUPI)、全局唯一临时身份标识(GUTI)、GUTI标识符(V-GUTI)、用户密钥k、UE侧的序列号 ${\mathit{SQN}_U}$ 和公钥 $p{k_N}$ .

(2) SN控制着基站, 用于给用户提供移动网络接口, 鉴权消息可以通过UE和SN之间的无线频道连接实现空口传输.

(3) HN是指用户注册网络, 存储着用户的身份信息. 它通过维护一个数据库参与鉴权, 存储的变量包括: SUPI^*、GUTI^*、V-GUTI^*、k^*、HN侧的序列号 ${\mathit{SQN}_H}$ 和私钥sk_N.

在鉴权协议中, 通常UE是客户端, HN是服务端, 二者共享SUPI、GUTI、k和V-GUTI. 但为了方便表述, 我们用“*”来区分这些变量在双侧的表示. SN负责二者鉴权消息的双向转发, 即将UE的信息传输到HN和HN的消息传输到UE. 这样做的原因是UE和HN的地理位置不会总是很近, 因此需要一个中介来确保通信可达. 事实上, SN和HN之间通过可信信道通信, 可以确保信息的安全稳定传输. 因此, 为了简化, 我们把HN和SN归为一个实体, 并用HN表示(这种做法已经被一些研究所采纳, 如Koutsos等人^[18]和Braeken等人^[8]的工作. 当然, 也有一些工作把HN和SN看作是单独实体, 如Basin等人^[6]和Cremers等人^[9]的研究).

3.2 5G-AKA协议

这里描述3GPP组织制定的5G-AKA协议, 该协议包含3个必备的通信阶段和一个非必须的重同步阶段.

(1) UE向HN发送初始化消息

UE通过向HN发送自己的身份信息开启一个鉴权会话. 事实上, 代表身份的变量为恒定不变的SUPI, 然而为了防止由于SUPI泄露而遭受一些外部攻击, 该变量通常会被密文传输. 实际上, UE会引进一个非对称加密算法, 同时结合一个新鲜的随机数r和公钥pk_N, 把SUPI转化为隐藏身份标识符SUCI:

$ \mathrm{SUCI} = \{ \mathrm{SUPI}\} _{p{k_N}}^r. $

而SUCI是临时的, 只能被使用一次, 因而可以确保身份信息不被公开. 接下来, SUCI被作为身份变量发送给HN.

(2) HN生成并转发检验消息给UE

HN一旦收到UE的身份信息, 会开启一个鉴权会话. 对于SUCI消息, HN会结合私钥 ${\mathit{SQN}_H}$ 使用非对称解密算法解析SUCI. 依据获得的SUPI, HN会在用户注册数据库中检索出 ${\mathit{SQN}_H}$ 和k. 然后, 两个哈希函数利用一个新生成的随机数r_m把 ${\mathit{SQN}_H}$ 和k^*融入检验变量 ${MAC^*}$ 和 ${CONC^*}$ 中, 即:

$ MA{C^*} = {f_1}({k^*}, \langle {\mathit{SQN}_H}, {r_m} \rangle ),\;\; {CONC^*} = {\mathit{SQN}_H} \oplus {f_5}({k^*}, {r_m}),$

其中, ${\oplus}$ 表示异或操作, f₁和f₅为二元哈希函数. 最后HN把完整的用于查验的消息 ${S^*}$ 发送给UE, 其中:

$ {S^*}{\text{ = }} \langle CON{C^*}, MA{C^*}, {r_m} \rangle . $

(3) UE执行检验并把结果反馈给HN

UE收到消息 ${S^*}$ 后, 首先解析出HN的序列号 ${\mathit{SQN}}_H^* = {\mathit{CONC}^*} \oplus {f_5}(k, {r_m}) $ , 然后计算出UE侧的身份变量MAC= ${f_1}(k, \langle {\mathit{SQN}}_H^*, {r_m} \rangle ) $ , 最后进行身份和新鲜度的检验, 即① $MA{C^*} = = MAC $ , ② ${{\mathit{SQN}}_U} < {\mathit{SQN}}_H^* $ . 其中, ==表示等价判断符号. 作为结果, 有3种情况.

● 如果①=True且②=True, 则鉴权成功, UE会给HN反馈消息 $X = {f_2}(k, {r_m})$ , 并把其自身的序列号 ${\mathit{SQN}_U}$ 设置为 $\mathit{SQN}_H^*$ .

● 如果①=True且②=False, 则新鲜度检验失败, 此时, UE首先生成变量CONC和MACS, 即:

$ {\mathit{CONC}} = {\mathit{SQN}_U} \oplus f_5^*(k, {r_m}), \;\; {\mathit{MACS}} = f_1^*(k, \langle {\mathit{SQN}_U}, {r_m} \rangle ){, } $

然后给HN返回重同步消息 $S = \langle \mathit{CONC}, \mathit{MACS} \rangle$ .

● 对于其他情况, UE直接给HN返回鉴权失败“Failure”消息.

响应发出后, UE侧完成认证流程并结束当前会话.

(4) HN侧进行重同步响应

当收到重同步响应消息时, HN从消息中恢复出UE的序列号 $\mathit{SQN}_U^*$ , 并生成HN侧身份变量 ${\mathit{MACS}^*}$ :

$ \mathit{SQN}_U^* = \mathit{CONC} \oplus f_5^*({k^*}, {r_m}){, }\;\; {\mathit{MACS}^*} = f_1^*({k^*}, \langle \mathit{SQN}_U^*, {r_m} \rangle). $

然后, 检验 ${\mathit{MACS}^*} = = MACS$ 是否成立. 如果通过, 则HN更新自身的序列号, 即 ${\mathit{SQN}_H} = \mathit{SQN}_U^* + 1$ . 这可以使 ${\mathit{SQN}_H}$ 的值回归到正常范围, 避免因 ${\mathit{SQN}_H}$ 的意外增加(比如遭受攻击)而导致新鲜度检验永久性失败. 如果不通过, HN不采取任何操作.

4 SM-AKA协议

我们在这里描述SM-AKA协议的详细设计, 它在5G-AKA及其一些修正版本^{[9, 13]}的基础上, 针对2种失败消息可区分、非对称加密方式计算复杂等缺陷改进. 依据GUTI是否可用, SM-AKA设计了2种运作机制, 分别为GUTI模式和SUPI模式. 每种模式都包含2次鉴权变量通信和1次信息检验, 总共3个步骤. 2种模式的差别主要体现在身份变量的选取, 集中于第1、2步骤, 而第3个步骤完全相同.

在第3.1节中, 我们介绍参与5G鉴权的实体所包含的基础变量. 其中的V-GUTI是区分GUTI和SUPI模式的依据. 这2种模式交替运行, 其选用机理为: HN侧默认选用GUTI模式, 从认证变量M中提取P并在数据库中检索对应身份信息的鉴权参数, 若存在且V-GUTI为True, 则SM-AKA会继续运行GUTI模式. 若检索不存在, 则跳转进入SUPI模式. 在UE侧, V-GUTI发挥作用后总会被置为False. 2种模式都包含完整的流程, 可以独立完成认证. 每当鉴权成功时, UE侧都会把V-GUTI置为True, 以便下次认证能够选用GUTI模式.

4.1 GUTI模式

本节详细描述协议的GUTI模式, 其包含3个步骤, 具体如图3. 值得注意的是, 只有当V-GUTI为True时, GUTI模式才会被选用.

(1) UE向HN通信阶段

一旦鉴权会话开启, UE就着眼于认证变量的生成. 首先, UE会产生一个随机数r, 并通过一个哈希函数把其转化为密文a, 以便直接在空气中传输:

$ a = {f_2}(k, {\rm{GUTI}}) \oplus r. $

紧接着, 结合时敏信息r和GUTI, 用于身份检验的变量MAC被生成:

$ MAC = {f_1}({\rm{GUTI}}, r) \oplus {\mathit{SQN}}{_U}. $

UE在此模式下将采用GUTI作为其身份的标志P, 即P=GUTI. 从而, 完整的认证变量可被获得并用M来表示:

$ M = (P, MAC, a). $

最后, M将被发送给HN. 发出后, 序列号 ${\mathit{SQN}_U}$ 的值增加1, 同时V-GUTI被设置为False以防止GUTI被重放.

(2) HN向UE通信阶段

HN在接收到认证变量后, 首先依据明文传输的GUTI在用户数据库中检索, 以获得用户密钥k^*和序列号 ${\mathit{SQN}_H}$ . 同时, HN侧的V-GUTI被更改False, 以表示GUTI不再可用. 然后, HN从M中恢复出被加密传输的随机数, 即:

$ {r^*} = {\pi _3}(M) \oplus {f_2}({k^*}, {\pi _1}(M)) . $

进一步, UE侧的序列号会由于随机数的解析成功被重载:

$ SQN_U^* = {f_1}({\pi _1}(M), {r^*}) \oplus {\pi _2}(M) . $

接下来, HN生成它的身份检验变量MAC^*:

$ MA{C^*} = {f_1}({\pi _1}(M), {r^*}) \oplus \mathit{SQN}_U^*. $

因此, 鉴权协议规定的两个检验可以被实施, 即:

$ ({\rm{i}})\;MA{C^*} = = {\pi _2}(M), \;\;\; ({\rm{ii}})\;\mathit{SQN}_U^* \geqslant {\mathit{SQN}_H}. $

对于结果, 如果检验(i)和(ii)均通过, 则代表HN侧鉴权成功. 此时, 新的临时身份标识符GUTI^*被生成, 并被加密为中间变量b:

$ b = {f_3}({r^*}, {k^*}) \oplus {{\rm{GUTI}}^*}. $

并且, ${\mathit{SQN}_H}$ 的值被更新为 ${\mathit{SQN}_U} + 1$ , V-GUTI被重置为True. 最后, HN进一步把认证变量补充完整, 并形成S:

$ S = ({f_4}( {\mathit{SQN}}_U^* + 1, {k^*}) \oplus {r^*}, b), $

S被发送给UE, 以用于开展最后的确认阶段.

(3) UE信息查验阶段

这一阶段在UE侧完成, 是鉴权的最后一步. 首先, UE根据S的组成以及自身的基础变量, 重载出被密文传输的GUTI^#:

$ {{\rm{GUTI}}^\# } = {\pi _3}(S) \oplus {f_3}(r, k). $

然后UE的确认变量S^*被计算:

$ {S^*} = {f_4}( {\mathit{SQN}_U}, k) \oplus r .$

紧接着, 检验 $({\rm{i}})\;{S^*} = = {\pi _1}(S)$ 被实行. 如果检验通过, 则UE侧鉴权成功. 此时, V-GUTI的值被置为True, 并且, GUTI被更新为GUTI^#, 以便在下一次鉴权中使用.

至此, GUTI模式下的SM-AKA协议流程结束, 特别的, 只有当UE和HN两侧的鉴权都成功时, 整个过程才为认证成功.

4.2 SUPI模式

我们在此细致描述协议的SUPI模式, 其只有在V-GUTI为False时才被选用. 图4刻画了SUPI模式的具体流程, 与GUTI模式类似, 它也通过3个步骤来完成鉴权, 且每个步骤都有相同的地方. 本节仅描述不同之处, 而其余部分可参考上述GUTI模式的实现.

(1) SUPI的加密传输

由于GUTI不再可用, 因而UE只能通过加密SUPI来完成身份信息的传递. 具体来说, UE首先结合随机数r和序列号, 采用一个基于公钥的非对称加密算法把SUPI化为隐藏变量P:

$ P = Enc({\rm{SUPI}}, {\mathit{SQN}_U})_{p{k_N}}^r ,$

其中, P代替GUTI充当身份变量进行传输.

从GUTI模式跳转到SUPI模式后, HN选用基于私钥的非对称解密算法把SUPI和UE的序列号从变量P中恢复:

$ {{\rm{SUPI}}^*}, {\mathit{SQN}}_U^* = Dec({\pi _1}(M), s{k_N}) .$

接下来, HN在用户数据库中检索SUPI, 以获取用户密钥k^*和 ${\mathit{SQN}_H}$ . 此部分已在图4中用红色方框标出.

(2) 身份检验变量

在此模式下, UE侧身份检验变量的生成不再依赖GUTI, 而是基于带有时效特征的序列号 ${\mathit{SQN}_U}$ 和随机数r, 以及带有身份特征的密钥k, 即:

$ MAC = {f_1}(k, \langle {\mathit{SQN}_U}, r \rangle) ,$

而在鉴权过程中, UE通过加密的方式把r传输给HN, 以便生成对应的MAC变量. r被隐藏为a的公式如下:

$ a = {f_2}(k, {\rm{SUPI}}) \oplus r .$

而在HN侧, 它首先需要恢复出r, 可通过下式实现:

$ {r^*} = {\pi _3}(M) \oplus {f_2}({k^*}, {{\rm{SUPI}}^*}), $

其中, ${\pi _3}(M)$ 指的是上述的隐藏变量a. 进而, 身份检验变量被计算:

$ MA{C^*} = {f_1}({k^*}, \langle \mathit{SQN}_U^*, {r^*} \rangle) .$

通过此, HN可以正常的进行两个检验. 此部分已在图4中用蓝色方框标出.

5 形式化分析

在本节, 我们形式化地评估SM-AKA协议的功能性和安全性. 我们主要从形式建模、证明目标与策略、攻击模型的设定等方面展开介绍. 此外, 对于鉴权协议的属性规范, 我们也做了必要的描述.

5.1 形式化简介

形式化分析主要通过把协议用规范化语言描述, 然后通过逻辑定理推导, 检验其是否满足某一方面的要求. 这个过程主要包括协议的流程和属性描述、协议的推导验证2个部分.

流程属性建模主要是把鉴权实体的信息生成、通信交互、变量处理等描述规范化, 同时, 还包含对攻击模型能力的模拟. 形式化描述语言基于数学模型, 克服自然语言或者程序语言描述的不精确性. 实际上, 由于形式化系统层出不穷, 因而吻合系统自身特点而构造的语言也多种多样, 这使得推理工具之间的兼容性很差. 因而, 业界往往会选择利用一些通用性较强的描述语言. 协议验证是对格式化后的属性实施推理, 判断各项属性是否达到预期目标, 得出对协议性能评估的结论. 它基于鉴权中有序的变量生成、传递、转化以及销毁的过程, 通过把属性要求设定为推理终点, 施行一系列的逻辑引导, 检验属性能够被满足. 随着移动网络技术的快速发展, 形式化验证已经变得十分重要, 成为协议研究必不可少的一环.

形式化分析通过推导证明完成目标的验证, 主要是检查逻辑上的缺陷, 对协议的安全隐私特性展开评估. 而对于性能效率等属性, 形式化难以应对, 因而, SM-AKA的性能分析主要通过理论探讨完成. 形式化分析应用于5G鉴权, 最大的难点就是如何把协议的表达方法从自然语言转化为逻辑语言, 使其能够输入到证明工具, 进行数学推理. 事实上, 协议流程通常是复杂的, 表述方式通常是多样化的. 而逻辑语言具有高精准性的特点, 即使存在一点差异, 也会对协议的含义造成很大偏差. 因此, 准确无误地把自然语言形式转化为逻辑表达是很具挑战性的. 同时, 属性要求以文本形式给出, 没有具象化阐述, 如何按照其含义精准的抽取出具体指标, 把其转化为标准的逻辑形式也是一大难点. 由于形式化语言丰富多样, 且高度凝练抽象, 因而需要花费大量精力完成标准化建模. 此外, 协议的分析需要模拟数量庞大的攻击可能, 通过多重搜索算法推理证明, 以检验攻击是否存在. 这一过程对逻辑推导、攻击解析提出了很高的要求, 需要经过复杂的循环演算才能检验协议的属性是否被满足. 为了应对这些困难, 本文主要采用Spthy语言建模协议流程和属性, 采用Tamarin证明器进行自动化的推导验证. 在本文中, 多重搜索算法主要指的是: Tamarin首先考虑协议所有的可行运行情况, 建立完整的状态空间, 然后依据一定的搜索方式在空间中查找符合特定条件的状态, 以期发现可能存在的协议漏洞.

5.2 属性要求

3GPP在移动通信标准文档的R16版本中对5G鉴权做出了属性要求, 为我们的形式化分析设定了明确的检验方向. 其以文本形式给出, 我们在此介绍, 具体如下.

(1) 认证属性. 协议应通过双端实体(此处指UE和HN)的一系列通信活动完成双向认证, 确保正常用户能够顺利接入服务网, 且提供服务的是合法服务网; 同时, 相同的会话钥不应该被生成两次, 即要确保其唯一性, 防止废弃的变量被非法重用.

(2) 保密属性. 协议应保证参与认证的永久性变量不被泄露, 包括密钥k、私钥 $s{k_N}$ 、序列号( ${\mathit{SQN}_U}$ , ${\mathit{SQN}_H}$ )和永久身份标识符SUPI. 而临时产生的鉴权变量, 如GUTI、SUCI等, 可以明文传输. 一些临时变量的公开可能会使协议遭受攻击, 因而需要融入对完整认证流程的考虑.

(3) 隐私属性. 协议应具备很好的防攻击能力, 保证用户隐私安全, 如通信行为、通信习惯、地理位置等, 这些信息都应具有不可追踪性. 同时, 协议应满足无连接性, 即让攻击者无法区分多个隐式目标之间的关系, 如判断两次追踪的UE是否为同一个UE.

(4) 性能属性. 在确保基本的认证和安全属性不受影响下, 协议应尽量简洁, 提升认证效率. 同时, 协议应尽可能地使用更少的变量和更低的资源. 协议应具备较强的抗干扰性, 确保鉴权能够长久稳定.

5.3 形式化工具

在推理验证协议属性的过程中, 我们不可避免的需要用到一些自动证明机. 随着形式化的不断发展, 业界已经开发出了各具特色的工具, 主要包括: AVISPA、ProVerif、Maude-NPA、Scyther、Tamarin等.

AVISPA^[20]的初衷是为了克服复杂协议的描述和证明的难题. 它提供了面向对象的标准化语言, 并整合了4种经典的证明器, 不仅可以发现协议的脆弱点, 还能够验证具有无限会话特性的协议. ProVerif^[19]通过若干预定义的规则判定事件是否会发生, 从而实现对协议属性的验证. 它解决了状态爆炸的难题, 可以模拟协议无限次数的执行. Maude-NPA^[24]在2009年被提出, 支持多种运算: 加解密、交换律、结合律等, 并且具备无限会话模型, 不仅能够完成逆向的漏洞挖掘, 还能正向的验证协议的安全性. Scyther^[25]对于具有无限轮数的协议可以给出具体的终止, 并且能够同时分析多个协议. 它在脆弱性查找、实体功能实现以及功能性证明发挥着重要作用. Tamarin^[17]利用Scyther的逆向搜索算法, 提供两种操作机制: 全自动分析和交互分析模式. 它基于集写规则和逻辑引理描述协议流程, 可以分析复杂的信息流, 支持加解密、异或等多种代数运算, 不仅支持Dolev-Yao模型, 还支持强安全模型. 为了证明和分析SM-AKA协议, 我们选择使用Tamarin证明器^[17]. 它是最先进的协议验证工具, 已经被大量用于分析基于密钥的通信协议, 如TESLA协议、YubiKey协议等. 它支持状态化的协议, 可以实现很大程度的自动化, 能够建模等价属性, 这些是验证无连接性要求的必要特征. 同时, 它可以模拟多种攻击方式. Tamarin支持众多的加密方法和代数运算, 尤其是鉴权协议严重依赖的异或运算. 综合来看, Tamarin完美融合了完成5G鉴权分析所需的全部特性.

Tamarin基于Spthy语言建模, 完成协议流程的描述, 利用时序逻辑和消息耦合, 完成协议属性的描述. Spthy是一种程序语言, 可把协议以编程语言的形式表达, 适用于计算机的编译运行, 可以用于协议的标准化建模. 在Tamarin中, Spthy语言首先被用于协议的程序化表达, 将自然语言文本描述的协议转化为计算机可编译、计算的逻辑形式. 在使用Spthy语言表述协议后, Tamarin工具根据内置的搜索算法对协议属性进行证明. 因此, Tamarin主要借助Spthy语言的标准化建模完成协议的形式化分析, 基于Spthy的标准化建模是采用Tamarin对协议进行形式化分析的第1步. Tamarin主要定义了两类对象: 多重集写rule和属性lemma, 其分别服务于协议的流程规范和属性描述. 前者主要把多个阶段性事实组合在一起以模拟当前通信实体的状态, 通过事实的消耗与演变, 实现实体状态的转变; 而后者使用数学逻辑语言把特定的阶段性事实组合在一起, 以时间顺序和全局限制精确定义各项属性, 并通过搜索算法验证协议是否满足各方面的要求. 此外, Tamarin通过一些内置的函数实现加解密运算、异或运算等, 我们在建模过程中不需要显式的写出计算过程, 而是以一种黑盒的形式实现所需的运算. 同时, 对于变量的生成、时效性、新鲜性等, 它也通过一些内置符号给出了约束. 对于检测到的攻击, Tamarin以攻击流程图的形式给出, 明确刻画攻击的参与实体、实现方式、协议薄弱点等要素. Tamarin是基于网页的工具, 以客户端-服务器的模式运行. 在全自动模式下, 用户通过客户端将基于Spthy语言的协议脚本上传至服务端, 随后, 服务端解析Spthy脚本, 自动化的逐一证明脚本中定义的属性lemma, 并暂存结论. 在完成所有的属性证明后, 服务端将结果以攻击流程图的形式返回客户端, 同时给出形式化分析的总结. 如果Spthy脚本中属性全部得到验证, 则Tamarin仅返回分析结论, 而不返回任何流程图.

5.4 攻击模型

在评估鉴权协议之前, 我们首先对攻击者能力作出假设, 以便模拟可能发生的攻击.

SM-AKA协议包括3个通信实体: UE、SN和HN. 事实上, SN和HN之间维护着一个安全信道, 可以提供封闭可靠的信息传输, 因此在鉴权协议的研究中, 它们被归纳为一个实体. 进一步的, 我们可以假设SN和HN之间的通信不存在攻击, 即在其中传输的消息均可以顺利通过且不会发生任何安全问题. 而UE和HN之间通过无线网络基站通信, 在这种场景下, 信息暴露在空气中, 攻击者仅通过简单的监听操作就可以接触到完整的信息内容, 因此这种通信被认为是不可靠传输. 在设计协议的过程中, 我们即要实现通信实体间的信息交互, 又要考虑到传输消息的加密性. 因此, 对于SM-AKA这样一个新协议来说, UE和HN之间的安全性研究至为重要. 我们主要对此展开形式化分析.

结合上述, 我们在UE和HN之间引入一个标准的Dolev-Yao攻击模型^[26]. 具体来说, 我们假设攻击者知悉SM-AKA协议的完整流程, 可以建立鉴权会话. 在DY模型中, 攻击者控制着整个通信网络, 可以窃听、拦截、伪造、注入、延迟和删除通信实体间被交换的消息, 同时可以进行公开的运算, 如异或、哈希等. 另外, 在现实中, 攻击者很难获取到存储在终端的用户信息. 因而, 我们假设攻击者只能接触到空口消息, 而无法知晓SUPI、用户密钥等存储在实体中的信息. 对于序列号、随机数等鉴权信息, 由于其数位比较大, 因而攻击者无法通过盲猜知晓其具体数值. 除了对已有的通信设施发挥作用, 攻击者还可以伪造基站, 因此, 攻击者可以重放捕获的消息, 实施一些重放攻击等. 同时, 攻击者也可以创造虚拟用户, 故攻击者可以对服务网发起非法鉴权会话等.

5.5 SM-AKA协议的形式建模

我们使用两种类型的规则描述SM-AKA的流程, 即注册rule和通信rule. 协议的属性要求通过两种类型的引理来实现, 即功能lemma和安全lemma, 其中, 前者对应于认证属性, 后者对应于保密和隐私属性, 而性能属性主要通过理论分析进行验证. 此外, 攻击模型的能力也通过多集重写规则表达, 即攻击rule. 而攻击尝试则通过引理实现, 即攻击lemma. 下面我们结合相应的例子详细说明每个对象的具体作用.

(1)流程定义

流程的形式化主要由两类规则完成. 注册rule主要用于生成实体终端, 并赋予其相应的基础身份认证信息. 涉及的实体有两个, 即UE和HN, 它们分别对应一个注册rule. 我们在此以UE的rule为例, 具体实现如下:

rule init_UE:

　　[Fr(~guti),Fr(~k),Fr(~sqn)]

　　　　 --[Register(~guti)]->

　　[!State_0_UE(~guti, ~k,~sqn)]

其中, Register(~)为活动事实, 是该rule的标签. 该规则首先初始化UE, 给其配备在第4.1节中规定的各项基本信息(紫色部分), 然后通过Register(~)触发, 获得初始事实(蓝色部分). 该事实是鉴权的起始状态, 在后续的认证步骤中被转化为代表下一阶段状态的事实. 上述创建了一个合法的UE, 这是协议建模的第1步. 实际上, 该rule还包含一些Tamarin的辅助证明项, 但为聚焦于协议流程, 同时便于理解, 我们仅描述其主干部分, 本文后续展示的rule也是如此.

通信rule是流程建模的主体部分, 主要实现信息的接收、处理和发送功能. 通信规则通常包含一些加解密、异或等操作, 在Tamarin中, 这些运算主要通过一些内置的函数来实现. 我们以第4.2节定义的通信流程为例:

rule ue_to_hn_GUTI:

　 let 　　　　　　　　　　　　　　　　　　　　　[!State_0_UE(~guti,~k,~sqn),

　　 P = ~guti 　　　　　　　　　　　　　　　　　　 　Sqn_UE(-guti,SqnUE,~sqn,count),

　　 a = f₂(~k,~supi,~a_n ~b_n,y_n)　　　　　　　　　　　　 Fr(~r)]

　　 MAC= f₁(~guti,r) XOR~sqn 　　　　　 in 　　　　　　　 -- [UE_Send_HN(~guti)]->

　　 M= <P, MAC,a> 　　　　　　　　　　　　　　　　[State_1_UE(~guti,SqnJ,~k,~sqn, ~r_n, v-guti),

　　 SqnJ = SqnUE+'l'　　　　　　　　　　　　　　　　 Sqn_UE(~guti,SqnJ,~sqn,count+'1'),

　　 v-guti ='0' 　　　　　　　　　　　　　　　　　　　 Out(M)]

其中, XOR为异或运算, f₁, f₂为哈希函数, Out(x)表示发出信息x. 该规则首先经过一系列的信息集成和演变, 生成鉴权所需的变量 $M = (P, MAC, a)$ , 然后基于UE的初始状态(紫色部分), 通过一个UE_Send_HN(~)活动事实触发流程, 完成3个子活动: 发出消息, 由Out(S)函数完成; 更新UE状态, 由State_0_UE转化为State_1_UE; 更新序列号和V-GUTI的值(蓝色部分). 至此, 协议的第一阶段描述完毕, 而剩余部分也将通过这种事实转换和变量更新的方式完成.

通过上述, 我们用形式语言刻画了认证流程, 完成了协议的规则建模.

(2) 属性定义

我们将形式化的描述SM-AKA的认证属性、保密和隐私属性, 其分别通过功能性lemma、安全性lemma实现.

功能性lemma通过给出一系列的可执行路径把既定的规则按照不同方式组合在一起, 检验协议是否满足功能要求. 执行路径都是基于协议的逻辑运行顺序而产生, 而一个引理往往仅表达局部的逻辑顺序. 下面, 我们给出一个UE的功能性lemma:

lemma executability_ue_to_hn:

　　　　 "(All guti #i.UE_Send_HN(guti)@i==>

　　　　　　　　 (Ex #j. Register(guti)@j&j<i)"

该lemma表示, 如果有活动UE_Send_HN(guti)在时间点i发生, 则在此之前必有Register(guti)活动发生. 这是一条针对第2节所述流程的执行路径, 即先init_UE rule, 然后ue_to_hn_GUTI rule. 这种执行顺序表示在鉴权过程中, 如果UE发出一条认证消息, 则这个UE必定经过注册阶段并被赋予基础身份变量. 这是协议正常实现双向鉴权功能的一环, 即要求终端必须是合法生成的, 且必须在参与鉴权之前完成这一过程.

安全性lemma主要是在正常轨迹的基础上, 把可能存在的情况考虑进来, 以探索协议的运行状况. 为了模拟一些情景, lemma做了特定的假设. 衡量这些假设的破坏性可以评估协议的安全属性, 以密钥k的保护为例:

lemma ue_to_hn_attack:

　"All guti #i.UE_Send_HN(guti)@i ==>

　　　　(Ex #j.Register(guti)@j&j<i)

　　　　| (Ex X k #r.Rev(X, k)@r&Honest(X)@i)"

上式除包含一个正常lemma之外(紫色部分), 还包含一个信息泄露假设, 即密钥发生泄露(蓝色部分). 该引理表明, 如果在时间点i, 活动UE_Send_HN(guti)被触发, 除了可以推断出一个合法UE被注册(紫色部分), 还可能是由于一个攻击者X在时间点i获取k并据此伪造一个非法UE. 而这个伪造的UE由于具备合法的密钥, 可以正常的参与认证, 这揭示密钥的泄露会给认证体系带来巨大的安全隐患.

我们还围绕着这两种类型定义其他的安全性lemma, 通过这些lemma来准确刻画协议属性, 为后续推理提供结束节点.

(3) 攻击能力定义

本节将攻击者的能力形式化, 以便将攻击行为整合到搜索证明中, 这通过攻击规则和攻击引理实现.

攻击rule客观陈述攻击者的能力, 表示其可以接触到什么层次的信息. 它也给出每个基本信息的暴露标准, 规范哪些变量是公开的, 哪些是私密的. 这里我们以UE的密钥k为例:

rule reveal_UE_k:

　　[!State_0_UE(~guti,~k,~sqn)]

　　　　 --[Rev(~guti, <' k', ~k>)]->

　　[Out(~k)]

其中, Out(x)表示发出消息x. Out函数发出的所有消息都被广播到空气中, 攻击者有能力捕捉到它. 该rule表示在UE的初始状态(紫色部分), 如果有Rev(x)活动, 密钥k将被发出(蓝色部分). 这意味着k将从私有变为公开, 将被攻击者捕获. 通常我们会将该rule视为一种假设, 以探索密钥泄漏时协议的安全状态. 该rule规定了攻击者获取密钥k的能力, 这种情况在现实中是很难实现的, 但我们希望能够模拟这种情形以查找潜在的脆弱点. 另外, 我们也形式化的定义其他的能力, 用于模拟可能的攻击方式.

攻击lemma基于预定义的rule发起攻击活动, 我们通过评估其可行性, 界定协议的安全性能, 以下式为例:

lemma reveal_sqn:

　　"(All X K sqn #i.Rev(X, k)@i & Honest(X)@i)==>

　　　　 (Ex#j. Rev(X, sqn)@j&j>i)"

上式表明, 当密钥k在时间点i被泄露, 之后可能存在一个时间点j使得序列号 ${\mathit{SQN}_U}$ 也被泄漏. 这描述一个在已知k的情况下, 攻击者试图获取 ${\mathit{SQN}_U}$ 的活动. 值得注意的是, 这里引用一个针对序列号的攻击rule(紫色部分), 其并没有在本文列出, 但其形式与reveal_UE_k rule类似. 证明器将通过判断该lemma是否为真来给出分析结论. 如果该lemma成立, 我们可以断定序列号的安全性高度依赖于密钥. 一旦密钥被公开, 序列号也将不会是私密的.

5.6 证明目标与证明策略

通过建模, 我们已经形式化的描述协议的流程、属性和攻击者的能力. 在本节, 我们将使用Tamarin证明器验证其属性定理. 我们主要介绍证明过程、证明目标以及采取的策略.

基于Tamarin的形式化分析主要分为协议建模、协议分析和得出结论3个阶段. 在协议建模阶段, 我们利用Spthy语言对协议流程程序化建模, 得到分析脚本, 以计算机能够理解的形式表述协议. 在第2阶段, Tamarin基于Spthy脚本展开自动化推理, 利用自身的搜索算法查找协议潜在的漏洞并构造攻击方式, Tamarin的推理界面如图5所示. 在第3阶段, Tamarin给出结论, 输出结果. 如果协议存在漏洞, 则结果包含一系列的攻击流程图, 反之, 则直接给出“属性已完成验证”的结论.

我们在第5.2节罗列了3GPP规定的5G鉴权要求, 目标就是评估SM-AKA协议能否满足这些属性. 就建模过程而言, 上述的rule主要提供一些陈述实体状态的事实, 是lemma的骨干组成部分, 并为其服务. 而lemma是协议属性的载体, 是真正需要被证明的部分. 按照既定的变量、时间点和活动, 我们可以对其逻辑推导, 以达到对属性评估的目的. 因此, Tamarin的证明目标就是以预定义的lemma为基础, 生成一个容纳所有可能状态的集合, 然后通过内置算法在状态空间搜索, 通过协议的模拟运行查找潜在的脆弱点. 同时, 它也会使用攻击模型对协议实施试探性攻击, 并通过攻击的结果来得出结论. 可以发现, Tamarin主要通过判断lemma描述的内容是否成立发挥作用, 因为lemma已经对属性要求做出了精确的定义. 我们的形式化目标就是通过推演标准化描述以间接完成属性验证.

在SM-AKA的建模中, 我们构建了27个rule, 其中18个用于协议流程, 9个用于攻击模型能力的描述. 我们构建了15个引理, 其中用于功能和安全属性的个数分别是6和9. 考虑到庞大的状态空间, 我们没有采用Tamarin的人机交互模式, 而是使用全自动模式开展对lemma的证明. 全自动模式的优势是操作简单, 不需要大量的人力, 这很适用于本协议的分析. 而产生的缺点就是状态空间不受人为引导, 会生成一些不切实际的协议状态, 从而带来不必要的逻辑推理. 受到之前工作^{[7, 8]}的启发, 我们添加了一些辅助lemma来粗略地指明推导方向, 限制Tamarin假定的协议状态, 以缩小搜索空间. 事实上, 一次性验证所有属性所需计算资源较大, 受限于实验条件, 我们把全部属性划分为若干份, 采取分阶段证明的策略. 我们在一台配有AMD 3900X的12线程处理器和16 GB内存的电脑上展开实验, 经过累计约12 h的自动分析, 完成了SM-AKA的形式化评估.

5.7 形式化分析结论

经过Spthy语言建模和Tamarin工具证明, 我们完成了SM-AKA协议的形式化分析. 图6展示了部分属性的分析结果, 可以发现, 图中lemma的证明结果均为“verified”, 即检验通过.

综合全部属性的形式化证明结果, 我们有以下结论.

(1) 功能属性得到验证, 主要包括鉴权功能、子模式切换、逻辑衔接、抗外部干扰等. 我们严格按照既定协议建模, 设定认证轨迹, 并依据属性引理推理, 成功证明了协议可以有序执行, 实现UE和HN之间的双向鉴权. 此外, 依据V-GUTI在SUPI和GUTI模式之间的切换也得到了验证; 在大量多次的模拟运行之后, 协议依然具备很好的鉴权性能.

(2)安全属性得到验证, 主要包括空口参数的不可破译、用户基础信息的私密、认证变量的防重放、伪基站伪UE的鉴别等. 在Dolev-Yao攻击模型的设定下, Tamarin没有给出任一攻击引理的成立条件, 而所定义的安全性引理也得到证明. 这说明SM-AKA具备很好的安全性能, 可以抵御所有已知的攻击方式.

(3) 我们通过开启两个形式化的UE认证会话, 让两个隐式UE分别依据功能性引理所描述的轨迹实施鉴权, 然后尝试用Tamarin确定正常状态和遭受攻击状态时两个UE的关系, 最终一无所获, 这证明SM-AKA可以满足协议的无连接性.

5.8 讨　论

本节我们从流程设计、变量优化等方面对SM-AKA协议的安全性和性能展开讨论.

(1)安全性

首先, SM-AKA协议通过SUPI和GUTI两种模式的交替运行实现了双向鉴权. 一方面, HN通过解析来自UE的认证变量, 实施两种检验, 完成用户身份的核查. 另一方面, UE通过处理来自HN的响应, 也实现对服务网是否合法的验证. 同时, 我们借鉴5G-AKA协议的一些优点, 把序列号融入变量维持其新鲜性, 可以确保鉴权消息仅一次有效. 这提升认证的时效性, 可以很好地抵御重放攻击.

其次, 鉴于5G-AKA协议可能遭受信息破译攻击^[7], 我们提出改进措施. 我们在第2节已经说明, 这种攻击是由于序列号的不完备加密秘方式造成的. 事实上, 在5G-AKA的重同步响应阶段, UE会发送消息: $CONC = {\mathit{SQN}_U} \oplus f_5^*(k, {r_m})$ . 而对于同一个终端(即秘钥k保持不变), 当攻击者通过伪基站向UE重演带有 ${r_m}$ 的消息S^*= $ \langle CON{C^*}, {\mathit{MAC}^*}, {r_m} \rangle $ 时, UE每次反馈到空口的消息都会包含 $f_5^*(k, {r_m})$ , 即 ${\mathit{CONC}_x} = {\mathit{SQN}_x} \oplus f_5^*(k, {r_m})$ . 如果捕捉两次CONC消息, 并经过一个与或操作, 就会得到 $CONC \oplus CON{C_x} = {\mathit{SQN}_U} \oplus {\mathit{SQN}_x}$ . 对于攻击者而言, 其中仅有 ${\mathit{SQN}_U}$ 和 ${\mathit{SQN}_x}$ 未知, 但它们有已知关系: ${\mathit{SQN}_x} = {\mathit{SQN}_U} + x$ , 且x已知. 基于此, 攻击者可以逐位破译用户的序列号 ${\mathit{SQN}_U}$ , 从而非法获取隐私. 而SM-AKA去掉重同步响应, 取而代之的是, 它采用两个子模式交替运行的机制. 当需要重同步响应时, SM-AKA会通过SUPI子模式把UE和HN的各项参数重新置于同步, 以完成协议的修复. 鉴于重同步响应导致序列号破译漏洞^[11], 在设计协议的过程中, 我们特别注重基础变量的空口传输. 在加密算法的设计上, 我们把多个变量聚合在一起, 同时融入随机数, 通过哈希算法来把它们集成在一起, 以提升消息的不可再造性. 我们也通过理论计算证明SM-AKA采用的加密方式无法被破译, 攻击者难以有所收获. 因此, 尽管5G-AKA重同步响应被剔除, 但SM-AKA通过增加子模式机制弥补其功能, 还通过优化加密方式阻断其引发的攻击.

此外针对5G-AKA协议的连接性攻击^[9], SM-AKA可以完全阻止它. 该攻击实现是因为S= $\langle CONC, MACS \rangle$ 和“Failure”两种失败消息, 由于它们的长度和组成不同, 故易于区分. 事实上, 5G-AKA协议在认证失败后, 会发送这两种消息的一种. 基于这个漏洞, 攻击者首先会监听一次目标UE₀的成功鉴权, 并捕获HN侧的消息 ${S^*}= \langle CON{C^*}, MA{C^*}, {r_m} \rangle$ . 然后在一个新的鉴权会话中, 攻击者会把 ${S^*}$ 作为鉴权变量发给一个未知UE_x. 由于该消息已经用过一次, 新鲜度检验必不会通过, 因而最终的鉴权不会成功, 故UE_x会返回错误消息. 而攻击者可以推断出消息的类型t, 如果t是身份失败消息(“Failure”), 则有UE₀≠UE_x, 如果t是重同步消息( $S = \langle CONC, MACS \rangle $ ), 则有UE₀=UE_x. 据此, 攻击者可以获知UE₀和UE_x的关系, 这打破了5G-AKA协议的无连接性, 而SM-AKA可以避免5G-AKA中的这种攻击. 不论鉴权成功与否, SM-AKA均有且只有M和S两种鉴权消息, 不存在因鉴权结果不同而产生不同消息的情况. 攻击者虽然可以继续从空口中捕捉到鉴权消息, 但已无法区分出它们的不同. 这打破了上述连接性攻击的基础, 加强了对子模式切换的保护, 使攻击无法成功. 相较于5G-AKA, SM-AKA通过优化空口消息的设计避免连接性攻击, 大大提升了鉴权的安全性.

类似地, 我们已在前文描述, AKA⁺协议也存在连接性攻击. AKA⁺协议之所以会遭受连接性攻击, 主要原因是两个子协议的鉴权流程和空口消息结构不同, 易被攻击者区分和利用, 导致用户隐私泄露. 而SM-AKA协议提升了对无连接性的保护, 能够完美防范这种攻击. SM-AKA协议和AKA⁺具有相似的鉴权模式, 即通过两个子协议交互的形式完成认证. 但SM-AKA重新设计了作用机制, 使两个子协议的流程(均为由UE向HE发送鉴权消息, 由HN向UE返回鉴权响应, 详见第4节)和变量结构(均为 $S = ({f_4}(SQN_U^* + 1, {k^*}) \oplus {r^*}, b)$ 和 $M = (P, MAC, a)$ , 详见第4节)保持一致, 避免被攻击者区分, 从而阻断上述的连接性攻击. 相较于AKA⁺, SM-AKA采用更完备的流程和消息发挥作用, 具有更好的安全性能.

(2) 性能

为了进一步探索协议的性能, 我们将SM-AKA与原始5G认证协议和最新变体进行比较. 考虑到延迟和计算复杂度, 我们选择4个对协议性能影响较大的指标. 首先, 通信次数(TC)是一个不可忽视的因素, 因为变量的空中传输需要经过发送、传输和接收的过程, 需要很长时间. 然后是非对称加密算法(AE)和哈希散列算法(HA). 文献[13]已经证明, 在计算复杂度方面, 这两种算法远远超过其他算法. 最后是随机数的数量(RN), 它的生成会消耗大量计算资源. 上述指标越小对协议性能越有利, 我们在表1中展示了比较结果.

综合来看, 无论是GUTI还是SUPI子协议, SM-AKA在TC (分别为2, 2)和RN (分别为1, 1)两个指标上都具有绝对优势. 而指标AE和HA的优势不是直观的, 我们首先对比AE和HA的性能. 为了探索计算消耗, Patonico等人^[27]使用带有ARM Cortex-M3 32 MHz时钟, 并同时配备512 KB闪存和32 KB内存的Zolertia REmote传感器作为微控制器进行实验测试. 结果显示, 非对称加解密算法AE耗时T_AE=342.39 ms, 而作为对比的哈希运算(HA)耗时T_HA=0.03 ms. 它们之间的量级差异是巨大的, 一个AE的时间消耗大概是HA的10⁴倍. 显然, 在HA差异不明显的情况下, 使用AE算法会使协议性能更差. 基于这个前提, 我们可以在必要时增加HA, 但要减少AE.

表中除了AKA⁺外, 其余协议均用到了AE算法. 对于SM-AKA, GUTI子协议没有用到AE, 因而其相较于这些协议具备性能优势. 而尽管SUPI子协议用到了AE算法, 但两个子协议交替运行的机制缓解了AE算法给SM-AKA性能带来的影响, 这是因为该机制降低了AE的平均使用次数. SM-AKA的两个子协议中, SUPI模式基于永久身份变量, 并使用AE, 运行效率相对较低. 而GUTI模式选用临时身份变量, 以增加几个HA为代价取缔AE, 大大提高了认证效率. 两种模式的选用取决于V-GUTI的值, 在执行过程中, 两种模式认证成功后都会把其置为True, 以为下一次选择GUTI模式做铺垫. 只有在协议运行出现差错时, V-GUTI的值才会为False. 这种情况下, 下一次的认证会选择SUPI模式. 因此, 在协议运行不出现差错时, GUTI模式总是会被选用, 而这在实际中是大多数情况. 因而, 综合GUTI和SUPI两个子协议来看, 每次鉴权AE的平均运行次数介于0–1之间, 且不会接近于1. 因此, 在表中HA相差不明显的事实下, 我们可以断定SM-AKA协议的HA和AE指标总体优于AKA⁺之外的协议.

由于AKA⁺协议和SM-AKA具有相似的运行机制, 我们可以从子协议的角度评估二者的性能. 由表中数据可知, 对于GUTI子协议, SM-AKA和AKA⁺的AE和RN相同, 而SM-AKA的TC和HA数量要较AKA⁺少. 对于SUPI子协议, 二者的AE、HA和RN相同, 而SM-AKA TC的数量要较AKA⁺少. 因而, 无论是GUTI还是SUPI, SM-AKA协议的性能都要优于AKA⁺. 综合来看, 在4个主要关系协议性能的指标上, SM-AKA从整体上取得了提升, 相较于5G-AKA等主流协议, 具有更高的认证效率.

6 结　论

在这篇文章中, 我们针对当前5G-AKA及其变种的缺陷, 提出一个新颖的鉴权协议: SM-AKA. 它利用SUPI和GUTI两个子模式的交替有序运行实现协议的高效认证, 大大降低认证延迟. 同时, 两种模式下信息变量的组成也变得一致, 以规避连接性攻击. 通过形式化评估, 我们证明该协议不仅可以取得UE和HN之间的双向认证, 还可以抵御当前的已知攻击, 具有优秀的功能和安全特性. 我们还通过对SM-AKA的理论分析展示其设计的合理性.

在未来, 我们将改进目前的形式化验证工具, 致力于提升其可视化效果, 以避免黑盒式的自动证明. 同时, 我们也将在UE、SN和HN这3个实体, 甚至5G网元的基础上展开协议分析, 以期发现并修复更为深层的脆弱点.