{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:40:30Z","timestamp":1774946430528,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540662228","type":"print"},{"value":"9783540486602","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_29","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"314-328","source":"Crossref","is-referenced-by-count":63,"title":["Towards an Automatic Analysis of Security Protocols in First-Order Logic"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"issue":"3","key":"29_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L. & Ganzinger, H. (1994),\u2019 Rewrite-based equational theorem proving with selection and simplification\u2019, Journal of Logic and Computation 4(3), 217\u2013247.","journal-title":"Journal of Logic and Computation"},{"key":"29_CR2","series-title":"Lect Notes Comput Sci","first-page":"161","volume-title":"Proceedings of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92","author":"B. Bogaert","year":"1992","unstructured":"Bogaert, B. & Tison, S. (1992), Equality and disequality constraints on direct subterms in tree automata, in A. Finkel & M. Jantzen, eds,\u2019 Proceedings of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92\u2019, Vol. 577 of LNCS, Springer, pp. 161\u2013171."},{"issue":"1","key":"29_CR3","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M. & Needham, R. (1990),\u2019 A logic of authentication\u2019, ACM Transactions on Computer Systems 8(1), 18\u201336.","journal-title":"ACM Transactions on Computer Systems"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Charatonik, W., McAllester, D., Niwinski, D., Podelski, A. & Walukiewicz, I. (1998), The horn mu-calculus, in `Proceedings 13th IEEE Symposium on Logic in Computer Science, LICS\u201998\u2019, IEEE Computer Society Press, pp. 58\u201369.","DOI":"10.1109\/LICS.1998.705643"},{"key":"29_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"Comon, H. & Delor, C. (1994),\u2019 Equational formulae with membership constraints\u2019, Information and Computation 112, 167\u2013216.","journal-title":"Information and Computation"},{"key":"29_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/BFb0052362","volume-title":"Rewriting Techniques and Applications, 9th International Conference, RTA-98","author":"F. Jacquemard","year":"1998","unstructured":"Jacquemard, F., Meyer, C. & Weidenbach, C. (1998), Unification in extensions of shallow equational theories, in T. Nipkow, ed.,\u2019 Rewriting Techniques and Applications, 9th International Conference, RTA-98\u2019, Vol. 1379 of LNCS, Springer, pp. 76\u201390."},{"key":"29_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/BFb0028734","volume-title":"Computer Aided Verification (CAV-98): 10th International Conference","author":"J. C. Mitchell","year":"1998","unstructured":"Mitchell, J. C. (1998), Finite-state analysis of security protocols, in A. J. Hu & M. Y. Vardi, eds,\u2019 Computer Aided Verification (CAV-98): 10th International Conference\u2019, Vol. 1427 of LNCS, Springer, pp. 71\u201376."},{"issue":"2","key":"29_CR8","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/155848.155852","volume":"27","author":"B. C. Neuman","year":"1993","unstructured":"Neuman, B. C. & Stubblebine, S. G. (1993),\u2019 A note on the use of timestamps as nonces\u2019, ACM SIGOPS, Operating Systems Review 27(2), 10\u201314.","journal-title":"ACM SIGOPS, Operating Systems Review"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Paulson, L. C. (1997), Proving properties of security protocols by induction, in J. Millen, ed.,\u2019 Proceedings of the 10th IEEE Computer Security Foundations Workshop\u2019, IEEE Computer Society, pp. 70\u201383.","DOI":"10.1109\/CSFW.1997.596788"},{"key":"29_CR10","unstructured":"Schneier, B. (1996), Applied Cryptography, 2 edn, Wiley."},{"key":"29_CR11","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-63104-6_12","volume":"1249","author":"J. Schumann","year":"1997","unstructured":"Schumann, J. (1997), Automatic verification of cryptographic protocols with setheo, in\u2019 Proceedings of the 14th International Conference on Automated Deduction, CADE-14\u2019, Vol. 1249 of LNAI, Springer, Townsville, Australia, pp. 87\u2013100.","journal-title":"Proceedings of the 14th International Conference on Automated Deduction, CADE-14"},{"key":"29_CR12","unstructured":"Weidenbach, C. (1998), Sorted unification and tree automata, in W. Bibel & P. H. Schmitt, eds,\u2019 Automated Deduction-A Basis for Applications\u2019, Vol. 1 of Applied Logic, Kluwer, chapter 9, pp. 291\u2013320."},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C. & Topic, D. (1999), System description: Spass version 1.0.0, in H. Ganzinger, ed.,\u2019 16th International Conference on Automated Deduction, CADE-16\u2019, LNAI, Springer. This volume.","DOI":"10.1007\/3-540-48660-7_34"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T08:56:15Z","timestamp":1556960175000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}