{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:27:54Z","timestamp":1742956074889,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031314759"},{"type":"electronic","value":"9783031314766"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-31476-6_17","type":"book-chapter","created":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T07:02:46Z","timestamp":1684220566000},"page":"307-350","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Strand Spaces with\u00a0Choice via\u00a0a\u00a0Process Algebra Semantics"],"prefix":"10.1007","author":[{"given":"Fan","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jose","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sonia","family":"Santiago","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,17]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M.: Leslie Lamport\u2019s properties and actions. In: Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed Computing, PODC 2001, p. 15 (2001)","DOI":"10.1145\/383962.383973"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 104\u2013115 (2001)","DOI":"10.1145\/360204.360213"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Durgin, N.A., Mitchell, J.C., Lincoln, P., Scedrov, A.: Relating strands and multiset rewriting for security protocol analysis. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW 2000, pp. 35\u201351 (2000)","DOI":"10.1109\/CSFW.2000.856924"},{"key":"17_CR4","unstructured":"Comon, H.: Disunification: a survey. In: Lassez, J.-L., Plotkin, G.D. (eds.) Computational Logic - Essays in Honor of Alan Robinson, pp. 322\u2013359. The MIT Press (1991)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-36206-1_10","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"F Crazzolara","year":"2002","unstructured":"Crazzolara, F., Winskel, G.: Composing strand spaces. In: Agrawal, M., Seth, A. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 97\u2013108. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36206-1_10"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Cremers, C., Horvat, M., Scott, S., van der Merwe, T.: Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication. In: IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, 22\u201326 May 2016, pp. 470\u2013485. IEEE Computer Society (2016)","DOI":"10.1109\/SP.2016.35"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"17_CR8","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA manual version 3.1 (2017). http:\/\/maude.cs.illinois.edu\/w\/index.php?title=Maude_Tools:_Maude-NPA"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: A rewriting-based forwards semantics for Maude-NPA. In: Proceedings of the 2014 Symposium and Bootcamp on the Science of Security, HotSoS 2014. ACM (2014)","DOI":"10.1145\/2600176.2600186"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.ic.2014.07.007","volume":"238","author":"S Escobar","year":"2014","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL protocol analyzer. Inf. Comput. 238, 157\u2013186 (2014)","journal-title":"Inf. Comput."},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-319-25527-9_16","volume-title":"Programming Languages with Applications to Biology and Security","author":"S Escobar","year":"2015","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Symbolic protocol analysis with disequality constraints modulo equational theories. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 238\u2013261. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25527-9_16"},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"FJ Thayer Fabrega","year":"1999","unstructured":"Thayer Fabrega, F.J., Herzog, J., Guttman, J.: Strand spaces: what makes a security protocol correct? J. Comput. Secur. 7, 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"issue":"1","key":"17_CR13","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.entcs.2009.06.017","volume":"242","author":"SB Fr\u00f6schle","year":"2009","unstructured":"Fr\u00f6schle, S.B.: Adding branching to the strand space model. Electr. Notes Theor. Comput. Sci. 242(1), 139\u2013159 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-76637-7_12","volume-title":"Programming Languages and Systems","author":"J Goubault-Larrecq","year":"2007","unstructured":"Goubault-Larrecq, J., Palamidessi, C., Troina, A.: A probabilistic applied pi\u2013calculus. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 175\u2013190. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76637-7_12"},{"key":"17_CR15","unstructured":"Lluch-Palop, J.: Verificaci\u00f3n autom\u00e1tica del protocolo TLS 1.3 usando Maude-NPA. Master\u2019s thesis, Universitat Polit\u00e8cnica de Val\u00e8ncia (2019). http:\/\/hdl.handle.net\/10251\/130041"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"issue":"1","key":"17_CR17","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR18","volume-title":"Communicating and Mobile Systems - The Pi-Calculus","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems - The Pi-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Olarte, C., Valencia, F.D.: The expressivity of universal timed CCP: undecidability of monadic FLTL and closure operators for security. In: 2008 Proceedings Principles and Practice of Declarative Programming, pp. 8\u201319 (2008)","DOI":"10.1145\/1389449.1389452"},{"key":"17_CR20","unstructured":"Rescorla, E.: The transport layer security (TLS) protocol version 1.3. Technical report draft-ietf-tls-tls13-12, IETF (2016)"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Yang, F., Escobar, S., Meadows, C.A., Meseguer, J., Santiago, S.: Strand spaces with choice via a process algebra semantics. In: Cheney, J., Vidal, G. (eds.) Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, UK, 5\u20137 September 2016, pp. 76\u201389. ACM (2016)","DOI":"10.1145\/2967973.2968609"}],"container-title":["Lecture Notes in Computer Science","Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-31476-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,20]],"date-time":"2024-10-20T12:39:28Z","timestamp":1729427968000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-31476-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031314759","9783031314766"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-31476-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 May 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}