Rhys John Miller
Academic and research departments
Faculty of Engineering and Physical Sciences, Department of Computer Science, Surrey Centre for Cyber Security.About
My research project
Security Analysis of Systems Using Emerging 5G TechnologiesThe forthcoming 5th generation of mobile networks (5G) makes a revolutionary promise: higher capacity and connectivity at greater speeds. To achieve this goal, 5G will need to use significantly more spectrum and some of these frequencies will be in bands higher than in traditional mobile networks, and therefore 5G will bank on millimetre waves (mmWaves). But, these do not travel well through physical obstacles or at the large distances over which today’s high-power cell towers broadcast their signal. To this end, 5G systems need to employ the so-called small-cells (which in fact now include micro-cells, pico-cells, femto-cells, etc). This amounts to using thousands of low-powered mini base-stations (or remote radio heads), placed significantly closer together than traditional cell towers are; the usage of these cells together to increase coverage is often term as “heterogenous networks” (HetNets).
Thus, we are concerned with a number of security aspects stemming to these two 5G technologies: (a) SC equates to new elements in the mobile architecture and therefore to new vulnerability entry points; moreover, the backend in 5G networks will be virtualised and functions may be moved around within the network, so the actual architecture will be fluid, changeable on-demand and this can open to further, new threats. In a systematic fashion, this project will undertake the formal security & privacy analysis of 5G-systems against 5G-driven security risks including the aforementioned threats stemming from SC.
Supervisors
The forthcoming 5th generation of mobile networks (5G) makes a revolutionary promise: higher capacity and connectivity at greater speeds. To achieve this goal, 5G will need to use significantly more spectrum and some of these frequencies will be in bands higher than in traditional mobile networks, and therefore 5G will bank on millimetre waves (mmWaves). But, these do not travel well through physical obstacles or at the large distances over which today’s high-power cell towers broadcast their signal. To this end, 5G systems need to employ the so-called small-cells (which in fact now include micro-cells, pico-cells, femto-cells, etc). This amounts to using thousands of low-powered mini base-stations (or remote radio heads), placed significantly closer together than traditional cell towers are; the usage of these cells together to increase coverage is often term as “heterogenous networks” (HetNets).
Thus, we are concerned with a number of security aspects stemming to these two 5G technologies: (a) SC equates to new elements in the mobile architecture and therefore to new vulnerability entry points; moreover, the backend in 5G networks will be virtualised and functions may be moved around within the network, so the actual architecture will be fluid, changeable on-demand and this can open to further, new threats. In a systematic fashion, this project will undertake the formal security & privacy analysis of 5G-systems against 5G-driven security risks including the aforementioned threats stemming from SC.
ResearchResearch interests
5G Security, Formal Verification, Security Analysis and Small Cells
Research interests
5G Security, Formal Verification, Security Analysis and Small Cells
Publications
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 sub- scribers 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"