LTE Security Procedures
Work on formal verification of LTE security presented at the 17th International Symposium on Research in Attacks, Intrusions and Defenses, RAID2014.
Among the objectives of LTE is to provide equal or better security compared to previous generations. One such improvement is that LTE introduces very granular key separation. LTE mandates the use of different session keys for specific protocols and purposes between the terminal and the nodes in the network.
Security protocols are procedures based on the message exchange between communicating agents allowing them to share secrets over a public network. They are intended to work correctly even in the presence of a malicious intruder who has full control over the communication medium. By full control, it is meant that the intruder can intercept, drop, forward or replay old messages. This is a very reasonable assumption in wireless communication settings. A security protocol is usually defined by a set of roles where each communicating agent plays a specific one. Correct requirements include properties such as secrecy and authentication.
Reasoning about security protocols is extremely difficult because it is usually impossible to anticipate all the intruder actions. In LTE, the security procedures are complex and typically involve more than two agents. For example a handover procedure can involve a user device such as a mobile phone or a surf tablet (UE), two base stations (eNodeB) and two Mobility Management nodes (MME). Now think of all the possible interleavings of the exchanged messages or even all the possible messages that the intruder can inject and which he could have collected from previous runs. In fact, there is an infinite number of possible scenarios.
Two weeks ago, I presented our paper “Formal Analysis of Security Procedures in LTE – A feasibility Study” at the RAID 2014 Symposium in Gothenburg. This was a joint work with Karl Norrman, another member of the Ericsson Research Security team. In this paper, we describe how we applied formal verification techniques to automatically prove the security properties of several LTE procedures previously never analyzed in this manner. We relied on a tool called ProVerif which takes as input a model of the procedure under analysis together with a set of security properties in a formal language. The tool then attempts to automatically prove the properties.
In case studies, we considered two security activation procedures, for the RRC and NAS protocols, and two types of handovers, over the X2 and S1 interfaces. In general, the goal of these procedures is to establish a secure communication between the UE and a target node in the network. For each procedure, we describe the corresponding formal model and discuss the result of the analysis. The security properties which we analyzed are secrecy of the established security parameters and mutual authentication between the UE and the target node. More details can be found in the paper available here.
The RAID conference, which was initially dedicated to intrusion detection, now seems to have a broader scope: network security, malware and binary analysis, authentication and privacy, web security, etc. It is highly ranked and has a very low acceptance rate, thus we are proud that our work was accepted!
Noamen Ben Henda, Ericsson Research