Formal Verification of 5GAKA-LCCO Protocol Supporting Forward Secrecy: Through Expanded BAN Logic

As 5G technology becomes more advanced and innovative, various vulnerabilities are being discovered. As technology develops further, not only in 5G but also in B5G and 6G, strong security is required, and research is underway to satisfy this. For example, standardization is underway to reuse credentials generated from 5G primary authentication in applications layer, and FS for keys is required for this standard to satisfy strong security. Therefore, 5G primary authentication protocols supporting FS have been proposed. Among the proposed protocols, 5GAKA-LCCO supports innovative Process and improved security compared to existing protocols. Therefore, we verify through BAN logic whether the 5GAKA-LCCO protocol truly satisfies the security properties. However, since BAN logic does not have rules to verify FS properties, we proposed new notations and rules for FS verification. Based on the expanded BAN logic, we verified the protocol and found that this protocol is not secure. 5GAKA-LCCO still does not support FS properties, and various vulnerabilities such as DoS attacks and synchronization problems exist.