{"id":"66054a29-6e43-45e5-89c9-66b9cf1193f4","arxiv_id":"2507.17491","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A stateless 5G AKA variant and a perfect-forward-secrecy extension pass ProVerif checks and add only small overhead over 5G-AKA.","lead":"This paper designs two upgraded 5G login-and-key protocols that drop the fragile sequence-number counter and give the second one extra protection for past sessions if long-term secrets leak. Both are formally checked with ProVerif and measured against the official 5G-AKA protocol.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Compatibility with existing USIMs is the load-bearing unsupported claim: the protocols require f1-f4 calls with non-standard inputs that the USIM command set does not expose, and the paper concedes this is experimentally unverified.","rationale":"The reader's conditionality is well-placed. The ProVerif analysis and the prototype code are genuine evidence that the protocol's security goals are met in a symbolic model and that the computational overhead is modest. However, the paper's central practical claim is compatibility with existing USIMs and infrastructure. This claim is load-bearing because it distinguishes the contribution from prior schemes (e.g., AKA-FS, Beyond-5G) that the paper itself marks as incompatible. The protocol's UE-side computation requires calling the 3GPP algorithms f1-f4 with inputs that are not available through the standardized USIM command interface. The long-term key k resides in the USIM, and the standard AUTHENTICATE command does not expose a general-purpose MAC/derivation function over arbitrary tuples. Therefore the proposed protocol cannot be executed by unmodified SIMs; it requires new USIM functionality. The manuscript itself acknowledges this in Remark 1 (UE/USIM abstraction) and Section VIII (compatibility 'not yet experimentally verified'), and Table I annotates the compatibility columns accordingly. This is an internal inconsistency, not merely an external disagreement: the abstract's 'fully compatible with existing SIM cards' is contradicted by the paper's own limitation statements. A concrete test, such as attempting to express the UE-side operations through TS 31.102 AUTHENTICATE commands, would settle the question. Until then, the CONDITIONAL verdict remains the right call: the security core is credible, but the headline compatibility claim needs to be softened to 'requires USIM software update' or supported by a real USIM implementation. I see no need to move the verdict.","tokens_in":22734,"tokens_out":19594,"duration_ms":207096,"concrete_test":"Implement the UE-side of Protocol I on a standard Java Card USIM simulator using only the TS 31.102 AUTHENTICATE command with 16-byte RAND and AUTN, without adding custom APDUs or applet code. If f1-f4 cannot be invoked with the inputs (kUE, R, IDSN) and (kUE, R), the compatibility claim is refuted. A complementary check: inspect the ProVerif model in the linked repository to see whether the UE process has direct access to k (i.e., the UE and USIM are a single entity); such a model proves security for an abstract UE that cannot be instantiated on an unmodified USIM.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's strongest claim is that both protocols are 'fully compatible with existing SIM cards and infrastructure.' This is load-bearing because it is the main differentiator from prior PFS schemes (AKA-FS, TSA-5G, 5G-AKA-FS), which the related-work table marks as USIM-incompatible. The protocols require the subscriber to compute MAC = f1(k, <kUE, R, IDSN>), RES = f2(k, <kUE, R>), CK = f3(k, <kUE, R>), IK = f4(k, <kUE, R>) (Protocol I) and analogous values with dhkey (Protocol II). The 3GPP USIM interface (TS 31.102) exposes only the AUTHENTICATE command, which takes a 16-byte RAND and optional AUTN and returns RES, CK, IK, or AUTS; it does not allow calling f1-f4 on an arbitrary tuple containing the ECIES-derived kUE and the UE-chosen R. Since k is stored only inside the USIM, the ME cannot compute these values itself. Therefore the protocol is implementable only if the USIM is updated with new commands or an operator-specific applet, contradicting 'fully compatible with existing SIM cards.' The paper's own Remark 1 abstracts UE and USIM as one entity, and the Conclusion (Section VIII) explicitly states that 'this compatibility has not yet been experimentally verified'; Table I also annotates the compatibility columns with 'not yet experimentally verified.' Thus the central deployment claim is both unsupported and inconsistent with the standardized USIM command set, regardless of the soundness of the ProVerif proofs.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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++.","tokens_in":23120,"tokens_out":9892,"duration_ms":105060,"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":[{"comment":"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.","section":"§V-B, Figs. 3-4, §VIII, Table I"},{"comment":"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.","section":"§VI-A, Remark 1"},{"comment":"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.","section":"§VII-B, Table V"}],"minor_comments":[{"comment":"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.","section":"Fig. 2"},{"comment":"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.","section":"§V-C, Fig. 4"},{"comment":"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.","section":"Table I"},{"comment":"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.","section":"Table II"}],"recommendation":"major_revision","confidential_remarks":"The main risk is the compatibility claim. If the authors cannot demonstrate that standard USIMs can execute the required f1-f4 calls, the manuscript should be reframed as a protocol requiring USIM applet or command-set changes, and the abstract, Table I, and conclusion should be revised accordingly. The formal verification appears competent and the implementation is a useful artifact, but the deployment claim is the principal differentiator and must be either substantiated or removed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: the core protocol design is genuinely new and the ProVerif artifacts are real, but the headline deployment claim doesn't survive contact with the USIM command set. The paper's own conclusion admits the compatibility is unverified; the stress-test note shows it's worse than unverified—the construction as written requires f1–f4 evaluations on inputs the standard AUTHENTICATE command never exposes.\n\nWhat's actually good: binding the UE challenge R inside the ECIES-encrypted SUCI is a clean way to make the protocol stateless, and reusing the ECIES ephemeral public key as DH material for PFS is a neat trick that avoids extra public-key operations. The ProVerif models cover the natural security goals—injective agreement on KSEAF, secrecy, indistinguishability—and the code is public. That's real evidence. The message-count reduction versus 5G-AKA is also real, and explicit key confirmation via kcMAC addresses a known 5G-AKA gap.\n\nSoft spots, in proportion. The USIM compatibility claim is the big one. Standard USIMs only expose AUTHENTICATE with a 16-byte RAND; they don't let the ME compute f1/f2/f3/f4 on a tuple containing the ECIES-derived kUE and the UE's own R. Since k never leaves the USIM, the ME can't compute those MACs or keys itself. So 'fully compatible with existing SIM cards' is not just unverified; it's likely inconsistent with TS 31.102 as it stands. The paper needs to either (a) scope the claim to updated USIMs with a new applet/command, or (b) show how it maps onto existing commands. That's a major revision, not a typo. Section VIII's admission is honest but doesn't fix the abstract and Table I.\n\nMinor: the performance table has no error bars and claims sub-percent differences; that needs repeated runs. The SN-side '48% increase' is a single hash, so fine. The comparison table annotations 'not yet experimentally verified' are appropriate.\n\nVerdict: the protocol logic and formal verification are worth taking seriously. This deserves peer review—it's not a desk reject—but the compatibility claim must be fixed before publication. I'd cite the stateless-challenge idea if the authors follow through, and I'd bring it to reading group as a case study in how formal verification can coexist with questionable platform assumptions.","headline":"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.","tokens_in":23622,"tokens_out":2307,"would_cite":true,"duration_ms":23532,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["5G-AKA","authentication and key agreement","perfect forward secrecy","stateless replay protection","active attack resistance","subscriber privacy","ProVerif","ECIES"],"falsifier":"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.","tokens_in":22582,"feed_emoji":"🔐","tokens_out":11212,"duration_ms":103843,"temperature":0.7,"pith_summary":"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.","feed_headline":"Stateless 5G-AKA beats replay attacks; variant adds forward secrecy","feed_subtitle":"Replay safety comes from bound random challenges; forward secrecy reuses ECIES' ephemeral key as DH.","key_machinery":"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.","core_discovery":"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].","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines the baseline 5G-AKA protocol and the security requirements that the new protocols are measured against.","marker":"[1]"},{"why":"Supplies the formal analysis of 5G-AKA that identifies active-attack exposure, missing key confirmation, and lack of forward secrecy, and whose requirement list the paper adopts.","marker":"[2]"},{"why":"Provides the component-based analysis and channel-binding assumptions that the paper's threat model borrows.","marker":"[3]"},{"why":"Shows the failure-message linkability attack that the mutually bound challenges are designed to defeat.","marker":"[5]"},{"why":"Shows the sequence-number inference attack that motivates dropping SQN-based freshness checking.","marker":"[7]"},{"why":"Demonstrates the encrypted-SUPI replay attack and prior AKA+ scheme that motivate active-attacker resistance and USIM compatibility constraints.","marker":"[8]"},{"why":"Documents the encrypted-SUPI replay attack that the paper's binding of R to SUCI is designed against.","marker":"[9]"},{"why":"Supplies the 5G-AKA' baseline, the standard-compatible active-attack fix the paper compares against and extends.","marker":"[13]"},{"why":"Names the ProVerif verifier used for the formal security analysis of both protocols.","marker":"[16]"},{"why":"Provides the Crypto++ library used to prototype both protocols and measure computation times.","marker":"[17]"}],"fun_headline_variants":["5G-AKA stateless fix removes replay risk","Mutual random challenges end 5G replay attacks","5G-AKA variant adds forward secrecy via ECIES","Stateless 5G-AKA keeps SIMs, drops sync burden","ProVerif verifies stateless 5G-AKA security"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["5G-AKA stateless fix removes replay risk","Mutual random challenges end 5G replay attacks","5G-AKA variant adds forward secrecy via ECIES","Stateless 5G-AKA keeps SIMs, drops sync burden","ProVerif verifies stateless 5G-AKA security"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000568,"raw_usage":{"total_tokens":2791,"prompt_tokens":1152,"completion_tokens":1639,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":768,"completion_tokens_details":{"reasoning_tokens":1554}},"tokens_in":768,"tokens_out":1639,"duration_ms":12365,"temperature":1.0,"reasoning_tokens":1554,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T14:48:14.197717+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"TS 33.501: Security Architecture and Procedures for 5G System- v18.5.0","cited_arxiv_id":null,"evidence_quote":"Defines the baseline 5G-AKA protocol and the security requirements that the new protocols are measured against."},{"cited_title":"Basin, J","cited_arxiv_id":null,"evidence_quote":"Supplies the formal analysis of 5G-AKA that identifies active-attack exposure, missing key confirmation, and lack of forward secrecy, and whose requirement list the paper adopts."},{"cited_title":"Cremers and M","cited_arxiv_id":null,"evidence_quote":"Provides the component-based analysis and channel-binding assumptions that the paper's threat model borrows."},{"cited_title":"Arapinis et al","cited_arxiv_id":null,"evidence_quote":"Shows the failure-message linkability attack that the mutually bound challenges are designed to defeat."},{"cited_title":"Borgaonkar, L","cited_arxiv_id":null,"evidence_quote":"Shows the sequence-number inference attack that motivates dropping SQN-based freshness checking."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Demonstrates the encrypted-SUPI replay attack and prior AKA+ scheme that motivate active-attacker resistance and USIM compatibility constraints."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Documents the encrypted-SUPI replay attack that the paper's binding of R to SUCI is designed against."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the 5G-AKA' baseline, the standard-compatible active-attack fix the paper compares against and extends."},{"cited_title":"Blanchet","cited_arxiv_id":null,"evidence_quote":"Names the ProVerif verifier used for the formal security analysis of both protocols."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the Crypto++ library used to prototype both protocols and measure computation times."}],"review_version":1}