{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T22:29:40Z","timestamp":1780352980516,"version":"3.54.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319255262","type":"print"},{"value":"9783319255279","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25527-9_16","type":"book-chapter","created":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T11:08:43Z","timestamp":1444216123000},"page":"238-261","source":"Crossref","is-referenced-by-count":8,"title":["Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories"],"prefix":"10.1007","author":[{"given":"Santiago","family":"Escobar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sonia","family":"Santiago","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,20]]},"reference":[{"issue":"2","key":"16_CR1","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0304-3975(94)00277-0","volume":"142","author":"F Baader","year":"1995","unstructured":"Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theor. Comput. Sci. 142(2), 229\u2013255 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Using horn clauses for analyzing security protocols. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series, vol. 5, pp. 86\u2013111. IOS Press, March 2011","DOI":"10.3233\/978-1-60750-714-7-86"},{"issue":"1","key":"16_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","volume":"75","author":"B Blanchet","year":"2008","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program. 75(1), 3\u201351 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"16_CR4","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. J. Symb. Comput. 7, 371\u2013425 (1989)","journal-title":"J. Symb. Comput."},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-54233-7_156","volume-title":"Automata, Languages and Programming","author":"H Comon","year":"1991","unstructured":"Comon, H.: Complete axiomatizations of some quotient term algebras. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) Automata, Languages and Programming. LNCS, vol. 510, pp. 469\u2013480. Springer, Heidelberg (1991)"},{"key":"16_CR6","unstructured":"Comon, H.: Disunification: a survey. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 322\u2013359 (1991)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"issue":"1","key":"16_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/JCS-2006-14101","volume":"14","author":"V Cortier","year":"2006","unstructured":"Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1\u201343 (2006)","journal-title":"J. Comput. Secur."},{"issue":"2","key":"16_CR9","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"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-33167-1_5","volume-title":"Computer Security \u2013 ESORICS 2012","author":"S Erbatur","year":"2012","unstructured":"Erbatur, S., et al.: Effective symbolic protocol analysis via equational irreducibility conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 73\u201390. Springer, Heidelberg (2012)"},{"key":"16_CR11","unstructured":"Escobar, S., Hendrix, J., Meadows, C., Meseguer, J.: Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proceedings of the 2nd International Workshop on Security and Rewriting Techniques (SecReT 2007) (2007)"},{"issue":"1\u20132","key":"16_CR12","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. Theor. Comput. Sci. 367(1\u20132), 162\u2013202 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Equational cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proceedings of the 1st International Workshop on Security and Rewriting Techniques (SecReT 2006). ENTCS, vol. 171, no. 4, pp. 23\u201336. Elsevier (2007)","DOI":"10.1016\/j.entcs.2007.02.053"},{"key":"16_CR14","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\/2008\/2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009)"},{"issue":"7\u20138","key":"16_CR15","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7\u20138), 898\u2013928 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"16_CR16","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."},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"1","key":"16_CR18","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":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Meseguer","year":"1997","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Presicce, F.P. (ed.) Recent Trends in Algebraic Development Techniques. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1997)"},{"issue":"4","key":"16_CR20","doi-asserted-by":"publisher","first-page":"575","DOI":"10.3233\/JCS-2009-0351","volume":"18","author":"S M\u00f6dersheim","year":"2010","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L., Basin, D.A.: Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols. J. Comput. Secur. 18(4), 575\u2013618 (2010)","journal-title":"J. Comput. Secur."},{"issue":"12","key":"16_CR21","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"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-319-11851-2_11","volume-title":"Security and Trust Management","author":"S Santiago","year":"2014","unstructured":"Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: A formal definition of protocol indistinguishability and its verification using Maude-NPA. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 162\u2013177. Springer, Heidelberg (2014)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-22444-7_11","volume-title":"Security and Trust Management","author":"R Sasse","year":"2011","unstructured":"Sasse, R., Escobar, S., Meadows, C., Meseguer, J.: Protocol analysis modulo combination of theories: a case study in Maude-NPA. In: Cuellar, J., Lopez, J., Barthe, G., Pretschner, A. (eds.) STM 2010. LNCS, vol. 6710, pp. 163\u2013178. Springer, Heidelberg (2011)"},{"key":"16_CR24","unstructured":"TeReSe: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"issue":"1\u20132","key":"16_CR25","first-page":"123","volume":"20","author":"P Thati","year":"2007","unstructured":"Thati, P., Meseguer, J.: Symbolic reachability analysis using narrowing and its application verification of cryptographic protocols. J. Higher-Order Symb. Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"J. Higher-Order Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Programming Languages with Applications to Biology and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25527-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T22:58:57Z","timestamp":1748645937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25527-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319255262","9783319255279"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25527-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}