Formal verification of LTE-UMTS and LTE-LTE handover procedures

Long Term Evolution (LTE) is the most recent standard in mobile communications, introduced by 3rd Generation Partnership Project (3GPP). Most of the works in literature about LTE security analyze authentication procedures, while handover procedures are far less considered. This paper focuses on the procedures that are activated when a mobile device moves between different LTE cells and between LTE and the older Universal Mobile Telecommunications System (UMTS) networks and completes previous results with a deeper formal analysis of these procedures. The analysis shows that security properties (secrecy of keys, including backward/forward secrecy, immunity from off-line guessing attacks, and network components authentication) hold almost as expected in nominal conditions, i.e. when all backhaul links are secured and all backhaul nodes are trusted. The paper also analyses how these security properties are affected by possible anomalous situations, such as a compromised backhaul node or a misconfiguration by which a backhaul link becomes not protected and can be accessed by an attacker. The analysis shows that some security properties hold even in these adverse cases while other properties are compromised.