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 modeling a rapidly changing system as it is developed and in the same time raising the assurance level before the system is deployed.
Noamen Ben Henda, Karl Norrman and Katharina Pfeffer.
© 2015 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.