{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T01:11:07Z","timestamp":1769908267165,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,30]],"date-time":"2022-05-30T00:00:00Z","timestamp":1653868800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EPSRC UK","award":["autopass"],"award-info":[{"award-number":["autopass"]}]},{"DOI":"10.13039\/100011403","name":"GCHQ","doi-asserted-by":"publisher","award":["5g-techsec"],"award-info":[{"award-number":["5g-techsec"]}],"id":[{"id":"10.13039\/100011403","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,30]]},"DOI":"10.1145\/3488932.3517421","type":"proceedings-article","created":{"date-parts":[[2022,5,24]],"date-time":"2022-05-24T04:23:26Z","timestamp":1653366206000},"page":"237-251","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["The 5G Key-Establishment Stack"],"prefix":"10.1145","author":[{"given":"Rhys","family":"Miller","sequence":"first","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ioana","family":"Boureanu","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Wesemeyer","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christopher J. P.","family":"Newton","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,5,30]]},"reference":[{"key":"e_1_3_2_2_1_1","first-page":"512","article-title":"a. 5G Security Assurance Specification (SCAS); Access and Mobility management Function (AMF)","volume":"33","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 a. 5G Security Assurance Specification (SCAS); Access and Mobility management Function (AMF) . Technical Specification (TS) 33 . 512 . 3GPP. Version 16.3.0. 3GPP. 2020 a. 5G Security Assurance Specification (SCAS); Access and Mobility management Function (AMF). Technical Specification (TS) 33.512. 3GPP. Version 16.3.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_2_1","first-page":"515","article-title":"b. 5G Security Assurance Specification (SCAS) for the Session Management Function (SMF) network product class","volume":"33","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 b. 5G Security Assurance Specification (SCAS) for the Session Management Function (SMF) network product class . Technical Specification (TS) 33 . 515 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/133500_133599\/133515\/16.02.00_60\/ts_133515v160200p.pdf Version 16.2.0. 3GPP. 2020 b. 5G Security Assurance Specification (SCAS) for the Session Management Function (SMF) network product class. Technical Specification (TS) 33.515. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/133500_133599\/133515\/16.02.00_60\/ts_133515v160200p.pdf Version 16.2.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_3_1","first-page":"244","article-title":"c. Interface between the Control Plane and the User Plane nodes","volume":"29","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 c. Interface between the Control Plane and the User Plane nodes . Technical Specification (TS) 29 . 244 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/129200_129299\/129244\/16.05.00_60\/ts_129244v160500p.pdf Version 16.5.0. 3GPP. 2020 c. Interface between the Control Plane and the User Plane nodes. Technical Specification (TS) 29.244. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/129200_129299\/129244\/16.05.00_60\/ts_129244v160500p.pdf Version 16.5.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_4_1","first-page":"501","article-title":"d. Non-Access-Stratum (NAS) protocol for 5G System (5GS)","volume":"24","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 d. Non-Access-Stratum (NAS) protocol for 5G System (5GS) . Technical Specification (TS) 24 . 501 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/124500_124599\/124501\/16.05.01_60\/ts_124501v160501p.pdf Version 16.5.1. 3GPP. 2020 d. Non-Access-Stratum (NAS) protocol for 5G System (5GS). Technical Specification (TS) 24.501. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/124500_124599\/124501\/16.05.01_60\/ts_124501v160501p.pdf Version 16.5.1.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_5_1","first-page":"415","article-title":"e. PDU session user plane protocol","volume":"38","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 e. PDU session user plane protocol . Technical Specification (TS) 38 . 415 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/138400_138499\/138415\/16.01.00_60\/ts_138415v160100p.pdf Version 16.1.0. 3GPP. 2020 e. PDU session user plane protocol. Technical Specification (TS) 38.415. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/138400_138499\/138415\/16.01.00_60\/ts_138415v160100p.pdf Version 16.1.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_6_1","unstructured":"3GPP. 2020 f. Release 16. https:\/\/www.3gpp.org\/release-16  3GPP. 2020 f. Release 16. https:\/\/www.3gpp.org\/release-16"},{"key":"e_1_3_2_2_7_1","first-page":"501","article-title":"g. System architecture for the 5G System (5GS)","volume":"23","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 g. System architecture for the 5G System (5GS) . Technical Specification (TS) 23 . 501 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/123500_123599\/123501\/16.06.00_60\/ts_123501v160600p.pdf Version 16.0.0. 3GPP. 2020 g. System architecture for the 5G System (5GS). Technical Specification (TS) 23.501. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/123500_123599\/123501\/16.06.00_60\/ts_123501v160600p.pdf Version 16.0.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_8_1","first-page":"501","article-title":"h. System architecture for the 5G System (5GS)","volume":"23","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 h. System architecture for the 5G System (5GS) . Technical Specification (TS) 23 . 501 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/123500_123599\/123501\/16.06.00_60\/ts_123501v160600p.pdf Version 16.0.0. 3GPP. 2020 h. System architecture for the 5G System (5GS). Technical Specification (TS) 23.501. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/123500_123599\/123501\/16.06.00_60\/ts_123501v160600p.pdf Version 16.0.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_9_1","first-page":"316","article-title":"i. Wireless and wireline onvergence access support for the 5G System (5GS)","volume":"23","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 i. Wireless and wireline onvergence access support for the 5G System (5GS) . Technical Specification (TS) 23 . 316 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/123300_123399\/123316\/16.04.00_60\/ts_123316v160400p.pdf Version 16.0.0. 3GPP. 2020 i. Wireless and wireline onvergence access support for the 5G System (5GS). Technical Specification (TS) 23.316. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/123300_123399\/123316\/16.04.00_60\/ts_123316v160400p.pdf Version 16.0.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_10_1","first-page":"423","article-title":"j. Xn Application Protocol (XnAP)","volume":"38","author":"GPP.","year":"2020","unstructured":"3 GPP. 2020 j. Xn Application Protocol (XnAP) . Technical Specification (TS) 38 . 423 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/138400_138499\/138423\/16.02.00_60\/ts_138423v160200p.pdf Version 16.2.0. 3GPP. 2020 j. Xn Application Protocol (XnAP). Technical Specification (TS) 38.423. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/138400_138499\/138423\/16.02.00_60\/ts_138423v160200p.pdf Version 16.2.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_11_1","first-page":"502","article-title":"Procedures for the 5G System","volume":"23","author":"GPP.","year":"2021","unstructured":"3 GPP. 2021 . Procedures for the 5G System . Technical Specification (TS) 23 . 502 . 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/123500_123599\/123502\/15.02.00_60\/ts_123502v150200p.pdf Version 16.7.0. 3GPP. 2021. Procedures for the 5G System. Technical Specification (TS) 23.502. 3GPP. https:\/\/www.etsi.org\/deliver\/etsi_ts\/123500_123599\/123502\/15.02.00_60\/ts_123502v150200p.pdf Version 16.7.0.","journal-title":"Technical Specification (TS)"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"e_1_3_2_2_13_1","volume-title":"RAID '14 (2014) (LNCS)","author":"Henda Noomene Ben","unstructured":"Noomene Ben Henda and Karl Norrman . [n.,d.]. Formal Analysis of Security Procedures in LTE - A Feasibility Study . In RAID '14 (2014) (LNCS) . Springer , 341--361. Noomene Ben Henda and Karl Norrman. [n.,d.]. Formal Analysis of Security Procedures in LTE - A Feasibility Study. In RAID '14 (2014) (LNCS). Springer, 341--361."},{"key":"e_1_3_2_2_14_1","volume-title":"An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In CSFW '14","author":"Blanchet Bruno","year":"2001","unstructured":"Bruno Blanchet . 2001 . An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In CSFW '14 . IEEE Computer Society, 82--96. Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In CSFW '14. IEEE Computer Society, 82--96."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.2478\/popets-2019-0039"},{"key":"e_1_3_2_2_17_1","unstructured":"Ioana Boureanu Stephan Wesemeyer Chris Newton and Rhys Miller. 2022. 5G Tamarin models and 5G Emulator. GitHub https:\/\/fmsec.github.io\/5gtechsec.github.io\/.  Ioana Boureanu Stephan Wesemeyer Chris Newton and Rhys Miller. 2022. 5G Tamarin models and 5G Emulator. GitHub https:\/\/fmsec.github.io\/5gtechsec.github.io\/."},{"key":"e_1_3_2_2_18_1","volume-title":"Network and System Security","author":"Chen Chien-Ming","unstructured":"Chien-Ming Chen , Tsu-Yang Wu , Raylin Tso , and Mu-En Wu. 2014. Security Analysis and Improvement of Femtocell Access Control . In Network and System Security . Springer International Publishing , Cham , 223--232. Chien-Ming Chen, Tsu-Yang Wu, Raylin Tso, and Mu-En Wu. 2014. Security Analysis and Improvement of Femtocell Access Control. In Network and System Security. Springer International Publishing, Cham, 223--232."},{"key":"e_1_3_2_2_19_1","volume-title":"On Post-compromise Security. In CSF '16","author":"Cohn-Gordon Katriel","year":"2016","unstructured":"Katriel Cohn-Gordon , Cas Cremers , and Luke Garratt . 2016 . On Post-compromise Security. In CSF '16 . 164--178. https:\/\/doi.org\/10.1109\/CSF.2016.19 10.1109\/CSF.2016.19 Katriel Cohn-Gordon, Cas Cremers, and Luke Garratt. 2016. On Post-compromise Security. In CSF '16. 164--178. https:\/\/doi.org\/10.1109\/CSF.2016.19"},{"key":"e_1_3_2_2_20_1","volume-title":"Formal verification of LTE-UMTS and LTE-LTE handover procedures","author":"Copet Piergiuseppe Bettassa","year":"2016","unstructured":"Piergiuseppe Bettassa Copet , Guido Marchetto , Riccardo Sisto , and Luciana Costa . [n.,d.] a. Formal verification of LTE-UMTS and LTE-LTE handover procedures ., Vol. 50 ( [n.,d.]), 92--106. https:\/\/doi.org\/10.1016\/j.csi. 2016 .08.009 10.1016\/j.csi.2016.08.009 Piergiuseppe Bettassa Copet, Guido Marchetto, Riccardo Sisto, and Luciana Costa. [n.,d.] a. Formal verification of LTE-UMTS and LTE-LTE handover procedures., Vol. 50 ( [n.,d.]), 92--106. https:\/\/doi.org\/10.1016\/j.csi.2016.08.009"},{"key":"e_1_3_2_2_21_1","volume-title":"ISCC '15","author":"Copet Piergiuseppe Bettassa","year":"2015","unstructured":"Piergiuseppe Bettassa Copet , Guido Marchetto , Riccardo Sisto , and Luciana Costa . [n.,d.] b. Formal verification of LTE-UMTS handover procedures . In ISCC '15 ( 2015 ). IEEE, 738--744. Piergiuseppe Bettassa Copet, Guido Marchetto, Riccardo Sisto, and Luciana Costa. [n.,d.] b. Formal verification of LTE-UMTS handover procedures. In ISCC '15 (2015). IEEE, 738--744."},{"key":"e_1_3_2_2_22_1","volume-title":"CCS '17","author":"Cremers Cas","unstructured":"Cas Cremers , Marko Horvat , Jonathan Hoyland , Sam Scott , and Thyla van der Merwe. 2017. A comprehensive symbolic analysis of TLS 1.3 . In CCS '17 . 1773--1788. Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A comprehensive symbolic analysis of TLS 1.3. In CCS '17. 1773--1788."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_2_24_1","volume-title":"Undecidability of Bounded Security Protocols. In FMSP'99","author":"Durgin N.","unstructured":"N. Durgin , P. Lincoln , J. Mitchell , and A. Scedrov . 1999 . Undecidability of Bounded Security Protocols. In FMSP'99 . ACM. N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. 1999. Undecidability of Bounded Security Protocols. In FMSP'99. ACM."},{"key":"e_1_3_2_2_25_1","volume-title":"SDS '20","author":"Kiyemba Edris Ed Kamya","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 SDS '20 . IEEE, 256--261. 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 SDS '20. IEEE, 256--261."},{"key":"e_1_3_2_2_26_1","unstructured":"Erricson. 2020. 5 key facts about 5G radio access networks. https:\/\/www.ericsson.com\/495922\/assets\/local\/policy-makers-and-regulators\/5-key-facts-about-5g-radio-access-networks.pdf.  Erricson. 2020. 5 key facts about 5G radio access networks. https:\/\/www.ericsson.com\/495922\/assets\/local\/policy-makers-and-regulators\/5-key-facts-about-5g-radio-access-networks.pdf."},{"key":"e_1_3_2_2_27_1","unstructured":"Infrastructure and Projects Authority. 2018. Analysis of the National Infrastructure and Construction Pipeline. https:\/\/www.gov.uk\/government\/publications\/national-infrastructure-and-construction-pipeline-2018  Infrastructure and Projects Authority. 2018. Analysis of the National Infrastructure and Construction Pipeline. https:\/\/www.gov.uk\/government\/publications\/national-infrastructure-and-construction-pipeline-2018"},{"key":"e_1_3_2_2_28_1","volume-title":"EuroS&P '19","author":"Koutsos Adrien","unstructured":"Adrien Koutsos . 2019. The 5G-AKA authentication protocol privacy . In EuroS&P '19 . IEEE , 464--479. Adrien Koutsos. 2019. The 5G-AKA authentication protocol privacy. In EuroS&P '19. IEEE, 464--479."},{"key":"e_1_3_2_2_29_1","unstructured":"Philippe Z Lin Charles Perine and Rainer Vosseler. 2017. Attacks From 4G\/5G Core Networks: Risks of the Industrial IoT in Compromised Campus Networks. https:\/\/documents.trendmicro.com\/assets\/white_papers\/wp-attacks-from-4G-5G-core-networks.pdf.  Philippe Z Lin Charles Perine and Rainer Vosseler. 2017. Attacks From 4G\/5G Core Networks: Risks of the Industrial IoT in Compromised Campus Networks. https:\/\/documents.trendmicro.com\/assets\/white_papers\/wp-attacks-from-4G-5G-core-networks.pdf."},{"key":"e_1_3_2_2_30_1","volume-title":"CAV '13 (2013) (LNCS)","author":"Meier Simon","unstructured":"Simon Meier , Benedikt Schmidt , Cas Cremers , and David Basin . [n.,d.]. The TAMARIN Prover for the Symbolic Analysis of Security Protocols . In CAV '13 (2013) (LNCS) . Springer , 696--701. Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. [n.,d.]. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In CAV '13 (2013) (LNCS). Springer, 696--701."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3448300.3467823"},{"key":"e_1_3_2_2_32_1","volume-title":"Partial-Order Reduction in the Weak Modal Mu-Calculus. In CONCUR '97 (LNCS","volume":"24","author":"Ramakrishma Y. S.","unstructured":"Y. S. Ramakrishma and S. A. Smolka . 1997 . Partial-Order Reduction in the Weak Modal Mu-Calculus. In CONCUR '97 (LNCS , Vol. 1243). Springer, 5-- 24 . Y. S. Ramakrishma and S. A. Smolka. 1997. Partial-Order Reduction in the Weak Modal Mu-Calculus. In CONCUR '97 (LNCS, Vol. 1243). Springer, 5--24."},{"key":"e_1_3_2_2_33_1","unstructured":"The Tamarin Team. 2016. Tamarin prover manual. https:\/\/tamarin-prover.github.io\/manual\/tex\/tamarin-manual.pdf [Online: accessed 09-April-2019].  The Tamarin Team. 2016. Tamarin prover manual. https:\/\/tamarin-prover.github.io\/manual\/tex\/tamarin-manual.pdf [Online: accessed 09-April-2019]."}],"event":{"name":"ASIA CCS '22: ACM Asia Conference on Computer and Communications Security","location":"Nagasaki Japan","acronym":"ASIA CCS '22","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2022 ACM on Asia Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3488932.3517421","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3488932.3517421","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:31:27Z","timestamp":1750188687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3488932.3517421"}},"subtitle":["In-Depth Formal Verification and Experimentation"],"short-title":[],"issued":{"date-parts":[[2022,5,30]]},"references-count":33,"alternative-id":["10.1145\/3488932.3517421","10.1145\/3488932"],"URL":"https:\/\/doi.org\/10.1145\/3488932.3517421","relation":{},"subject":[],"published":{"date-parts":[[2022,5,30]]},"assertion":[{"value":"2022-05-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}