EAP-AKA’协议在5G网络中的形式化验证和性能评估

significant research conducted on primary authentication but mostlycovers 5G-AKA protocol, hence why this paper is focussing on verifyingEAP-AKA’ protocol with ProVerif [2] proof verifier and evaluating itsperformance using analytical and simulation methods.The main contribution of this paper is summarized as follows:• It interprets security properties and models the EAP-AKA’ proto-col as described in the 3GPP standard.• It conducts a formal analysis and verification of the protocol toautomatically identify the security properties.• It presents our security consideration on EAP-AKA’, to provide thebasis for future formal analysis and verification of next-generationAKA protocols.• It evaluates EAP-AKA’ protocol’s performance using two modelsand compares with 5G-AKA.0Array 16（2022）1002540p://creativecommons.org/licenses/by/4.0/）。0ScienceDirect提供的内容列表0Array0期刊主页：www.elsevier.com/locate/array05G网络接入安全的EAP-AKA’协议的形式化和评估0Ed Kamya Kiyemba Edris a，�，Mahdi Aiash a，Jonathan Loo b0a英国中部大学科学与技术学院，伦敦亨登Burroughs，NW4 4BT；b英国西伦敦大学计算与工程学院，伦敦伊灵圣玛丽路，W5 5RF0文章信息0关键词：5G，EAP-AKA’，安全协议，形式化方法，验证，认证，ProVerif，应用pi演算，性能评估0摘 要0第五代移动网络（5G）将通过增强的安全性和隐私支持终端用户的体验质量（QoE），在访问服务时将得到改善。终端用户和网络运营商将依赖认证和密钥协商（AKA）协议提供的安全保障。AKA协议已经为5G网络标准化，可扩展认证协议（EAP）-AKA’协议是为用户设备（UE）和网络相互认证而指定的主要认证机制之一。本文对EAP-AKA’协议进行建模，并根据5G安全标准对EAP-AKA’协议进行了广泛的形式化验证，以确定该协议是否在5G网络中是可验证安全的。它使用ProVerif，一个安全协议验证器，对EAP-AKA’协议进行了安全评估。它还提供了支持安全验证的安全属性，以及用于评估协议性能的定量属性。最后，它比较了EAP-AKA’和5G-AKA协议的安全性和性能结果。01. 引言0第五代移动网络（5G）将支持物联网（IoT）和车联网（V2X）等应用，以及用户移动性，密集连接和大规模机器类型通信（mMTC）。移动设备和多媒体应用的巨大增长导致了对无缝连接和移动数据流量快速增长的需求。5G将受到可视化、边缘计算和设备对设备（D2D）通信等技术的支持。通过新一代无线接入网络（ngRAN），移动用户设备将能够访问5G网络服务，因此安全访问驱动5G安全标准要求，如第三代合作伙伴计划（3GPP）在[1]中规定的那样。用户和移动网络运营商应该能够依赖5G安全提供的认证、保密和完整性等安全属性。为了访问网络，UE必须经过认证，还需要额外的认证和授权才能访问由MNO或其他数据网络（DN）提供的服务。UE、服务网络（SN）和家庭网络（HN）使用认证和密钥协商（AKA）协议来保证安全。5G标准[1]涵盖了5G中最重要的安全需求，并指定了可扩展认证协议（EAP）-AKA’作为主要认证中使用的方法之一。对主要认证进行了大量的研究，但主要涵盖了5G-AKA协议，因此本文重点验证EAP-AKA’协议，并使用分析和仿真方法评估其性能。本文的主要贡献总结如下：0� 通讯作者。电子邮件地址：ee351@live.mdx.ac.uk（E.K.K. Edris），m.aiash@live.mdx.ac.uk（M. Aiash），jonathan.loo@uwl.ac.uk（J. Loo）。0本文的其余部分结构如下。第2节介绍了EAP框架、5G安全和形式化方法的相关工作。第3节介绍了基于3GPP标准的EAP–AKA'协议。第4节介绍了协议建模并讨论了安全要求。第5节讨论了协议的形式化。第6节对EAP-AKA'进行了形式化安全分析和安全0• 它解释了安全属性，并将EAP-AKA'协议建模为3GPP标准中描述的那样。 • 它对协议进行了形式化分析和验证，以自动识别安全属性。 •它提出了我们对EAP-AKA'的安全考虑，为未来对下一代AKA协议进行形式化分析和验证提供了基础。 •它使用两个模型评估了EAP-AKA'协议的性能，并与5G-AKA进行了比较。Array 16 (2022) 10025420考虑。第7节介绍了协议的性能评估。结论和未来工作总结在第8节。0E.K.K. Edris等人0[3-5]的作者回顾了EAP概念，该概念在02. 相关工作0此外，EAP-AKA'可用于对UE进行认证0在请求评论（RFC）3748中作为认证框架进行了规范化[6]。它可以在专用链路、有线和无线网络上使用，并且可以直接在数据链路层上运行，而不需要IP地址。3GPP设计了EAP-AKA协议，然后由EAP WG在RFC4187[7]中确认。随后，它被指定为用于UMTS的认证和会话密钥分发的EAP方法。身份隐私支持、结果指示和快速重新认证过程都被添加到EAP-AKA中。这使得AKA方法在EAP框架内成为主要认证的可能，后来在RFC9048[8]中得到改进，增加了一个新的EAP方法EAP-AKA'。添加了一个新的密钥派生函数，将派生密钥与接入网络的名称绑定，以防止绑定攻击[4]。02.1. 认证过程0通过相互认证和会话密钥协议，交换消息以验证彼此。5G系统支持UE和SN之间由HN授权的AKA。它提供了在5G内的加密、完整性和重放保护以及隐私，使得UE可以通过SN安全地访问HN。5G支持用于在5G中访问网络和在外部DN中访问服务的主要认证和次要认证方法。EAP框架可以用于这两种方法，如5G标准中规定的那样[1]。02.2. 使用形式化方法和自动证明验证协议0由于使用了强抽象、简化和0在过去，属性分析、形式化方法和自动验证已经被应用于像AKA这样的身份验证协议，但是只能提供弱保证。为了提供可靠的保证，已经使用形式化方法来检查安全协议[3,4,11]。大多数验证方法和工具在处理AKA协议的属性时会遇到困难，比如在EAP-AKA'中，由于加密原语的应用，如序列号（SQN）和异或（XOR），它们的代数特性使得符号推理变得困难[12]。因此，手动证明评估对于某些工具来说并不合适。0许多自动验证工具，如Tamarin [13] Auto-0自动验证互联网安全协议和应用程序(AVISPA) [14]和ProVerif[2]等工具可用于此分析。ProVerif评估了加密协议的安全性，并使用Dolev–Yao模型来促进用户定义的等式理论和各种安全特性的验证。ProVerif还识别了由重写规则和满足有限变体属性的方程式指定的加密原语。为了支持协议推理，语法与形式化语义相结合。因此，我们认为ProVerif是我们分析的合适工具。在[3,5]中，它被应用于正式检查AKA协议的安全特性保证。0[5]中的作者对5G EAP-0通过符号模型验证和分析来验证AK’A协议的安全性。他们还正式验证了该协议的安全性。通过对5GEAP-TLS认证协议的安全相关特性进行彻底的形式化调查，[3]中的作者使用ProVerif审查了EAP。作者讨论了EAP框架，并基于5G-AKA分析了安全特性[12,15]。[16]中的作者基于Lowe的分类对安全性进行了分析，并使用Tamarin正式对EAP-AKA’进行了建模和检查。相关工作正式使用各种自动化工具对EAP-AKA’协议进行了形式化方法分析，但未评估协议的有效性。相比之下，本研究使用了下一节中涵盖的两种技术对协议的性能进行了形式化分析和评估。03. EAP-AKA’协议03GPP将EAP-AKA’协议定义为主要方法之一0在5G安全标准中，AKA协议在移动设备和其HN之间进行认证[1]。认证协议包括一个主控功能，使HN操作员能够确定设备是否在每个网络中进行了认证，并做出最终的认证决定。协议成功运行后，所有各方应能够推导并达成一个锚定密钥，用于生成UE和本地网络中的下一代节点B（gNodeB）之间通信的会话密钥。此外，对于UE和外部DN之间的次要认证，EAP方法是首选。03.1. EAP架构概述05G系统包括以下内容：0• UE：存储通用子-0带有对称加密算法、HMAC和会话计数器等加密能力的用户识别模块（USIM）、用户永久标识符（SUPI）、其HN的公钥、密钥K。0• HN：包括支持安全功能和数据库的0认证，生成向量并存储用户订阅数据。0• SN：UE连接的无线接入网络，用于接入0HN。0如图1所示，5G的安全架构包括0如[1,11]中所述，包括UE、安全锚定功能（SEAF）、认证服务器功能（AUSF）、认证凭证存储和处理功能（ARPF）和统一数据管理（UDM）。SEAF部署在SN中，而AUSF和ARPF位于HN中。此外，UE与ARPF共享秘密密钥和其他信息，在AKA过程中使用。当UE将订阅唯一标识SUPI发送到HN时，它被加密为订阅隐藏标识（SUCI），并且只能由HN解密。UE和SEAF必须实现相互认证，并在通信之前必须拥有会话密钥，因为这发生在不安全的无线信道上，而SEAF、AUSF和ARPF之间的通信发生在假定安全的有线信道上。0数组16（2022）1002540•  对等体由UE表示。 •  透传认证器由SEAF表示。30图1.  5G系统架构。0E.K.K. Edris等人0图2.  5G EAP实体。0EAP请求/响应中的主要EAP-AKA’属性为AT_RAND、AT_AUTN、AT_RES、AT_MAC、AT_KDF、AT_KDF_INPUT、AT_MAC、AT_AUTS。根据5G安全规范[8]，EAP-AKA’中已经进行了一些重大变化，如下所示：0在UE和HN之间的成功身份验证过程中，从  � ����  派生  � ����时，UE的身份和接入网络ID被用作密钥派生中的输入03.2. 密钥派生04. EAP-AKA’协议建模0使用at_kdf_input参数进行密钥派生。与身份验证相关的密钥包括密钥：K、CK、IK、CK’和IK’，用于生成EMSK（ � ����  ），然后  � ����，后来用于派生其他密钥以保护UE和其他网络实体之间的通信。此外，CK’和IK’的KDF输入参数相同，只是通过256位输出分隔，其中CK的128位最高有效位，IK的128位最低有效位[10]。0数组16（2022）1002540在这种建模中，用于身份验证向量（AV）的值在表1中定义：它们包括一个随机nonceRAND作为挑战，AUTN作为用于验证挑战新鲜性和真实性的认证令牌，以及作为对挑战的预期回复的XRES。EAP-AKA’协议模拟了四个实体（UE，SEAF，AUSF和ARPF/UDM）。重点是身份验证和身份验证失败，而不是重新身份验证。使用具有椭圆曲线集成加密方案（ECIES）配置文件的XOR和HN公钥来隐藏SQN和SUPI。通过在密钥派生参数链中包含‘‘SNN’’，强制执行与SN绑定的锚定密钥� ����，确保锚定密钥专用于网络和UE之间的身份验证过程。直接利用ARPF和USIM进行5G身份验证提供了更强的保证，类似于EAP-AKA’中的快速重新身份验证。40E.K.K. Edris等人0表1 5GEAP-AKA’符号和描述。0表1 符号说明0符号说明04.1.安全假设和要求0如果假定SN和HN之间的通道是安全的，0根据TS33.501标准，它应该使用加密原语、密钥和HMAC来提供机密性、完整性、真实性和重放保护。如果SN-HN通道不安全，它将面临与UE-SN通道相同的攻击[11]。0执行直径协议的实体以及0如果攻击者的能力增强，AKA本身可能会受到威胁。这一假设得到了5G特性的支持，这些特性增加了攻击者的攻击向量[11]。攻击者也可能控制实际的USIM卡，这种情况下，攻击者可能可以访问USIM中包含的所有秘密值，包括SUPI、K和SQN。尽管EAP-AKA’缺乏密码套件协商能力，但它具有确定密钥派生函数的机制。SHA-256提供了相当于EAP-AKA[8]的相互认证、保密性、密码绑定和会话独立性等安全特性。还假定由于SHA-256是伪随机函数，攻击者将无法以任何实际可行的方式推断出预共享密钥。EAP-AKA’使用不同的标识符来识别认证的UE。尽管协议密钥强度排除了暴力攻击，但它并不提供通道绑定。0保密性、机密性、完整性、真实性和隐私性是0EAP-AKA’协议的期望安全特性[1]。UE必须安全地假定只有其HN授权的SN才能用于认证。UE必须使用隐式密钥认证和确认来与SNN进行认证。在密钥确认后，UE必须与其HN就SNN达成弱一致。0在UE和HN之间的AKA过程中，SN必须能够0通过对SUPI进行认证来验证UE。EAP-AKA’负责维护 � ����的保密性，因为它是锚定密钥。它强调相同的 � ����不应该被生成两次。5G对隐私有明确要求，SUPI和SQN必须在被动攻击的情况下保持机密，以避免数据泄露等攻击。通过通信渠道，利用这些安全特性来构建和维护0长期IPSec、(D)TLS或DIAMETER会话。SEAF和AUSF是基于直径的系统，可以在IPSec或TLS上运行。03GPP试图解决虚假基站和非法基站的安全问题0通过增加主控制来防止否认。这是通过AUSF向ARPF发送认证确认、HN确认UE的身份并授权SN发送SNN给UE来实现的[1,11]。假设EAP-AKA’提供与EAP-AKA相同或更好的安全性。然而，EAP-AKA’可能受到与5G-AKA协议相同的攻击，如监视、定位、解同步和可链接性攻击，这会影响隐私属性[18]。0目前尚未发现任何泄露AKA的攻击0在最初假定的信任模型和EAP-AKA’[8]下定义的安全属性。尽管如此，直径协议仍然容易受到中间人、恶意软件和DDoS攻击[11,19]。直径依赖点对点原则，而不是端到端加密。此外，由于直径使用相同的路由进行请求/响应消息交换，拦截和信息收集是可能的。04.2. 协议消息交换0EAP-AKA’协议过程分为以下三个阶段0使用认证向量（AV）和交换消息（msg）分阶段进行，如表1所示。阶段1：初始化和方法选择它涉及初始化和认证方法选择。如图3所示，SEAF启动与UE的认证过程。Msg1. SEAF → UE：（EAP-Request/Identity）1.SEAF向UE发送身份请求。Msg2. UE → SEAF：（SUCI）2.UE在msg2中发送包含SUCI和HNID的认证请求。Msg3. SEAF →AUSF：（SUCI，SNN）3.SEAF接收msg2并在msg3中向AUSF发送SUCI和SN名称。Msg4. AUSF →ARPF：（SUCI，SNN）AUSF向UDM/ARPF发送msg4。在使用SNN之前，AUSF检查并验证SEAF是否被授权。当ARPF接收msg4时，SUCI通过SIDF解密为SUPI，并选择认证方法。0第2阶段：协议EAP-AKA’协议以EAP挑战-响应的形式在实体之间流动，如图4所示。Msg5.ARPF → AUSF：EAP-AKA’AV（RAND，AUTN，XRES，SNN，CK’  ∥IK’，SUPI）UDM/ARPF在收到SUPI后生成认证向量AV。首先生成RAND和SQN，然后生成XRES和AUTN。计算CK和IK，以及CK’和IK’。在msg4中，ARPF向AUSF发送EAP-Response/AKA’AV，表示将使用EAP-AKA’。Msg6. AUSF →SEAF：（RAND，AUTN，SNN）当AUSF接收msg5时，它在向SEAF发送msg6中存储XRES和SUPI。Msg7. SEAF →UE：（RAND，AUTN，ngKSI，ABBA）在Auth-Request的msg7中，SEAF向UE发送RAND和AUTN。必须在此消息中包含ABBA参数，以启用绑定下行保护。Msg8. UE →SEAF：（RES，MAC）当UE接收msg7时，它将RAND和AUTN转发给USIM，后者检查AUTN是否可以接受以验证AV的新鲜度。它生成AK并获取SQN。然后生成MAC2，检查（i）如果MAC2 =MAC和（ii）如果SQN在范围内，如果SQNUE  事件（beginUE（u，a，r，k））。查询u：主机，a：主机，r：一次性数字，kseaf：密钥，k：密钥；注入事件（endAUSF（u，a，r，k））==>注入事件（beginUE（u，a，r，k））。0该协议在ProVerif中使用安全的pubsec通道进行建模和运行，对协议没有影响，也没有发现攻击。然而，当协议在受损的通道上运行时，认证并未如5G标准所假设的那样保持。这是对5G-AKA协议的类似攻击[11]。根据ProVerif结果，UE的身份保密性、长期密钥、锚密钥和UE对SN的认证在图6中得到保持。然而，SN对UE的认证在非注入和注入协议中均未得到保持。UE接收了消息4并发送了消息5，如e1所示，表明SEAF发送了消息4。所有协议参数都作为这些事件的参数。70数组16（2022）1002540E.K.K. Edris等人。0图6. EAP-AKA’不安全的ProVerif结果。0图7. 攻击跟踪。0除了e2，它检查xsqn = xor(xored sqn, ak)，xmac = f1((xsqn, xrand),ki)，xmac = mac和xsqn = sqnue。如果输入为真，则传达 ���消息；否则，发送MAC_failure或synch_failure消息以进行认证失败或重新认证启动。然而，因为msg4可以被重放，导致一个e1对应多个e2，这种对应关系在ProVerif中无法直接证明。该研究还发现，事件e2具有res作为参数，在autn和rand被发送之前无法执行，即在e1之前。这在ProVerif中失败为假。05.3. EAP-AKA’协议的攻击0如图6和7所示，ProVerif结果表明协议受到了攻击。攻击者的行为被表示0通过攻击推导表示的真正攻击，但攻击跟踪是攻击过程的可执行跟踪。推导和跟踪是一系列步骤、输入和通信通道上的输出，以及相关事件。0• 查询事件(endSEAF(x1_80)) ==>事件(beginSEAF(x1_80))，当攻击者使用attacker(suci_4228)获得suci_4228时，攻击者的目标得以实现0Array 16 (2022) 1002548• Mutual Entity Authentication: If RES = XRES, the UE is implicitlyauthenticated to the HN and SN, as SNN is included in the suc-cessful authentication and 𝐾𝑆𝐸𝐴𝐹 confirmation. This is enforcedwhen SUPI and SNN are transmitted to the HN and are proven tohold.• Mutual Key Authentication: The UE and HN authentication ispredicated on the secrecy of 𝐾𝑆𝐸𝐴𝐹 , it is implicitly authenticatedby incorporating 𝐾𝐴𝑈𝑆𝐹 and SNN in its derivation parameters.• Mutual Key Confirmation: This condition is enforced by a success-ful AKA roundtrip between the entities and with 𝐾𝑆𝐸𝐴𝐹 confirma-tion.• Key Freshness: Although there is no function in ProVerif to checkkey freshness, the UE validates the AUTN freshness during theauthentication process by checking if SQNUE > SQNHN. Addi-tionally, every 𝐾𝑆𝐸𝐴𝐹 is linked to SN by SNN, which guaranteesthe key freshness, 𝐾𝑆𝐸𝐴𝐹 from prior sessions cannot be reused innew sessions.• Unknown-Key Share: In ProVerif, the reachability property isutilized to check for aliveness. This attack is prevented by theentities’ identity and key binding. SUPI, HNID and SNN in thederivation of 𝐾𝑆𝐸𝐴𝐹 , and the dependence on a preshared key Kbetween UE and HN also prove this condition. Moreover, 𝐾𝑆𝐸𝐴𝐹is only provided to SEAF after AUSF has verified the RES andMAC2.• Key Compromise Impersonation Resilience: 𝐾𝑆𝐸𝐴𝐹 is implicitlyauthenticated and stays a secret. However, even if the attackerdiscovers 𝐾𝑆𝐸𝐴𝐹 keys used in all previous sessions and the keyK material is compromised, the current session remains confi-dential. It does not, however, hold for forward secrecy or post-compromise secrecy. EAP-AKA’ fails to meet these standards be-cause knowing key K allows an attacker to deduce all previousand future keys.0E.K.K. Edris等06. 协议安全性分析0图8. EAP-AKA’安全结果。0本节使用[20,21]中定义的分类法对EAP-AKA’协议的安全性进行分析，用于检查形式方法的结果。06.1. 安全性分析106.2. 安全分析20•保密性：由于SUPI的保密性得到维护，因此满足了此要求。通过使用XOR和匿名密钥在传输和存储中保护密钥派生参数。F1和F*提供了  ���的隐私保护。协议的机密性得到维护，隐私得到保护。 •存活性：HN从SN获取UE的存活性，UE同意在  ���上进行非注射协议。此外，HN通过与UE在  � ����上进行注射协议获得新的存活性。 •  弱协议：当SN在  ��� �上获得与UE的非注射协议以及使用 ���作为参数的密钥确认时，满足了此要求。然而，正如ProVerif结果所示，弱协议不成立。 •  非注射协议：在  � ����  确认和  ����  成为SUPI的一部分后，UE在  ���上获得了与其HN的非注射协议。UE从SN和UE处分别获得了  � ����的注射协议。这是因为  � ����  的推导涉及从HN处的��  _ ����和从SN处的SNN，任何与HN在  � ����上的协议都确保了UE连接到授权的SN。但由于信道安全假设的改变，SN-UE认证失败。 •  注射协议：UE和SN之间在  � ����上的注射协议对于协议的目标至关重要，为各方之间建立此协议意味着  � ����不能在同一会话中推导两次。因此，在  � ����  推导中使用  ��  _ ����确保了HN和UE之间在  � ����  上的注射协议。值得注意的是，与HN在  � ����上的任何协议都会告知UESN是值得信赖的。为确保与SN的会话是由HN授权的，UE从HN处获得了  � ����的注射协议。另一方面，SN无法从UE处获得相同级别的信任，因为SN-UE注射协议不会发生。0必须考虑到密钥K可能通过窃听通信渠道、黑客攻击USIM卡、USIM供应商、移动供应商或侧信道泄露[11]。这将允许攻击者冒充用户向SN发送流量，危及UE的隐私。另一方面，密钥的误用可能导致SN代表UE发送流量。然而，仅知道在一个会话中建立的  � ����  是不足以从以前的会话或未来的会话中推导出  � ����的[5G]。EAP-AKA’协议中的网络名称绑定也有助于减轻一些影响旧EAP-AKA协议的攻击，如隐私攻击，但其配置不应基于请求发起地的位置，除非可以使用加密方法确认位置信息。如果SN从HN为UE请求大量的认证运行以诱导DoS，重新同步和跟踪/监视机制应通过限制认证尝试次数来防止这种类型的攻击[8]。90Array 16 (2022) 1002540E.K.K. Edris等人。0图9.  EAP-AKA状态转换系统。0表3 进程扩展。0术语语法0�，�.�  ∶∶= 扩展进程 � 普通进程 �  ∣  � 并行组合 ��.� 变量限制 ��.�名称限制 { � ∕ � } 活跃替换0此外，[12，18，22]忽视了当今攻击者的复杂性。他们假设现有的安全机制将保护直径协议、信道和HN实体，但他们没有考虑到[19，23，24]中的攻击，即即使安全网络也可能受到威胁，导致更大的攻击向量[11]。由于SN和UE之间的非注射和注射协议失败，重放攻击是可能的。然而，在重放消息经过一轮到达HN后，SQN和不可链接性问题[18]可以得到解决。重新同步是通过检查AUTS中发送的SQNUE是否大于SQNHN，或将SQNHN设置为SQNUE来实现的。因此，如果标准规定不足，协议的脆弱性可能允许5G中的多种攻击。另一个额外的措施是使用Diffie-Hellman密钥交换实现完美前向保密性，但在移动设备资源方面计算成本太高。此外，依赖AUSF中  � ����的认证不如ARPF和USIM之间的直接认证强[11]。当在HN环境中使用安全通信信道和更强大的机制，如加密技术和随机性，再次模拟协议时，发现UE和SN的认证与5G标准假设的一样。0在图8上显示了非单射和单射协议的安全机制。还应增强保护直径会话的安全机制。07. 协议性能评估0本节评估了[25]中的分析和模拟方法评估了协议的性能。EAP-AKA’协议在[11]中进行了评估并与5G-AKA协议进行了比较。07.1. 分析性能评估0[25,26]中的分析建模将增强标签与协议验证中使用的ProVerif和Appliedpi-calculus过程的每个通信和每个解密相关联。它受到基于标记的相似性[27]的增强操作语义的支持，构建有限状态空间的过程，并保持其语法上下文的通信输出和输入组件。特定过程的每个前缀都被赋予上下文标签�，过程的并行组合（|）定义了整个系统。如表3所示，使用限制运算符���形成新名称，它在变量�的过程�中作为静态绑定器运行。系统的转换可用于演示通信，分别用于EAP-AKA’和5G-AKA协议的图9和10。为了评估诸如进行加密和解密的密码学过程等转换的定量方面，从其标签派生的各个转换被分配成本[26]。协议的成本以原语动作的时间开销、转换成本的形式给出，这些成本是通过检查增强标签确定的。假设每个实体都有其处理单元，对每个标签∥�，输出和输入给予相同的成本。100Array 16 (2022) 1002540E.K.K. Edris等人。0图10. 5G-AKA状态转换系统。0表4成本描述。0术语描述0�消息大小���th加密大小�单元加密成本�单元解密成本�单元输出成本��状态的标签��标签的成本0转换，传输成本等于���+∑��=1����解密成本等于���，这些术语在表4中指定。关于其标签��的协议成本��在第7.1.2节中给出。密码学原语、系统架构、协议和加密算法，如ECC、SQN、AKA挑战和XOR，影响成本。07.1.1.定量测量增强的操作语义用于获取生成连续时间马尔可夫链（CTMC）过程所需的可量化数据[28]。CTMC由许多状态、标记的转换和一系列随机值组成，这些随机值的概率取决于先前状态的值[29]。在[26]中，当计算转换的指数分布时，成本被视为指数分布的参数，共享源和目标的弧被折叠，导致数字过程�。此外，参数速率�与转换相关联，以估计系统切换的速率或转换概率0表5协议的成本标签。0EAP-AKA’ 5G-AKA0c1 = 2s + e c1 = 2s+e c2 = 3s c2 = 3s c3 = 3s c3 = 3s c4= d c4 = d c5 = 5s + 8e c5 = 5s+7e c6 = 5s c6 = 5s c7 =5s c7 = 5s c8 = 5d c8 = 4d c9 = 2s + e c9 = s+e c10 = 2sc10 = s c11 = d c11 = 2s C12 = 2s c12 = 2s C13 = s c13= d0从与过程��绑定到��。因此，它等同于从��到��的所有可行转换成本的总和，速率与转换系统内的个体成本相关，如[26]中所述。CTMCC被表示为一个有向图，其中节点是C的状态，可以从彼此到达的状态由弧连接，如图9和10所示。因此，过程在状态之间切换的速率可以组织成一个表示为�的方阵/生成器矩阵。图的邻接矩阵包含了过程的CTMC的表示（����（�））。此外，�的元素被用来说明瞬时转换速率[26]。两个状态��和��之间的转换速率，用符号�（��，��）表示，是这些状态之间转换发生的速率，使用等式（1）。11E.K.K. Edris et al.𝐐𝟏 =⎜⎜⎜⎜⎜⎜⎜⎜⎜⎜⎝𝑙1−00000000000𝑙3𝑠𝑠𝑙4000−𝑑𝑑00000000𝑙50000−0000000𝑙7𝑠𝑠𝑙80000000−5𝑑5𝑑0000𝑙900000000−𝑥𝑥