Description
Mobile communication networks connect much of the world’s population. The security of users’ calls, text messages, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose.In this talk, I will report on our formalization of the 5G standard’s AKA protocol and show how the application of symbolic protocol verification has helped us discover and repair authentication flaws inthe standard.Joint work with David Basin, Jannik Dreier, Lucca Hirschi, Ralf Sasse, and Vincent Stettler.