# 5G-AKA-FS: A 5G Authentication and Key Agreement Protocol for Forward Secrecy
## 5 Formal Verification
### Formal Verification via ProVerif
#### 5.2.3 Assertions
2022-00207416, A study on PQC optimization and security protocol migration to neutralize advanced quantum attacks in Beyond 5G-based next-generation IoT computing environments, 100%). Not applicable. ## References

* [1] European 5G Performance Trails its International Peers. Available online: [[https://www.gsma.com/membership/resources/european-5g-performance-trails-its-international-peers/](https://www.gsma.com/membership/resources/european-5g-performance-trails-its-international-peers/)]([https://www.gsma.com/membership/resources/european-5g-performance-trails-its-international-peers/](https://www.gsma.com/membership/resources/european-5g-performance-trails-its-international-peers/))(accessed on 10 December 2023). * [2] [PERSON]; [PERSON]; [PERSON] 5G is real: Evaluating the compliance of the 3 GPP 5G new radio system with the ITU IMT-2020 requirements. _IEEE Access_**2020**, \(8\), 42828-42840. [CrossRef]
* [3] 3 GPP. Security Architecture and Procedures for 5G System TS33.501 v18.2.0. Technical Report, The 3 rd Generation Partnership Project. 2023. Available online: [https://portal.3 gpp.org/desktopmodules/Specifications/SpecificationDetails.aspx?specificationId=3196](https://portal.3 gpp.org/desktopmodules/Specifications/SpecificationDetails.aspx?specificationId=3196) (accessed on 10 December 2023). * [4] 3 GPP. 3 GPP System Architecture Evolution (SAE)--Security Architecture (Release 17) TS33.401 V17.4.0. Technical Report, The 3 rd Generation Partnership Project. 2023. Available online: [https://portal.3 gpp.org/desktopmodules/Specifications/SpecificationDetails.aspx?specificationId=2296](https://portal.3 gpp.org/desktopmodules/Specifications/SpecificationDetails.aspx?specificationId=2296) (accessed on 10 December 2023)
* [5] [PERSON]; [PERSON]; [PERSON] Improved Extensible Authentication Protocol Method for 3 rd Generation Authentication and Key Agreement (EAP-AKA). Technical Report, 2009. Available online:. (accessed on 10 December 2023). [CrossRef]
* [6] [PERSON]; [PERSON] Extensible Authentication Protocol Method for 3 rd Generation Authentication and Key Agreement (EAP-AKA). Technical Report. 2006. Available online: [[https://www.rfc-editor.org/rfc/rfc4187](https://www.rfc-editor.org/rfc/rfc4187)]([https://www.rfc-editor.org/rfc/rfc4187](https://www.rfc-editor.org/rfc/rfc4187)) (accessed on 10 December 2023). * [7] [PERSON]; [PERSON] Security and protocol exploit analysis of the 5G specifications. _IEEE Access_**2019**, \(7\), 24956-24963. [CrossRef]
* [8] [PERSON]; [PERSON] New 3 GPP security features in 5G phase 1. In Proceedings of the 4 st IEEE Conference on Standards for Communications and Networkin (CSCN '18), Paris, France, 29-31 October 2018; IEEE: Piscataway, NJ, USA, 2018; pp. 1-6. [CrossRef]
* [9] [PERSON]; [PERSON]; [PERSON]; [PERSON] A survey on security and privacy of 5G technologies: Potential solutions, recent advancements, and future directions. _IEEE Commun. Surv. Tutorials_**2019**, _22_, 196-248. [CrossRef]
* [10] [PERSON]; [PERSON]; [PERSON] Toward a secure access to 5G network. In Proceedings of the 17 st IEEE Conference on Trust, Security and Privacy in Computing and Communications (TrustCom '18)/ 12 th IEEE Conference On Big Data Science And Engineering (TrustCom/BigDataSE '18), New York, NY, USA, 1-3 August 2018; pp. 1121-1128. [CrossRef]
* [11] [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] [PERSON] 5 GReasoner: A property-directed security and privacy analysis framework for 5G cellular network protocol. In Proceedings of the 26 st ACM SIGSAC Conference on Computer and Communications Security (CCS'19), London, UK, 11-15 November 2019; ACM Press: New York, NY, USA, 2019; pp. 669-684. [CrossRef]
* [12] [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] Security for 4G and 5G cellular networks: A survey of existing authentication and privacy-preserving schemes. _J. Netw. Comput. Appl._**2018**, _101_, 55-82. [CrossRef]
* [13] [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] A formal analysis of 5G authentication.