Formalizing and Verifying Generations of AKA Protocols
Angela Rellstab · Repository for Publications and Research Data (ETH Zurich) · 2019
Mobile networks are connecting the world.More and more mobile network subscribers rely on a secure connection for their communication.The Authentication and Key Agreement (AKA) protocol variants used in mobile networks are crucial to ensure integrity and confidentiality of communication.In this thesis, we analyze different AKA protocol variants currently deployed by leveraging formal models and the Tamarin security protocol verification tool.Specifically, we first formally model individual AKA protocol variants and present the necessary requirements, i.e., minimal assumptions, to satisfy certain security properties.Second, we provide a comparison of the resulting security guarantees of individual AKA protocol variants.Finally, we formally analyze combinations of AKA protocol variants to model the co-existence of multiple mobile network generations.The analysis shows that newer AKA protocol variants improve security guarantees compared to older variants.However, the newest standard is still unable to satisfy certain security properties without extra assumptions that are not part of the actual protocol specification.When combining multiple AKA protocol variants, as happens in the real world, stronger assumptions must be made to satisfy the same security properties.i• We present a generic flow of the AKA protocol variants currently used in 3G, 4G, and 5G.• We formally model AKA protocol variants used in 3G, 4G, and 5G: 3G AKA, 4G EPS AKA, 5G AKA, and 5G EAP AKA'.The individual AKA protocol models build on the same generic model that includes sequence numbers as state, the resynchronization mechanism, and the XOR operator.Additionally, the serving and home network are mod-