Pith. sign in

REVIEW 3 major objections 4 minor 34 references

Active Attack Resilience in 5G: A New Take on Authentication and Key Agreement

T0 review · 3 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Pith's one-line read The paper claims two redesigned 5G-AKA protocols meet all major 3GPP and academic security requirements, resist passive and active attacks, remove sequence-number resync, and give one variant perfect forward secrecy while staying…

desk verdict Useful ProVerif-backed AKA variants with a genuinely stateless design, but the central 'works with existing SIMs' claim is probably false and is explicitly unverified. read the letter →

arxiv 2507.17491 v2 pith:B3IJXMED submitted 2025-07-23 cs.CR cs.NI

classification cs.CRcs.NI
keywords 5G-AKAauthenticationandkeyagreementperfectforwardsecrecystatelessreplayprotectionactiveattackresistancesubscriberprivacyProVerifECIES
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

5G-AKA, the 3GPP-standard authentication and key agreement protocol, has three known weaknesses: it is designed mainly against passive eavesdroppers, it needs an in-sync sequence number to stop replay, and it has no perfect forward secrecy. The paper argues all three can be fixed without leaving the 3GPP cryptographic toolbox or replacing SIM cards. Protocol I turns the one-sided home-network challenge into a pair of mutually bound random challenges, so replay freshness no longer needs sequence numbers; Protocol II reuses the ECIES ephemeral key as Diffie-Hellman material to add forward secrecy. The paper reports ProVerif verification and a prototype showing the requirements are met at minor computational cost. It also states in the conclusion that compatibility with existing SIM cards has not yet been experimentally verified.

What carries the argument

The load-bearing mechanism is the mutual binding of two fresh random challenges plus, for forward secrecy, the doubling of the ECIES ephemeral key as Diffie-Hellman material. In Protocol I the subscriber's random $R$ is encrypted inside SUCI and authenticated with a MAC from the long-term key $k$; the home network returns $R_{\mathrm{HN}}$ with a MAC computed from $K_{\mathrm{SEAF}}$ that also serves as key confirmation. Protocol II has both sides derive a session secret $dhkey$ from $C_0$ and $R_{\mathrm{HN}}$ before computing $K_{\mathrm{SEAF}}$, so the finished key cannot be reconstructed from long-term secrets alone. This is what replaces the sequence-number freshness check and what blocks the known linkability attacks.

What would settle it

Run both protocols on a real 5G USIM through the standardized card command interface and check whether f1-f4 can be called with the non-standard inputs (the ECIES-derived $k_{\mathrm{UE}}$, the random $R$, and $ID_{\mathrm{SN}}$) and whether the card returns RES plus the key-confirmation MAC. If the card cannot, the compatibility claim fails. A complementary falsifier is a ProVerif model in which the UE and USIM are separate processes and SUCI can be produced on the host device; if subscriber indistinguishability is lost, the active-attack guarantee depends on the paper's trust-boundary assumption.

Watch

Extended reading notes

Core claim

The paper's central discovery is that the two structural weaknesses it identifies in 5G-AKA are fixable within the 3GPP primitive set. It replaces the home network's sequence-number freshness check with a pair of mutually bound random challenges: the subscriber sends its own random $R$ inside the ECIES-encrypted SUCI together with a MAC computed with the long-term key $k$, and the home network returns its random $R_{\mathrm{HN}}$ together with a MAC that doubles as key confirmation of $K_{\mathrm{SEAF}}$. Because each run's messages are bound to both challenges, replaying a captured SUCI or challenge produces a MAC failure rather than a distinguishable synchronization failure. Protocol II reuses the ECIES ephemeral public key $C_0$ as Diffie-Hellman material, so the anchor key is derived from an ephemeral shared secret; the paper states that a later compromise of $k$ and the home network's private key then does not expose past $K_{\mathrm{SEAF}}$ values. The paper reports that ProVerif confirms injective agreement on $K_{\mathrm{SEAF}}$, secrecy of $K_{\mathrm{SEAF}}$ and SUPI, subscriber indistinguishability under an active attacker, and PFS for Protocol II. It claims both protocols therefore meet the security requirements of the 3GPP standard and of the formal analysis in [2].

Load-bearing premise

The whole compatibility claim rests on the unverified premise that today's SIM cards can execute the protocol's modified challenge-response steps: the formal model treats the phone and the SIM as one unit, and the paper's conclusion says that compatibility has not yet been experimentally verified.

Editorial extensions

If this is right

  • Operators that adopt Protocol I can remove sequence-number resynchronization entirely, cutting the authentication flow from 13 or 9 messages to 7 and eliminating a whole class of desynchronization failures.
  • Protocol II gives a concrete forward-secrecy upgrade path: past session keys are safe even if a subscriber's long-term key and the home network's private key are both later compromised.
  • Because the two challenges are bound to the same run, the known failure-message, sequence-number-inference, and encrypted-SUPI replay attacks no longer yield a distinguishing response.
  • The measured cost is modest at the user device, within 0.13% of 5G-AKA for Protocol II, at the price of roughly doubling the serving network's hashing work and raising home-network cost by about 21%.
  • If the compatibility claim holds, both protocols need only software changes on the subscriber, serving network, and home network, avoiding the SIM replacement that prior PFS-oriented AKA designs required.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper leaves implicit that the stateless design may save more on lossy radio links than the message count suggests: without SQN, a failed run no longer triggers a resynchronization round, so link-level retransmission, not protocol restart, becomes the recovery path.
  • The same idea of reusing the ECIES ephemeral public key as DH material could be exported to other identity-concealing authentication designs that already pay for ECIES, giving them forward secrecy at essentially zero extra public-key operations.
  • The security proof's sensitivity to the UE-versus-USIM boundary is a natural next test: if operators generate SUCI on the host device, the paper's Remark 1 suggests the trust boundary shifts and the indistinguishability result may need to be re-proved.
  • A field experiment comparing authentication success rates of Protocol I, 5G-AKA, and 5G-AKA' under controlled packet loss would tell whether the operational overhead comparison favors the stateless design in practice.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes two 5G authentication and key agreement protocols. Protocol I removes the sequence-number-based replay protection of 5G-AKA by having the subscriber generate a random challenge R inside an ECIES-encrypted SUCI and by binding all subsequent authentication messages to that challenge; Protocol II extends Protocol I with an ephemeral Diffie-Hellman exchange that reuses the ECIES ephemeral public key to provide perfect forward secrecy. The authors verify both protocols with ProVerif for mutual authentication, key secrecy, subscriber indistinguishability, and, for Protocol II, PFS, and they report a performance comparison against 5G-AKA and 5G-AKA' implemented with Crypto++.

Significance. If the security and compatibility claims are substantiated, the paper makes a useful contribution: a stateless 5G AKA variant with active-attacker resilience and a PFS extension at small reported overhead, backed by machine-checkable ProVerif proofs and a reproducible implementation. The formal verification and the careful comparison with prior AKA enhancements are strengths. The central unresolved issue is the claim of compatibility with existing USIM cards. The protocols require f1-f4 to be evaluated on inputs that the standard USIM command interface does not expose, and the paper itself concedes that compatibility has not been experimentally verified. Unless that claim can be established, the contribution reduces to a protocol variant requiring USIM-applet or command-set changes, which would place it closer to the prior PFS schemes that Table I distinguishes it from.

major comments (3)
  1. [§V-B, Figs. 3-4, §VIII, Table I] The claim that the protocols are 'fully compatible with existing SIM cards' is not supported by the protocol definitions. Protocol I requires the subscriber to compute MAC=f1(k,<kUE,R,IDSN>), RES=f2(k,<kUE,R>), CK=f3(k,<kUE,R>), and IK=f4(k,<kUE,R>), and Protocol II similarly uses f1-f4 with kUE and the ECIES ephemeral public key as inputs. In a standard USIM, the long-term key k is accessible only inside the card, and the USIM command interface referenced through the paper's own discussion of TS 31.121/TS 33.501 exposes the AUTHENTICATE command with a 16-byte RAND and optional AUTN, returning RES/CK/IK or AUTS; it does not allow f1-f4 to be evaluated on an arbitrary tuple containing an ECIES-derived kUE, an internally chosen R, and IDSN. The mobile equipment cannot compute these values itself because it does not know k. The protocols therefore require either new USIM commands or an operator-specific applet, contradicting the abstract's and conclusion's compatibility claim. Table I marks the USIM compatibility column as 'not yet experimentally verified,' and §VIII explicitly states that compatibility has not been experimentally verified. Because Table I presents USIM compatibility as the main differentiator from AKA-FS, TSA-5G, and 5G-AKA-FS, this issue is load-bearing.
  2. [§VI-A, Remark 1] The ProVerif model treats the subscriber as a single process containing both UE and USIM, abstracting away exactly the trust boundary on which the compatibility claim depends. This is acknowledged in Remark 1, but the implication is not addressed: if the protocol is adapted to work through the standard USIM command interface, the trust boundary and the set of values available to the USIM and to the mobile equipment change, and the formal analysis would need to be redone for that adapted protocol. As written, the security proofs do not cover attacks that exploit the SIM-UE interface, even though Remark 1 itself cites SecureSIM and SIMurai to argue that such attacks are realistic in current deployments.
  3. [§VII-B, Table V] The performance comparison is presented as exact microsecond values with claimed differences of 0.05% and 0.13% at the subscriber side, but the paper reports no error bars, standard deviations, number of repetitions, or details of the measurement methodology beyond the use of the CHRONO library. At these sub-percent levels, the differences are within plausible measurement noise, so the claim of 'minor computational overhead' is not yet quantitatively supported. The authors should report statistics over many runs and ideally a sensitivity analysis with respect to hardware and network conditions.
minor comments (4)
  1. [Fig. 2] Figure 2 appears to be an unfinished screenshot from a diagramming tool, including UI artifacts such as '88% Give Feedback to Microsoft' and a ribbon menu; it should be replaced with a clean architecture diagram.
  2. [§V-C, Fig. 4] In Protocol II, the inputs to f1-f4 change from R in Protocol I to C0, and C1 is no longer bound to R in the encrypted payload; the text does not explain this change. Please justify the modification or correct the inconsistency between the textual description and the figure.
  3. [Table I] The table footnote uses the same ✓ symbol for both 'property supported by the protocol' and 'functionality required by the protocol,' which is confusing; please use distinct symbols or separate columns.
  4. [Table II] Table II is difficult to parse: the row 'Agreement on KSEAF I I I I I I' does not indicate which pair of parties each 'I' refers to, and the same ambiguity affects the rows for IDSN and SUPI. Please restructure the table or add a clearer legend.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: the ProVerif security analysis is self-contained and the performance comparison is measured; the unverified USIM compatibility claim is a missing experimental support, not a circular step.

full rationale

The paper's claimed derivation chain is not circular. The security requirements are taken from external sources (3GPP TS 33.501, Basin et al. CCS'18, Lowe's authentication taxonomy) and encoded as ProVerif queries under a Dolev-Yao attacker; there are no fitted parameters, no quantity estimated from a subset of data and then relabeled as a prediction, and no load-bearing self-citation chain. The PFS result for Protocol II is obtained from a standard Diffie-Hellman modeling equation (exp(exp(g,x),y)=exp(exp(g,y),x)) and from attacker knowledge of long-term keys, not from the property being proved. The one notable unsupported assertion is compatibility with existing USIMs: both protocols call f1-f4 on non-standard tuples such as <kUE,R,IDSN> (Figures 3-4), which the standardized USIM AUTHENTICATE command does not expose, and the paper itself concedes in Section VIII that 'this compatibility has not yet been experimentally verified' and in Table I that the compatibility columns are 'not yet experimentally verified.' That is a deployment/correctness gap, not an equivalence of output to input, so it does not constitute circularity and does not raise the circularity score beyond 1.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The security claims rest on standard cryptographic hardness assumptions and on two deployment assumptions (private SN-HN channel, USIM-resident SUCI generation). The USIM assumption is the most fragile and is unverified.

assumptions (4)
  • domain assumption Cryptographic primitives f1-f4, KDF, SHA256, and ECIES are ideal (perfect one-way and unforgeable) as modeled in ProVerif.
    Modeling choices in Section VI-A treat these as constructors with no algebraic weaknesses; real instances might not match.
  • domain assumption Computational Diffie-Hellman holds for the curve used (SECP 256 R1 in implementation) for Protocol II's PFS.
    The PFS claim in Protocol II relies on the inability to compute RHN*C0 from C0, dhHN, and skHN.
  • domain assumption The SN-HN channel is authenticated and private, and messages are bound to a unique session ID.
    Stated in Section IV-B; inherited from 3GPP and prior analysis [3].
  • ad hoc to paper UE and USIM are a single entity, and SUCI is generated inside the USIM without exposing SUPI on the SIM-UE interface.
    Remark 1 in Section IV-A; this sidesteps the known SIM-UE attack surface and is not true for all deployments.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Active Attack Resilience in 5G: A New Take on Authentication and Key Agreement." pith.science (2026). https://pith.science/paper/B3IJXMED

@misc{pith2026250717491,
  author       = {Pith},
  title        = {Pith review of: Active Attack Resilience in 5G: A New Take on Authentication and Key Agreement},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/B3IJXMED}},
  note         = {Machine review of arXiv:2507.17491}
}
read the original abstract

As 5G networks expand into critical infrastructure, secure and efficient user authentication is more important than ever. The 5G-AKA protocol, standardized by 3GPP in TS 33.501, is central to authentication in current 5G deployments. It provides mutual authentication, user privacy, and key secrecy. However, despite its adoption, 5G-AKA has known limitations in both security and performance. While it focuses on protecting privacy against passive attackers, recent studies show its vulnerabilities to active attacks. It also relies on a sequence number mechanism to prevent replay attacks, requiring perfect synchronization between the device and the core network. This stateful design adds complexity, causes desynchronization, and incurs extra communication overhead. More critically, 5G-AKA lacks Perfect Forward Secrecy (PFS), exposing past communications if long-term keys are compromised-an increasing concern amid sophisticated threats. This paper proposes an enhanced authentication protocol that builds on 5G-AKA's design while addressing its shortcomings. First, we introduce a stateless version that removes sequence number reliance, reducing complexity while staying compatible with existing SIM cards and infrastructure. We then extend this design to add PFS with minimal cryptographic overhead. Both protocols are rigorously analyzed using ProVerif, confirming their compliance with all major security requirements, including resistance to passive and active attacks, as well as those defined by 3GPP and academic studies. We also prototype both protocols and evaluate their performance against 5G-AKA and 5G-AKA' (USENIX'21). Our results show the proposed protocols offer stronger security with only minor computational overhead, making them practical, future-ready solutions for 5G and beyond.

Figures

Figures reproduced from arXiv: 2507.17491 by the authors.

Figure 1
Figure 1. A high-level overview of the 5G-AKA protocol, where dotted and solid arrows represent open channels and authenticated [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Overall Architecture, where dotted and solid arrows [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. A high-level overview of our protocol I, where dotted and solid arrows represent open channels and authenticated [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: A high-level overview of our protocol II, where dotted and solid arrows represent open channels and authenticated [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages

  1. [1]

    TS 33.501: Security Architecture and Procedures for 5G System- v18.5.0

    3GPP. TS 33.501: Security Architecture and Procedures for 5G System- v18.5.0. 2024, https://portal.3gpp.org/desktopmodules/Specifications/ SpecificationDetails.aspx?specificationId=3169, [Accessed: 4-April- 2024]

  2. [2]

    Basin, J

    D. Basin, J. Dreier, L. Hirschi, S. Radomirovic, R. Sasse, and V . Stettler. A Formal Analysis of 5G Authentication. In Proc. of the 2018 ACM CCS, page 1383–1396, 2018

  3. [3]

    Cremers and M

    C. Cremers and M. Dehnel-Wild. Component-based formal analysis of 5G-AKA: Channel assumptions and session confusion. In Proc. of the NDSS, 2019

  4. [4]

    Miller, I

    R. Miller, I. Boureanu, S. Wesemeyer, and C. J. P. Newton. The 5G Key- Establishment Stack: In-Depth Formal Verification and Experimentation. In Proceedings of the 2022 ACM on Asia Conference on Computer and Communications Security, ASIA CCS ’22, page 237–251, 2022

  5. [5]

    Arapinis et al

    M. Arapinis et al. New privacy issues in mobile telephony: fix and verification. In Proceedings of the 2012 ACM Conference on Computer and Communications Security , CCS ’12, page 205–216, 2012

  6. [6]

    M. S. A. Khan and C. J. Mitchell. ”improving air interface user privacy in mobile telephony”. In Security Standardisation Research, pages 165– 184, Cham, 2015. Springer International Publishing

  7. [7]

    Borgaonkar, L

    R. Borgaonkar, L. Hirschi, S. Park, and A. Shaik. New Privacy Threat on 3G, 4G, and Upcoming 5G AKA Protocols. Proc. of PETS , 2019(3):108–127, 2019

  8. [8]

    A. Koutsos. The 5G-AKA Authentication Protocol Privacy. In 2019 IEEE European Symposium on Security and Privacy (EuroS&P) , pages 464–479, 2019

Show all 34 references
  1. [9]

    P. A. Fouque, C. Onete, and B. Richard. Achieving Better Privacy for the 3GPP AKA Protocol. In Proceedings on PoPETs’16, page 255–275, 2016

  2. [10]

    Free 5GC - Link the World, https://www.free5gc.org/ [Accessed: 4th Sept. 2024]

  3. [11]

    Open5gcore - the next mobile core network testbed plat- form, https: //www.open5gcore.org/ [Online Access: 4th Sept. 2024]

  4. [12]

    Open5gcore - the next mobile core network testbed plat- form, https: //www.openairinterface.org/ [Online Access: 4th Sept. 2024]

  5. [13]

    Y . Wang, Z. Zhang, and Y . Xie. Privacy-Preserving and Standard- Compatible AKA Protocol for 5G. In 30th USENIX Security Symposium (USENIX Security 21) , pages 3595–3612. USENIX Association, Aug. 2021

  6. [14]

    A. Braeken. Symmetric key based 5G AKA authentication protocol sat- isfying anonymity and unlinkability. Computer Networks, 181:107424, 2020

  7. [15]

    Munilla, M

    J. Munilla, M. Burmester, and R. Barco. An enhanced symmetric-key based 5G-AKA protocol. Computer Networks, 198:108373, 2021

  8. [16]

    Blanchet

    B. Blanchet. ”Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif” , pages 54–87. 2014

  9. [17]

    https://www.cryptopp.com/ [Online Access: 4th Sept. 2024]

  10. [18]

    M. Khan, P. Ginzboorg, K. J ¨arvinen, and V . Niemi. ”defeating the downgrade attack on identity privacy in 5g”. In Security Standardisation Research, pages 95–119, Cham, 2018. Springer International Publishing

  11. [19]

    van den Broek, R

    F. van den Broek, R. Verdult, and J. de Ruiter. Defeating IMSI Catchers. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS ’15, page 340–351, 2015

  12. [20]

    Arkko, K

    J. Arkko, K. Norrman, M. N ¨aslund, and B. Sahlin. A USIM Compatible 5G AKA Protocol with Perfect Forward Secrecy. In 2015 IEEE Trustcom/BigDataSE/ISPA, volume 1, pages 1205–1209, 2015

  13. [21]

    F. Liu, J. Peng, and M. Zuo. Toward a Secure Access to 5G Network. In 2018 17th IEEE TrustCom/BigDataSE , pages 1121–1128, 2018

  14. [22]

    You et al

    I. You et al. 5G-AKA-FS: A 5G Authentication and Key Agreement Protocol for Forward Secrecy. Sensors, 24(1), 2024

  15. [23]

    M. T. Damir et al. A Beyond-5G Authentication and Key Agreement Protocol. In Network and System Security , pages 249–264, 2022

  16. [24]

    https://github.com/tamarin-prover/tamarin-prover, [Accessed: 14- Aug.- 2024]

    Tamarin (develop). https://github.com/tamarin-prover/tamarin-prover, [Accessed: 14- Aug.- 2024]

  17. [25]

    TR 33.902: Formal Analysis of the 3G Authentication Protocol (Release 4), Sept

    3GPP. TR 33.902: Formal Analysis of the 3G Authentication Protocol (Release 4), Sept. 2001. https://portal.3gpp.org/desktopmodules/ Specifications/SpecificationDetails.aspx?specificationId=2337, [Accessed: 14- Aug.- 2024]

  18. [26]

    3GPP TS 31.121: UICC- terminal interface; Universal Subscriber Identity Module (USIM) appli- cation test specification

    3rd Generation Partnership Project (3GPP). 3GPP TS 31.121: UICC- terminal interface; Universal Subscriber Identity Module (USIM) appli- cation test specification. https://www.3gpp.org/DynaReport/31121.htm,

  19. [27]

    J. Zhao, B. Ding, Y . Guo, Z. Tan, and S. Lu. Securesim: rethinking authentication and access control for sim/esim. In Proceedings of the 27th Annual International Conference on Mobile Computing and Networking, MobiCom ’21, page 451–464, 2021

  20. [28]

    T. P. Lisowski, M. Chlosta, J. Wang, and M. Muench. SIMurai: Slicing through the complexity of SIM card security research. In 33rd USENIX Security Symposium (USENIX Security 24) , pages 4481–4498. USENIX Association, Aug. 2024

  21. [29]

    3GPP TS 33.105: 3G Security; Cryptographic algorithm requirements

    3rd Generation Partnership Project (3GPP). 3GPP TS 33.105: 3G Security; Cryptographic algorithm requirements. https: //portal.3gpp.org/desktopmodules/Specifications/SpecificationDetails. aspx?specificationId=2264, 2024. Version 18.0.0

  22. [30]

    V . Shoup. A Proposal for an ISO Standard for Public Key Encryption. Cryptology ePrint Archive, Paper 2001/112, 2001. https://eprint.iacr.org/ 2001/112

  23. [31]

    G. Lowe. A hierarchy of authentication specifications. In Proceedings 10th Computer Security Foundations Workshop , pages 31–43, 1997

  24. [32]

    https://bblanche.gitlabpages.inria.fr/proverif/

    ProVerif 2.05. https://bblanche.gitlabpages.inria.fr/proverif/

  25. [33]

    Dolev and A

    D. Dolev and A. Yao. On the Security of Public Key Protocols. IEEE Transactions on Information Theory , 29(2):198–208, 1983

  26. [34]

    https://github.com/yhirose/cpp-httplib [Online Access: 4th Sept. 2024]. APPENDIX A ELLIPTIC CURVE INTEGRATED ENCRYPTION SCHEME (ECIES) [30] 5G uses ECIES cryptographic primitive to protect the unique identity of the subscribers (please refer to 3GPP TS 33.501 [1]). ECIES is a ...

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.