一个切换认证的5G鉴权协议及其形式化分析.pdf

一个切换认证的 5G 鉴权协议及其形式化分析*刘逸冰,周刚(中国人民解放军信息工程大学数据与目标工程学院,河南郑州450002)通信作者:刘逸冰,E-mail:摘要:随着移动通信的发展,迎来了第 5 代移动通信技术(5G).5G 认证与密钥协商(5Gauthenticationandkeyagreement,5G-AKA)协议的提出主要是为了实现用户和服务网络的双向鉴权.然而,最近的研究认为其可能会遭受信息破译和消息重放攻击.同时,发现当前 5G-AKA 的一些变种不能满足协议的无连接性.针对上述缺陷,提出一个改进方案:SM-AKA.SM-AKA 由两个并行子协议组成,通过巧妙的模式切换使更加轻量的子协议(GUTI 子模块)被频繁采用,而另一个子协议(SUPI 子模块)则主要用于异常发生时的鉴权.依据这种机制,它不仅实现用户和归属网之间的高效认证,还能提升鉴权的稳定性.此外,变量的新鲜性也得到有效维持,可以防止消息的重放,而严格的加解密方式进一步提升协议的安全性.最后,对 SM-AKA 展开完整的评估,通过形式建模、攻击假定和Tamarin 推导,证明该方案可以达到鉴权和隐私目标,而理论分析部分也论证了协议性能上的优势.关键词:5G 鉴权;认证协议;形式化分析;移动网络中图法分类号:TP311中文引用格式:刘逸冰,周刚.一个切换认证的5G鉴权协议及其形式化分析.软件学报,2023,34(8):37083725.http:/ Authentication Protocol Based on Sub-mode Switching Operation and Its Formal AnalysisLIUYi-Bing,ZHOUGang(SchoolofDataandTargetEngineering,PLAInformationEngineeringUniversity,Zhengzhou450002,China)Abstract:With the development of the Internet,the 5th generation(5G)of mobile communication technology emerges.The 5Gauthentication and key agreement(5G-AKA)protocol is proposed mainly to achieve two-way authentication between users and servicenetworks.However,recent research suggests that the protocol may be subject to information deciphering and message replay attacks.Atthesametime,itisfoundthatsomevariantsofthecurrent5G-AKAcannotsatisfytheprotocolsunlinkability.Therefore,inresponsetothese shortcomings,this study proposes an improvement plan called SM-AKA.SM-AKA is composed of two parallel sub-protocols in anovelway.Inaddition,throughtheflexiblemodeswitching,lightweightsub-protocols(GUTIsubmodule)arefrequentlyadopted,andtheother sub-protocol(SUPI submodule)is used to deal with abnormalities caused by authentication.Therefore,this mechanism not onlyrealizestheefficientauthenticationbetweenusersandnetworksbutalsoimprovesthestabilityoftheprotocol.Furthermore,thefreshnessofvariableshasbeeneffectivelymaintainedtopreventthereplayofmessages,andstrictencryptionanddecryptionmethodshavefurtherstrengthened the security of the protocol.Finally,the study carries out a complete evaluation of SM-AKA.Through formal modeling,attackassumptions,andTamarinderivation,itisprovedthattheplancanachievetheauthenticationandprivacygoals,andthetheoreticalanalysishasdemonstratedtheperformanceadvantageoftheprotocol.Key words:5Gauthentication;authenticationprotocol;formalanalysis;mobilenetwork*本文由“形式化方法与应用”专题特约编辑陈立前副教授、孙猛教授推荐.收稿时间:2021-09-05;修改时间:2021-10-14;采用时间:2022-01-10;jos 在线出版时间:2022-03-24CNKI 网络首发时间:2023-02-23软件学报ISSN1000-9825,CODENRUXUEWE-mail:Journal of Software,2023,34(8):37083725doi:10.13328/ki.jos.006617http:/中国科学院软件研究所版权所有.Tel:[phone] 引言随着通信技术的发展,移动设备已经广泛普及,比如手机、智能手表等.据统计,目前已有 50 亿人都是移动通信用户,这是一个庞大的群体1.他们通过多种多样的设备来享受移动网络提供的丰富服务,并被国际移动电信组织(3rdgenerationpartnershipprojec,3GPP)制定的安全机制所保护.在漫长的发展历程中,移动通信技术已经走过了最初的 2G、惊喜的 3G 和成熟的 4G 时代,今天正处于 5G 时代,即第 5 代移动网络.每一代移动网络的发展都离不开安全这一主题,都会形成一系列的安全机制,而其中一个极其重要的机制是用户设备(userequipment,UE)和归属网(homenetwork,HN)之间的双向认证.事实上,3G 已经存在较为稳定的认证方法,即认证与密钥协商机制(authenticationandkeyagreement,AKA).到了 4G,AKA 方法得到进一步发展,演变为更加成熟和安全的 EPS-AKA 和 EAP-AKA 协议.现如今,经 3GPP 在前人基础上长达数年的研究,5G 的鉴权与认证协议最终形成2.该协议的目标是在包含通用用户身份模块(universalsubscriberidentitymodule,USIM)的设备和归属网络之间提供一个双向鉴权机制,以使双方在信息读取、网络接入等权限问题上达成一致.在确保隐私安全的情况下,用户可以正常的享用移动通信服务.为了实现这一目标,AKA 协议会在认证成功之后,赋予 UE和 HN 一个共享会话密钥以保障后续双方的信息通信.经过 3GPP 组织反复的商榷,最终确立的 5G 鉴权协议有两种,即 5G-AKA 和 EPS-AKA.事实上,它们的设计目标是一致的,而其中的差异也只关乎法律因素3.因此,就本文聚焦的隐私安全来说,它们没有不同,在此,本文主要选取 5G-AKA 协议展开研究和讨论.近些年,针对认证协议的研究取得了巨大的进展,业界已经发现了一些关于 5G-AKA 协议的脆弱性,如:不同类型的失败消息的可区分性可能会使鉴权结果泄露、序列号的不完善加密可能会导致其被破解以及 SUPI 的非对称加密可能会带来较高计算复杂度.同时,协议分析逐渐大量采用形式化分析方法46.一些研究者通过形式化手段分析 5G-AKA,发现了协议中的一些缺陷,如 SUPI 在 UE 侧的不可靠存储、会话密钥的弱私密性等7,8.针对当前 5G 认证协议存在的缺陷,一些安全研究人员提出了改进方案.Koutsos 等人9提出了具有两阶段子协议的AKA+方案,其最大的特色是设计了两个子协议相互补充的机制,其总体运行模式如图 1.它采用新颖的交替运行实现了认证协议所有的功能,两个子协议互为补充,分别应对不同的情况,是一个较为优秀的改进方案.AKA+协议会依据 V-GUTI 的值来决定选用哪个子模块,而鉴权的结果,即成功或者失败,又会反过来影响 V-GUTI 的值.作者还证明了该协议不仅可以很好地抵抗现有攻击,还取得了较高的平均认证效率.Yes失败成功成功失败GUTI 模块被选用SUPI 模块被选用No 更新:不更新:下一次鉴权开启鉴权V-GUTI=True?V-GUTI=TrueV-GUTI=False图1AKA+运行机制通过分析 AKA+方案独特的工作模式,如图 1,我们发现了其存在一个脆弱点.在该协议中,用户永久身份标识(subscriptionpermanentidentifier,SUPI)和全局唯一临时标识(globallyuniquetemporaryidentity,GUTI)子协议传输的消息结构和组成不同,因而,我们在实际观测中可以识别认证网正在运行何种子协议.据此,我们设计了一种连接性攻击,总体过程如图 2.具体来说,当需要判断一个隐式 UEx与目标 UE0的关系时,攻击者首先监测 UEx刘逸冰等:一个切换认证的 5G 鉴权协议及其形式化分析3709和 UE0一次成功的 AKA+认证.根据协议规定,UE0和 UEx的 GUTI 标识符(V-GUTI)都会被设置为 True.接下来,攻击者让 UE0再进行一次 AKA+认证,并通过消息截断的方式使其认证失败,此时 UE0的 GUTI 会被消耗,即 V-GUTI变为 False.最后,UE0和 UEx再进行一次 AKA+认证.通过观察传输的消息类型,攻击者能够判断是哪个子协议在运行.作为结果,有两种情况.如果 UEx运行的是 SUPI 子协议,则有 UE0=UEx,即未知的 UEx即是目标 UE0.如果 UEx运行的是 GUTI 子协议,则有 UE0UEx,即未知的 UEx不是目标 UE0.UE0UEx正常运行 AKA+正常运行 AKA+正常运行 AKA+正常运行 AKA+使 AKA+鉴权失败如果 GUTI 模块被采用,则有:UExUE0 SUPI 模块被采用如果 SUPI 模块被采用,则有:UEx=UE0V-GUTI=TrueV-GUTI=False图2针对 AKA+协议的连接性攻击因此,攻击者可以推断出 UEx和目标 UE0之间的关系,这违背了协议的无连接性要求,即攻击者通过对协议的攻击,能够探知多个隐式目标之间的关系,如判断两次跟踪的未知 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 鉴权协议上投入了大量的精力,取得了可观的进展.在此,我们主要从脆3710软件学报2023 年第 34 卷第 8 期弱性挖掘、协议改进和形式化分析 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结合 AVISPA20和 SPAN21对其提出的 SEL-AKA 协议展开安全属性评估,并得到一些很有价值的结论.Braeken等人13使用 RUBIN 逻辑22检验其提出的协议,验证了协议拥有的优良特性.Koutsos 等人9使用 BANA-COMON 逻辑23评估其提出的 AKA+协议,有力地证明了协议能够满足其声明的若干要求.在本文,我们针对 5G-AKA 和 AKA+协议的缺陷,提出改进方案.相较于现有研究,该方案采取一种交替运行的模式,不仅可以抵御已知的攻击,还能够大大提高鉴权的平均效率.同时,改进方案减少通信步骤,降低资源消耗.而通过形式化验证,我们证明了该方案可以满足协议的包括无连接性在内的诸多要求,具有很强的安全特性.刘逸冰等:一个切换认证的 5G 鉴权协议及其形式化分析3711此外,由于认证过程中使用较多的异或操作,为了更真实的建模 SM-AKA 协议,我们选用功能强大且支持异或操作的 Tamarin 形式化工具.3 预知识本节将阐述我们聚焦的 5G-AKA 协议,同时介绍参与认证的实体.3.1 实体描述认证协议主要涉及 3 个实体:UE、服务网络(servicenetwork,SN)和归属网络(homenetwork,HN),其中:SQNUpkN(1)UE 是指获取通信服务的载体,例如移动电话.每个 UE 都包含一张 USIM 卡,它存储一组用于鉴权的变量:用户永久身份标识(SUPI)、全局唯一临时身份标识(GUTI)、GUTI 标识符(V-GUTI)、用户密钥 k、UE 侧的序列号和公钥.(2)SN 控制着基站,用于给用户提供移动网络接口,鉴权消息可以通过 UE 和 SN 之间的无线频道连接实现空口传输.SQNH(3)HN 是指用户注册网络,存储着用户的身份信息.它通过维护一个数据库参与鉴权,存储的变量包括:SUPI*、GUTI*、V-GUTI*、k*、HN 侧的序列号和私钥 skN.在鉴权协议中,通常 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 和公钥 pkN,把 SUPI 转化为隐藏身份标识符 SUCI:SUCI=SUPIrpkN.而 SUCI 是临时的,只能被使用一次,因而可以确保身份信息不被公开.接下来,SUCI 被作为身份变量发送给 HN.(2)HN 生成并转发检验消息给 UESQNHSQNHSQNHMACCONCHN 一旦收到 UE 的身份信息,会开启一个鉴权会话.对于 SUCI 消息,HN 会结合私钥使用非对称解密算法解析 SUCI.依据获得的 SUPI,HN 会在用户注册数据库中检索出和 k.然后,两个哈希函数利用一个新生成的随机数 rm把和 k*融入检验变量和中,即:MAC=f1(k,SQNH,rm),CONC=SQNH f5(k,rm),S其中,表示异或操作,f1和 f5为二元哈希函数.最后 HN 把完整的用于查验的消息发送给 UE,其中:S=CONC,MAC,rm.(3)UE 执行检验并把结果反馈给 HNSSQNH=CONC f5(k,rm)f1(k,SQNH,rm)MAC=MACSQNU SQNHUE 收到消息后,首先解析出 HN 的序列号,然后计算出 UE 侧的身份变量 MAC=,最后进行身份和新鲜度的检验,即,.其中,=表示等价判断符号.作为结果,有 3 种情况.X=f2(k,rm)SQNUSQNH如果=True 且=True,则鉴权成功,UE 会给 HN 反馈消息,并把其自身的序列号设置为.3712软件学报2023 年第 34 卷第 8 期如果=True 且=False,则新鲜度检验失败,此时,UE 首先生成变量 CONC 和 MACS,即:CONC=SQNU f5(k,rm),MACS=f1(k,SQNU,rm),S=CONC,MACS然后给 HN 返回重同步消息.对于其他情况,UE 直接给 HN 返回鉴权失败“Failure”消息.响应发出后,UE 侧完成认证流程并结束当前会话.(4)HN 侧进行重同步响应SQNUMACS当收到重同步响应消息时,HN 从消息中恢复出 UE 的序列号,并生成 HN 侧身份变量:SQNU=CONC f5(k,rm),MACS=f1(k,SQNU,rm).MACS=MACSSQNH=SQNU+1SQNHSQNH然后,检验是否成立.如果通过,则 HN 更新自身的序列号,即.这可以使的值回归到正常范围,避免因的意外增加(比如遭受攻击)而导致新鲜度检验永久性失败.如果不通过,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=f2(k,GUTI)r.紧接着,结合时敏信息 r 和 GUTI,用于身份检验的变量 MAC 被生成:MAC=f1(GUTI,r)SQNU.UE 在此模式下将采用 GUTI 作为其身份的标志 P,即 P=GUTI.从而,完整的认证变量可被获得并用 M 来表示:M=(P,MAC,a).SQNU最后,M 将被发送给 HN.发出后,序列号的值增加 1,同时 V-GUTI 被设置为 False 以防止 GUTI 被重放.(2)HN 向 UE 通信阶段SQNHHN 在接收到认证变量后,首先依据明文传输的 GUTI 在用户数据库中检索,以获得用户密钥 k*和序列号.同时,HN 侧的 V-GUTI 被更改 False,以表示 GUTI 不再可用.然后,HN 从 M 中恢复出被加密传输的随机数,即:r=3(M)f2(k,1(M).进一步,UE 侧的序列号会由于随机数的解析成功被重载:SQNU=f1(1(M),r)2(M).刘逸冰等:一个切换认证的 5G 鉴权协议及其形式化分析3713M=(P,MAC,a)输入 S:UEHN新鲜的随机数 rSQNU+1SQNU输入 M:UE 侧鉴权成功HN 侧鉴权成功SQNH=SQNU*+1V-GUTI=True:a=f2(k,GUTI)rMAC=f1(GUTI,r)SQNUP=GUTIV-GUTI=False:找到信息且V-GUTI=True:V-GUTI=False,继续鉴权否则转到SUPI子协议的步骤2r*=3(M)f2(k*,1(M)SQNU*=f1(k,1(M),r*)2(M)MAC*=f1(1(M),r*)SQNU*GUTI*=new GUTI#b=f3(r*,k*)GUTI*V-GUTI=TrueGUTI#=3(S)f3(r,k)S=(f4(SQNU*+1,k*)r*,b)S*=f4(SQNU,k)rV-GUTI=TrueGUTI=GUTI#如果(i)和(ii):检索 1(M):k*,SQNH,V-GUTI检验:(i)1(S)=S*如果(i):(i)2(M)=MAC*,(ii)SQNHSQNU*检验:图3GUTI 子协议具体流程接下来,HN 生成它的身份检验变量 MAC*:MAC=f1(1(M),r)SQNU.因此,鉴权协议规定的两个检验可以被实施,即:(i)MAC=2(M),(ii)SQNU SQNH.对于结果,如果检验(i)和(ii)均通过,则代表 HN 侧鉴权成功.此时,新的临时身份标识符 GUTI*被生成,并被加密为中间变量 b:b=f3(r,k)GUTI.SQNHSQNU+1并且,的值被更新为,V-GUTI 被重置为 True.最后,HN 进一步把认证变量补充完整,并形成 S:S=(f4(SQNU+1,k)r,b),S 被发送给 UE,以用于开展最后的确认阶段.3714软件学报2023 年第 34 卷第 8 期(3)UE 信息查验阶段这一阶段在 UE 侧完成,是鉴权的最后一步.首先,UE 根据 S 的组成以及自身的基础变量,重载出被密文传输的 GUTI#:GUTI#=3(S)f3(r,k).然后 UE 的确认变量 S*被计算:S=f4(SQNU,k)r.(i)S=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 模式的实现.UE 侧检验与 GUTI 的更新UEHN新鲜的随机数 rM=(P,MAC,a)SQNUSQNU+1输入 M:检验:HN 侧鉴权成功SQNH=SQNU*+1a=f2(k,SUPI)rV-GUTI=False:MAC=f1(k,)P=Enc(SUPI,SQNU)pkNrSUPI*,SQNU*=Dec(1(M),skN)检索SUPI*:k*,SQNHr*=3(M)f2(k*,SUPI*)MAC*=f1(k,)IF(i)and(ii):GUTI*=new GUTI#b=f3(r*,k*)GUTI*V-GUTI=True(i)2(M)=MAC*,(ii)SQNHSQNU*图4SUPI 子协议具体流程刘逸冰等:一个切换认证的 5G 鉴权协议及其形式化分析3715(1)SUPI 的加密传输由于 GUTI 不再可用,因而 UE 只能通过加密 SUPI 来完成身份信息的传递.具体来说,UE 首先结合随机数 r和序列号,采用一个基于公钥的非对称加密算法把 SUPI 化为隐藏变量 P:P=Enc(SUPI,SQNU)rpkN,其中,P 代替 GUTI 充当身份变量进行传输.从 GUTI 模式跳转到 SUPI 模式后,HN 选用基于私钥的非对称解密算法把 SUPI 和 UE 的序列号从变量 P 中恢复:SUPI,SQNU=Dec(1(M),skN).SQNH接下来,HN 在用户数据库中检索 SUPI,以获取用户密钥 k*和.此部分已在图 4 中用红色方框标出.(2)身份检验变量SQNU在此模式下,UE 侧身份检验变量的生成不再依赖 GUTI,而是基于带有时效特征的序列号和随机数 r,以及带有身份特征的密钥 k,即:MAC=f1(k,SQNU,r),而在鉴权过程中,UE 通过加密的方式把 r 传输给 HN,以便生成对应的 MAC 变量.r 被隐藏为 a 的公式如下:a=f2(k,SUPI)r.而在 HN 侧,它首先需要恢复出 r,可通过下式实现:r=3(M)f2(k,SUPI),3(M)其中,指的是上述的隐藏变量 a.进而,身份检验变量被计算:MAC=f1(k,SQNU,r).通过此,HN 可以正常的进行两个检验.此部分已在图 4 中用蓝色方框标出.5 形式化分析在本节,我们形式化地评估 SM-AKA 协议的功能性和安全性.我们主要从形式建模、证明目标与策略、攻击模型的设定等方面展开介绍.此外,对于鉴权协议的属性规范,我们也做了必要的描述.5.1 形式化简介形式化分析主要通过把协议用规范化语言描述,然后通过逻辑定理推导,检验其是否满足某一方面的要求.这个过程主要包括协议的流程和属性描述、协议的推导验证 2 个部分.流程属性建模主要是把鉴权实体的信息生成、通信交互、变量处理等描述规范化,同时,还包含对攻击模型能力的模拟.形式化描述语言基于数学模型,克服自然语言或者程序语言描述的不精确性.实际上,由于形式化系统层出不穷,因而吻合系统自身特点而构造的语言也多种多样,这使得推理工具之间的兼容性很差.因而,业界往往会选择利用一些通用性较强的描述语言.协议验证是对格式化后的属性实施推理,判断各项属性是否达到预期目标,得出对协议性能评估的结论.它基于鉴权中有序的变量生成、传递、转化以及销毁的过程,通过把属性要求设定为推理终点,施行一系列的逻辑引导,检验属性能够被满足.随着移动网络技术的快速发展,形式化验证已经变得十分重要,成为协议研究必不可少的一环.形式化分析通过推导证明完成目标的验证,主要是检查逻辑上的缺陷,对协议的安全隐私特性展开评估.而对于性能效率等属性,形式化难以应对,因而,SM-AKA 的性能分析主要通过理论探讨完成.形式化分析应用于 5G鉴权,最大的难点就是如何把协议的表达方法从自然语言转化为逻辑语言,使其能够输入到证明工具,进行数学推理.事实上,协议流程通常是复杂的,表述方式通常是多样化的.而逻辑语言具有高精准性的特点,即使存在一点差异,也会对协议的含义造成很大偏差.因此,准确无误地把自然语言形式转化为逻辑表达是很具挑战性的.同时,属性要求以文本形式给出,没有具象化阐述,如何按照其含义精准的抽取出具体指标,把其转化为标准的逻辑形式也是一大难点.由于形式化语言丰富多样,且高度凝练抽象,因而需要花费大量精力完成标准化建模.此外,协议的分3716软件学报2023 年第 34 卷第 8 期析需要模拟数量庞大的攻击可能,通过多重搜索算法推理证明,以检验攻击是否存在.这一过程对逻辑推导、攻击解析提出了很高的要求,需要经过复杂的循环演算才能检验协议的属性是否被满足.为了应对这些困难,本文主要采用 Spthy 语言建模协议流程和属性,采用 Tamarin 证明器进行自动化的推导验证.在本文中,多重搜索算法主要指的是:Tamarin 首先考虑协议所有的可行运行情况,建立完整的状态空间,然后依据一定的搜索方式在空间中查找符合特定条件的状态,以期发现可能存在的协议漏洞.5.2 属性要求3GPP 在移动通信标准文档的 R16 版本中对 5G 鉴权做出了属性要求,为我们的形式化分析设定了明确的检验方向.其以文本形式给出,我们在此介绍,具体如下.(1)认证属性.协议应通过双端实体(此处指 UE 和 HN)的一系列通信活动完成双向认证,确保正常用户能够顺利接入服务网,且提供服务的是合法服务网;同时,相同的会话钥不应该被生成两次,即要确保其唯一性,防止废弃的变量被非法重用.skNSQNUSQNH(2)保密属性.协议应保证参与认证的永久性变量不被泄露,包括密钥 k、私钥、序列号(,)和永久身份标识符 SUPI.而临时产生的鉴权变量,如 GUTI、SUCI 等,可以明文传输.一些临时变量的公开可能会使协议遭受攻击,因而需要融入对完整认证流程的考虑.(3)隐私属性.协议应具备很好的防攻击能力,保证用户隐私安全,如通信行为、通信习惯、地理位置等,这些信息都应具有不可追踪性.同时,协议应满足无连接性,即让攻击者无法区分多个隐式目标之间的关系,如判断两次追踪的 UE 是否为同一个 UE.(4)性能属性.在确保基本的认证和安全属性不受影响下,协议应尽量简洁,提升认证效率.同时,协议应尽可能地使用更少的变量和更低的资源.协议应具备较强的抗干扰性,确保鉴权能够长久稳定.5.3 形式化工具在推理验证协议属性的过程中,我们不可避免的需要用到一些自动证明机.随着形式化的不断发展,业界已经开发出了各具特色的工具,主要包括:AVISPA、ProVerif、Maude-NPA、Scyther、Tamarin 等.AVISPA20的初衷是为了克服复杂协议的描述和证明的难题.它提供了面向对象的标准化语言,并整合了 4种经典的证明器,不仅可以发现协议的脆弱点,还能够验证具有无限会话特性的协议.ProVerif19通过若干预定