A formal security analysis of the fast authentication procedure based on the security context in 5G networks

The security context, generally stored in the universal subscriber identity module card or the baseband chip, is the critical information applied by the subscriber to access the 5G network during the fast authentication procedure. Once exposed or illegally used, the security context can be exploited to derive various keys for authentication and encryption. Despite its importance, challenges and questions still remain in the previous relevant research. To fill this gap, by adopting the security protocol verification tool ProVerif, we provide a comprehensive formal model of the fast authentication procedure based on the security context to analyze whether security goals can be met. Unfortunately, we uncover two vulnerabilities, including one never reported before. Our analysis shows that these vulnerabilities stem from fundamental design flaws in the cellular network protocol and thus apply to the 4G network. These vulnerabilities could be exploited to launch several attacks, including impersonation and eavesdropping. We have validated these attacks using 5 mobile phones from 5 different baseband manufacturers through experimentation in three mobile carriers. We find an insecure implementation of one of these phones, which exposed it to replay attacks. And we further discuss the security threats posed by the impersonation attack, such as location spoofing and one-tap authentication bypass, which is verified on 10 popular apps. We finally propose several countermeasures to eliminate these security issues. Actually, we have reported the novel vulnerability to the GSM Association and received a confirmation in the form of a coordinated vulnerability disclosure (CVD) number CVD-2022-0057.