PaperlayerView exact revision on arXiv

Source-linked AI summary

A Formal Analysis of 5G Authentication

David Basin, Jannik Dreier, Lucca Hirschi, Saša Radomirović, Ralf Sasse, Vincent Stettler

arXiv:1806.10360v4cs.CR

TL;DR

5G AKA lacked a comprehensive formal analysis of whether its standardized security goals and assumptions were sufficient for protecting mobile communications. The paper formalizes the protocol and standards, then uses automated Tamarin analysis to show that several critical authentication and privacy properties fail under the standard’s stated assumptions.

  • Problem

    5G AKA lacked a comprehensive formal analysis of its security goals and assumptions, which matter for protecting users’ mobile communications.

  • Method

    The authors formally interpret the 5G standard, construct a detailed automated model of 5G AKA, and systematically verify its confidentiality, authentication, and privacy properties using Tamarin.

  • Results

    Several critical authentication properties fail before key confirmation or require assumptions missing from the standard, while an active attacker can trace subscribers.

  • Takeaways & Limitations

    The analysis supports explicit recommendations and provably secure fixes for the identified attacks and weaknesses.

  • Takeaways & Limitations

    The analysis covers one of 5G’s two authentication methods, leaving other AKA variants for future analysis.

Abstract

from arXiv · show

Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.

1 INTRODUCTION

This paper presents the first faithful, comprehensive formal analysis of 5G AKA, interpreting 3GPP’s security assumptions and goals and evaluating them automatically. The analysis identifies missing goals, minimal assumptions, violated authentication properties, and provably secure fixes.

  • Formalization: The authors formally interpret the 5G standard’s assumptions and goals across confidentiality, authentication, and privacy, identifying missing security goals and flaws in stated goals.This required analyzing 722 pages across four 3GPP documents.
  • Formal Model: They provide the first faithful formal model of an AKA protocol, including the full protocol state machine, message flows, and symbolic cryptographic abstractions.Dedicated inductive lemmas and proof strategies make the model amenable to automated reasoning.
  • Security Evaluation: Using Tamarin, the authors conduct the first comprehensive formal security evaluation of 5G AKA and automatically determine the minimal assumptions needed for each security goal.The analysis targets varied adversarial settings and fine-grained confidentiality, authentication, and privacy properties.
  • Security Results: Some critical authentication properties are violated before key confirmation, while others hold only under assumptions that the standard does not clearly mandate.The findings expose weaknesses in the standardized security guarantees of 5G AKA.
  • Recommendations: The paper makes explicit recommendations with provably secure fixes for the attacks and weaknesses discovered in the 5G AKA analysis.The model also supports precise formal comparisons between AKA protocols across network generations.

2 5G AUTHENTICATION PROTOCOLS

The 5G ecosystem uses UE, SN, and HN entities to authenticate subscribers and establish secure channels. It specifies 5G AKA and EAP-AKA’, with 5G AKA combining SUPI-hiding initialization, challenge-response authentication, replay protection, and optional re-synchronization.

  • Architecture: The architecture comprises User Equipment with a USIM, Home Networks responsible for subscriber authentication, and Serving Networks providing connectivity.The UE communicates with the SN over an insecure wireless channel, while the SN communicates with the HN over an authenticated wired channel.
  • Authentication protocols: 3GPP specifies two authentication methods, 5G AKA and EAP-AKA’, and leaves the choice to the HN after subscriber identification.The protocols rely on cryptographic messages described in the paper’s appendix.
  • Initialization Protocol: Initialization protects subscriber privacy by sending SUCI, a randomized encryption of the SUPI under the HN’s public key, together with the HN identifier.The random nonce Rs is included in the encrypted payload, and idHN enables the SN to identify the relevant HN.
  • 5G AKA: 5G AKA uses a challenge-response phase and optional re-synchronization, with K as a long-term shared secret and SQN providing replay protection.SQN values stored by the UE and HN can become out of sync, for example because of message loss.
  • 5G AKA: The HN constructs a fresh authenticated challenge, the subscriber verifies its MAC and freshness, and successful validation derives KSEAF for securing later communication.The HN sends the SN a hash of the expected response rather than the full RES∗, while AUTN authenticates the challenge and its sequence number.
  • EAP-AKA’: EAP-AKA’ uses the same shared-secret challenge-response and SQN-based replay-protection mechanisms as 5G AKA, but changes the flow and some key-derivation functions.The analysis focuses on 5G AKA and does not describe EAP-AKA’ differences in detail.

3 THREAT MODEL AND SECURITY GOALS

This section formalizes 5G AKA’s threat model and translates 3GPP’s informal claims into precise security goals. It also identifies underspecified or missing requirements, including key agreement, session binding, privacy, and secrecy under compromise.

  • Formal security goals: The authors derive formal security goals from 3GPP documents using Lowe’s authentication taxonomy to remove ambiguity before formalization.They support their interpretations with relevant TS and TR excerpts and references.
  • Threat model: The model allows passive eavesdropping and active message manipulation between subscribers and serving networks, while considering compromised serving networks and subscriber credentials.Compromised serving networks expose authenticated home-network channels, and compromised USIMs reveal SUPI, K, and SQN.
  • Threat model: SQN is modeled as initially unknown to the attacker because it is a 48-bit or 43-bit counter and online queries require a correct MAC.The passage characterizes SQN guessing as having very low probability and rules out offline guessing attacks.
  • Secrecy and privacy: 5G AKA fails forward and post-compromise secrecy because knowledge of K lets an attacker derive all past and future session keys.The section also argues that privacy requirements should address active attackers and untraceability, not merely confidentiality of SUPI and SQN.
  • Authentication and key agreement: The standard omits agreement on KSEAF, although subscribers and serving networks should achieve at least non-injective agreement and obtain a distinct key in each session.The authors identify this as a critical requirement for an authenticated key exchange protocol.
  • Authentication and key agreement: Home networks require present-session assurance that subscribers are attached to the serving network, while subscribers require injective agreement on KSEAF with trusted home networks.Agreement only on a serving-network name from a past session is considered too weak; KSEAF binds the session to SNname.

4 FORMAL MODELS

The section formalizes 5G AKA security analysis in Tamarin, defining its symbolic execution and security-property framework, modeling choices, and approaches to the protocol’s statefulness and XOR complexity. The resulting model supports automated analysis and can be adapted to other AKA-family protocols.

  • 4.1 The Tamarin Prover: Tamarin is used as a state-of-the-art symbolic verifier supporting stateful protocols, automation, and equivalence properties needed for privacy analysis.Its symbolic cryptography treats messages as terms with specified algebraic equations and assumes black-box cryptographic primitives.
  • 4.1 The Tamarin Prover: Tamarin models protocol executions with multiset rewrite rules and a Dolev-Yao attacker controlling network communication while remaining limited by cryptographic knowledge.The attacker can intercept, delete, modify, delay, inject, and construct messages, but cannot forge signatures or decrypt without keys.
  • 4.2 Formalizing Security Goals in Tamarin: Security goals are expressed as trace or equivalence properties, with Tamarin checking all executions and attacker behaviors for proofs or counterexamples.Trace properties use first-order logic with timepoints, while unlinkability uses observational equivalence between protocol instances differing in selected terms.
  • 4.3 Modeling Choices: The symbolic model omits message lengths and usually publicly known constants, while accounting for length-based type-flaw prevention through modeling assumptions.These simplifications delimit the model’s scope and exclude certain length-based misinterpretations.
  • 4.4 Tamarin Models of 5G AKA: The authors built an automated Tamarin model of 5G AKA and released the model and documentation online using Tamarin v1.4.0 with XOR support.The model is intended to enable automated security analyses.
  • 4.4 Tamarin Models of 5G AKA: 5G AKA’s mutable, persistent SQN states over unbounded natural numbers make bounded-session verification impractical and exclude most verification tools.The protocol’s statefulness is one major source of modeling complexity.
  • 4.4.1 Challenges.: XOR-based concealment of SQNs further enlarges the search space because symbolic reasoning must handle associativity, commutativity, cancellation, and neutral elements.The authors describe this as a challenge for analyzing a large-scale real-world protocol.
  • 4.4.3 Our Models.: The model generalizes to other AKA-family protocols through localized modifications, with roughly 300 LoC for 5G AKA’s main protocol flow requiring adaptation.Other components, including role instantiation and compromise modeling, would largely remain unchanged.

5 SECURITY ANALYSIS

The formal analysis finds that 5G AKA violates several critical authentication and privacy goals under standard assumptions, while identifying binding-channel and key-confirmation conditions and proposing secure fixes.

  • Authentication: 5G AKA violates agreement on KSEAF between subscribers and SNs, including weak agreement from subscribers toward SNs, under the standard’s assumptions.The failures arise from an unbound SN–HN channel and sending SUPI separately from the earlier KSEAF-bearing message, allowing concurrent-session mismatches.
  • Authentication: Assuming the SN–HN channel is binding satisfies the previously violated properties under reasonable threat models.Table 3 reports the additional guarantees obtained for UEs and SNs under this assumption.
  • Key confirmation: A successful key-confirmation roundtrip is required for all subscriber-side agreement properties except weak agreement toward HNs.The standard does not require subscribers to wait for confirmation or define the roundtrip as part of authentication, postponing security to later procedures.
  • Privacy: 5G AKA keeps the SUPI confidential even against active attackers, but remains vulnerable to traceability attacks.An attacker can replay an SN message and distinguish a previously observed subscriber from a different one using Synchronization-failure versus MAC-failure responses.
  • Recommendations: The authors recommend explicit injective-agreement requirements, a binding SN–HN channel or sending ⟨SUPI, SUCI⟩, and protocol changes that make key confirmation unnecessary.These recommendations are presented as provably secure fixes while reducing required communications.

6 CONCLUSION · A NOTATIONS AND ACRONYMS

The paper formally analyzes 5G AKA, exposing underspecified goals and assumptions, violated properties, and weaknesses linked to implicit authentication and absent key confirmation. The conclusion also highlights tool-based analysis for evaluating protocol changes, while the appendices document terminology and message formats.

  • 6 CONCLUSION: The study formally analyzes one of the two 5G authentication methods, including its standard assumptions, security goals, formal protocol model, and automated Tamarin evaluation.The authors state that their models are substantially more detailed than those of previous work.
  • 6 CONCLUSION: The 5G standard underspecifies or omits security goals and assumptions, including agreement on the session key.The missing central goals are identified during the authors’ analysis of the standard.
  • 6 CONCLUSION: Tamarin shows that some security properties, especially session-key agreement, are violated without additional assumptions.The conclusion describes session-key agreement as a striking example of a violated agreement property.
  • 6 CONCLUSION: The authors critique implicit authentication and the lack of key confirmation because these design choices introduce protocol weaknesses.The critique concerns protocol use under the standard’s authentication design.
  • 6 CONCLUSION: Once a protocol model is constructed, tool-based analysis can quickly test standard changes and evaluate alternative design options.The authors present this as a major benefit of tool-based protocol-design analysis.
  • A NOTATIONS AND ACRONYMS: Table 6 describes the cryptographic message format while abstracting away AMF, other constants, and sub-message lengths.The table documents the message representation used in the paper.

B THE EAP-AKA’ PROTOCOL · C LOWE’S TAXONOMY AND TAMARIN MODELING · C.1 Introductory Example: Secrecy

The paper presents EAP-AKA’ and contrasts its key derivation and message flow with 5G AKA. It then introduces Lowe’s taxonomy and illustrates Tamarin secrecy modeling through SUPI confidentiality.

  • B THE EAP-AKA’ PROTOCOL: EAP-AKA’ derives KSEAF from KAUSF, as in 5G AKA, but derives KAUSF differently from the master key MK.The protocol description states that KSEAF is derived from KAUSF exactly as in 5G AKA, while KAUSF uses a different derivation.
  • B THE EAP-AKA’ PROTOCOL: KAUSF is defined as the substring MK[1152...1407], with MK derived using KDF operations over IK, CK, SNname, EAP-AKA’, and SUPI.The notation [x..y] denotes the substring from bit x to y.
  • B THE EAP-AKA’ PROTOCOL: EAP-AKA’ authenticates messages with AT_MAC, whose key is Kaut = MK[1152...1407].AT_MAC covers the other sub-messages in the same message.
  • B THE EAP-AKA’ PROTOCOL: Unlike 5G AKA, EAP-AKA’ binds xRES and SNname through their shared MAC rather than directly binding SNname to xRES.The challenge xRES does not directly bind SNname, but MACing both with Kaut de facto binds them together.
  • B THE EAP-AKA’ PROTOCOL: In EAP-AKA’, SN acts as a pass-through until HN authentication succeeds, then receives SUPI and KSEAF from HN.This differs from 5G AKA, where SN obtains KSEAF in the first message.
  • C LOWE’S TAXONOMY AND TAMARIN MODELING: Lowe’s taxonomy defines aliveness, recent aliveness, weak agreement, non-injective agreement, and injective agreement for protocol analysis.The paper first demonstrates property modeling in Tamarin, then models aliveness and non-injective agreement; the other properties follow similarly.
  • C.1 Introductory Example: Secrecy: The introductory Tamarin example models secrecy as the property that a subscriber’s SUPI is never revealed to the attacker.Claim_Secret(a,k) facts are produced when a subscriber or HN rule accesses or stores SUPI, while K(t) records attacker knowledge.

C.2 Aliveness

This section defines aliveness as a responder having previously run the protocol when an initiator completes a run apparently with that responder, and formalizes the property in Tamarin.

  • C.2 Aliveness: Aliveness requires that when initiator A completes a run apparently with responder B, B has previously been running the protocol.This is Lowe’s definition of aliveness.
  • C.2 Aliveness: The Tamarin model represents aliveness claims with Claim_commit(a,b, ⟨A, B⟩) and protocol-execution claims with Claim_running(b, B).Claim_commit records agent a’s claim that it established b’s aliveness, while Claim_running records b’s protocol run.
  • C.2 Aliveness: The formal definition models aliveness of role A towards role B using a trace formula over these claim facts.The property is stated as Definition C.2 in the Tamarin model.
  • C.2 Aliveness: Tamarin’s trace semantics make an explicit timestamp-order constraint unnecessary because a later Claim_running fact cannot satisfy the property in an execution prefix ending at Claim_commit.If Claim_running occurs only after Claim_commit, the prefix containing the commit but not the running fact falsifies the property.

C.3 Non-injective Agreement · D SECURITY ASSUMPTIONS AND GOALS · D.1 Security Assumptions and Threat Model

The paper defines non-injective agreement as an initiator–responder property requiring prior participation and agreement on specified data. It then frames 5G authentication security assumptions and goals as precise formal statements grounded in relevant 3GPP specifications.

  • C.3 Non-injective Agreement: Non-injective agreement requires an initiator that completes a run with an apparent responder to have a corresponding prior responder run.The responder must have been acting as responder and apparently communicating with the initiator.
  • C.3 Non-injective Agreement: The property additionally requires both agents to agree on the values of every specified variable in the data set ts.The set ts contains free variables appearing in the protocol description.
  • C.3 Non-injective Agreement: The non-injective-agreement example concerns a role A attempting to establish agreement on data t with a role B.The passage introduces this scenario before presenting its formal model.
  • C.3 Non-injective Agreement: Non-injective agreement on data t is modeled through a formal formula for role A toward role B.This formula is given as Definition C.3.
  • D SECURITY ASSUMPTIONS AND GOALS: The security-assumptions-and-goals section interprets authentication-relevant assumptions and goals as precise formal statements.It extends Section 3 and focuses on security assumptions and goals relevant to 5G authentication methods.
  • D.1 Security Assumptions and Threat Model: The interpretation is supported by excerpts from 3GPP Technical Specification and Technical Requirement documents.Earlier-generation 3G and 4G documents may also be cited when relevant.

D.1.1 Assumptions on Channels. · D.1.2 Assumptions on Cryptographic Primitives. · D.1.3 Assumptions on Parties.

The model assumes protected SN–HN core-network communication, hostile subscriber–SN radio channels, and specified protections for cryptographic functions. It further parameterizes guarantees by compromised network agents and parties, including compromised SNs, USIMs, and HNs.

  • D.1.1 Assumptions on Channels.: SN–HN communication is assumed to provide confidentiality, integrity, authenticity, and replay protection.These protections are specified for the E2E core network channel.
  • D.1.1 Assumptions on Channels.: E2E core-network interconnection security requires confidentiality and/or integrity between source and destination networks, with SEPPs at their edges.The requirement is attributed to TS 33.501, Section 5.9.3.
  • D.1.1 Assumptions on Channels.: The subscriber–SN radio channel permits passive eavesdropping and active manipulation, interception, and message injection.The analysis therefore considers active attackers unless explicitly stated otherwise.
  • D.1.2 Assumptions on Cryptographic Primitives.: The model assumes f1, f1*, f3, f4, f5, and f5* provide integrity and confidentiality, while f2 provides integrity.The standards do not explicitly specify these security requirements, and f1 and f1* are underspecified.
  • D.1.2 Assumptions on Cryptographic Primitives.: Analyses are parametrized by compromised scenarios, including attackers who compromise selected SNs and use their authenticated SN–HN channels to eavesdrop on or inject messages.In the worst case, a property holds only when the attacker cannot compromise any agent.
  • D.1.3 Assumptions on Parties.: The protocol’s increased-home-control feature is intended to prevent fraud such as registering a serving AMF that is absent from the visited network.This assumption is linked to TS 33.501, Section 6.1.4.1.
  • D.1.3 Assumptions on Parties.: Attackers may control genuine or compromised USIMs and, for compromised subscribers, access SUPI, K, and SQN.The attacker may also access K, skHN, and SUPI from compromised HNs.

D.1.4 Assumptions on Data Protection. · D.2 Security Requirements

The section states data-protection assumptions for subscriber credentials, sequence numbers, and the HN private key, then extracts and interprets the security goals that 5G-AKA should achieve under the 5G standard.

  • D.1.4 Assumptions on Data Protection.: Subscriber credentials, including K and SUPI, are assumed initially secret when held by uncompromised agents.The standards require credential integrity protection and K confidentiality protection in the UE through tamper-resistant secure hardware.
  • D.2 Security Requirements: Together, the requirements define a formal-analysis basis combining protected subscription data, assumptions about hidden state, and standards-derived 5G-AKA goals.
  • D.1.4 Assumptions on Data Protection.: The security-assessment scheme for tamper-resistant secure hardware is outside the scope of 3GPP specifications.
  • D.1.4 Assumptions on Data Protection.: SQN is a 48-bit counter, or a 43-bits counter in some situations, and is therefore guessable only with very low probability.The threat model assumes SQN is unknown when an attack starts, while the attacker knows how it increments during the attack.
  • D.1.4 Assumptions on Data Protection.: The model additionally assumes that the private asymmetric key skHN is initially private, although this assumption is not explicit in the specification.
  • D.2 Security Requirements: The analysis extracts and interprets the security goals that 5G-AKA should achieve according to the 5G standard.

D.2.1 Authentication Properties. · D.2.2 Confidentiality Properties.

The paper translates 5G’s semi-formal authentication claims into precise Lowe-taxonomy security goals modeled in Tamarin, covering relationships among subscribers, serving networks, and home networks. It also defines confidentiality requirements for KSEAF, including cross-session secrecy, while distinguishing them from forward and post-compromise secrecy.

  • D.2.1 Authentication Properties.: 5G authentication claims are formalized using Lowe’s taxonomy, whose four levels precisely characterize guarantees between protocol agents and map to Tamarin security definitions.The taxonomy includes aliveness and weak agreement among its authentication levels.
  • D.2.1 Authentication Properties.: The primary authentication and key agreement procedure must mutually authenticate the UE and network and establish the KSEAF anchor key for later security procedures.KSEAF is provided by the home network’s AUSF to the serving network’s SEAF.
  • D.2.1 Authentication Properties.: Subscribers must obtain non-injective agreement on SNname with authorized serving networks after key confirmation, while serving networks must obtain non-injective agreement on SUPI with subscribers.The specification treats some of these guarantees as implicit until an additional KSEAF key-confirmation roundtrip occurs.
  • D.2.1 Authentication Properties.: The UE’s serving-network authentication is limited to weak agreement with the SN after key confirmation and does not authenticate a particular entity, such as an AMF.The standard provides this authentication through successful later use of keys resulting from the agreement procedure.
  • D.2.1 Authentication Properties.: Serving networks must obtain non-injective agreement on SUPI with home networks, ensuring UE authorization through an authenticated subscription profile.The home network supplies the subscription profile on which serving-network authorization is based.
  • D.2.2 Confidentiality Properties.: 5G confidentiality should protect KSEAF, K, and skHN, and ensure that learning one session’s KSEAF does not reveal keys from previous or later sessions.The model considers these requirements directly for KSEAF rather than the complete key hierarchy.
  • D.2.2 Confidentiality Properties.: Backward security prevents deriving previous keys from a known current key, whereas forward security prevents predicting future keys, including keys after n or more handovers.These definitions are stated in the standards for general key sequences and illustrated for KgNB derivation.
  • D.2.2 Confidentiality Properties.: The paper distinguishes cross-session KSEAF confidentiality from forward secrecy and post-compromise secrecy, which do not hold in the later analysis.A session’s KSEAF should remain confidential even if the attacker learns KSEAF keys from every other session.

D.2.3 Privacy Properties.

The section formalizes 5G privacy requirements around SUPI and SQN confidentiality, and argues that authentication methods should provide subscriber anonymity and untraceability against passive attackers. It also highlights that existing 3G privacy requirements left anonymity and untraceability insufficiently defined.

  • Anonymity and Untraceability: Anonymity and untraceability were 3G requirements but were defined unclearly, motivating the section’s proposed formalization and its passive-attacker requirement for 5G.The section notes that 3G required these properties only against passive attackers.
  • Confidentiality of SUPI: 5G authentication must keep the SUPI secret because it uniquely identifies subscribers and enables location attacks.The standards define SUCI as a privacy-preserving identifier containing the concealed SUPI.
  • Confidentiality of SQN: SQN must remain secret because it can reveal authentication history, correlate with device age and activity, and support user tracing.The stated formal requirement protects SQN against passive attackers.

D.2.4 Other Properties.

This section covers key reuse, key separation, and bidding-down prevention as additional 5G security properties. Backward-compatibility properties are left for future work because they require analyzing 5G protocols together with older-generation authentication protocols.

  • Key reuse: Key reuse from SQN counter wraparound could enable attacks compromising encryption or forging message authentication codes.The analysis treats this concern through injective agreement on established KSEAF keys for different party pairs.
  • Backward compatibility: Backward-compatibility security goals are not analyzed because they require combining 5G authentication protocols with older-generation protocols.The paper leaves this analysis as future work.
  • Key separation: KSEAF shall be cryptographically separate from the earlier-generation key KASME and specific to UE–5G core authentication.
  • Bidding-down prevention: 5G shall prevent bidding-down attacks that make supported security features appear unsupported to the UE or network entities.
Loading 1806.10360v4…