{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T17:15:07Z","timestamp":1770225307763,"version":"3.49.0"},"reference-count":42,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Systems Architecture"],"published-print":{"date-parts":[[2022,5]]},"DOI":"10.1016\/j.sysarc.2022.102478","type":"journal-article","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T12:40:10Z","timestamp":1648557610000},"page":"102478","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":12,"special_numbering":"C","title":["Formal Analysis of 5G Authentication and Key Management for Applications (AKMA)"],"prefix":"10.1016","volume":"126","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2072-0836","authenticated-orcid":false,"given":"Tengshun","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuling","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5377-9351","authenticated-orcid":false,"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jinghui","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuangqing","family":"Xiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhan","family":"Xiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bifei","family":"Mao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.sysarc.2022.102478_b1","series-title":"TS33.501 V17.1.0 security architecture and procedures for 5G system (release 17)","author":"3GPP","year":"2021"},{"key":"10.1016\/j.sysarc.2022.102478_b2","series-title":"TS33.535 V17.4.0 authentication and key management for applications (AKMA) based on 3GPP credentials in the 5G system (5GS)","author":"3GPP","year":"2021"},{"key":"10.1016\/j.sysarc.2022.102478_b3","doi-asserted-by":"crossref","unstructured":"S. Meier, B. Schmidt, C. Cremers, D.A. Basin, The TAMARIN prover for the symbolic analysis of security protocols, in: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, 2013, pp. 696\u2013701.","DOI":"10.1007\/978-3-642-39799-8_48"},{"issue":"2","key":"10.1016\/j.sysarc.2022.102478_b4","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public key protocols","volume":"29","author":"Dolev","year":"1983","journal-title":"IEEE Trans. Inf. Theory"},{"key":"10.1016\/j.sysarc.2022.102478_b5","doi-asserted-by":"crossref","unstructured":"B.A. LaMacchia, K.E. Lauter, A. Mityagin, Stronger security of authenticated key exchange, in: Provable Security, First International Conference, ProvSec 2007, Wollongong, Australia, November 1-2, 2007, Proceedings, 2007, pp. 1\u201316.","DOI":"10.1007\/978-3-540-75670-5_1"},{"key":"10.1016\/j.sysarc.2022.102478_b6","doi-asserted-by":"crossref","unstructured":"G. Lowe, A hierarchy of authentication specification, in: 10th Computer Security Foundations Workshop, CSFW \u201997, June 10-12, 1997, Rockport, Massachusetts, USA, 1997, pp. 31\u201344.","DOI":"10.1109\/CSFW.1997.596782"},{"key":"10.1016\/j.sysarc.2022.102478_b7","doi-asserted-by":"crossref","unstructured":"B. Schmidt, S. Meier, C.J.F. Cremers, D.A. Basin, Automated analysis of Diffie-Hellman protocols and advanced security properties, in: 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012, 2012, pp. 78\u201394.","DOI":"10.1109\/CSF.2012.25"},{"key":"10.1016\/j.sysarc.2022.102478_b8","series-title":"Dependable Software Engineering. Theories, Tools, and Applications - 7th International Symposium, SETTA 2021","first-page":"102","article-title":"Formal analysis of 5G AKMA","volume":"vol. 13071","author":"Yang","year":"2021"},{"key":"10.1016\/j.sysarc.2022.102478_b9","series-title":"TS33.220 V17.2.0 generic authentication architecture (GAA); generic bootstrapping architecture (GBA)","author":"3GPP","year":"2021"},{"key":"10.1016\/j.sysarc.2022.102478_b10","series-title":"TS33.163 V16.2.0 battery efficient security for very low throughput machine type communication (MTC) devices (BEST)","author":"3GPP","year":"2019"},{"key":"10.1016\/j.sysarc.2022.102478_b11","series-title":"TR33.835 V16.1.0 study on authentication and key management for applications based on 3GPP credential in 5G","author":"3GPP","year":"2020"},{"key":"10.1016\/j.sysarc.2022.102478_b12","series-title":"Proceedings of the 5th ACM Workshop on Security Standardisation Research Workshop, London, UK, November 11, 2019","first-page":"45","article-title":"Privacy preserving AKMA in 5G","author":"Khan","year":"2019"},{"issue":"3","key":"10.1016\/j.sysarc.2022.102478_b13","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/MCOMSTD.101.2100015","article-title":"AKMA: delegated authentication system of 5G","volume":"5","author":"Khan","year":"2021","journal-title":"IEEE Commun. Stand. Mag."},{"key":"10.1016\/j.sysarc.2022.102478_b14","series-title":"Security and Cryptography for Networks, 7th International Conference, SCN 2010, Amalfi, Italy, September 13-15, 2010. Proceedings","first-page":"219","article-title":"A new security model for authenticated key agreement","volume":"vol. 6280","author":"Sarr","year":"2010"},{"key":"10.1016\/j.sysarc.2022.102478_b15","series-title":"Advances in Cryptology - CRYPTO \u201993, 13th Annual International Cryptology Conference, Santa Barbara, California, USA, August 22-26, 1993, Proceedings","first-page":"232","article-title":"Entity authentication and key distribution","volume":"vol. 773","author":"Bellare","year":"1993"},{"key":"10.1016\/j.sysarc.2022.102478_b16","series-title":"Advances in Cryptology - EUROCRYPT 2001, International Conference on the Theory and Application of Cryptographic Techniques, Innsbruck, Austria, May 6-10, 2001, Proceeding","first-page":"453","article-title":"Analysis of key-exchange protocols and their use for building secure channels","volume":"vol. 2045","author":"Canetti","year":"2001"},{"key":"10.1016\/j.sysarc.2022.102478_b17","series-title":"Advances in Cryptology - CRYPTO 2005: 25th Annual International Cryptology Conference, Santa Barbara, California, USA, August 14-18, 2005, Proceedings","first-page":"546","article-title":"HMQV: A high-performance secure Diffie-Hellman protocol","volume":"vol. 3621","author":"Krawczyk","year":"2005"},{"key":"10.1016\/j.sysarc.2022.102478_b18","series-title":"1996 IEEE Symposium on Security and Privacy, May 6-8, 1996, Oakland, CA, USA","first-page":"174","article-title":"Security properties and CSP","author":"Schneider","year":"1996"},{"key":"10.1016\/j.sysarc.2022.102478_b19","series-title":"Using CSP for Protocol Analysis: the Needham-Schroeder Public-Key Protocol","author":"Schneider","year":"1996"},{"key":"10.1016\/j.sysarc.2022.102478_b20","unstructured":"B. Donovan, P. Norris, G. Lowe, Analyzing a library of security protocols using casper and FDR, in: Workshop on Formal Methods and Security Protocols, 1999."},{"issue":"1","key":"10.1016\/j.sysarc.2022.102478_b21","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","article-title":"A logic of authentication","volume":"8","author":"Burrows","year":"1990","journal-title":"ACM Trans. Comput. Syst."},{"issue":"1","key":"10.1016\/j.sysarc.2022.102478_b22","doi-asserted-by":"crossref","first-page":"1:1","DOI":"10.1145\/3127586","article-title":"The applied pi calculus: Mobile values, new names, and secure communication","volume":"65","author":"Abadi","year":"2018","journal-title":"J. ACM"},{"key":"10.1016\/j.sysarc.2022.102478_b23","series-title":"14th IEEE Computer Security Foundations Workshop, CSFW-14 2001, 11-13 June 2001, Cape Breton, Nova Scotia, Canada","first-page":"82","article-title":"An efficient cryptographic protocol verifier based on prolog rules","author":"Blanchet","year":"2001"},{"key":"10.1016\/j.sysarc.2022.102478_b24","series-title":"Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings","first-page":"281","article-title":"The AVISPA tool for the automated validation of internet security protocols and applications","volume":"vol. 3576","author":"Armando","year":"2005"},{"issue":"3","key":"10.1016\/j.sysarc.2022.102478_b25","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lamport","year":"1994","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.sysarc.2022.102478_b26","series-title":"Lecture Notes in Computer Science","article-title":"All About Maude - a High-Performance Logical Framework, how to Specify, Program and Verify Systems in Rewriting Logic","year":"2007"},{"issue":"1\u20132","key":"10.1016\/j.sysarc.2022.102478_b27","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","article-title":"A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties","volume":"367","author":"Escobar","year":"2006","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.sysarc.2022.102478_b28","series-title":"Advancing Automated Security Protocol Verification","author":"Meier","year":"2013"},{"key":"10.1016\/j.sysarc.2022.102478_b29","series-title":"Security and Trust Management - 8th International Workshop, STM 2012, Pisa, Italy, September 13-14, 2012, Revised Selected Papers","first-page":"257","article-title":"Yubisecure? Formal security analysis results for the yubikey and yubihsm","volume":"vol. 7783","author":"K\u00fcnnemann","year":"2012"},{"issue":"3","key":"10.1016\/j.sysarc.2022.102478_b30","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1109\/TDSC.2016.2601610","article-title":"Design, analysis, and implementation of ARPKI: An attack-resilient public-key infrastructure","volume":"15","author":"Basin","year":"2018","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"10.1016\/j.sysarc.2022.102478_b31","series-title":"Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, on, Canada, October 15-19, 2018","first-page":"1383","article-title":"A formal analysis of 5G authentication","author":"Basin","year":"2018"},{"key":"10.1016\/j.sysarc.2022.102478_b32","series-title":"Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017","first-page":"1773","article-title":"A comprehensive symbolic analysis of TLS 1.3","author":"Cremers","year":"2017"},{"key":"10.1016\/j.sysarc.2022.102478_b33","series-title":"30th USENIX Security Symposium, USENIX Security 2021, August 11-13, 2021","first-page":"3595","article-title":"Privacy-preserving and standard-compatible AKA protocol for 5G","author":"Wang","year":"2021"},{"key":"10.1016\/j.sysarc.2022.102478_b34","series-title":"TR33.902 V4.0.0 3G security; formal analysis of the 3G authentication protocol","author":"3GPP","year":"2001"},{"issue":"1","key":"10.1016\/j.sysarc.2022.102478_b35","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00766-010-0115-7","article-title":"A privacy threat analysis framework: Supporting the elicitation and fulfillment of privacy requirements","volume":"16","author":"Deng","year":"2011","journal-title":"Requir. Eng."},{"issue":"3","key":"10.1016\/j.sysarc.2022.102478_b36","doi-asserted-by":"crossref","first-page":"477","DOI":"10.2307\/40041279","article-title":"A taxonomy of privacy","volume":"154","author":"Solove","year":"2006","journal-title":"Univ. Pa. Asian Law Rev."},{"key":"10.1016\/j.sysarc.2022.102478_b37","series-title":"Financial Cryptography and Data Security, 13th International Conference, FC 2009, Accra Beach, Barbados, February 23-26, 2009. Revised Selected Papers","first-page":"362","article-title":"Relations among privacy notions","volume":"vol. 5628","author":"Bohli","year":"2009"},{"key":"10.1016\/j.sysarc.2022.102478_b38","series-title":"Computer Security - ESORICS 2013 - 18th European Symposium on Research in Computer Security, Egham, UK, September 9-13, 2013. Proceedings","first-page":"499","article-title":"Enforcing privacy in the presence of others: Notions, formalisations and relations","volume":"vol. 8134","author":"Dong","year":"2013"},{"key":"10.1016\/j.sysarc.2022.102478_b39","series-title":"TS33.102 V16.0.0 3G security; security architecture","author":"3GPP","year":"2020"},{"key":"10.1016\/j.sysarc.2022.102478_b40","series-title":"TS33.401 V16.3.0 3GPP system architecture evolution (SAE); security architecture","author":"3GPP","year":"2020"},{"key":"10.1016\/j.sysarc.2022.102478_b41","series-title":"Tamarin-prover manual: Security protocol analysis in the symbolic model","author":"Tamarin\u00a0Team","year":"2021"},{"key":"10.1016\/j.sysarc.2022.102478_b42","series-title":"IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016","first-page":"325","article-title":"Modeling human errors in security protocols","author":"Basin","year":"2016"}],"container-title":["Journal of Systems Architecture"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1383762122000601?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1383762122000601?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T13:36:12Z","timestamp":1761312972000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1383762122000601"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5]]},"references-count":42,"alternative-id":["S1383762122000601"],"URL":"https:\/\/doi.org\/10.1016\/j.sysarc.2022.102478","relation":{},"ISSN":["1383-7621"],"issn-type":[{"value":"1383-7621","type":"print"}],"subject":[],"published":{"date-parts":[[2022,5]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Formal Analysis of 5G Authentication and Key Management for Applications (AKMA)","name":"articletitle","label":"Article Title"},{"value":"Journal of Systems Architecture","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.sysarc.2022.102478","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2022 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"102478"}}