一个切换认证的5G鉴权协议及其形式化分析.pdf
《一个切换认证的5G鉴权协议及其形式化分析.pdf》由会员分享,可在线阅读,更多相关《一个切换认证的5G鉴权协议及其形式化分析.pdf(18页珍藏版)》请在咨信网上搜索。
1、一个切换认证的 5G 鉴权协议及其形式化分析*刘逸冰,周刚(中国人民解放军信息工程大学数据与目标工程学院,河南郑州450002)通信作者:刘逸冰,E-mail:摘要:随着移动通信的发展,迎来了第 5 代移动通信技术(5G).5G 认证与密钥协商(5Gauthenticationandkeyagreement,5G-AKA)协议的提出主要是为了实现用户和服务网络的双向鉴权.然而,最近的研究认为其可能会遭受信息破译和消息重放攻击.同时,发现当前 5G-AKA 的一些变种不能满足协议的无连接性.针对上述缺陷,提出一个改进方案:SM-AKA.SM-AKA 由两个并行子协议组成,通过巧妙的模式切换使更加
2、轻量的子协议(GUTI 子模块)被频繁采用,而另一个子协议(SUPI 子模块)则主要用于异常发生时的鉴权.依据这种机制,它不仅实现用户和归属网之间的高效认证,还能提升鉴权的稳定性.此外,变量的新鲜性也得到有效维持,可以防止消息的重放,而严格的加解密方式进一步提升协议的安全性.最后,对 SM-AKA 展开完整的评估,通过形式建模、攻击假定和Tamarin 推导,证明该方案可以达到鉴权和隐私目标,而理论分析部分也论证了协议性能上的优势.关键词:5G 鉴权;认证协议;形式化分析;移动网络中图法分类号:TP311中文引用格式:刘逸冰,周刚.一个切换认证的5G鉴权协议及其形式化分析.软件学报,2023,
3、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 comm
4、unication 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.Atthesame
5、time,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,lightweightsu
6、b-protocols(GUTIsubmodule)arefrequentlyadopted,andtheother sub-protocol(SUPI submodule)is used to deal with abnormalities caused by authentication.Therefore,this mechanism not onlyrealizestheefficientauthenticationbetweenusersandnetworksbutalsoimprovesthestabilityoftheprotocol.Furthermore,thefreshne
7、ssofvariableshasbeeneffectivelymaintainedtopreventthereplayofmessages,andstrictencryptionanddecryptionmethodshavefurtherstrengthened the security of the protocol.Finally,the study carries out a complete evaluation of SM-AKA.Through formal modeling,attackassumptions,andTamarinderivation,itisprovedtha
8、ttheplancanachievetheauthenticationandprivacygoals,andthetheoreticalanalysishasdemonstratedtheperformanceadvantageoftheprotocol.Key words:5Gauthentication;authenticationprotocol;formalanalysis;mobilenetwork*本文由“形式化方法与应用”专题特约编辑陈立前副教授、孙猛教授推荐.收稿时间:2021-09-05;修改时间:2021-10-14;采用时间:2022-01-10;jos 在线出版时间:2
9、022-03-24CNKI 网络首发时间:2023-02-23软件学报ISSN1000-9825,CODENRUXUEWE-mail:Journal of Software,2023,34(8):37083725doi:10.13328/ki.jos.006617http:/中国科学院软件研究所版权所有.Tel:+86-10-62562563 1 引言随着通信技术的发展,移动设备已经广泛普及,比如手机、智能手表等.据统计,目前已有 50 亿人都是移动通信用户,这是一个庞大的群体1.他们通过多种多样的设备来享受移动网络提供的丰富服务,并被国际移动电信组织(3rdgenerationpartner
10、shipprojec,3GPP)制定的安全机制所保护.在漫长的发展历程中,移动通信技术已经走过了最初的 2G、惊喜的 3G 和成熟的 4G 时代,今天正处于 5G 时代,即第 5 代移动网络.每一代移动网络的发展都离不开安全这一主题,都会形成一系列的安全机制,而其中一个极其重要的机制是用户设备(userequipment,UE)和归属网(homenetwork,HN)之间的双向认证.事实上,3G 已经存在较为稳定的认证方法,即认证与密钥协商机制(authenticationandkeyagreement,AKA).到了 4G,AKA 方法得到进一步发展,演变为更加成熟和安全的 EPS-AKA
11、和 EAP-AKA 协议.现如今,经 3GPP 在前人基础上长达数年的研究,5G 的鉴权与认证协议最终形成2.该协议的目标是在包含通用用户身份模块(universalsubscriberidentitymodule,USIM)的设备和归属网络之间提供一个双向鉴权机制,以使双方在信息读取、网络接入等权限问题上达成一致.在确保隐私安全的情况下,用户可以正常的享用移动通信服务.为了实现这一目标,AKA 协议会在认证成功之后,赋予 UE和 HN 一个共享会话密钥以保障后续双方的信息通信.经过 3GPP 组织反复的商榷,最终确立的 5G 鉴权协议有两种,即 5G-AKA 和 EPS-AKA.事实上,它们
12、的设计目标是一致的,而其中的差异也只关乎法律因素3.因此,就本文聚焦的隐私安全来说,它们没有不同,在此,本文主要选取 5G-AKA 协议展开研究和讨论.近些年,针对认证协议的研究取得了巨大的进展,业界已经发现了一些关于 5G-AKA 协议的脆弱性,如:不同类型的失败消息的可区分性可能会使鉴权结果泄露、序列号的不完善加密可能会导致其被破解以及 SUPI 的非对称加密可能会带来较高计算复杂度.同时,协议分析逐渐大量采用形式化分析方法46.一些研究者通过形式化手段分析 5G-AKA,发现了协议中的一些缺陷,如 SUPI 在 UE 侧的不可靠存储、会话密钥的弱私密性等7,8.针对当前 5G 认证协议存
13、在的缺陷,一些安全研究人员提出了改进方案.Koutsos 等人9提出了具有两阶段子协议的AKA+方案,其最大的特色是设计了两个子协议相互补充的机制,其总体运行模式如图 1.它采用新颖的交替运行实现了认证协议所有的功能,两个子协议互为补充,分别应对不同的情况,是一个较为优秀的改进方案.AKA+协议会依据 V-GUTI 的值来决定选用哪个子模块,而鉴权的结果,即成功或者失败,又会反过来影响 V-GUTI 的值.作者还证明了该协议不仅可以很好地抵抗现有攻击,还取得了较高的平均认证效率.Yes失败成功成功失败GUTI 模块被选用SUPI 模块被选用No 更新:不更新:下一次鉴权开启鉴权V-GUTI=T
14、rue?V-GUTI=TrueV-GUTI=False图1AKA+运行机制通过分析 AKA+方案独特的工作模式,如图 1,我们发现了其存在一个脆弱点.在该协议中,用户永久身份标识(subscriptionpermanentidentifier,SUPI)和全局唯一临时标识(globallyuniquetemporaryidentity,GUTI)子协议传输的消息结构和组成不同,因而,我们在实际观测中可以识别认证网正在运行何种子协议.据此,我们设计了一种连接性攻击,总体过程如图 2.具体来说,当需要判断一个隐式 UEx与目标 UE0的关系时,攻击者首先监测 UEx刘逸冰等:一个切换认证的 5G
15、鉴权协议及其形式化分析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,即未知
16、的 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+协议的工作模式是新颖的,在运行效率上具有很大的优势.其总是
17、倾向于采用速度更快的 GUTI 子协议,而 SUPI 子协议也在为使用高效的 GUTI 模块服务.受此启发,也鉴于上述指出的脆弱点,我们提出了具有两阶段平行子模块的 SM-AKA 协议.该协议与 AKA+有类似的工作模式,即包含一个 SUPI 子模块和一个 GUTI 子模块.不同的是,我们令两个子模块的鉴权变量具有相同的组成和结构,从而确保子协议不可区分.该协议包含 3 个认证阶段,分别是:UE 向 HN 发送身份消息,开启鉴权流程;HN 向 UE 发送结果,同时更新用于后续认证的变量;UE 完成最后的信息检验,决定是否更新 GUTI.此外,我们对提出的 SM-AKA 协议实施了全面的形式化分
18、析,并得出较有价值的结论.本文中我们做了如下贡献.(1)提出一个改进的认证方案,即 SM-AKA.它不仅可以提供稳定可靠的交互认证,还可以有效阻止所有已知的针对 5G-AKA 及其一些修正版本的攻击.(2)在认证协议中仅用到一个随机数和两次消息传输,并通过新颖的交替运行模式更多的选用轻便的子模块,这给协议带来了较高的运行效率.(3)对 SM-AKA 协议开展一次精细的形式化分析,完成了对其各项属性的评估.同时,完整的分析证明过程也给形式化验证的发展提供一个经典示范.本文第 2、3 节描述了 5G-AKA 的协议细节及当前研究进展.第 4 节介绍 SM-AKA 协议的鉴权流程.第 5 节对提出的
19、改进方案展开了形式化验证和讨论.最后,在第 6 节中给出结论.2 相关工作随着 5G 时代的到来,研究人员在 5G 鉴权协议上投入了大量的精力,取得了可观的进展.在此,我们主要从脆3710软件学报2023 年第 34 卷第 8 期弱性挖掘、协议改进和形式化分析 3 个方面阐述相关研究.目前,业界已经发现了鉴权协议的一些脆弱点.Arapinis 等人10利用变量的结构缺陷,提出了一种连接性攻击,尽管这种攻击的设计初衷是针对 4G 通信的,但其对 5G-AKA 依然适用9.具体来说,由于协议在认证失败后,会产生两种错误消息,这两种消息的长度和组成不同,因而易于区分.攻击者利用这一缺陷能够判断两个未
20、知 UE 之间的关系,从而打破协议的无连接性.攻击能够顺利实现的另一个原因是消息通过空口传输,攻击者很容易在空气中捕捉到它.在鉴权中,空口传输是不可避免的,因而只能通过改进消息设计阻止可能的攻击.聚焦于序列号的加密机制,Borgaonkar 等人11利用变量的不完备加密,巧妙地设计了一种信息破译攻击.攻击者主要通过收集大量鉴权失败响应发挥破译算法的作用.具体来说,攻击者首先令 UE 和 HN 之间反复进行鉴权,并通过信息截断等手段,让鉴权结果交替出现成功和失败.而在每次获取失败响应时,攻击者都会通过重放过时的消息以确保结果是重同步类型的,所谓“重放”是指把同一消息重复发送超过两次.经过大量的重
21、复操作,攻击者可以收集到多条重新步类型的失败响应.然后依据异或计算的特点,攻击者采用迭代的方式逐位计算出序列号的二进制编码.最后攻击者可以根据破译的编码在一段时间内的变化推断出用户的隐私,如通信活动、地理位置等.Arapinis 等人10提出了 Fixed-AKA 协议,以应对可能发生的针对消息类型的攻击.该协议通过公钥加密的方式令两种失败消息具有相同的外部组成,从而使攻击者无法仅通过观测消息的长度和结构就获悉消息的类型,故可以阻断攻击行为的进行.通过研究,Fouque 等人12发现上述协议在变量的新鲜度维持上存在缺陷(新鲜度是指消息的唯一性、时效性、不可重用性,即确保消息是唯一生成,同时融入
22、时效信息且不能被重用),以致其容易遭受一种重放攻击.于是,新的改进协议 PRIV-AKA 被提出.该协议通过使服务侧的序列号只有在收到用户侧的确认消息后才会增加.这维持了鉴权变量的新鲜性,避免消息重放.同时,PRIV-AKA 吸收 Fixed-AKA 的优势,使鉴权失败消息的类型不可区分.然而,Koutsos 等人9发现,PRIV-AKA 无法满足协议的无连接性要求,攻击者能够轻松的区分目标用户和未知用户之间的关系.于是,他们提出了 AKA+协议,通过对 SUPI 和 GUTI 的交叉运用,以及对子协议优先级的设定,很好地满足了 UE 和 HN 之间双向认证需求.同时,AKA+每成功运行一次都
23、会为下一次的鉴权生成 GUTI,这使得相对高效的 GUTI 子协议可以被更多的使用.此外,Braeken 等人13提出了一个两阶段鉴权协议.它设计了一个身份注册阶段,通过把 SUPI 和私钥整合为动态的身份变量来实现信息的加密传输.并且,该协议仅使用了 2 次空口传输,具有很高的认证效率.该协议着重于满足协议在效率和安全方面的需求,是一个较为优秀的改进方案.聚焦于提升鉴权效率,Gharsallah 等人14提出了 SEL-AKA 协议.协议去除了认证对全局公钥体系的依赖,取而代之的是,用一个新提出的参数发挥相应的作用.通过其在用户端和服务端的共享,该参数完成了信息在双端的交换.分析表明,SEL
24、-AKA 很大程度上简化了流程和计算,满足了鉴权在功能和效率方面的要求.另外,Braeken 等人15在空口消息中,创新的使用随机数来取代序列号,以减少协议所需的通信步骤的数量.而 Han 等人16则采用了一种新的模式,把移动边缘计算用于鉴权,大大丰富了用于变量检验的算力,可以明显降低认证延迟.形式化分析作为一种强有力的属性验证方法,出现在大量 5G 鉴权协议的研究工作中,用于评估其安全有效性.具体来说,Basin 等人7使用 Tamarin 证明器17展开协议的安全属性验证,其把参与鉴权的终端归为 3 个实体,即 UE、服务网络和 HN,然后通过 Tamarin 的规则描述协议内容,通过引理
25、给出隐私目标.最终,分析结果显示,5G-AKA 无法满足无连接性要求以及可能遭受一些特定情况下的攻击.类似的,Cremers 等人8也使用 Tamarin 对5G-AKA 展开分析,并得到了很有价值的结论.不同的是,后者进一步细化协议的参与者,引入分别执行用户管理和认证管理的单元,使协议分析更加精细.当然,定义的规则和引理也更加复杂.另外,Edris 等人18采用 ProVerif工具19对 5G-AKA 展开形式化验证.除此之外,也有一些针对 5G-AKA 协议变种的分析案例.如 Gharsallah 等人14结合 AVISPA20和 SPAN21对其提出的 SEL-AKA 协议展开安全属性
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 一个 切换 认证 协议 及其 形式化 分析
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。