Computer Science Seminar Series

Abstract

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 show how the application of formal methods has helped us discover and repair authentication flaws in the 5G standard. In particular, I will give an introduction to our security protocol modeling language and the automated protocol verification tool Tamarin. No specialist knowledge will be assumed.
Joint work with David Basin, Jannik Dreier, Lucca Hirschi, Ralf Sasse, and Vincent Stettler.

Bio

Dr. Sasa Radomirovic is a senior lecturer at the University of Dundee after previously having been a senior scientist at ETH Zurich in Switzerland. Radomirovic received a PhD in number theory from Rutgers University, USA and moved on to cryptographic protocols and formal methods for information security at NTNU Norway and the University of Luxembourg. Over the last ten years his research has focused on modeling and verification of security and privacy critical systems.

Host: Manuel Maarek