5G-AKA-HPQC: Hybrid Post-Quantum Cryptography Protocol for Quantum-Resilient 5G Primary Authentication with Forward Secrecy

Ilsun You; I Wayan Adi Juliawan Pawana; Yongho Ko

REVIEW 4 major objections 5 minor 2 cited by

5G-AKA-HPQC: Hybrid Post-Quantum Cryptography Protocol for Quantum-Resilient 5G Primary Authentication with Forward Secrecy

T0 review · 4 major / 5 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2502.02851 v1 pith:TCRQOOGU submitted 2025-02-05 cs.CR

Yongho Ko , I Wayan Adi Juliawan Pawana , Ilsun You This is my paper · ORCID

classification cs.CR

keywords 5G-AKApost-quantumcryptographyhybridkeyencapsulationmechanismX-WingforwardsecrecySUPIconcealmentSVOlogicProVerif

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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

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

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.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the 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.

The 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.

None 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.

Referee Report

4 major / 5 minor

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.

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 (4)

[Section III-B, Axiom 1 (PFSA)] 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 III-C, Hypotheses H1-H3 and Lemma 3] 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 III-D, Algorithms 1-6 and ProVerif reproducibility] 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.
[Abstract, Section IV, and Section V] 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.

minor comments (5)

[Section I-A, Table I] 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 III-C, RAND notation] 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 III-B] 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 II, Step 2.3] 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.
[Table IV] 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.

Circularity Check

2 steps flagged · score 8.0 of 10

The SVO verification is circular: PFS is concluded from a custom axiom whose consequent is PFS, and SUPI concealment is 'proved' using hypotheses H1-H3 that the derivation itself could not establish and whose later proof depends on H1.

self definitional [Section III-B (Extension of SVO Logic), Axiom 1; applied in Lemma 5 (Section III-C.6)]
"Axiom 1 (Perfect Forward Secrecy). The Perfect Forward Secrecy Axiom (PFSA) is designed to account for two cases. ... if the condition (i) and (ii) hold, then the key P F0( (P K) ←− − − − − →Q satisfies Perfect Forward Secrecy."

Lemma 5 proves PFS by saying: 'Based on the derivations (D3b) and (D5a) and supported by the novel perfect forward secrecy axiom, it is proved that the key ... achieves perfect forward secrecy.' The derivations D3b and D5a only express beliefs about ephemeral public keys; the property that the resulting key satisfies perfect forward secrecy is exactly the consequent of the newly added PFSA axiom. Thus the formal 'result' assumes the target property as an axiom instead of deriving it from the protocol's cryptographic construction.
other [Section III-C.5 (Derivation) and Lemma 3 (Section III-C.6)]
"The derivation (D13) and (D1c) cannot be extended further and concluded at this point. As a result, (H1) is introduced to continue the analysis. Similarly, (D17) and (D19) cannot be evolved further and must end here. Therefore, (H2) and (H3) are added to advance the analysis. (H1), (H2) and (H3) can be vulnerabilities in this protocol."

Lemma 3 states: 'Later the derivations (D56), (D57), and (D58) proves the hypothesis (H1), (H2) and (H3) respectively. This implies that the derivation (D1b) is held, stating that HN believes UE says SUPI.' But D56-D58 are derived from D54, which is derived through D53/D52/D51; D51 is 'HN believes UE ICK ←→ HN by (D1e), (A14), (A15), (D1e), (A51)', and D1e rests on D1d, which uses (H1) with the KA axiom. Hence the purported proof of H1-H3 depends on H1 itself. The assumptions introduced because the derivation stalled are later 'proven' only by a chain containing those same assumptions, so Lemma 3 does not independently establish SUPI concealment.

full rationale

The paper's central claim is that the protocol was 'rigorously verified using formal methods such as SVO Logic and ProVerif' (Abstract and Section V). The SVO analysis contains two load-bearing circular steps. First, Lemma 5 obtains perfect forward secrecy by invoking the custom PFSA axiom, whose consequent is precisely the PFS property; this makes the target result an axiom rather than a derivation. Second, the derivation stalls at D13/D17, and the authors introduce hypotheses H1-H3 to continue; Lemma 3 then claims D56-D58 prove those hypotheses, but D56-D58 sit downstream of D51-D1e-D1d, and D1d applies the KA axiom with (H1). The proof of H1 therefore uses H1, so the SUPI-concealment lemma is not established. The ProVerif material does not provide independent machine-checked confirmation in the manuscript: Algorithms 1-6 contain undefined functions such as 'letfun PQC Encaps(pubKey): bitstring, bitstring' and incomplete process syntax, and no tool output is reproduced in the paper. These observations concern the paper's principal verification claim, not a peripheral self-citation, so the appropriate score is high. The protocol design may still be worth cryptographic scrutiny, but the formal verification result as presented reduces, in its two key lemmas, to assumptions and an axiom that contain the conclusions.

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

The central security claims rest on standard crypto assumptions, one pre-provisioning assumption, an unenforced deletion assumption, and two paper-specific logical devices: the PFSA axiom and hypotheses H1-H3. The last two carry the PFS and mutual-authentication conclusions in SVO and are not derived from the protocol's own mechanics.

assumptions (7)

domain assumption X-Wing (ML-KEM-768 + X25519) is a secure hybrid KEM as specified by the IETF draft
Used in Section II as the cryptographic core; security is inherited from external standardization, not proven in this paper.
domain assumption The 5G AKA functions f1-f5, KDF (ANSI-X9.63, HMAC-SHA256) are secure
Inherited from 3GPP TS 33.501 and used unchanged in Steps 2.1 and 2.3.
domain assumption The HN's X-Wing public key PK_HN is pre-provisioned inside the USIM and remains authentic
Stated in Section II-A: 'the proposed protocol also assumes that the X-Wing pk of home network is stored inside the USIM.'
domain assumption UE's ephemeral private key skUE is deleted immediately after the protocol run
Section IV-F: 'the corresponding private key skUE is deleted immediately after the protocol execution'; no mechanism is specified to enforce this.
ad hoc to paper PFSA Axiom 1: belief in mutually-owned ephemeral public keys is sufficient to conclude PFS
Introduced in Section III-B specifically to let the SVO logic conclude perfect forward secrecy; this is the property under proof, not a standard SVO axiom.
ad hoc to paper H1, H2, H3: HN believes P Kδ(UE, pk2UE), a shared secret ss1UE exists, and pk2UE is fresh
Introduced in Section III-C after D13/D17 dead-end; the paper itself states these 'can be vulnerabilities.'
domain assumption Initial SVO state assumptions A11-A62 hold (parties believe their keys, SN-HN share Ksh, etc.)
Listed in Section III-C.1; these are standard protocol-environment assumptions, but they are asserted rather than derived.

how reviews work

0 comments

Cite this review

Pith. "Pith review of 5G-AKA-HPQC: Hybrid Post-Quantum Cryptography Protocol for Quantum-Resilient 5G Primary Authentication with Forward Secrecy." pith.science (2026). https://pith.science/paper/TCRQOOGU

@misc{pith2026250202851,
  author       = {Pith},
  title        = {Pith review of: 5G-AKA-HPQC: Hybrid Post-Quantum Cryptography Protocol for Quantum-Resilient 5G Primary Authentication with Forward Secrecy},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TCRQOOGU}},
  note         = {Machine review of arXiv:2502.02851}
}

read the original abstract

5G enables digital innovation by integrating diverse services, making security especially primary authentication crucial. Two standardized protocols, 5G AKA and EAP AKA', handle authentication for 3GPP and non 3GPP devices. However, 5G AKA has vulnerabilities, including linkability attacks. Additionally, quantum computing poses threats, requiring quantum resistant cryptography. While post-quantum cryptography (PQC) is being standardized, its real world robustness remains unproven. Conventional cryptographic schemes offer reliability due to decades of practical use. To bridge this gap, IETF is standardizing hybrid PQC (HPQC), combining classical and quantum resistant methods. Ensuring forward secrecy and quantum resilience in 5G-AKA is critical. To address these issues, we propose 5G AKA HPQC, a protocol maintaining compatibility with existing standards while enhancing security by integrating keys derived from Elliptic Curve Integrated Encryption Scheme (ECIES) and PQC Key Encapsulation Mechanism (KEM). We validate its security using SVO Logic and ProVerif, confirming its robustness. Performance evaluations assess computational and communication overheads, demonstrating a balance between security and efficiency. This research provides key insights into quantum-safe authentication, contributing to future standardization of secure mobile authentication protocols.

Figures

Figures reproduced from arXiv: 2502.02851 by the authors.

**Figure 2.** Formal verification categorization A. SVO Logic 1. Belief Axiom (BA) (P believes φ ∧ P believes(φ → ψ)) → P believes ψ [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

**Figure 3.** Verification result of ProVerif of 5G-AKA-HPQC Protocol. [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Future-Proofing Authentication Against Insecure Bootstrapping for 5G Networks: Feasibility, Resiliency, and Accountability
cs.CR 2025-10 reject novelty 5.0 of 10

BORG authenticates 5G SIB1 broadcasts with a compact hierarchical threshold signature, while showing NIST post-quantum signatures require impractical fragmentation — but its fail-stop forgery detection fails against D...
Analysis of Post-Quantum Cryptography in User Equipment in 5G and Beyond
cs.CR 2025-07 conditional novelty 4.0 of 10

In a virtual 5G setup, ML-KEM with ML-DSA gives the lowest handshake latency and CPU use, while SPHINCS+ and HQC add large overhead.

Reference graph

Works this paper leans on

10 extracted references · 10 canonical work pages · cited by 2 Pith papers

[1]

draft-connolly-cfrg-xwing-kem-06

X-Wing: general-purpose hybrid post-quantum KEM. draft-connolly-cfrg-xwing-kem-06. 2024. Available online: https://datatracker.ietf.org/doc/draft-connolly-cfrg-xwing-kem/ (accessed on 5 February 2025)

work page 2024
[2]

Requeset for Comments 7748

Elliptic Curves for Security. Requeset for Comments 7748. 2016. Avail- able online: https://datatracker.ietf.org/doc/html/rfc7748 (accessed on 5 February 2025)

work page 2016
[3]

draft-kampanakis-ml-kem- ikev2-09

Post-quantum Hybrid Key Exchange with ML-KEM in the Internet Key Exchange Protocol Version 2 (IKEv2). draft-kampanakis-ml-kem- ikev2-09. 2024. Available online: https://datatracker.ietf.org/doc/draft- kampanakis-ml-kem-ikev2/ (accessed on 5 February 2025)

work page 2024
[4]

On unifying some cryptographic protocol logics

Syverson, P.F.; van Oorschot, P.C. On unifying some cryptographic protocol logics. In Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, Oakland, CA, USA, 16–18 May 1994; pp. 14–28

work page 1994
[5]

Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif

Blanchet, B. Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. In Foundations of Security Analysis and Design VII; Springer: Cham, Switzerland, 2014; pp. 54–87

work page 2014
[6]

ISO/IEC 29128-1:2023

ISO. ISO/IEC 29128-1:2023. Information Security, Cybersecurity and Privacy Protection—Verification of Cryptographic Protocols—Part 1: Framework. Technical Report. The International Organization for Standardization: Geneva, Switzerland, 2023. Available online: https://standards.iteh.ai/catalog/standards/iso/5a8c7c4d-434f-4816-a4e0- b33660dd311c/iso-iec-291...

work page 2023
[7]

A Beyond-5G Authentication and Key Agreement Protocol

Damir, M.T.; Meskanen, T.; Ramezanian, S.; Niemi, V . A Beyond-5G Au- thentication and Key Agreement Protocol. arXiv 2022, arXiv:2207.06144

work page Pith review arXiv 2022
[8]

Requeset for Comments 9180

Hybrid Public Key Encryption. Requeset for Comments 9180. Internet Engineering Task Force. 2022. Available online: https://datatracker.ietf.org/doc/rfc9180/ (accessed on 5 February 2025)

work page 2022

Show all 10 references

[9]

Technical Report TS 33.501, 3rd Generation Partnership Project

Security Architecture and Procedure for 5G Systems. Technical Report TS 33.501, 3rd Generation Partnership Project. 2024. Available online: https://portal.3gpp.org/desktopmodules/Specifications/SpecificationDetail s.aspx?specificationId=3169 (accessed on 5 February 2025)

2024
[10]

Improved Extensible Authentication Protocol Method for 3GPP Mobile Network Authentication and Key Agreement (EAP-AKA’)

Arkko, J.; Lehtovirta, V .; Torvinen, V .; Eronen, P. Improved Extensible Authentication Protocol Method for 3GPP Mobile Network Authentication and Key Agreement (EAP-AKA’). Requeset for Comments 9048, Internet Engineering Task Force. 2021. Available online: https://datatracke...

2021

Pith tools

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

[1] [1]

draft-connolly-cfrg-xwing-kem-06

X-Wing: general-purpose hybrid post-quantum KEM. draft-connolly-cfrg-xwing-kem-06. 2024. Available online: https://datatracker.ietf.org/doc/draft-connolly-cfrg-xwing-kem/ (accessed on 5 February 2025)

work page 2024

[2] [2]

Requeset for Comments 7748

Elliptic Curves for Security. Requeset for Comments 7748. 2016. Avail- able online: https://datatracker.ietf.org/doc/html/rfc7748 (accessed on 5 February 2025)

work page 2016

[3] [3]

draft-kampanakis-ml-kem- ikev2-09

Post-quantum Hybrid Key Exchange with ML-KEM in the Internet Key Exchange Protocol Version 2 (IKEv2). draft-kampanakis-ml-kem- ikev2-09. 2024. Available online: https://datatracker.ietf.org/doc/draft- kampanakis-ml-kem-ikev2/ (accessed on 5 February 2025)

work page 2024

[4] [4]

On unifying some cryptographic protocol logics

Syverson, P.F.; van Oorschot, P.C. On unifying some cryptographic protocol logics. In Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, Oakland, CA, USA, 16–18 May 1994; pp. 14–28

work page 1994

[5] [5]

Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif

Blanchet, B. Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. In Foundations of Security Analysis and Design VII; Springer: Cham, Switzerland, 2014; pp. 54–87

work page 2014

[6] [6]

ISO/IEC 29128-1:2023

ISO. ISO/IEC 29128-1:2023. Information Security, Cybersecurity and Privacy Protection—Verification of Cryptographic Protocols—Part 1: Framework. Technical Report. The International Organization for Standardization: Geneva, Switzerland, 2023. Available online: https://standards.iteh.ai/catalog/standards/iso/5a8c7c4d-434f-4816-a4e0- b33660dd311c/iso-iec-291...

work page 2023

[7] [7]

A Beyond-5G Authentication and Key Agreement Protocol

Damir, M.T.; Meskanen, T.; Ramezanian, S.; Niemi, V . A Beyond-5G Au- thentication and Key Agreement Protocol. arXiv 2022, arXiv:2207.06144

work page Pith review arXiv 2022

[8] [8]

Requeset for Comments 9180

Hybrid Public Key Encryption. Requeset for Comments 9180. Internet Engineering Task Force. 2022. Available online: https://datatracker.ietf.org/doc/rfc9180/ (accessed on 5 February 2025)

work page 2022