{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T01:06:59Z","timestamp":1775610419213,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T00:00:00Z","timestamp":1652832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100008885","name":"Lloyd's Register Foundation","doi-asserted-by":"publisher","award":["G0095"],"award-info":[{"award-number":["G0095"]}],"id":[{"id":"10.13039\/100008885","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006041","name":"Innovate UK","doi-asserted-by":"publisher","award":["104227"],"award-info":[{"award-number":["104227"]}],"id":[{"id":"10.13039\/501100006041","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/S016627\/1, EP\/T027037\/1"],"award-info":[{"award-number":["EP\/S016627\/1, EP\/T027037\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,18]]},"DOI":"10.1145\/3524482.3527654","type":"proceedings-article","created":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T22:06:57Z","timestamp":1658441217000},"page":"91-101","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Automating cryptographic protocol language generation from structured specifications"],"prefix":"10.1145","author":[{"given":"Roberto","family":"Metere","sequence":"first","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, UK"}]},{"given":"Luca","family":"Arnaboldi","sequence":"additional","affiliation":[{"name":"The University of Edinburgh, Edinburgh, UK"}]}],"member":"320","published-online":{"date-parts":[[2022,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127586"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_19"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363262"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"e_1_3_2_1_7_1","volume-title":"Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends\u00ae in Privacy and Security 1, 1--2","author":"Blanchet Bruno","year":"2016","unstructured":"Bruno Blanchet . 2016. Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends\u00ae in Privacy and Security 1, 1--2 ( 2016 ), 1--135. Bruno Blanchet. 2016. Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends\u00ae in Privacy and Security 1, 1--2 (2016), 1--135."},{"key":"e_1_3_2_1_8_1","unstructured":"Bruno Blanchet et al. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules.. In csfw Vol. 1. 82--96.  Bruno Blanchet et al. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules.. In csfw Vol. 1. 82--96."},{"key":"e_1_3_2_1_9_1","unstructured":"James Clark Steve DeRose etal 1999. XML path language (XPath) version 1.0.  James Clark Steve DeRose et al. 1999. XML path language (XPath) version 1.0."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-015-0306-9"},{"key":"e_1_3_2_1_11_1","unstructured":"Wei Dai. [n.d.]. Crypto++\u00ae library. https:\/\/cryptopp.com\/  Wei Dai. [n.d.]. Crypto++\u00ae library. https:\/\/cryptopp.com\/"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings DARPA Information Survivability Conference and Exposition. DISCEX'00","volume":"1","author":"Denker Grit","year":"2000","unstructured":"Grit Denker and Jonathan Millen . 2000 . CAPSL integrated protocol environment . In Proceedings DARPA Information Survivability Conference and Exposition. DISCEX'00 , Vol. 1 . IEEE, 207--221. Grit Denker and Jonathan Millen. 2000. CAPSL integrated protocol environment. In Proceedings DARPA Information Survivability Conference and Exposition. DISCEX'00, Vol. 1. IEEE, 207--221."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2018.2832984"},{"key":"e_1_3_2_1_14_1","volume-title":"Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach","author":"Bhargavan Nadim","unstructured":"Kobeissi, Nadim and Bhargavan , Karthikeyan and Blanchet , Bruno. 2017. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach . In IEEE EuroS &P. Kobeissi, Nadim and Bhargavan, Karthikeyan and Blanchet, Bruno. 2017. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In IEEE EuroS&P."},{"key":"e_1_3_2_1_15_1","volume-title":"Security Analysis of Automotive Protocols. In Computer Science in Cars Symposium. 1--12","author":"Lauser Timm","year":"2020","unstructured":"Timm Lauser , Daniel Zelle , and Christoph Krau\u00df . 2020 . Security Analysis of Automotive Protocols. In Computer Science in Cars Symposium. 1--12 . Timm Lauser, Daniel Zelle, and Christoph Krau\u00df. 2020. Security Analysis of Automotive Protocols. In Computer Science in Cars Symposium. 1--12."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_2_1_17_1","volume-title":"Securing the Electric Vehicle Charging Infrastructure. arXiv preprint arXiv:2105.02905","author":"Metere Roberto","year":"2021","unstructured":"Roberto Metere , Myriam Neaimeh , Charles Morisset , Carsten Maple , Xavier Bellekens , and Ricardo M Czekster . 2021. Securing the Electric Vehicle Charging Infrastructure. arXiv preprint arXiv:2105.02905 ( 2021 ). Roberto Metere, Myriam Neaimeh, Charles Morisset, Carsten Maple, Xavier Bellekens, and Ricardo M Czekster. 2021. Securing the Electric Vehicle Charging Infrastructure. arXiv preprint arXiv:2105.02905 (2021)."},{"key":"e_1_3_2_1_18_1","unstructured":"ThinkAsynch. [n.d.]. Asio C++ Library. https:\/\/think-async.com\/Asio\/  ThinkAsynch. [n.d.]. Asio C++ Library. https:\/\/think-async.com\/Asio\/"},{"key":"e_1_3_2_1_19_1","volume-title":"W3C XML schema definition language (XSD) 1.1 part 1: Structures","author":"Thompson Henry S","year":"2009","unstructured":"Henry S Thompson , Noah Mendelsohn , D Beech , and M Maloney . 2009. W3C XML schema definition language (XSD) 1.1 part 1: Structures . The World Wide Web Consortium (W 3C), W3C Working Draft Dec 3 ( 2009 ). Henry S Thompson, Noah Mendelsohn, D Beech, and M Maloney. 2009. W3C XML schema definition language (XSD) 1.1 part 1: Structures. The World Wide Web Consortium (W3C), W3C Working Draft Dec 3 (2009)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3073087"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.052"}],"event":{"name":"FormaliSE '22: International Conference on Formal Methods in Software Engineering","location":"Pittsburgh Pennsylvania","acronym":"FormaliSE '22","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the IEEE\/ACM 10th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527654","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524482.3527654","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:51Z","timestamp":1750183791000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527654"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,18]]},"references-count":21,"alternative-id":["10.1145\/3524482.3527654","10.1145\/3524482"],"URL":"https:\/\/doi.org\/10.1145\/3524482.3527654","relation":{},"subject":[],"published":{"date-parts":[[2022,5,18]]},"assertion":[{"value":"2022-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}