{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T04:48:51Z","timestamp":1780807731005,"version":"3.54.1"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2023,11,20]],"date-time":"2023-11-20T00:00:00Z","timestamp":1700438400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,12,31]]},"abstract":"<jats:p>As IoT in a multi-server environment increases resources\u2019 utilization, more and more problems of IoT authentication and key agreement are being revealed. The Authentication and Key Agreement (AKA) protocol plays an important role in solving these problems. Many AKA protocols have been proposed, and some of them support their own verifications. However, a unifying verification framework for multi-server IoT is lacking. In this article, we propose a formal verification framework of AKA protocols for multi-server IoT (FVF-AKA). It supports the construction of CSP models for the AKA protocol, the implementation of the CSP models in PAT with C#, and the verification of formal models. With the help of C#, many complex functions in the AKA protocol can be implemented. We also design an algorithm to support automatic conversion from the CSP model to the PAT model. FVF-AKA can verify four fundamental properties (deadlock freedom, entity legitimacy, timeout delay, and session key consistency). It also supports the verification of security properties for the AKA protocol suffering from four different attacks (relay attacks, denial of service attacks, server spoofing attacks, and session key attacks). Our approach can be applied to most AKA protocols for multi-server IoT generally. By applying FVF-AKA to two AKA protocols, we can verify whether they satisfy the fundamental properties and analyze their security properties in vulnerable environments. Our work would help to analyze the AKA protocol for multi-server IoT and provide the foundation for the analysis of enhancing its security and robustness.<\/jats:p>","DOI":"10.1145\/3599731","type":"journal-article","created":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T11:34:13Z","timestamp":1685014453000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0977-2256","authenticated-orcid":false,"given":"Yuan","family":"Fei","sequence":"first","affiliation":[{"name":"Shanghai Normal University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6213-5520","authenticated-orcid":false,"given":"Jiaqi","family":"Yin","sequence":"additional","affiliation":[{"name":"Northwestern Polytechnical University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,11,20]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"371","volume-title":"ATVA","author":"Liu Yang","year":"2010","unstructured":"Yang Liu, Jun Sun, and Jin Song Dong. 2010. Developing model checkers using PAT. In ATVA. 371\u2013377."},{"key":"e_1_3_2_3_2","volume-title":"3G Security: Formal Analysis of the 3G Authentication Protocol","year":"2000","unstructured":"Third Generation Partnership Project (3GPP). 2000. 3G Security: Formal Analysis of the 3G Authentication Protocol. Technical Report TS 33.902 v3.1.0."},{"key":"e_1_3_2_4_2","first-page":"742","volume-title":"Network and System Security - 7th International Conference (NSS\u201913). Proceedings (Lecture Notes in Computer Science)","volume":"7873","author":"Aiash Mahdi","year":"2013","unstructured":"Mahdi Aiash. 2013. A formally verified initial authentication and key agreement protocol in heterogeneous environments using Casper\/FDR. In Network and System Security - 7th International Conference (NSS\u201913). Proceedings (Lecture Notes in Computer Science), Javier L\u00f3pez, Xinyi Huang, and Ravi S. Sandhu (Eds.), Vol. 7873. Springer, 742\u2013748."},{"key":"e_1_3_2_5_2","volume-title":"2014 IEEE REGION 10 SYMPOSIUM","author":"Alezabi Kamal Ali","year":"2014","unstructured":"Kamal Ali Alezabi, Fazirulhisyam Hashim, Shaiful Jahari Hashim, and Borhanuddin M. Ali. 2014. An efficient authentication and key agreement protocol for 4G (LTE) networks. In 2014 IEEE REGION 10 SYMPOSIUM."},{"key":"e_1_3_2_6_2","first-page":"205","volume-title":"the ACM Conference on Computer and Communications Security (CCS\u201912)","author":"Arapinis Myrto","year":"2012","unstructured":"Myrto Arapinis, Loretta Ilaria Mancini, Eike Ritter, Mark Ryan, Nico Golde, Kevin Redon, and Ravishankar Borgaonkar. 2012. New privacy issues in mobile telephony: Fix and verification. In the ACM Conference on Computer and Communications Security (CCS\u201912), Ting Yu, George Danezis, and Virgil D. Gligor (Eds.). ACM, 205\u2013216."},{"key":"e_1_3_2_7_2","article-title":"Formal analysis of 5G authentication","volume":"1806","author":"Basin David A.","year":"2018","unstructured":"David A. Basin, Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, Ralf Sasse, and Vincent Stettler. 2018. Formal analysis of 5G authentication. CoRR abs\/1806.10360 (2018).","journal-title":"CoRR"},{"key":"e_1_3_2_8_2","first-page":"139","volume-title":"Advances in Cryptology (EUROCRYPT\u201900), International Conference on the Theory and Application of Cryptographic Techniques, Proceeding (Lecture Notes in Computer Science)","volume":"1807","author":"Bellare Mihir","year":"2000","unstructured":"Mihir Bellare, David Pointcheval, and Phillip Rogaway. 2000. Authenticated key exchange secure against dictionary attacks. In Advances in Cryptology (EUROCRYPT\u201900), International Conference on the Theory and Application of Cryptographic Techniques, Proceeding (Lecture Notes in Computer Science), Bart Preneel (Ed.), Vol. 1807. Springer, 139\u2013155."},{"key":"e_1_3_2_9_2","first-page":"232","volume-title":"Advances in Cryptology (CRYPTO \u201993), 13th Annual International Cryptology Conference, Proceedings (Lecture Notes in Computer Science)","volume":"773","author":"Bellare Mihir","year":"1993","unstructured":"Mihir Bellare and Phillip Rogaway. 1993. Entity authentication and key distribution. In Advances in Cryptology (CRYPTO \u201993), 13th Annual International Cryptology Conference, Proceedings (Lecture Notes in Computer Science), Douglas R. Stinson (Ed.), Vol. 773, Springer, 232\u2013249."},{"key":"e_1_3_2_10_2","first-page":"57","volume-title":"Proceedings of the 27th Annual ACM Symposium on Theory of Computing","author":"Bellare Mihir","year":"1995","unstructured":"Mihir Bellare and Phillip Rogaway. 1995. Provably secure session key distribution: The three party case. In Proceedings of the 27th Annual ACM Symposium on Theory of Computing, Frank Thomson Leighton and Allan Borodin (Eds.). ACM, 57\u201366."},{"key":"e_1_3_2_11_2","first-page":"30","volume-title":"Cryptography and Coding, 6th IMA International Conference, Proceedings (Lecture Notes in Computer Science)","volume":"1355","author":"Blake-Wilson Simon","year":"1997","unstructured":"Simon Blake-Wilson, Don Johnson, and Alfred Menezes. 1997. Key agreement protocols and their security analysis. In Cryptography and Coding, 6th IMA International Conference, Proceedings (Lecture Notes in Computer Science), Michael Darnell (Ed.), Vol. 1355, Springer, 30\u201345."},{"key":"e_1_3_2_12_2","first-page":"339","volume-title":"Selected Areas in Cryptography\u201998 (SAC\u201998), Proceedings (Lecture Notes in Computer Science)","volume":"1556","author":"Blake-Wilson Simon","year":"1998","unstructured":"Simon Blake-Wilson and Alfred Menezes. 1998. Authenticated diffie-hellman key agreement protocols. In Selected Areas in Cryptography\u201998 (SAC\u201998), Proceedings (Lecture Notes in Computer Science), Stafford E. Tavares and Henk Meijer (Eds.), Vol. 1556, Springer, 339\u2013361."},{"key":"e_1_3_2_13_2","first-page":"69","volume-title":"Information Security and Privacy, 13th Australasian Conference (ACISP\u201908), Proceedings (Lecture Notes in Computer Science)","volume":"5107","author":"Boyd Colin","year":"2008","unstructured":"Colin Boyd, Yvonne Cliff, Juan Manuel Gonz\u00e1lez Nieto, and Kenneth G. Paterson. 2008. Efficient one-round key exchange in the standard model. In Information Security and Privacy, 13th Australasian Conference (ACISP\u201908), Proceedings (Lecture Notes in Computer Science), Yi Mu, Willy Susilo, and Jennifer Seberry (Eds.), Vol. 5107, Springer, 69\u201383."},{"issue":"3","key":"e_1_3_2_14_2","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","article-title":"A theory of communicating sequential processes","volume":"31","author":"Brookes Stephen D.","year":"1984","unstructured":"Stephen D. Brookes, C. A. R. Hoare, and A. W. Roscoe. 1984. A theory of communicating sequential processes. J. ACM 31, 3 (1984), 560\u2013599.","journal-title":"J. ACM"},{"key":"e_1_3_2_15_2","first-page":"453","volume-title":"Advances in Cryptology (EUROCRYPT\u201901), International Conference on the Theory and Application of Cryptographic Techniques, Proceeding (Lecture Notes in Computer Science)","volume":"2045","author":"Canetti Ran","year":"2001","unstructured":"Ran Canetti and Hugo Krawczyk. 2001. Analysis of key-exchange protocols and their use for building secure channels. In Advances in Cryptology (EUROCRYPT\u201901), International Conference on the Theory and Application of Cryptographic Techniques, Proceeding (Lecture Notes in Computer Science), Birgit Pfitzmann (Ed.), Vol. 2045. Springer, 453\u2013474."},{"issue":"1","key":"e_1_3_2_16_2","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/COMST.2019.2951818","article-title":"A survey on security aspects for 3GPP 5G networks","volume":"22","author":"Cao Jin","year":"2020","unstructured":"Jin Cao, Maode Ma, Hui Li, Ruhui Ma, Yunqing Sun, Pu Yu, and Lihui Xiong. 2020. A survey on security aspects for 3GPP 5G networks. IEEE Commun. Surv. Tutorials 22, 1 (2020), 170\u2013195.","journal-title":"IEEE Commun. Surv. Tutorials"},{"key":"e_1_3_2_17_2","first-page":"199","article-title":"Identity-based key agreement protocols from pairings","volume":"2006","author":"Chen Liqun","year":"2006","unstructured":"Liqun Chen, Zhaohui Cheng, and Nigel P. Smart. 2006. Identity-based key agreement protocols from pairings. IACR Cryptol. ePrint Arch. 2006 (2006), 199.","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_3_2_18_2","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1109\/SP.2018.00033","volume-title":"2018 IEEE Symposium on Security and Privacy (SP\u201918), Proceedings","author":"Cheval Vincent","year":"2018","unstructured":"Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2018. DEEPSEC: Deciding equivalence properties in security protocols theory and practice. In 2018 IEEE Symposium on Security and Privacy (SP\u201918), Proceedings. IEEE Computer Society, 529\u2013546."},{"key":"e_1_3_2_19_2","volume-title":"26th Annual Network and Distributed System Security Symposium (NDSS\u201919)","author":"Cremers Cas","year":"2019","unstructured":"Cas Cremers and Martin Dehnel-Wild. 2019. Component-based formal analysis of 5G-AKA: Channel assumptions and session confusion. In 26th Annual Network and Distributed System Security Symposium (NDSS\u201919). The Internet Society."},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1109\/SDS49854.2020.9143899","volume-title":"2020 7th International Conference on Software Defined Systems (SDS\u201920)","author":"Edris Ed Kamya Kiyemba","year":"2020","unstructured":"Ed Kamya Kiyemba Edris, Mahdi Aiash, and Jonathan Kok-Keng Loo. 2020. Formal verification and analysis of primary authentication based on 5G-AKA protocol. In 2020 7th International Conference on Software Defined Systems (SDS\u201920). IEEE, 256\u2013261."},{"issue":"3","key":"e_1_3_2_21_2","article-title":"Comparative modelling and verification of Pthreads and Dthreads","volume":"30","author":"Fei Yuan","year":"2018","unstructured":"Yuan Fei, Huibiao Zhu, Xi Wu, Huixing Fang, and Shengchao Qin. 2018. Comparative modelling and verification of Pthreads and Dthreads. Journal of Software: Evolution and Process 30, 3 (2018), 1\u201333.","journal-title":"Journal of Software: Evolution and Process"},{"issue":"4","key":"e_1_3_2_22_2","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1515\/popets-2016-0039","article-title":"Achieving better privacy for the 3GPP AKA protocol","volume":"2016","author":"Fouque Pierre-Alain","year":"2016","unstructured":"Pierre-Alain Fouque, Cristina Onete, and Benjamin Richard. 2016. Achieving better privacy for the 3GPP AKA protocol. Proc. Priv. Enhancing Technol. 2016, 4 (2016), 255\u2013275.","journal-title":"Proc. Priv. Enhancing Technol."},{"key":"e_1_3_2_23_2","article-title":"Communicating Sequential Processes. Prentice-Hall International","author":"Hoare C. A. R.","year":"1985","unstructured":"C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs.","journal-title":"Englewood Cliffs"},{"key":"e_1_3_2_24_2","first-page":"333","volume-title":"Proceedings of the 2009 ACM Symposium on Information, Computer and Communications Security (ASIACCS\u201909)","author":"Huang Hai","year":"2009","unstructured":"Hai Huang and Zhenfu Cao. 2009. An ID-based authenticated key exchange protocol based on bilinear Diffie-Hellman problem. In Proceedings of the 2009 ACM Symposium on Information, Computer and Communications Security (ASIACCS\u201909), Wanqing Li, Willy Susilo, Udaya Kiran Tupakula, Reihaneh Safavi-Naini, and Vijay Varadharajan (Eds.). ACM, 333\u2013342."},{"key":"e_1_3_2_25_2","volume-title":"25th Annual Network and Distributed System Security Symposium (NDSS\u201918)","author":"Hussain Syed Rafiul","year":"2018","unstructured":"Syed Rafiul Hussain, Omar Chowdhury, Shagufta Mehnaz, and Elisa Bertino. 2018. LTEInspector: A systematic approach for adversarial testing of 4G LTE. In 25th Annual Network and Distributed System Security Symposium (NDSS\u201918). The Internet Society."},{"key":"e_1_3_2_26_2","volume-title":"The 1st International Conference on Future Generation Communication Technologies","author":"Idrissi Younes El Hajjaji El","year":"2012","unstructured":"Younes El Hajjaji El Idrissi, Noureddine Zahid, and Mohamed Jedra. 2012. Security analysis of 3GPP (LTE)\u2013WLAN interworking and a new local authentication method based on EAP-AKA. In The 1st International Conference on Future Generation Communication Technologies."},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"15793","DOI":"10.1007\/s11042-017-5548-2","article-title":"Smart card-based secure authentication protocol in multi-server IoT environment","volume":"79","author":"Bae Won il","year":"2020","unstructured":"Won il Bae and Jin Kwak. 2020. Smart card-based secure authentication protocol in multi-server IoT environment. Multimedia Tools and Applications 79 (2020), 15793\u201315811.","journal-title":"Multimedia Tools and Applications"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","first-page":"89562","DOI":"10.1109\/ACCESS.2020.2993111","article-title":"Dependability analysis of 5G-AKA authentication service from server and user perspectives","volume":"8","author":"Jiang Lili","year":"2020","unstructured":"Lili Jiang, Xiaolin Chang, Jing Bai, Jelena V. Misic, Vojislav B. Misic, and Zhi Chen. 2020. Dependability analysis of 5G-AKA authentication service from server and user perspectives. IEEE Access 8 (2020), 89562\u201389574.","journal-title":"IEEE Access"},{"issue":"2","key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"277","DOI":"10.15388\/20-INFOR415","article-title":"Authenticated key agreement protocol based on provable secure cryptographic functions","volume":"31","author":"Kilciauskas Ausrys","year":"2020","unstructured":"Ausrys Kilciauskas, Gintaras Butkus, and Eligijus Sakalauskas. 2020. Authenticated key agreement protocol based on provable secure cryptographic functions. Informatica 31, 2 (2020), 277\u2013298.","journal-title":"Informatica"},{"issue":"1","key":"e_1_3_2_30_2","doi-asserted-by":"crossref","first-page":"111","DOI":"10.3745\/JIPS.2011.7.1.111","article-title":"Security framework for RFID-based applications in smart home environment","volume":"7","author":"Konidala Divyan M.","year":"2011","unstructured":"Divyan M. Konidala, Daeyoung Kim, Chan Yeob Yeun, and Byoungcheon Lee. 2011. Security framework for RFID-based applications in smart home environment. J. Inf. Process. Syst. 7, 1 (2011), 111\u2013120.","journal-title":"J. Inf. Process. Syst."},{"key":"e_1_3_2_31_2","first-page":"464","volume-title":"IEEE European Symposium on Security and Privacy (EuroS&P\u201919)","author":"Koutsos Adrien","year":"2019","unstructured":"Adrien Koutsos. 2019. The 5G-AKA authentication protocol privacy. In IEEE European Symposium on Security and Privacy (EuroS&P\u201919). IEEE, 464\u2013479."},{"key":"e_1_3_2_32_2","first-page":"549","volume-title":"Advances in Cryptology (ASIACRYPT\u201905), 11th International Conference on the Theory and Application of Cryptology and Information Security, Proceedings (Lecture Notes in Computer Science)","volume":"3788","author":"Kudla Caroline","year":"2005","unstructured":"Caroline Kudla and Kenneth G. Paterson. 2005. Modular security proofs for key agreement protocols. In Advances in Cryptology (ASIACRYPT\u201905), 11th International Conference on the Theory and Application of Cryptology and Information Security, Proceedings (Lecture Notes in Computer Science), Bimal K. Roy (Ed.), Vol. 3788. Springer, 549\u2013565."},{"key":"e_1_3_2_33_2","first-page":"1","volume-title":"Provable Security, 1st International Conference (ProvSec\u201907), Proceedings (Lecture Notes in Computer Science)","volume":"4784","author":"LaMacchia Brian A.","year":"2007","unstructured":"Brian A. LaMacchia, Kristin E. Lauter, and Anton Mityagin. 2007. Stronger security of authenticated key exchange. In Provable Security, 1st International Conference (ProvSec\u201907), Proceedings (Lecture Notes in Computer Science), Willy Susilo, Joseph K. Liu, and Yi Mu (Eds.), Vol. 4784, Springer, 1\u201316."},{"issue":"11","key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"770","DOI":"10.1145\/358790.358797","article-title":"Password authentification with insecure communication","volume":"24","author":"Lamport Leslie","year":"1981","unstructured":"Leslie Lamport. 1981. Password authentification with insecure communication. Commun. ACM 24, 11 (1981), 770\u2013772.","journal-title":"Commun. ACM"},{"issue":"6","key":"e_1_3_2_35_2","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1007\/s10207-014-0231-3","article-title":"Anonymity guarantees of the UMTS\/LTE authentication and connection protocol","volume":"13","author":"Lee Ming-Feng","year":"2014","unstructured":"Ming-Feng Lee, Nigel P. Smart, Bogdan Warinschi, and Gaven J. Watson. 2014. Anonymity guarantees of the UMTS\/LTE authentication and connection protocol. Int. J. Inf. Sec. 13, 6 (2014), 513\u2013527.","journal-title":"Int. J. Inf. Sec."},{"key":"e_1_3_2_36_2","volume-title":"2011 7th International Conference on Wireless Communications, Networking and Mobile Computing","author":"Li Xiehua","year":"2011","unstructured":"Xiehua Li and Yongjun Wang. 2011. Security enhanced authentication and key agreement protocol for LTE\/SAE network. In 2011 7th International Conference on Wireless Communications, Networking and Mobile Computing."},{"issue":"2","key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"763","DOI":"10.1016\/j.jnca.2011.11.009","article-title":"An efficient and security dynamic identity based authentication protocol for multi-server architecture using smart cards","volume":"35","author":"Li Xiong","year":"2012","unstructured":"Xiong Li, Yongping Xiong, Jian Ma, and Wendong Wang. 2012. An efficient and security dynamic identity based authentication protocol for multi-server architecture using smart cards. J. Netw. Comput. Appl. 35, 2 (2012), 763\u2013769.","journal-title":"J. Netw. Comput. Appl."},{"key":"e_1_3_2_38_2","first-page":"81","volume-title":"3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE\u201909)","author":"Liu Yang","year":"2009","unstructured":"Yang Liu, Jun Pang, Jun Sun, and Jianhua Zhao. 2009. Verification of population ring protocols in PAT. In 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE\u201909). 81\u201389."},{"issue":"4","key":"e_1_3_2_39_2","article-title":"Secret sharing-based authentication and key agreement protocol for machine-type communications","volume":"15","author":"Lopes Ana Paula Golembiouski","year":"2019","unstructured":"Ana Paula Golembiouski Lopes, Lucas O. Hilgert, Paulo R. L. Gondim, and Jaime Lloret. 2019. Secret sharing-based authentication and key agreement protocol for machine-type communications. Int. J. Distributed Sens. Networks 15, 4 (2019), 1\u201321.","journal-title":"Int. J. Distributed Sens. Networks"},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1109\/CSFW.1997.596782","volume-title":"10th Computer Security Foundations Workshop (CSFW \u201997)","author":"Lowe Gavin","year":"1997","unstructured":"Gavin Lowe. 1997. A hierarchy of authentication specification. In 10th Computer Security Foundations Workshop (CSFW \u201997). IEEE Computer Society, 31\u201344."},{"issue":"10","key":"e_1_3_2_41_2","doi-asserted-by":"crossref","first-page":"659","DOI":"10.1109\/32.637148","article-title":"Using CSP to detect errors in the TMN protocol","volume":"23","author":"Lowe Gavin","year":"1997","unstructured":"Gavin Lowe and A. W. Roscoe. 1997. Using CSP to detect errors in the TMN protocol. IEEE Trans. Software Eng. 23, 10 (1997), 659\u2013669.","journal-title":"IEEE Trans. Software Eng."},{"key":"e_1_3_2_42_2","volume-title":"Handbook of Applied Cryptography","author":"Menezes Alfred","year":"1996","unstructured":"Alfred Menezes, Paul C. van Oorschot, and Scott A. Vanstone. 1996. Handbook of Applied Cryptography. CRC Press."},{"issue":"2","key":"e_1_3_2_43_2","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/j.compeleceng.2011.03.001","article-title":"Strongly secure identity-based authenticated key agreement protocols","volume":"37","author":"Ni Liang","year":"2011","unstructured":"Liang Ni, Gongliang Chen, Jianhua Li, and Yanyan Hao. 2011. Strongly secure identity-based authenticated key agreement protocols. Comput. Electr. Eng. 37, 2 (2011), 205\u2013217.","journal-title":"Comput. Electr. Eng."},{"key":"e_1_3_2_44_2","first-page":"226","volume-title":"24th IEEE International Conference on Advanced Information Networking and Applications Workshops (WAINA\u201910)","author":"Ota Haruki","year":"2010","unstructured":"Haruki Ota, Shinsaku Kiyomoto, and Toshiaki Tanaka. 2010. Security verification for authentication and key exchange protocols, revisited. In 24th IEEE International Conference on Advanced Information Networking and Applications Workshops (WAINA\u201910). IEEE Computer Society, 226\u2013233."},{"key":"e_1_3_2_45_2","volume-title":"The Theory and Practice of Concurrency","author":"Roscoe A. W.","year":"1997","unstructured":"A. W. Roscoe. 1997. The Theory and Practice of Concurrency. Prentice Hall."},{"key":"e_1_3_2_46_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"Roscoe A. W.","year":"2010","unstructured":"A. W. Roscoe. 2010. Understanding Concurrent Systems. Springer."},{"key":"e_1_3_2_47_2","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1109\/SP.2014.19","volume-title":"2014 IEEE Symposium on Security and Privacy (SP\u201914)","author":"Schmidt Benedikt","year":"2014","unstructured":"Benedikt Schmidt, Ralf Sasse, Cas Cremers, and David A. Basin. 2014. Automated verification of group key agreement protocols. In 2014 IEEE Symposium on Security and Privacy (SP\u201914). IEEE Computer Society, 179\u2013194."},{"key":"e_1_3_2_48_2","first-page":"47","volume-title":"Advances in Cryptology (CRYPTO \u201984), Proceedings (Lecture Notes in Computer Science)","volume":"196","author":"Shamir Adi","year":"1984","unstructured":"Adi Shamir. 1984. Identity-based cryptosystems and signature schemes. In Advances in Cryptology (CRYPTO \u201984), Proceedings (Lecture Notes in Computer Science), G. R. Blakley and David Chaum (Eds.), Vol. 196, Springer, 47\u201353."},{"issue":"1","key":"e_1_3_2_49_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s11704-013-3091-5","article-title":"Model checking with fairness assumptions using PAT","volume":"8","author":"Si Yuanjie","year":"2014","unstructured":"Yuanjie Si, Jun Sun, Yang Liu, Jin Song Dong, Jun Pang, Shao Jie Zhang, and Xiaohu Yang. 2014. Model checking with fairness assumptions using PAT. Frontiers of Computer Science 8, 1 (2014), 1\u201316.","journal-title":"Frontiers of Computer Science"},{"key":"e_1_3_2_50_2","first-page":"111","article-title":"An identity based authenticated key agreement protocol based on the weil pairing","volume":"2001","author":"Smart Nigel P.","year":"2001","unstructured":"Nigel P. Smart. 2001. An identity based authenticated key agreement protocol based on the weil pairing. IACR Cryptol. ePrint Arch. 2001 (2001), 111.","journal-title":"IACR Cryptol. ePrint Arch."},{"issue":"2","key":"e_1_3_2_51_2","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1016\/j.jnca.2010.11.011","article-title":"A secure dynamic identity based authentication protocol for multi-server architecture","volume":"34","author":"Sood Sandeep K.","year":"2011","unstructured":"Sandeep K. Sood, Anil Kumar Sarje, and Kuldip Singh. 2011. A secure dynamic identity based authentication protocol for multi-server architecture. J. Netw. Comput. Appl. 34, 2 (2011), 609\u2013618.","journal-title":"J. Netw. Comput. Appl."},{"key":"e_1_3_2_52_2","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation, 3rd International Symposium (ISoLA\u201908), Proceedings","author":"Sun Jun","year":"2008","unstructured":"Jun Sun, Yang Liu, and Jin Song Dong. 2008. Model checking CSP revisited: Introducing a process analysis toolkit. In Leveraging Applications of Formal Methods, Verification and Validation, 3rd International Symposium (ISoLA\u201908), Proceedings. 307\u2013322."},{"issue":"1","key":"e_1_3_2_53_2","first-page":"3","article-title":"Modeling and verifying hierarchical real-time systems using stateful timed CSP","volume":"22","author":"Sun Jun","year":"2013","unstructured":"Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, and \u00c9tienne Andr\u00e9. 2013. Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Softw. Eng. Methodol. 22, 1 (2013), 3.","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"e_1_3_2_54_2","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification, 21st International Conference, (CAV\u201909)","author":"Sun Jun","year":"2009","unstructured":"Jun Sun, Yang Liu, Jin Song Dong, and Jun Pang. 2009. PAT: Towards flexible verification under fairness. In Computer Aided Verification, 21st International Conference, (CAV\u201909). 709\u2013714."},{"key":"e_1_3_2_55_2","first-page":"1605","volume-title":"2013 IEEE International Conference on High Performance Computing and Communications (HPCC\u201913), and IEEE International Conference on Embedded and Ubiquitous Computing (EUC\u201913)","author":"Tang Chunyu","year":"2013","unstructured":"Chunyu Tang, David A. Naumann, and Susanne Wetzel. 2013. Analysis of authentication and key establishment in inter-generational mobile telephony. In 2013 IEEE International Conference on High Performance Computing and Communications (HPCC\u201913), and IEEE International Conference on Embedded and Ubiquitous Computing (EUC\u201913). IEEE, 1605\u20131614."},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1145\/2810103.2813615","volume-title":"Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security","author":"Broek Fabian van den","year":"2015","unstructured":"Fabian van den Broek, Roel Verdult, and Joeri de Ruiter. 2015. Defeating IMSI catchers. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Indrajit Ray, Ninghui Li, and Christopher Kruegel (Eds.). ACM, 340\u2013351."},{"issue":"8","key":"e_1_3_2_57_2","doi-asserted-by":"crossref","first-page":"1358","DOI":"10.1007\/s11432-009-0135-4","article-title":"Perfect forward secure identity-based authenticated key agreement protocol in the escrow mode","volume":"52","author":"Wang Shengbao","year":"2009","unstructured":"Shengbao Wang, Zhenfu Cao, ZhaoHui Cheng, and Kim-Kwang Raymond Choo. 2009. Perfect forward secure identity-based authenticated key agreement protocol in the escrow mode. Sci. China Ser. F Inf. Sci. 52, 8 (2009), 1358\u20131370.","journal-title":"Sci. China Ser. F Inf. Sci."},{"issue":"1","key":"e_1_3_2_58_2","first-page":"66","article-title":"Hierarchical key derivation scheme for group-oriented communication systems","volume":"1","author":"Wang Shiuh-Jeng","year":"2010","unstructured":"Shiuh-Jeng Wang, Yuh-Ren Tsai, Chien-Chih Shen, and Pin-You Chen. 2010. Hierarchical key derivation scheme for group-oriented communication systems. Int. J. Inf. Technol. Commun. Convergence 1, 1 (2010), 66\u201376.","journal-title":"Int. J. Inf. Technol. Commun. Convergence"},{"issue":"1","key":"e_1_3_2_59_2","first-page":"4","article-title":"On secure communication in integrated heterogeneous wireless networks","volume":"1","author":"Xie Bin","year":"2010","unstructured":"Bin Xie, Anup Kumar, David Zhao, Ranga Reddy, and Bing He. 2010. On secure communication in integrated heterogeneous wireless networks. Int. J. Inf. Technol. Commun. Convergence 1, 1 (2010), 4\u201323.","journal-title":"Int. J. Inf. Technol. Commun. Convergence"},{"issue":"1","key":"e_1_3_2_60_2","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/j.jcss.2013.07.004","article-title":"A lightweight dynamic pseudonym identity based authentication and key agreement protocol without verification tables for multi-server architecture","volume":"80","author":"Xue Kaiping","year":"2014","unstructured":"Kaiping Xue, Peilin Hong, and Changsha Ma. 2014. A lightweight dynamic pseudonym identity based authentication and key agreement protocol without verification tables for multi-server architecture. J. Comput. Syst. Sci. 80, 1 (2014), 195\u2013206.","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_3_2_61_2","first-page":"503","volume-title":"4th IEEE International Conference on Data Science in Cyberspace (DSC\u201919)","author":"Zhang Jingjing","year":"2019","unstructured":"Jingjing Zhang, Qiang Wang, Lin Yang, and Tao Feng. 2019. Formal verification of 5G-EAP-TLS authentication protocol. In 4th IEEE International Conference on Data Science in Cyberspace (DSC\u201919). IEEE, 503\u2013509."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3599731","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3599731","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:11Z","timestamp":1750178831000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3599731"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,20]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12,31]]}},"alternative-id":["10.1145\/3599731"],"URL":"https:\/\/doi.org\/10.1145\/3599731","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,11,20]]},"assertion":[{"value":"2021-12-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-05-18","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}