A formal analysis of 5g authentication

David Basin; Jannik Dreier; Lucca Hirschi; Saša Radomirovic; Ralf Sasse; Vincent Stettler

doi:10.1145/3243734.3243846

A formal analysis of 5g authentication

David Basin, Jannik Dreier, Lucca Hirschi, Saša Radomirovic, Ralf Sasse, Vincent Stettler

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

304 Citations (Scopus)

160 Downloads (Pure)

Abstract

Mobile communication networks connect much of the world’s population. The security of users’ calls, SMSs, 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. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.

Original language	English
Title of host publication	CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security
Publisher	Association for Computing Machinery
Pages	1383-1396
Number of pages	14
ISBN (Electronic)	9781450356930
DOIs	https://doi.org/10.1145/3243734.3243846
Publication status	Published - Oct 2018
Event	25th ACM Conference on Computer and Communications Security 2018 - Toronto, Canada Duration: 15 Oct 2018 → 15 Oct 2018

Conference

Conference	25th ACM Conference on Computer and Communications Security 2018
Abbreviated title	CCS 2018
Country/Territory	Canada
City	Toronto
Period	15/10/18 → 15/10/18

Keywords

5G standard
AKA protocol
Authentication protocols
Formal analysis
Symbolic verification

ASJC Scopus subject areas

Software
Computer Networks and Communications

Access to Document

10.1145/3243734.3243846

Download pdf
©2018. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, https://doi.org/10.1145/3243734.3243846
Accepted author manuscript, 1.06 MB

https://arxiv.org/abs/1806.10360

Cite this

@inproceedings{46dbf3b28a494fb59c8dc627e8c8263e,

title = "A formal analysis of 5g authentication",

abstract = "Mobile communication networks connect much of the world{\textquoteright}s population. The security of users{\textquoteright} calls, SMSs, 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. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.",

keywords = "5G standard, AKA protocol, Authentication protocols, Formal analysis, Symbolic verification",

author = "David Basin and Jannik Dreier and Lucca Hirschi and Sa{\v s}a Radomirovic and Ralf Sasse and Vincent Stettler",

year = "2018",

month = oct,

doi = "10.1145/3243734.3243846",

language = "English",

pages = "1383--1396",

booktitle = "CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security",

publisher = "Association for Computing Machinery",

address = "United States",

note = "25th ACM Conference on Computer and Communications Security 2018, CCS 2018 ; Conference date: 15-10-2018 Through 15-10-2018",

}

Basin, D, Dreier, J, Hirschi, L, Radomirovic, S, Sasse, R & Stettler, V 2018, A formal analysis of 5g authentication. in CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, pp. 1383-1396, 25th ACM Conference on Computer and Communications Security 2018, Toronto, Canada, 15/10/18. https://doi.org/10.1145/3243734.3243846

TY - GEN

T1 - A formal analysis of 5g authentication

AU - Basin, David

AU - Dreier, Jannik

AU - Hirschi, Lucca

AU - Radomirovic, Saša

AU - Sasse, Ralf

AU - Stettler, Vincent

PY - 2018/10

Y1 - 2018/10

N2 - Mobile communication networks connect much of the world’s population. The security of users’ calls, SMSs, 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. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.

AB - Mobile communication networks connect much of the world’s population. The security of users’ calls, SMSs, 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. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.

KW - 5G standard

KW - AKA protocol

KW - Authentication protocols

KW - Formal analysis

KW - Symbolic verification

UR - http://www.scopus.com/inward/record.url?scp=85056873194&partnerID=8YFLogxK

U2 - 10.1145/3243734.3243846

DO - 10.1145/3243734.3243846

M3 - Conference contribution

AN - SCOPUS:85056873194

SP - 1383

EP - 1396

BT - CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security

PB - Association for Computing Machinery

T2 - 25th ACM Conference on Computer and Communications Security 2018

Y2 - 15 October 2018 through 15 October 2018

ER -

A formal analysis of 5g authentication

Abstract

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this