Formal Security Reassessment of the 5G-AKA-FS Protocol: Methodological Corrections and Augmented Verification...

Area of Science:

• Computer Science
• Cybersecurity
• Network Security

Background:

• The 5G-AKA protocol, essential for 5G network authentication, suffers from vulnerabilities like linkability attacks, compromising user privacy.
• Previous work introduced the 5G-AKA-Forward Secrecy (5G-AKA-FS) protocol to mitigate these risks by incorporating forward secrecy.
• Initial BAN-logic verification of 5G-AKA-FS revealed minor errors, necessitating a more robust security validation.

Purpose of the Study:

• To correct the BAN-logic verification errors for the 5G-AKA-FS protocol.
• To conduct a more rigorous formal security analysis of 5G-AKA-FS.
• To validate the enhanced security and privacy offered by 5G-AKA-FS against advanced threats.

Main Methods:

• Corrected the initial BAN-logic verification of the 5G-AKA-FS protocol.
• Applied an extended SVO logic for advanced formal security analysis, including a new forward secrecy axiom.
• Enhanced the ProVerif analysis with a stronger adversarial model for comprehensive validation.

Main Results:

• The BAN-logic verification errors in 5G-AKA-FS were successfully corrected.
• The extended SVO logic and enhanced ProVerif analysis confirmed the security of 5G-AKA-FS.
• The protocol demonstrates resilience against sophisticated linkability and privacy attacks.

Conclusions:

• The refined formal verification confirms the security and reliability of the 5G-AKA-FS protocol.
• 5G-AKA-FS effectively addresses privacy concerns and linkability attacks in 5G networks.
• This study provides a validated framework for future 5G security protocol verification.