Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification Techniques
The 5G-AKA protocol, a foundational component for 5G network authentication, has been found vulnerable to various security threats, including linkability attacks that compromise user privacy. To address these vulnerabilities, we previously proposed the 5G-AKA-Forward Secrecy (5G-AKA-FS) protocol, wh...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-12-01
|
| Series: | Sensors |
| Subjects: | |
| Online Access: | https://www.mdpi.com/1424-8220/24/24/7979 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | The 5G-AKA protocol, a foundational component for 5G network authentication, has been found vulnerable to various security threats, including linkability attacks that compromise user privacy. To address these vulnerabilities, we previously proposed the 5G-AKA-Forward Secrecy (5G-AKA-FS) protocol, which introduces an ephemeral key pair within the home network (HN) to support forward secrecy and prevent linkability attacks. However, a re-evaluation uncovered minor errors in the initial BAN-logic verification and highlighted the need for more rigorous security validation using formal methods. In this paper, we correct the BAN-logic verification and advance the formal security analysis by applying an extended SVO logic, which was adopted as it provides a higher level of verification compared to BAN logic, incorporating a new axiom specifically for forward secrecy. Additionally, we enhance the ProVerif analysis by employing a stronger adversarial model. These refinements in formal verification validate the security and reliability of 5G-AKA-FS, ensuring its resilience against advanced attacks. Our findings offer a comprehensive reference for future security protocol verification in 5G networks |
|---|---|
| ISSN: | 1424-8220 |