{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,16]],"date-time":"2026-09-16T16:58:55Z","timestamp":1789577935158,"version":"build-2803163510"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031773815","type":"print"},{"value":"9783031773822","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-77382-2_3","type":"book-chapter","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T19:26:23Z","timestamp":1732562783000},"page":"33-51","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["User-Guided Verification of\u00a0Security Protocols via\u00a0Sound Animation"],"prefix":"10.1007","author":[{"given":"Kangfeng","family":"Ye","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roberto","family":"Metere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Poonam","family":"Yadav","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,11,26]]},"reference":[{"key":"3_CR1","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. CCS \u201918, New York, NY, USA, Association for Computing Machinery, pp. 1383\u20131396 (2018)","DOI":"10.1145\/3243734.3243846"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Peltonen, A., Sasse, R., Basin, D.: A comprehensive formal analysis of 5G handover. In: Proceedings of the 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks. WiSec \u201921, New York, NY, USA, Association for Computing Machinery, pp. 1\u201312 (2021)","DOI":"10.1145\/3448300.3467823"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Mancini, L., Ritter, E., Ryan, M., Golde, N., Redon, K., Borgaonkar, R.: New privacy issues in mobile telephony: fix and verification. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security. CCS \u201912, New York, NY, USA, Association for Computing Machinery, pp. 205\u2013216 (2012)","DOI":"10.1145\/2382196.2382221"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Akon, M., Yang, T., Dong, Y., Hussain, S.R.: Formal analysis of access control mechanism of 5G core network. In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. CCS \u201923, New York, NY, USA, Association for Computing Machinery, pp. 666\u2013680 (2023)","DOI":"10.1145\/3576915.3623113"},{"key":"3_CR5","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 (May 2017)","DOI":"10.1109\/SP.2017.26"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Basin, D., Cremers, C., Dreier, J., Sasse, R.: Tamarin: verification of large-scale, real world. cryptographic protocols. IEEE Secur. Priv. Mag. 20(3), 24\u201332 (2022)","DOI":"10.1109\/MSEC.2022.3154689"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 - a modern refinement checker for CSP. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 187\u2013201 (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"issue":"1\u20132","key":"3_CR9","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. Theoret. Comput. Sci. 367(1\u20132), 162\u2013202 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Armando, A., et al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, pp. 281\u2013285. Springer, Berlin Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_27","DOI":"10.1007\/11513988_27"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends$$\\text{\\textregistered} $$ Priv. Secur. 1(1-2), 1\u2013135 (2016)","DOI":"10.1561\/3300000004"},{"issue":"4","key":"3_CR12","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/3157831.3157835","volume":"4","author":"D Basin","year":"2017","unstructured":"Basin, D., Cremers, C., Dreier, J., Sasse, R.: Symbolically analyzing security protocols using tamarin. ACM SIGLOG News 4(4), 19\u201330 (2017)","journal-title":"ACM SIGLOG News"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"owe, G.: Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR. In: Margaria, T., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol. 1055. Springer, Berlin, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_43","DOI":"10.1007\/3-540-61042-1_43"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Miller, R., Boureanu, I., Wesemeyer, S., Newton, C.J.P.: The 5G key-establishment stack: in-depth formal verification and experimentation. In: Proceedings of the 2022 ACM on Asia Conference on Computer and Communications Security. ASIA CCS \u201922, New York, NY, USA, Association for Computing Machinery, pp. 237\u2013251 (2022)","DOI":"10.1145\/3488932.3517421"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Kazmierczak, E., Winikoff, M., Dart, P.W.: Verifying model oriented specifications through animation. In: 5th Asia-Pacific Software Engineering Conference (APSEC \u201998), 2-4 December 1998, Taipei, Taiwan, ROC, IEEE Computer Society, pp. 254\u2013261 (1998)","DOI":"10.1109\/APSEC.1998.733727"},{"key":"3_CR16","unstructured":"Boichut, Y., Genet, T., Glouche, Y., Heen, O.: Using animation to improve formal specifications of security protocols. In: 2nd Conference on Security in Network Architectures and Information Systems (SARSSI 2007), pp. 169\u2013182 (2007)"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Dutle, A.M., Mu\u00f1oz, C.A., Narkawicz, A.J., Butler, R.W.: Software Validation via Model Animation. In: Blanchette, J., Kosmatov, N. (eds.) Tests and Proofs. TAP 2015. Lecture Notes in Computer Science, vol. 9154. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21215-9_6","DOI":"10.1007\/978-3-319-21215-9_6"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Xia, L.y., et al.: Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4(POPL), 1\u201332 (2019)","DOI":"10.1145\/3371119"},{"key":"3_CR19","unstructured":"Xia, L.y.: Executable Denotational Semantics with Interaction Trees. PhD thesis, University of Pennsylvania (2022)"},{"key":"3_CR20","unstructured":"Foster, S., Hur, C.K., Woodcock, J.: Formally verified simulations of state-rich processes using interaction trees in Isabelle\/HOL. In Haddad, S., Varacca, D., eds.: 32nd International Conference on Concurrency Theory (CONCUR 2021). Volume 203 of Leibniz International Proceedings in Informatics (LIPIcs)., Dagstuhl, Germany, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 20:1\u201320:18 (2021)"},{"key":"3_CR21","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Int. (1985)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer (2011)","DOI":"10.1007\/978-1-84882-258-0"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"100940","DOI":"10.1016\/j.jlamp.2023.100940","volume":"137","author":"K Ye","year":"2024","unstructured":"Ye, K., Foster, S., Woodcock, J.: Formally verified animation for RoboChart using interaction trees. J. Logical Algebraic Methods Program. 137, 100940 (2024)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G., (eds.) Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. Volume 6009 of Lecture Notes in Computer Science., Springer pp. 103\u2013117 (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9","DOI":"10.1007\/978-3-642-12251-4_9"},{"issue":"1","key":"3_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoret. Comput. Sci. 192(1), 3\u201329 (1998)","journal-title":"Theoret. Comput. Sci."},{"issue":"12","key":"3_CR26","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"RM Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"issue":"6","key":"3_CR27","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.: New directions in cryptography. IEEE Trans. Inf. Theory 22(6), 644\u2013654 (1976)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"3_CR28","unstructured":"Paulson, L.C.: Mechanized proofs of security protocols: needham-schroeder with public keys. Technical report, University of Cambridge (1997)"},{"key":"3_CR29","unstructured":"Schneider, S.: Using CSP for protocol analysis: The Needham-Schroeder Public-Key Protocol. Technical report (February 1997)"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Cremers, C., Mauw, S.: Operational semantics of security protocols, pp. 66\u201389. Springer, Berlin Heidelberg (2005). https:\/\/doi.org\/10.1007\/11495628_4","DOI":"10.1007\/11495628_4"},{"key":"3_CR31","unstructured":"Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial (2023)"},{"key":"3_CR32","unstructured":"Meier, S.: Advancing automated security protocol verification. PhD thesis (2013)"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Merkle, R.C.: Secure communications over insecure channels. Commun. ACM 21(4), pp. 294\u2013299 (1978)","DOI":"10.1145\/359460.359473"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Using ProVerif to analyze protocols with diffie-hellman exponentiation. In: 2009 22nd IEEE Computer Security Foundations Symposium pp. 157\u2013171 (2009)","DOI":"10.1109\/CSF.2009.17"},{"issue":"2","key":"3_CR35","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"3_CR36","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/BF00124891","volume":"2","author":"W Diffie","year":"1992","unstructured":"Diffie, W., Van Oorschot, P.C., Wiener, M.J.: Authentication and authenticated key exchanges. Des. Codes Crypt. 2(2), 107\u2013125 (1992)","journal-title":"Des. Codes Crypt."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77382-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T20:02:18Z","timestamp":1732564938000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77382-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,26]]},"ISBN":["9783031773815","9783031773822"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77382-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,26]]},"assertion":[{"value":"26 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}