Formal verification of the security for dual connectivity in LTE

We describe our experiences from using formal verification tools during the standardization process of Dual Connectivity, a new feature in LTE developed by 3GPP. To the best of our knowledge, this is the first report of its kind in the telecom industry. We present a model for key establishment of this feature and provide a detailed account on its formal analysis using three popular academic tools in order to automatically prove the security properties of secrecy, agreement and key freshness. The main purpose of using the tools during standardization is to evaluate their suitability for modelling a rapidly changing system as it is developed and in the same time raising the assurance level before the system is deployed.