{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T21:07:01Z","timestamp":1778965621025,"version":"3.51.4"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032206831","type":"print"},{"value":"9783032206848","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-20684-8_14","type":"book-chapter","created":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T14:07:31Z","timestamp":1773670051000},"page":"237-252","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated Symbolic Verification of\u00a0Quantum Cryptographic Protocols"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8714-4626","authenticated-orcid":false,"given":"Rolando","family":"Trujillo-Rasua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9970-9105","authenticated-orcid":false,"given":"Jesse","family":"Laeuchli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1804-3319","authenticated-orcid":false,"given":"Reynaldo","family":"Gil-Pons","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,3,17]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Abulkasim, H., Mashatan, A., Ghose, S.: Security improvements for privacy-preserving quantum multiparty computation based on circular structure. Quantum Inf. Process. 21(1), 25 (2022). https:\/\/doi.org\/10.1007\/s11128-021-03357-w","DOI":"10.1007\/s11128-021-03357-w"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Bennett, C.H., Brassard, G.: Quantum cryptography: public key distribution and coin tossing. Theor. Comput. Sci. 560, 7\u201311 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.05.025, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397514004241","DOI":"10.1016\/j.tcs.2014.05.025"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Brassard, G., Crepeau, C., Jozsa, R., Langlois, D.: A quantum bit commitment scheme provably unbreakable by both parties. In: Proceedings of 1993 IEEE 34th Annual Foundations of Computer Science. pp. 362\u2013371 (1993). https:\/\/doi.org\/10.1109\/SFCS.1993.366851","DOI":"10.1109\/SFCS.1993.366851"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-33475-7_9","volume-title":"Theoretical Computer Science","author":"Y Deng","year":"2012","unstructured":"Deng, Y., Feng, Y.: Open Bisimulation for Quantum Processes. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 119\u2013133. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33475-7_9"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Feng, Y., Duan, R., Ji, Z., Ying, M.: Probabilistic bisimulations for quantum processes. Inf. Comput. 205(11), 1608\u20131639 (2007). https:\/\/doi.org\/10.1016\/j.ic.2007.08.001, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540107000855","DOI":"10.1016\/j.ic.2007.08.001"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Nagarajan, R.: Techniques for formal modelling and analysis of quantum systems. In: Coecke, B., Ong, L., Panangaden, P. (eds.) Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky: Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday, pp. 264\u2013276. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38164-5_18, https:\/\/doi.org\/10.1007\/978-3-642-38164-5_18","DOI":"10.1007\/978-3-642-38164-5_18"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Hillery, M., Ziman, M., Bu\u017eek, V., Bielikov\u00e1, M.: Towards quantum-based privacy and voting. Phys. Lett. A 349(1), 75\u201381 (2006). https:\/\/doi.org\/10.1016\/j.physleta.2005.09.010, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0375960105014738","DOI":"10.1016\/j.physleta.2005.09.010"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Hirschi, L.: Symbolic abstractions for quantum protocol verification (2019). https:\/\/doi.org\/10.48550\/arXiv.1904.04186, http:\/\/arxiv.org\/abs\/1904.04186, arXiv:1904.04186","DOI":"10.48550\/arXiv.1904.04186"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Khan, M., Aman, M., Sikdar, B.: Soteria: A quantum-based device attestation technique for the internet of things. IEEE Internet Things J. PP (2023). https:\/\/doi.org\/10.1109\/JIOT.2023.3346397","DOI":"10.1109\/JIOT.2023.3346397"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Kubota, T., Kakutani, Y., Kato, G., Kawano, Y., Sakurada, H.: Semi-automated verification of security proofs of quantum cryptographic protocols. J. Symb. Comput. 73, 192\u2013220 (2016). https:\/\/doi.org\/10.1016\/j.jsc.2015.05.001, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0747717115000462","DOI":"10.1016\/j.jsc.2015.05.001"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Laeuchli, J., Rasua, R.T.: Approaches to quantum remote memory attestation (2025). https:\/\/arxiv.org\/abs\/2503.04311","DOI":"10.1049\/qtc2.70019"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Laeuchli, J., Trujillo-Rasua, R.: Software-based remote memory attestation using quantum entanglement. Quantum Inf. Process. 23(6), 208 (2024). https:\/\/doi.org\/10.1007\/s11128-024-04421-x","DOI":"10.1007\/s11128-024-04421-x"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Lalire, M.: Relations among quantum processes: bisimilarity and congruence. Math. Struct. Comp. Sci. 16(3), 407\u2013428 (2006). https:\/\/doi.org\/10.1017\/S096012950600524X","DOI":"10.1017\/S096012950600524X"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Lo, H.K., Chau, H.F.: Is quantum bit commitment really possible? Phys. Rev. Lett. 78, 3410\u20133413 (1997). https:\/\/doi.org\/10.1103\/PhysRevLett.78.3410, https:\/\/link.aps.org\/doi\/10.1103\/PhysRevLett.78.3410","DOI":"10.1103\/PhysRevLett.78.3410"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.A.: The TAMARIN prover for the symbolic analysis of security protocols. In: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, pp. 696\u2013701 (2013).https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Moulick, S.R., Panigrahi, P.K.: Quantum cheques. Quantum Inf. Process. 15(6), 2475\u20132486 (2016). https:\/\/doi.org\/10.1007\/s11128-016-1273-4","DOI":"10.1007\/s11128-016-1273-4"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Qin, X., Deng, Y., Du, W.: Verifying Quantum Communication Protocols with Ground Bisimulation. In: TCS 2012. LNCS, pp. 21\u201338. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_2","DOI":"10.1007\/978-3-030-45237-7_2"},{"key":"14_CR18","unstructured":"Rasua, R.T.: Tamarin theory for quantum protocols (2026). https:\/\/github.com\/rolandotr\/quantum-protocols-theory"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Vaccaro, J.A., Spring, J., Chefles, A.: Quantum protocols for anonymous voting and surveying. Phys. Rev. A 75, 012333 (2007). https:\/\/doi.org\/10.1103\/PhysRevA.75.012333","DOI":"10.1103\/PhysRevA.75.012333"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Yang, Y., Liu, B., Xu, G., Zhou, Y., Shi, W.: Practical quantum anonymous private information retrieval based on quantum key distribution. IEEE Trans. Inf. Forensics Secur. 18, 4034\u20134045 (2023). https:\/\/doi.org\/10.1109\/TIFS.2023.3288989","DOI":"10.1109\/TIFS.2023.3288989"},{"issue":"4","key":"14_CR21","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/s11128-021-03072-6","volume":"20","author":"C Zhang","year":"2021","unstructured":"Zhang, C., Long, Y., Li, Q.: Quantum summation using d-level entanglement swapping. Quantum Inf. Process. 20(4), 137 (2021)","journal-title":"Quantum Inf. Process."}],"container-title":["Lecture Notes in Computer Science","Juggling Formal Methods and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-20684-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T20:14:48Z","timestamp":1778962488000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-20684-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032206831","9783032206848"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-20684-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"17 March 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}