{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:46:24Z","timestamp":1767339984162,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":18,"publisher":"Springer Singapore","isbn-type":[{"type":"print","value":"9789811674426"},{"type":"electronic","value":"9789811674433"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-981-16-7443-3_13","type":"book-chapter","created":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T17:54:45Z","timestamp":1636480485000},"page":"222-233","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Proving Mutual Authentication Property of 5G-AKA Protocol Based on PCL"],"prefix":"10.1007","author":[{"given":"Tong","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Meihua","family":"Xiao","sequence":"additional","affiliation":[]},{"given":"Ri","family":"Ouyang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,10]]},"reference":[{"key":"13_CR1","unstructured":"GSMA Global Mobile Trends 2017. https:\/\/www.gsma.com\/globalmobiletrends\/. Accessed 6 May 2018"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Kobeissi, N., Bhargavan, K., Blanchet, B.: Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In: Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach. IEEE (2017)","DOI":"10.1109\/EuroSP.2017.38"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy (SP). IEEE (2017)","DOI":"10.1109\/SP.2017.26"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Cremers, C., Horvat, M., Hoyland, J., et al.: A comprehensive symbolic analysis of TLS 1.3. In: ACM SIGSAC Conference, pp. 1773\u20131788. ACM (2017)","DOI":"10.1145\/3133956.3134063"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Cremers, C., Horvat, M., Scott, S., et al.: Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication. In: EEE Symposium on Security and Privacy (SP). IEEE (2016)","DOI":"10.1109\/SP.2016.35"},{"issue":"6","key":"13_CR6","doi-asserted-by":"publisher","first-page":"817","DOI":"10.3233\/JCS-130472","volume":"21","author":"B David","year":"2013","unstructured":"David, B., Cas, C., Simon, M.: Provably repairing the ISO\/IEC 9798 standard for entity authentication. J. Comput. Secur. 21(6), 817\u2013846 (2013)","journal-title":"J. Comput. Secur."},{"issue":"30","key":"13_CR7","first-page":"33","volume":"1","author":"J Wang","year":"2019","unstructured":"Wang, J., Zhan, N.J., Feng, X.Y., Liu, Z.M.: Overview of formal methods. J. Softw. 1(30), 33\u201361 (2019)","journal-title":"J. Softw."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Datta, A., Derek, A., Mitchell, J., et al.: A derivation system for security protocols and its logical formalization. In: Proceedings of 16th IEEE Computer Security Foundations Workshop, pp. 109\u2013125. IEEE (2003)","DOI":"10.1109\/CSFW.2003.1212708"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Li, X., Zhang, X.: Formal verification for EAP-AKA protocol in 3G networks. In: 2009 International Conference on Computational Intelligence and Software Engineering. IEEE (2009)","DOI":"10.1109\/CISE.2009.5363413"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-48285-7_20","volume-title":"Advances in Cryptology \u2014 EUROCRYPT \u201993","author":"C Boyd","year":"1994","unstructured":"Boyd, C., Mao, W.: On a limitation of BAN logic. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 240\u2013247. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-48285-7_20"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Mancini, L., Ritter, E., Ryan, M.: New privacy issues in mobile telephony: fix and verification. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, pp. 205\u2013216. ACM, New York (2012)","DOI":"10.1145\/2382196.2382221"},{"issue":"3","key":"13_CR12","first-page":"108","volume":"2019","author":"R Borgaonkar","year":"2019","unstructured":"Borgaonkar, R., Hirschi, L., Park, S., Shaik, A.: New privacy threat on 3G, 4G, and upcoming 5G AKA protocols. Proc. Priv. Enhanc. Technol. 2019(3), 108\u2013127 (2019)","journal-title":"Proc. Priv. Enhanc. Technol."},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"624","DOI":"10.1007\/978-3-319-07782-6_56","volume-title":"Wireless Algorithms, Systems, and Applications","author":"C Hahn","year":"2014","unstructured":"Hahn, C., Kwon, H., Kim, D., Kang, K., Hur, J.: A privacy threat in 4th generation mobile telephony and its countermeasure. In: Cai, Z., Wang, C., Cheng, S., Wang, H., Gao, H. (eds.) WASA 2014. LNCS, vol. 8491, pp. 624\u2013635. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07782-6_56"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Hu, X., Liu, C., Liu, S., You, W., Zhao, Y.: A Systematic analysis method for 5G non-access stratum signalling security. IEEE Access pp(99), 125424\u2013125441 (2019)","DOI":"10.1109\/ACCESS.2019.2937997"},{"key":"13_CR15","unstructured":"TS 33.501: Security architecture and procedures for 5G system. https:\/\/www.tech-invite.com\/3m33\/tinv-3gpp-33-501.htmls. Accessed 2 Aug 2020"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Basin, D., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: A formal analysis of 5G authentication. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp. 1383\u20131396. ACM, Toronto (2018)","DOI":"10.1145\/3243734.3243846"},{"issue":"1","key":"13_CR17","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/j.entcs.2007.02.012","volume":"172","author":"A Datta","year":"2007","unstructured":"Datta, A., Roy, A., Mitchell, J., et al.: Protocol composition logic (PCL). Electron. Notes Theor. Comput. Sci. 172(1), 311\u2013358 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Datta, A., Derek, A., Mitchell, J. et al.: Secure protocol composition. In: Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering, pp. 11\u201323. ACM (2003)","DOI":"10.1145\/1035429.1035431"}],"container-title":["Communications in Computer and Information Science","Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-16-7443-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T21:02:57Z","timestamp":1726088577000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-16-7443-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9789811674426","9789811674433"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-981-16-7443-3_13","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"10 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NCTCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"National Conference of Theoretical Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Yinchuan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"39","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nctcs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.ccf.org.cn\/TCS2021","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"CCF Consys","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"145","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}