The 5G Key-Establishment Stack: In-Depth Formal Verification and Experimentation.

We formally analyse the security of each 5G authenticated key-establisment (AKE) procedures: the 5G registration, the 5G authentication and key agreement (AKA) and 5G handovers. We also study the security of their composition, which we call the 5GAKE_stack. Our security analysis focuses on aspects of multi-party AKEs that occur in the 5GAKE_stack. We also look at the consequences this AKE (in)security has over critical mobile-networks' objects such as the Protocol Data Unit (PDU) sessions, which are used to bill subscribers and ensure quality of service as per their contracts/plans. In our assessments, we augment the standard Dolev-Yao model with different levels of trust and threat by considering honest, honest-but-curious, as well as completely rogue radio nodes. We formally prove security in the first case, and insecurity in the latter two as well as making formal recommendations on this. We carry out our formal analysis using the Tamarin-Prover. Lastly, we also present an emulator of the 5GAKE_stack. This can be a useful "5G API"-like tool for the community to experiment with the 5GAKE_stack, since the 5G networks are not yet fully deployed and mobile networks are proprietary and closed "loops".