A formal analysis of 5g authentication
- Submitting institution
-
Heriot-Watt University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 27416322
- Type
- E - Conference contribution
- DOI
-
10.1145/3243734.3243846
- Title of conference / published proceedings
- CCS '18: Proceedings of the 2018 ACM SIGSAC 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
- Significance: Published in ACM CCS, 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 committee has acknowledged the security vulnerabilities we have found in CVD-2018 0012 posted in the GSMA Mobile Security Hall of Fame. Originality: First faithful modeling and symbolic formal verification of a complex, real-world cryptographic protocol with unbounded, mutable state. Contribution: First rigorous formalisation of the 5G mobile standard's security goals. Discovery of vulnerabilities in the 5G authentication and key agreement protocol and provision of formally verified fixes.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
