{"id":"04c95095-3e9f-4e02-a8af-9ce3e7bf5fad","arxiv_id":"2502.02851","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"A hybrid post-quantum 5G authentication protocol combining X-Wing KEM with ECIES, claimed to provide mutual authentication, SUPI concealment, and forward secrecy, but with a circular formal proof.","lead":"5G-AKA-HPQC is a proposed 5G login protocol that wraps the post-quantum X-Wing key exchange around the standard 5G-AKA handshake to protect user identity and session keys. The authors use logic and model checking to argue for forward secrecy and quantum resistance, though the formal proof contains circular steps.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The SVO verification is not a proof: PFS and SUPI-concealment lemmas depend on unproven hypotheses H1-H3 and the custom PFSA axiom, so the 'rigorously verified' claim is unsupported.","rationale":"The reader's weakest_assumption identifies exactly the same load-bearing weakness: the SVO proof imports unproven hypotheses H1-H3 and a custom PFSA axiom that assumes forward secrecy, and then uses circular derivations to 'prove' those hypotheses. My independent reading confirms this. The paper itself flags H1-H3 as potential vulnerabilities, and the PFSA axiom is not a standard SVO rule but a bespoke inference that essentially grants the desired conclusion. The ProVerif section refers to a GitHub repository but no models or results are reproducible from the text; Algorithms 1-6 contain undefined functions (e.g., 'XWingKeyEncap', 'calc ue suci') and incomplete process code, so the claimed machine-checked verification cannot be audited. Because the strongest claim in the paper is that the protocol provides PFS and that this was rigorously verified, the circularity of the formal proof strikes at the heart of the contribution. The protocol design may be salvageable, but the submitted text does not support the central verification claim. I agree with the reader's REJECT and do not recommend changing the verdict.","tokens_in":22042,"tokens_out":5770,"duration_ms":51895,"concrete_test":"Re-run the SVO derivation from Section III-C with H1-H3 removed and with the PFSA axiom disabled; if Lemmas 3 and 5 cannot be re-derived, the verification is circular and the security claims are unsupported. Alternatively, encode the derivation in a proof assistant such as Coq and check whether Lemmas 1-5 go through without assuming H1-H3 or PFSA.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section III-C explicitly states after D13 and D17 that the derivation 'cannot be extended further' and that hypotheses H1, H2, H3 are introduced, with the authors themselves noting these 'can be vulnerabilities in this protocol.' Lemma 3 then claims to prove H1-H3 via D56-D58, but D56-D58 derive from D54, which uses D51, which uses D1e, which was obtained using H1-H3 (via D14-D16). This is a circular dependency, so the SUPI-concealment lemma is not established. Lemma 5 (PFS) rests entirely on the new PFSA axiom (Section III-B), a non-standard rule that infers perfect forward secrecy from the parties' beliefs about ownership of ephemeral keys rather than from the protocol's cryptographic properties. If PFSA is invalid, the PFS claim is unsupported. Since the abstract and Section V claim the protocol was 'rigorously verified using formal methods such as SVO Logic and ProVerif,' and the ProVerif models are not actually included (Algorithms 1-6 contain undefined functions and incomplete processes), the paper's central verification claim is not substantiated.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes 5G-AKA-HPQC, a modification of the 3GPP 5G-AKA primary authentication protocol that replaces the SUCI encryption and challenge-response key material with keys derived from X-Wing, a hybrid post-quantum KEM combining ML-KEM-768 and X25519. The protocol is intended to remain compatible with 5G-AKA while adding quantum resistance, SUPI concealment, and perfect forward secrecy for the anchor key KSEAF. The authors claim to validate the protocol with SVO logic and ProVerif, and they state that performance evaluations demonstrate a balance between security and efficiency. The central security claims are that mutual authentication, secure key exchange, SUPI concealment, resistance to malicious serving networks, and perfect forward secrecy are all achieved and formally verified.","tokens_in":22321,"tokens_out":5468,"duration_ms":50699,"significance":"If the claims were substantiated, the protocol would be a useful contribution: it applies a concrete, IETF-standardization-track hybrid KEM to 5G primary authentication, preserves the 3GPP message flow, and explicitly addresses linkability and long-term-key compromise. The idea of using the X-Wing ciphertext as the RAND and deriving HPK from the decapsulated secret is technically interesting and clearly presented at the protocol level. However, the significance is currently limited by the fact that the formal verification is not a proof as written: the SVO derivation depends on hypotheses the authors cannot derive and on a new axiom that essentially assumes perfect forward secrecy, and the ProVerif models are not included or reproducible. The promised performance evaluation is also absent. The paper's value is therefore mainly as a protocol proposal awaiting sound analysis rather than as a verified security result.","major_comments":[{"comment":"The Perfect Forward Secrecy Axiom is not a harmless extension of SVO logic; it assumes the property under proof. Axiom 1 states that if each party believes the other owns a subset of ephemeral public keys, then the derived key satisfies perfect forward secrecy. No cryptographic mechanism (e.g., ephemeral key deletion, DH security, KEM security, or a game-based reduction) is invoked. Lemma 5 then concludes PFS directly from PFSA applied to D3b and D5a. This is a circular step: the axiom's consequent is exactly the PFS claim that the verification is supposed to establish. Unless the axiom is replaced by a derivation from standard cryptographic assumptions or by a formal definition of PFS that is independent of the conclusion, the PFS claim in Section IV-F is unsupported.","section":"Section III-B, Axiom 1 (PFSA)"},{"comment":"The SVO derivation is explicitly stuck after D13 and D17: the text states that the derivation 'cannot be extended further' and that H1, H2, and H3 are introduced, with the authors' own annotation that these hypotheses 'can be vulnerabilities in this protocol.' Lemma 3 then claims to prove H1-H3 via D56-D58. However, D56-D58 are derived from D54, which uses D51, and D51 is derived from D1e, which itself was obtained using H1-H3 (through D14-D16 and D1d). The dependency is circular: the hypotheses are used to build D1e, and the same hypotheses are later 'proved' using a chain that passes through D1e. Consequently, the SUPI-concealment lemma and the derivations D1a-D1e that feed Lemma 1 (mutual authentication) and Lemma 2 (secure key exchange) are not established. The hypotheses must be discharged independently or removed from the proof.","section":"Section III-C, Hypotheses H1-H3 and Lemma 3"},{"comment":"The paper claims in Section III-D that the ProVerif models are publicly accessible through a GitHub repository, but no URL, repository name, or commit hash is provided anywhere in the manuscript. The pseudocode in Algorithms 1-6 is also incomplete and internally inconsistent: Algorithm 1 declares functions such as PQC Encaps, Encaps, and XWingKeyGen with no bodies; Algorithms 2-4 use undefined functions including calc ue suci, calc ue mac, calc hn key, XWingKeyDec, get hn keys4supi, and XWingKeyEnc; Algorithm 3 calls SHA with two arguments; Algorithm 4 contains syntactically invalid lines such as 'in(sch, , RES');' and 'if XRES' <> RES; true then exit;'. Algorithms 5 and 6 are both labeled 'Main Process without FS', even though one is intended to model the PFS scenario. The ProVerif results summarized in Table V and Figure 3 therefore cannot be reproduced or checked, and the central claim that the protocol was 'rigorously verified' with ProVerif is not substantiated.","section":"Section III-D, Algorithms 1-6 and ProVerif reproducibility"},{"comment":"The abstract and conclusions state that performance evaluations assess computational and communication overheads, and Section V mentions 'a comparative analysis was conducted to evaluate the security properties and computational/communication overheads.' However, the manuscript contains no performance evaluation: there are no benchmark measurements, no complexity tables, no communication-size calculations, and no comparison with 5G-AKA or EAP-AKA'. Section IV contains only security discussion, and no performance data appears in any figure or table. The claimed balance between security and efficiency is therefore unsupported by the current text.","section":"Abstract, Section IV, and Section V"}],"minor_comments":[{"comment":"There are multiple typos in the notation and running text, including 'Anonimity Key', 'secrete', 'Requeset for Comments', 'simbol X with 6 letter', and 'ars as follows'. The paper would benefit from a careful proofreading pass.","section":"Section I-A, Table I"},{"comment":"The SVO formalization writes RAND as ({ss1HN}pk1UE, pkHN), but in the protocol RAND is set to the X-Wing ciphertext cHN, whose second component is a fresh ephemeral ECDH public key generated inside X-Wing.Enc(), not the HN's long-term public key pkHN. This mismatch between the protocol description and the formal model should be reconciled, since PKδ(HN, pkHN) is used in several derivations.","section":"Section III-C, RAND notation"},{"comment":"The sentence introducing the PFSA axiom is duplicated verbatim ('New Axiom : We present the new axiom...'), and the notation 'P allows fps' is not defined in a way that connects it to a cryptographic definition of forward secrecy.","section":"Section III-B"},{"comment":"Step 2.3 lists '5) ME computes RES*...' immediately after a numbered item '4) Run the SIM card command...', but the SIM card subroutine itself contains steps 5-1 through 5-8; the numbering is confusing and should be cleaned up.","section":"Section II, Step 2.3"},{"comment":"Rows Q4 and Q5 are listed twice in the table, and the row labeled 'PFS supported issue True' is awkwardly worded; the query for PFS is expressed as a phase-1 disclosure rather than as a formal query, which makes the table hard to interpret.","section":"Table IV"}],"recommendation":"reject","confidential_remarks":"The manuscript's headline contribution is the claim of rigorous formal verification, but the SVO proof is circular and the ProVerif artifacts are not present. The PFSA axiom and the H1-H3 hypotheses are load-bearing, and the authors themselves flag them as potential vulnerabilities. Because these issues concern the central security claims and not just presentation, I do not think a revision within the normal review cycle can resolve them without essentially rewriting the security analysis. The missing performance evaluation further weakens the paper. I would recommend rejection, though the underlying protocol idea—using X-Wing ciphertext as RAND and deriving HPK from the decapsulated secret—may be worth pursuing in a future, properly analyzed submission."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The protocol design is genuinely new and worth studying. Using the X-Wing ciphertext as RAND, deriving HPK from a fresh UE key pair plus HN-side encapsulation, and folding it into the standard 5G-AKA message flow is a concrete, plausible construction. The authors are also candid about known problems: they admit the availability vulnerability from the missing SUCI freshness, and they flag H1-H3 as potential vulnerabilities. That honesty is a mark in their favor.\n\nThe problem is the verification. The SVO proof does not establish the two headline claims of PFS and SUPI concealment. The new PFSA axiom basically asserts that mutual belief in ephemeral key ownership gives forward secrecy, which is a strong assumption that needs cryptographic justification, not a primitive of SVO. The derivation stalls at D13/D17, and the added hypotheses H1-H3 are then \"proved\" through D56-D58, which trace back through D51 and D1e to the same hypotheses. That is circular. The ProVerif story is weaker still: there is no actual code, no GitHub link despite the text saying models are publicly accessible, and the algorithms are full of undefined functions (e.g., PQC_Encaps, XWingKeyGen). And the abstract promises performance evaluations, but the paper has none. So the two main selling points—rigorously verified security and balanced efficiency—are not supported by this submission.\n\nNone of this means the protocol is broken. It may well be sound. But the current text overclaims, and the evidence is not there. The paper would benefit from a serious referee: the design deserves attention, and the questions are timely for IETF/3GPP hybrid PQC discussions. I would send it to peer review, but with the expectation of major revision—or maybe rejection if the verification issues cannot be fixed. For a reading group, it is a useful case study of what counts as a formal proof and why unproven axioms and circular dependencies matter.","headline":"A concrete hybrid-PQC 5G-AKA design, but the claimed formal verification is circular and the performance results are missing; worth reviewing with major revision.","tokens_in":22802,"tokens_out":2145,"would_cite":false,"duration_ms":21203,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proposes 5G-AKA-HPQC, which claims to make 5G primary authentication quantum-resilient and forward-secret by deriving a hybrid key from X-Wing and ECIES, verified through SVO logic and ProVerif.","keywords":["5G-AKA","post-quantum cryptography","hybrid key encapsulation mechanism","X-Wing","forward secrecy","SUPI concealment","SVO logic","ProVerif"],"falsifier":"Run the ProVerif model exactly as specified but with the UE's ephemeral private key $sk_{UE}$ added to the phase-1 reveal along with $K$ and $sk_{HN}$; if the tool then demonstrates that an attacker can derive $HPK$ or $K_{SEAF}$, the forward-secrecy claim fails. Independently, delete the hypotheses H1-H3 from the SVO axiom set and re-run derivations D56-D58; if they do not go through, Lemma 3's proof of SUPI concealment is circular.","tokens_in":21843,"feed_emoji":"🔐","tokens_out":7216,"duration_ms":61836,"temperature":0.7,"pith_summary":"The paper proposes 5G-AKA-HPQC, an upgrade to the 5G primary authentication protocol that blends a classical elliptic-curve key exchange (ECIES) with the post-quantum hybrid KEM X-Wing. The protocol derives a hybrid key $HPK$ from the combined shared secrets, uses the X-Wing ciphertext itself as the random challenge $RAND$, and derives the anchor key $K_{SEAF}$ from $HPK$ together with the usual 5G-AKA key material. The central claims are that this preserves mutual authentication and SUPI concealment, resists a malicious serving network, and gives perfect forward secrecy: even if the long-term keys $K$ and $sk_{HN}$ are later compromised, past session keys remain secret. The authors back these claims with a hand-written SVO Logic proof and a ProVerif model, and they measure the added computational and communication overhead. If the claims hold, 5G networks can adopt hybrid post-quantum cryptography without changing the standard 3GPP message flow.","feed_headline":"Quantum-safe keys keep past 5G sessions secret","feed_subtitle":"A hybrid post-quantum X-Wing key is folded into 5G-AKA so future key leaks cannot expose old sessions.","key_machinery":"The load-bearing object is $HPK$, the Hybrid Public Key: a fresh key derived from the shared secret produced by X-Wing, the IETF hybrid post-quantum/traditional KEM that combines ML-KEM-768 with X25519 ECDH. The protocol's key trick is to set the challenge $RAND$ to the X-Wing ciphertext that the home network sends to the device, so that the same public value that drives the standard 5G-AKA functions also carries the quantum-safe key-agreement material. $HPK$ is then mixed into every authentication value and into the derivation of $K_{SEAF}$, which is what the paper claims converts the standard protocol into one with forward secrecy.","core_discovery":"On the paper's own terms, the discovery is that the 5G-AKA challenge-response can be made quantum-resilient and forward-secret by re-using the existing SUCI transmission as the first half of a hybrid key exchange. The UE encapsulates to the home network's X-Wing public key; the home network then encapsulates to the UE's freshly generated X-Wing public key, and the resulting ciphertext plays the role of $RAND$ in the standard challenge-response. Both parties derive the hybrid key $HPK$ from the X-Wing shared secret, and use $RAND \\oplus HPK$ in place of $RAND$ when computing $MAC$, $AK$, $CK$, $IK$, and $XRES$. The paper asserts that this construction, verified in SVO Logic and ProVerif, yields mutual authentication, SUPI concealment, resistance to malicious serving networks, and perfect forward secrecy of $HPK$ and of the anchor key $K_{SEAF}$, while remaining wire-compatible with the 3GPP 5G-AKA procedure.","pith_inferences":["The SVO proof is not self-contained: the authors introduce hypotheses H1-H3 at the points where the derivation cannot be extended further, and then prove those hypotheses later through derivations that themselves rely on the same hypotheses; a reader should treat the formal assertions as provisional until those hypotheses are derived or independently justified.","The protocol's compatibility goal comes at a price the paper acknowledges: the SUCI carries no freshness value, so the availability and linkability weaknesses of standard 5G-AKA are deliberately preserved, and a complete fix would likely require a non-standard protocol change.","The PFS guarantee rests on the UE deleting its ephemeral private key immediately after each run; making that deletion a physical property of the USIM is a deployment requirement, and any implementation that retains the key for debugging or roaming would void the guarantee.","The same hybrid-key construction would likely transfer to EAP-AKA' for non-3GPP access, since that protocol shares the same $K_{SEAF}$-derivation structure."],"forward_implications":["If the claims hold, 5G primary authentication can move to hybrid post-quantum security inside the existing 3GPP message sequence, avoiding a fork of the standard.","The SUPI stays concealed even against an adversary who later obtains the long-term keys, because the SUCI encryption key is derived from the fresh X-Wing encapsulation.","Compromise of the home network's long-term private key or the USIM's long-term key $K$ would not expose past $HPK$ or $K_{SEAF}$ values, so past sessions remain confidential.","A serving network that turns malicious cannot obtain the anchor key before the UE's response is verified by the home network, closing the early-key-exposure gap seen in faster AKA variants.","The added cost is one or two X-Wing encapsulation/decapsulation operations plus associated ciphertext bytes, a measurable but bounded overhead over plain 5G-AKA."],"supporting_citations":[{"why":"Supplies X-Wing, the hybrid PQ/T KEM (ML-KEM-768 plus X25519) that the protocol uses both for SUCI encryption and for the HPK negotiation.","marker":"[1]"},{"why":"Supplies the SVO modal logic framework used for the belief, authentication, and forward-secrecy derivations.","marker":"[4]"},{"why":"Supplies ProVerif, the symbolic verification tool used to run the security queries and attack-trace analysis.","marker":"[5]"},{"why":"Supplies the DMRN protocol, the efficiency-first AKA variant against which the malicious-SN behavior is compared.","marker":"[7]"},{"why":"Supplies the IETF HPKE context that motivates the hybrid post-quantum approach and the choice of X-Wing.","marker":"[8]"},{"why":"Supplies the 3GPP 5G-AKA standard, the compatibility target and the source of the f1-f5 functions and message flow.","marker":"[9]"},{"why":"Supplies EAP-AKA', the other standardized authentication protocol used as a baseline in the security and performance comparison.","marker":"[10]"}],"fun_headline_variants":["5G-AKA gets post-quantum upgrade with X-Wing hybrid keys","Hybrid X-Wing key gives 5G-AKA forward secrecy against quantum attacks","Post-quantum 5G-AKA: SUCI becomes key exchange for quantum-safe forward secrecy","X-Wing hybrid key folds into 5G-AKA to protect past sessions from quantum leaks","5G-AKA adds X-Wing hybrid key exchange for quantum-resistant forward secrecy"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The security proofs rest on three assumptions the authors could not derive from the protocol plus a new axiom that assumes that mutual belief in fresh ephemeral keys implies forward secrecy; the authors themselves write that those three assumptions can be vulnerabilities in this protocol.","fun_headline_variants_meta":{"raw":{"variants":["5G-AKA gets post-quantum upgrade with X-Wing hybrid keys","Hybrid X-Wing key gives 5G-AKA forward secrecy against quantum attacks","Post-quantum 5G-AKA: SUCI becomes key exchange for quantum-safe forward secrecy","X-Wing hybrid key folds into 5G-AKA to protect past sessions from quantum leaks","5G-AKA adds X-Wing hybrid key exchange for quantum-resistant forward secrecy"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000774,"raw_usage":{"total_tokens":3456,"prompt_tokens":1008,"completion_tokens":2448,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":624,"completion_tokens_details":{"reasoning_tokens":2334}},"tokens_in":624,"tokens_out":2448,"duration_ms":16591,"temperature":1.0,"reasoning_tokens":2334,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T10:52:29.250772+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the ProVerif model exactly as specified but with the UE's ephemeral private key $sk_{UE}$ added to the phase-1 reveal along with $K$ and $sk_{HN}$; if the tool then demonstrates that an attacker can derive $HPK$ or $K_{SEAF}$, the forward-secrecy claim fails. Independently, delete the hypotheses H1-H3 from the SVO axiom set and re-run derivations D56-D58; if they do not go through, Lemma 3's proof of SUPI concealment is circular.","supporting_citations":[{"cited_title":"draft-connolly-cfrg-xwing-kem-06","cited_arxiv_id":null,"evidence_quote":"Supplies X-Wing, the hybrid PQ/T KEM (ML-KEM-768 plus X25519) that the protocol uses both for SUCI encryption and for the HPK negotiation."},{"cited_title":"On unifying some cryptographic protocol logics","cited_arxiv_id":null,"evidence_quote":"Supplies the SVO modal logic framework used for the belief, authentication, and forward-secrecy derivations."},{"cited_title":"Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif","cited_arxiv_id":null,"evidence_quote":"Supplies ProVerif, the symbolic verification tool used to run the security queries and attack-trace analysis."},{"cited_title":"A Beyond-5G Authentication and Key Agreement Protocol","cited_arxiv_id":"2207.06144","evidence_quote":"Supplies the DMRN protocol, the efficiency-first AKA variant against which the malicious-SN behavior is compared."},{"cited_title":"Requeset for Comments 9180","cited_arxiv_id":null,"evidence_quote":"Supplies the IETF HPKE context that motivates the hybrid post-quantum approach and the choice of X-Wing."},{"cited_title":"Technical Report TS 33.501, 3rd Generation Partnership Project","cited_arxiv_id":null,"evidence_quote":"Supplies the 3GPP 5G-AKA standard, the compatibility target and the source of the f1-f5 functions and message flow."},{"cited_title":"Improved Extensible Authentication Protocol Method for 3GPP Mobile Network Authentication and Key Agreement (EAP-AKA’)","cited_arxiv_id":null,"evidence_quote":"Supplies EAP-AKA', the other standardized authentication protocol used as a baseline in the security and performance comparison."}],"review_version":1}