# 5G-AKA-FS: A 5G Authentication and Key Agreement Protocol for Forward Secrecy
## 5 Formal Verification
### Formal Verification via ProVerif
#### 5.2.3 Assertions
In Proceedings of the 25 st ACM SIGSAC Conference on Computer and Communications Security (CCS'18), Toronto, Canada, 15-19 October 2018; ACM Press: New York, NY, USA, 2018; pp. 1383-1396. [CrossRef]
* [14] [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] Security for 5G and beyond. _IEEE Commun. Surv. Tutorials_**2019**, _21_, 3682-3722. [CrossRef]
* [15] [PERSON]; [PERSON] Formal verification and analysis of 5G AKA protocol using mixed strand space model. _Electronics_**2022**, _11_, 1333. [CrossRef]
* [16] [PERSON]; [PERSON]; [PERSON] Privacy-Preserving and Standard-Compatible AKA Protocol for 5G. In Proceedings of the 30 th USENIX Security Symposium (USENIX Security '21), Online, 11-13 August 2021; USENIX Association: Vancouver, BC, Canada, 2021; pp. 3595-3612. Available online: [[https://www.usenix.org/conference/usenixsecurity21/presentation/wang-yuchen](https://www.usenix.org/conference/usenixsecurity21/presentation/wang-yuchen)]([https://www.usenix.org/conference/usenixsecurity21/presentation/wang-yuchen](https://www.usenix.org/conference/usenixsecurity21/presentation/wang-yuchen)) (accessed on 10 December 2023). * [17] [PERSON]; [PERSON] 5G-IPAKA: An improved primary authentication and key agreement protocol for 5g networks. _Information_**2022**, _13_, 125. [CrossRef]
* [18] 3 GPP. Authentication and Key Management for Applications (AKMA) Based on 3 GPP Credentials in the 5G System (5 GS) TS 33.535 (Release 18). Technical Report, The 3 rd Generation Partnership Project, 2023. Available online: [https://portal.3 gpp.org/desktopmodules/Specifications/SpecificationDetails.aspx?specificationId=3690](https://portal.3 gpp.org/desktopmodules/Specifications/SpecificationDetails.aspx?specificationId=3690) (accessed on 10 December 2023). * [19] [PERSON]; [PERSON]; [PERSON] Forward Secrecy for the Extensible Authentication Protocol Method for Authentication and Key Agreement (EAP-AKA 'FS). Internet-Draft draft-ietf-emnu-aka-pfs-11, Internet Engineering Task Force. 2023. Available online: [[https://datatracker.ietf.org/doc/draft-ietf-emu-aka-pfs/11/](https://datatracker.ietf.org/doc/draft-ietf-emu-aka-pfs/11/)]([https://datatracker.ietf.org/doc/draft-ietf-emu-aka-pfs/11/](https://datatracker.ietf.org/doc/draft-ietf-emu-aka-pfs/11/)) (accessed on 10 December 2023). * [20] [PERSON] The SUCI-AKA Authentication Protocol for 5G Systems. In Proceedings of the 13 rd NISK Conference on Norwegian Information Security (NISK'20), Online, 23-25 November 2020. Available online: [[https://ois.bibsys.no/index.php/NIK/article/view/885](https://ois.bibsys.no/index.php/NIK/article/view/885)]([https://ois.bibsys.no/index.php/NIK/article/view/885](https://ois.bibsys.no/index.php/NIK/article/view/885)) (accessed on 10 December 2023). * [21] [PERSON]; [PERSON] 5 GAKA-LCCO: A secure 5G authentication and key agreement protocol with less communication and computation overhead. _Information_**2022**, _13_, 257. [CrossRef]
* [22] [PERSON]; [PERSON]; [PERSON] A logic of authentication. _ACM Trans. Comput. Syst. (TOCS)_**1990**, \(8\), 18-36. [CrossRef]
* [23] [PERSON]; [PERSON]; [PERSON]; [PERSON] ProVerif 2.04: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. Proverif User Manual, 2021. Available online: [[https://blanche.gitlabpages.inria.fr/proverif/manual.pdf](https://blanche.gitlabpages.inria.fr/proverif/manual.pdf)]([https://blanche.gitlabpages.inria.fr/proverif/manual.pdf](https://blanche.gitlabpages.inria.fr/proverif/manual.pdf)) (accessed on 10 December 2023). * _[PERSON] (2001)_ _[PERSON] A Proposal for an ISO Standard for Public Key Encryption. Cryptology ePrint Archive, Paper 2001/112. 2001. Available: online:_ [[https://eprint.iacr.org/2001/112](https://eprint.iacr.org/2001/112)]([https://eprint.iacr.org/2001/112](https://eprint.iacr.org/2001/112)) (accessed on 10 December 2023). * _Research (2009)_ _Research, C. SEC 1: Elliptic Curve Cryptography. Standards for Efficient Cryptography. 2009.