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!
|
| _version_ | 1850086814382030848 |
|---|---|
| author | Yongho Ko I Wayan Adi Juliawan Pawana Ilsun You |
| author_facet | Yongho Ko I Wayan Adi Juliawan Pawana Ilsun You |
| author_sort | Yongho Ko |
| collection | DOAJ |
| description | 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 |
| format | Article |
| id | doaj-art-c75a74aeac2743df871137d2e18b7ffb |
| institution | DOAJ |
| issn | 1424-8220 |
| language | English |
| publishDate | 2024-12-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Sensors |
| spelling | doaj-art-c75a74aeac2743df871137d2e18b7ffb2025-08-20T02:43:21ZengMDPI AGSensors1424-82202024-12-012424797910.3390/s24247979Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification TechniquesYongho Ko0I Wayan Adi Juliawan Pawana1Ilsun You2Department of Financial Information Security, Kookmin University, Seoul 02707, Republic of KoreaDepartment of Financial Information Security, Kookmin University, Seoul 02707, Republic of KoreaDepartment of Financial Information Security, Kookmin University, Seoul 02707, Republic of KoreaThe 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 networkshttps://www.mdpi.com/1424-8220/24/24/79795G securityforward secrecy (FS)5G-AKA-FSProVerif |
| spellingShingle | Yongho Ko I Wayan Adi Juliawan Pawana Ilsun You Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification Techniques Sensors 5G security forward secrecy (FS) 5G-AKA-FS ProVerif |
| title | Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification Techniques |
| title_full | Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification Techniques |
| title_fullStr | Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification Techniques |
| title_full_unstemmed | Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification Techniques |
| title_short | Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification Techniques |
| title_sort | formal security reassessment of the 5g aka fs protocol methodological corrections and augmented verification techniques |
| topic | 5G security forward secrecy (FS) 5G-AKA-FS ProVerif |
| url | https://www.mdpi.com/1424-8220/24/24/7979 |
| work_keys_str_mv | AT yonghoko formalsecurityreassessmentofthe5gakafsprotocolmethodologicalcorrectionsandaugmentedverificationtechniques AT iwayanadijuliawanpawana formalsecurityreassessmentofthe5gakafsprotocolmethodologicalcorrectionsandaugmentedverificationtechniques AT ilsunyou formalsecurityreassessmentofthe5gakafsprotocolmethodologicalcorrectionsandaugmentedverificationtechniques |