A Formal Analysis of 5G Authentication
- Submitting institution
-
University of Dundee
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 34181607
- Type
- E - Conference contribution
- DOI
-
10.1145/3243734.3243846
- Title of conference / published proceedings
- 25th ACM Conference on Computer and Communications Security
- First page
- 1383
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- October
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
5
- Research group(s)
-
-
- Citation count
- 38
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper describes the first faithful modelling and symbolic formal verification of a complex, real-world cryptographic protocol with unbounded, mutable state. It reports on the discovery of vulnerabilities in the 5G authentication and key agreement protocol, and the provision of formally verified fixes. It was published in ACM CCS (acceptance rate 17%), a top-tier conference in Computer Security and the flagship annual conference of ACM's Special Interest Group on Security, Audit and Control (SIGSAC). The 5G mobile communication standard committee has acknowledged the security vulnerabilities found in the GSMA Mobile Security Hall of Fame (CVD-2018 0012).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -