Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK Option
The 5th Generation Mobile Communication (5G) plays a significant role in the Fourth Industrial Revolution (4IR), facilitating significant improvements and innovations in various fields. The 3rd Generation Partnership Project (3GPP) is currently standardizing the Authentication and Key Management for...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-11-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/14/23/11152 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850061257941450752 |
|---|---|
| author | Yongho Ko I Wayan Adi Juliawan Pawana Taeho Won Philip Virgil Astillo Ilsun You |
| author_facet | Yongho Ko I Wayan Adi Juliawan Pawana Taeho Won Philip Virgil Astillo Ilsun You |
| author_sort | Yongho Ko |
| collection | DOAJ |
| description | The 5th Generation Mobile Communication (5G) plays a significant role in the Fourth Industrial Revolution (4IR), facilitating significant improvements and innovations in various fields. The 3rd Generation Partnership Project (3GPP) is currently standardizing the Authentication and Key Management for Application (AKMA) system for the 5G convergence applications (5G cAPPs). The Transport Layer Security (TLS) is recommended as the application-specific Ua* protocol between User Equipment (UE) and Application Function (AF) to securely transmit the AKMA identifiers of UE as well as guarantee traffic protection. Among TLS protocols, session resumption in TLS 1.2 and the Pre-Shared Key (PSK) modes of TLS 1.3 are particularly desirable for Ua*. Unfortunately, the integration of PSK options of TLS 1.3, namely PSK-only, PSK-(EC)DHE, and 0-RTT (0 Round-Trip Time) modes, with AKMA has not yet been thoroughly investigated; hence, security, performance, compatibility, and effectiveness remain uncertain. In response, this paper explores the integration of the TLS 1.3 PSK options with AKMA and investigates the said metrics by conducting formal security verification and emulating exemplary applications. According to the formal verification and experimental results, the PSK-(EC)DH mode shows a security strength trade-off with efficiency. On the one hand, the 0-RTT mode demonstrates better efficiency but exhibits drawbacks on forward secrecy and replay attacks. The result suggests that 0-RTT mode has to be approved to ensure seamless integration of the TLS 1.3 PSK option with AKMA. In addition, adjustment on the AKMA architecture is also imperative to enhance security level. |
| format | Article |
| id | doaj-art-576899fc3ced457a9bd44b64f75be7dc |
| institution | DOAJ |
| issn | 2076-3417 |
| language | English |
| publishDate | 2024-11-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Applied Sciences |
| spelling | doaj-art-576899fc3ced457a9bd44b64f75be7dc2025-08-20T02:50:18ZengMDPI AGApplied Sciences2076-34172024-11-0114231115210.3390/app142311152Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK OptionYongho Ko0I Wayan Adi Juliawan Pawana1Taeho Won2Philip Virgil Astillo3Ilsun You4Department of Financial Information Security, Kookmin University, Seoul 02707, Republic of KoreaDepartment of Financial Information Security, Kookmin University, Seoul 02707, Republic of KoreaDepartment of Financial Information Security, Kookmin University, Seoul 02707, Republic of KoreaDepartment of Computer Engineering, University of San Carlos, Cebu 6000, PhilippinesDepartment of Financial Information Security, Kookmin University, Seoul 02707, Republic of KoreaThe 5th Generation Mobile Communication (5G) plays a significant role in the Fourth Industrial Revolution (4IR), facilitating significant improvements and innovations in various fields. The 3rd Generation Partnership Project (3GPP) is currently standardizing the Authentication and Key Management for Application (AKMA) system for the 5G convergence applications (5G cAPPs). The Transport Layer Security (TLS) is recommended as the application-specific Ua* protocol between User Equipment (UE) and Application Function (AF) to securely transmit the AKMA identifiers of UE as well as guarantee traffic protection. Among TLS protocols, session resumption in TLS 1.2 and the Pre-Shared Key (PSK) modes of TLS 1.3 are particularly desirable for Ua*. Unfortunately, the integration of PSK options of TLS 1.3, namely PSK-only, PSK-(EC)DHE, and 0-RTT (0 Round-Trip Time) modes, with AKMA has not yet been thoroughly investigated; hence, security, performance, compatibility, and effectiveness remain uncertain. In response, this paper explores the integration of the TLS 1.3 PSK options with AKMA and investigates the said metrics by conducting formal security verification and emulating exemplary applications. According to the formal verification and experimental results, the PSK-(EC)DH mode shows a security strength trade-off with efficiency. On the one hand, the 0-RTT mode demonstrates better efficiency but exhibits drawbacks on forward secrecy and replay attacks. The result suggests that 0-RTT mode has to be approved to ensure seamless integration of the TLS 1.3 PSK option with AKMA. In addition, adjustment on the AKMA architecture is also imperative to enhance security level.https://www.mdpi.com/2076-3417/14/23/111523GPP AKMA5G/6G security5G cAPPTLS 1.3ProVerifformal security verification |
| spellingShingle | Yongho Ko I Wayan Adi Juliawan Pawana Taeho Won Philip Virgil Astillo Ilsun You Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK Option Applied Sciences 3GPP AKMA 5G/6G security 5G cAPP TLS 1.3 ProVerif formal security verification |
| title | Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK Option |
| title_full | Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK Option |
| title_fullStr | Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK Option |
| title_full_unstemmed | Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK Option |
| title_short | Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK Option |
| title_sort | toward an era of secure 5g convergence applications formal security verification of 3gpp akma with tls 1 3 psk option |
| topic | 3GPP AKMA 5G/6G security 5G cAPP TLS 1.3 ProVerif formal security verification |
| url | https://www.mdpi.com/2076-3417/14/23/11152 |
| work_keys_str_mv | AT yonghoko towardaneraofsecure5gconvergenceapplicationsformalsecurityverificationof3gppakmawithtls13pskoption AT iwayanadijuliawanpawana towardaneraofsecure5gconvergenceapplicationsformalsecurityverificationof3gppakmawithtls13pskoption AT taehowon towardaneraofsecure5gconvergenceapplicationsformalsecurityverificationof3gppakmawithtls13pskoption AT philipvirgilastillo towardaneraofsecure5gconvergenceapplicationsformalsecurityverificationof3gppakmawithtls13pskoption AT ilsunyou towardaneraofsecure5gconvergenceapplicationsformalsecurityverificationof3gppakmawithtls13pskoption |