(2019) Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion.
|
Text
CrDe2018-5G.pdf - Accepted Version Download (893kB) | Preview |
Abstract
The 5G mobile telephony standards are nearing completion; upon adoption these will be used by billions across the globe. Ensuring the security of 5G communication is of the utmost importance, building trust in a critical component of everyday life and national infrastructure. We perform fine-grained formal analysis of 5G’s main authentication and key agreement protocol (AKA), and provide the first models to explicitly consider all parties defined by the protocol specification. Our analysis reveals that the security of 5G-AKA critically relies on unstated assumptions on the inner workings of the underlying channels. In practice this means that following the 5G-AKA specification, a provider can easily and ‘correctly’ implement the standard insecurely, leaving the protocol vulnerable to a security-critical race condition. We provide the first models and analysis considering component and channel compromise in 5G, whose results further demonstrate the fragility and subtle trust assumptions of the 5G-AKA protocol. We propose formally verified fixes to the encountered issues, and have worked with 3GPP to ensure these fixes are adopted.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Unspecified |
| Conference: | NDSS Network and Distributed System Security Symposium |
| Depositing User: | Cas Cremers |
| Date Deposited: | 11 Jan 2019 13:42 |
| Last Modified: | 18 Jul 2019 12:09 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/2758 |
Actions
Actions (login required)
 |
View Item |