{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:01:44Z","timestamp":1765666904944},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_22","type":"book-chapter","created":{"date-parts":[[2010,9,27]],"date-time":"2010-09-27T20:20:02Z","timestamp":1285618802000},"page":"294-307","source":"Crossref","is-referenced-by-count":91,"title":["The Finite Variant Property: How to Get Rid of Some Algebraic Properties"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Comon-Lundh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phanie","family":"Delaune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"22_CR1","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0304-3975(93)90108-6","volume":"118","author":"H. Comon","year":"1993","unstructured":"Comon, H.: Complete axiomatizations of some quotient term algebras. Theoretical Computer Science\u00a0118(2), 167\u2013191 (1993)","journal-title":"Theoretical Computer Science"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24727-2_1","volume-title":"Foundations of Software Science and Computation Structures","author":"H. Comon-Lundh","year":"2004","unstructured":"Comon-Lundh, H.: Intruder theories (ongoing work). In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 1\u20134. Springer, Heidelberg (2004), Invited talk, slides available at \n                  \n                    http:\/\/www.lsv.ens-cachan.fr\/~comon\/biblio.html"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-44881-0_12","volume-title":"Rewriting Techniques and Applications","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: New decidability results for fragments of firstorder logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 148\u2013164. Springer, Heidelberg (2003)"},{"key":"22_CR4","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. Research Report LSV-04-17, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France, 21 pages (2004)"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1109\/LICS.2003.1210067","volume-title":"Proc. of 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003)","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proc. of 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), Ottawa, Canada, pp. 271\u2013280. IEEE Comp. Soc. Press, Los Alamitos (2003)"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1145\/1030083.1030121","volume-title":"Proc. 11th ACM Conference on Computer and Communications Security (CCS 2004)","author":"S. Delaune","year":"2004","unstructured":"Delaune, S., Jacquemard, F.: A decision procedure for the verification of security protocols with explicit destructors. In: Proc. 11th ACM Conference on Computer and Communications Security (CCS 2004), Washington, USA, pp. 278\u2013287. ACM, New York (2004)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, ch. 6, Elsevier and MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol.\u00a087, pp. 318\u2013324. Springer, Heidelberg (1980)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Hullot, J.-M.: A catalogue of canonical term rewriting systems. Technical Report CSL-114, Computer Science Laboratory, SRI, CA, USA (1980)","DOI":"10.21236\/ADA087641"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-44881-0_13","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"2003","unstructured":"Kapur, D., Narendran, P., Wang, L.: An E-unification algorithm for analyzing protocols that use modular exponentiation. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 165\u2013179. Springer, Heidelberg (2003)"},{"key":"22_CR11","unstructured":"Kirchner, C.: M\u00e9thodes et Outils de Conception Syst\u00e9matique d\u2019Algorithmes d\u2019Unification dans les Th\u00e9ories \u00c9quationnelles. PhD thesis, Universit\u00e9 de Nancy I (1985)"},{"key":"22_CR12","unstructured":"Meadows, C., Narendran, P.: A unification algorithm for the group Diffie-Hellman protocol. In: Proc. of the Workshop on Issues in the Theory of Security (WITS 2002), Portland, USA (2002)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","first-page":"261","volume-title":"Automated Deduction - Cade-13","author":"P. Narendran","year":"1996","unstructured":"Narendran, P., Guo, Q., Wolfram, D.: Unification and matching modulo nilpotence. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 261\u2013274. Springer, Heidelberg (1996)"},{"issue":"2","key":"22_CR14","doi-asserted-by":"publisher","first-page":"636","DOI":"10.2307\/2275552","volume":"62","author":"P. Narendran","year":"1997","unstructured":"Narendran, P., Pfenning, F., Statman, R.: On the unification problem for cartesian closed categories. Journal of Symbolic Logic\u00a062(2), 636\u2013647 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"22_CR15","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/CSFW.1997.596790","volume-title":"Proc. 10th Computer Security Foundations Workshop (CSFW 1997)","author":"L. Paulson","year":"1997","unstructured":"Paulson, L.: Mechanized proofs for a recursive authentication protocol. In: Proc. 10th Computer Security Foundations Workshop (CSFW 1997), Rockport, USA, pp. 84\u201395. IEEE Comp. Soc. Press, Los Alamitos (1997)"},{"key":"22_CR16","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/800119.803894","volume-title":"Proc. of the 6th Annual ACM Symposium on Theory of Computing","author":"C. Rackoff","year":"1974","unstructured":"Rackoff, C.: On the complexity of the theories of weak direct products (preliminary report). In: Proc. of the 6th Annual ACM Symposium on Theory of Computing, pp. 149\u2013160. ACM Press, New York (1974)"},{"issue":"1","key":"22_CR17","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/S0020-0190(97)00180-4","volume":"65","author":"P.Y.A. Ryan","year":"1998","unstructured":"Ryan, P.Y.A., Schneider, S.A.: An attack on a recursive authentication protocol: A cautionary tale. Information Processing Letters\u00a065(1), 7\u201310 (1998)","journal-title":"Information Processing Letters"},{"issue":"5","key":"22_CR18","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/0747-7171(92)90016-W","volume":"14","author":"R. Treinen","year":"1992","unstructured":"Treinen, R.: A new method for undecidability proofs of first order theories. Journal of Symbolic Computation\u00a014(5), 437\u2013457 (1992)","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-45446-2_27","volume-title":"Theoretical Computer Science","author":"E. Viola","year":"2001","unstructured":"Viola, E.: E-unifiability via narrowing. In: Restivo, A., Ronchi Della Rocca, S., Roversi, L. (eds.) ICTCS 2001. LNCS, vol.\u00a02202, pp. 426\u2013438. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:49:16Z","timestamp":1558291756000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}