Dependency-Graph Enabled Formal Analysis for 5G AKA Protocols: Assumption Propagation and Verification

The 5G authentication and key agreement protocol (AKA) is intended to provide security assurance for users, net-work operators, and machine-to-machine communications. It is a critical component of everyday life and national infrastructure. In this paper, we conduct a high-resolution and in-depth formal analysis of the AKA protocol, addressing hidden assumptions stemming from the underlying dependencies among entities. We categorize the direct properties among identifiers in each protocol session into confidentiality, integrity, authentication, and accounting. We further uncover the indirect dependencies among identifiers through the propagation of assumptions in the designed dependency graph. The formal models are generated from both the direct and indirect dependencies and are verified using Pro Verif. Our approach reveals four major vulnerability types across four sub-procedures. This includes three vulner-abilities previously identified in existing research, as well as one newly discovered vulnerability type. The solutions proposed to address these vulnerabilities have been validated through formal verification and over-the-air (OTA) testing. We present the first formal models that consider hidden assumptions and their propagation in 5G, and demonstrate the fragility of the 5G-AKA protocol through experimental practice. We have also included formally verified fixes for the encountered vulnerabilities.