Rhys John Miller

Rhys John Miller

PhD Student

Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

portfolio

publications

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

Published in ASIACCS, 2022

We formally analyse the security of each 5G authenticated key establisment (AKE) procedures: the 5G registration, the 5G authen tication 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”.

Download here

talks

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

Published:

In this presentation, we study the security of each part of the 5G authenticated key-establishment (AKE) procedures. We also look at the consequences this AKE (in)security has over critical mobile-networks’ objects such as PDU sessions. We carry out our formal analyses using the Tamarin formal protocol-verifier. We augmented the standard Dolev-Yao model with different levels of trust and threat, considering: honest, honest-but-curious, as well as rogue radio nodes. 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.

teaching