{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T05:08:45Z","timestamp":1736140125381,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540305538"},{"type":"electronic","value":"9783540316503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_38","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T09:44:25Z","timestamp":1132652665000},"page":"549-564","source":"Crossref","is-referenced-by-count":12,"title":["Algebraic Intruder Deductions"],"prefix":"10.1007","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[]},{"given":"Sebastian","family":"M\u00f6dersheim","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"38_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-27836-8_7","volume-title":"Automata, Languages and Programming","author":"M. Abadi","year":"2004","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 46\u201358. Springer, Heidelberg (2004)"},{"key":"38_CR2","first-page":"62","volume-title":"Proceedings of CSFW 2005","author":"M. Abadi","year":"2005","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under (many more) equational theories. In: Proceedings of CSFW 2005, pp. 62\u201376. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"38_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/3-540-36135-9_14","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"A. Armando","year":"2002","unstructured":"Armando, A., Compagna, L.: Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 210\u2013225. Springer, Heidelberg (2002)"},{"key":"38_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"38_CR5","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. Journal of Symbolic Computation\u00a021, 211\u2013243 (1996)","journal-title":"Journal of Symbolic Computation"},{"key":"38_CR6","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","volume-title":"Handbook of Automated Reasoning","author":"F. Baader","year":"2001","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning, vol.\u00a0I, pp. 445\u2013532. Elsevier Science, Amsterdam (2001)"},{"key":"38_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N.: Completion for rewriting modulo a congruence. Theoretical Computer Science\u00a067, 173\u2013201 (1989)","journal-title":"Theoretical Computer Science"},{"key":"38_CR8","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1145\/948109.948154","volume-title":"Proceedings of CCS 2003","author":"D. Basin","year":"2003","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols. In: Proceedings of CCS 2003, pp. 335\u2013344. ACM Press, New York (2003)"},{"key":"38_CR9","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: Algebraic Intruder Deductions (Extended Version). Technical Report 485, Dep.\u00a0of Computer Science, ETH Zurich (2005), Available at, http:\/\/www.infsec.ethz.ch"},{"issue":"3","key":"38_CR10","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D. Basin","year":"2005","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model checker for security protocols. International Journal of Information Security\u00a04(3), 181\u2013208 (2005)","journal-title":"International Journal of Information Security"},{"key":"38_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-45694-5_32","volume-title":"CONCUR 2002 - Concurrency Theory","author":"M. Boreale","year":"2002","unstructured":"Boreale, M., Buscemi, M.G.: A framework for the analysis of security protocols. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 483\u2013498. Springer, Heidelberg (2002)"},{"key":"38_CR12","first-page":"261","volume-title":"Proceedings of LICS 2003","author":"Y. Chevalier","year":"2003","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: An NP Decision Procedure for Protocol Insecurity with XOR. In: Proceedings of LICS 2003, pp. 261\u2013270. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"38_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-24597-1_11","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"Y. Chevalier","year":"2003","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 124\u2013135. Springer, Heidelberg (2003)"},{"key":"38_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1007\/11523468_52","volume-title":"Automata, Languages and Programming","author":"Y. Chevalier","year":"2005","unstructured":"Chevalier, Y., Rusinowitch, M.: Combining Intruder Theories. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 639\u2013651. Springer, Heidelberg (2005)"},{"key":"38_CR15","doi-asserted-by":"crossref","first-page":"5","DOI":"10.26636\/jtit.2002.4.149","volume":"4","author":"H. Comon","year":"2002","unstructured":"Comon, H., Shmatikov, V.: Is It Possible to Decide Whether a Cryptographic Protocol Is Secure Or Not? Journal of Telecommunications and Information Technology\u00a04, 5\u201315 (2002)","journal-title":"Journal of Telecommunications and Information Technology"},{"key":"38_CR16","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.\u00a03467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"38_CR17","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security (to appear)","DOI":"10.3233\/JCS-2006-14101"},{"key":"38_CR18","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1145\/1030083.1030121","volume-title":"Proceedings of 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: Proceedings of CCS 2004, pp. 278\u2013287. ACM Press, New York (2004)"},{"key":"38_CR19","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory\u00a02(29) (1983)","DOI":"10.1109\/TIT.1983.1056650"},{"key":"38_CR20","unstructured":"Durgin, N., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: Undecidability of Bounded Security Protocols. In: Proceedings of the FLOC 1999 Workshop on Formal Methods and Security Protocols, FMSP 1999 (1999)"},{"key":"38_CR21","unstructured":"IETF: The Internet Engineering Task Force, http:\/\/www.ietf.org"},{"issue":"4","key":"38_CR22","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal of Computing\u00a015(4), 1155\u20131194 (1986)","journal-title":"SIAM Journal of Computing"},{"key":"38_CR23","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":"38_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-32033-3_23","volume-title":"Term Rewriting and Applications","author":"P. Lafourcade","year":"2005","unstructured":"Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for AC-like equational theories with homomorphisms. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 308\u2013322. Springer, Heidelberg (2005)"},{"issue":"1","key":"38_CR25","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G. Lowe","year":"1998","unstructured":"Lowe, G.: Casper: a Compiler for the Analysis of Security Protocols. Journal of Computer Security\u00a06(1), 53\u201384 (1998)","journal-title":"Journal of Computer Security"},{"key":"38_CR26","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Journal of Higher-Order and Symbolic Computation (to appear)"},{"key":"38_CR27","first-page":"47","volume-title":"Proceedings of CSFW 2003","author":"J.K. Millen","year":"2003","unstructured":"Millen, J.K., Shmatikov, V.: Symbolic protocol analysis with products and Diffie-Hellman exponentiation. In: Proceedings of CSFW 2003, pp. 47\u201361. IEEE Computer Society Press, Los Alamitos (2003)"},{"issue":"2","key":"38_CR28","first-page":"402","volume":"54","author":"J. Siekmann","year":"1989","unstructured":"Siekmann, J., Szab\u00f3, P.: The undecidability of the D A unification problem. Journal of Symbolic Computation\u00a054(2), 402\u2013414 (1989)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T20:12:01Z","timestamp":1736107921000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/11591191_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}