{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T01:06:50Z","timestamp":1775610410078,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540412854","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-44404-1_10","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T19:20:51Z","timestamp":1194981651000},"page":"131-160","source":"Crossref","is-referenced-by-count":39,"title":["Compiling and Verifying Security Protocols"],"prefix":"10.1007","author":[{"given":"Florent","family":"Jacquemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micha\u00ebl","family":"Rusinowitch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Vigneron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-58843-4","volume-title":"Programming Satan\u2019s computer","author":"R. Anderson","year":"1995","unstructured":"R. Anderson. Programming Satan\u2019s computer. volume 1000 of Lecture Notes in Computer Science. Springer-Verlag. 148"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair, N. Dershowitz, and D. Plaisted. Completion without Failure. In H. A\u00eft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques, pages 1\u201330. Academic Press inc., 1989. 152","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"10_CR3","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Associative-Commutative Superposition","author":"L. Bachmair","year":"1995","unstructured":"L. Bachmair and H. Ganzinger. Associative-Commutative Superposition. In N. Dershowitz and N. Lindenstrauss, editors, Proc. 4th CTRS Workshop, Jerusalem (Israel), volume 968 of LNCS, pages 1\u201314. Springer-Verlag, 1995. 153"},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-46701-7_3","volume-title":"Secure Networking \u2014 CQRE [Secure]\u2019 99","author":"D. Basin","year":"1999","unstructured":"D. Basin. Lazy infinite-state analysis of security protocols. In Secure Networking \u2014 CQRE [Secure]\u2019 99, LNCS 1740, pages 30\u201342. Springer-Verlag, Berlin, 1999. 132"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"D. Bolignano. Towards the formal verification of electronic commerce protocols. In IEEE Computer Security Foundations Workshop, pages 133\u2013146. IEEE Computer Society, 1997. 131, 142","DOI":"10.1109\/CSFW.1997.596802"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving Theorems with the Modification Method. SIAM J. of Computing, 4:412\u2013430, 1975. 152","journal-title":"SIAM J. of Computing"},{"key":"10_CR7","unstructured":"J. Clark and J. Jacob. A survey of authentication protocol literature. http:\/\/www.cs.york.ac.uk\/~jac\/papers\/drareviewps.ps , 1997. 131, 150, 151, 155"},{"key":"10_CR8","unstructured":"G. Denker, J. Meseguer, and C. Talcott. Protocol specification and analysis in Maude. In Formal Methods and Security Protocols, 1998. LICS\u2019 98 Workshop. 131, 133, 152"},{"key":"10_CR9","unstructured":"G. Denker and J. Millen. Capsl intermediate language. In Formal Methods and Security Protocols, 1999. FLOC\u2019 99 Workshop. 131, 132"},{"key":"10_CR10","first-page":"244","volume":"B","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 244\u2013320. North-Holland, 1990. 133, 139","journal-title":"Handbook of Theoretical Computer Science"},{"key":"10_CR11","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29:198\u2013208, 1983. Also STAN-CS-81-854, May 1981, Stanford U. 133, 137","journal-title":"IEEE Transactions on Information Theory"},{"key":"10_CR12","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00263448","volume":"8","author":"E. Domenjoud","year":"1992","unstructured":"E. Domenjoud. A technical note on AC-unification. the number of minimal unifiers of the equation \u00e1x1 + \u2026 + \u00e1xp =AC \u03b2y1 + \u2026 + \u03b2yq. JAR, 8:39\u201344, 1992. 153","journal-title":"JAR"},{"key":"10_CR13","unstructured":"R. Focardi and R. Gorrieri. Cvs: A compiler for the analysis of cryptographic protocols. In 12th IEEE Computer Security Foundations Workshop. IEEE Computer Society, 1999. 131"},{"issue":"3","key":"10_CR14","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch. Proving Refutational Completeness of Theorem-Proving Strategies: the Transfinite Semantic Tree Method. JACM, 38(3):559\u2013587, July 1991. 152","journal-title":"JACM"},{"key":"10_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"Canonical forms and unification","author":"J.-M. Hullot","year":"1980","unstructured":"J.-M. Hullot. Canonical forms and unification. In 5th International Conference on Automated Deduction, volume 87, pages 318\u2013334. Springer-Verlag, LNCS, july 1980. 131, 137"},{"key":"10_CR16","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"D. E. Knuth and P. B. Bendix. Simple Word Problems in Universal Algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, 1970. 152"},{"issue":"1","key":"10_CR17","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G. Lowe","year":"1998","unstructured":"G. Lowe. Casper: a compiler for the analysis of security protocols. Journal of Computer Security, 6(1):53\u201384, 1998. 131, 132, 132, 133, 136","journal-title":"Journal of Computer Security"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"G. Lowe. Towards a completeness result for model checking of security protocols. In 11th IEEE Computer Security Foundations Workshop, pages 96\u2013105. IEEE Computer Society, 1998. 134","DOI":"10.1109\/CSFW.1998.683159"},{"issue":"1","key":"10_CR19","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"1","author":"C. Meadows","year":"1992","unstructured":"C. Meadows. Applying formal methods to the analysis of a key management protocol. Journal of Computer Security, 1(1):5\u201336, 1992. 133","journal-title":"Journal of Computer Security"},{"issue":"2","key":"10_CR20","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"C. Meadows. The NRL protocol analyzer: an overview. Journal of Logic Programming, 26(2):113\u2013131, 1996. 133","journal-title":"Journal of Logic Programming"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"J. Millen. CAPSL: Common Authentication Protocol Specification Language. Technical Report MP 97B48, The MITRE Corporation, 1997. 132, 132, 133","DOI":"10.1145\/304851.304879"},{"key":"10_CR22","unstructured":"J. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Mur\u00f6. In IEEE Symposium on Security and Privacy, pages 141\u2013154. IEEE Computer Society, 1997. 131"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 2000. 152","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"1","key":"10_CR24","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. Paulson","year":"1998","unstructured":"L. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1):85\u2013128, 1998. 131","journal-title":"Journal of Computer Security"},{"key":"10_CR25","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"G. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. JACM, 28:233\u2013264, 1981. 153","journal-title":"JACM"},{"key":"10_CR26","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building-in equational theories. Machine Intelligence, 7:73\u201390, 1972. 152","journal-title":"Machine Intelligence"},{"key":"10_CR27","unstructured":"G. A. Robinson and L. T. Wos. Paramodulation and First-Order Theorem Proving. In B. Meltzer and D. Mitchie, editors, Machine Intelligence 4, pages 135\u2013150. Edinburgh University Press, 1969. 152"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. In 8th IEEE Computer Security Foundations Workshop, pages 98\u2013107. IEEE Computer Society, 1995. 132","DOI":"10.1109\/CSFW.1995.518556"},{"issue":"1","key":"10_CR29","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF01270929","volume":"6","author":"M. Rusinowitch","year":"1995","unstructured":"M. Rusinowitch and L. Vigneron. Automated Deduction with Associative-Commutative Operators. Applicable Algebra in Engineering, Communication and Computation, 6(1):23\u201356, January 1995. 152, 153","journal-title":"Applicable Algebra in Engineering, Communication and Computation"},{"key":"10_CR30","unstructured":"B. Schneier. Applied Cryptography. John Wiley, 1996. 133"},{"issue":"4","key":"10_CR31","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J. R. Slagle","year":"1974","unstructured":"J. R. Slagle. Automated Theorem-Proving for theories with Simplifiers, Commutativity and Associativity. JACM, 21(4):622\u2013642, 1974. 152","journal-title":"JACM"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"P. Syverson, C. Meadows, and I. Cervesato. Dolev-Yao is no better than Machiavelli. In WITS\u201900. Workshop on Issues in the Theory of Security, 2000. 146","DOI":"10.21236\/ADA464936"},{"key":"10_CR33","series-title":"Lect Notes Comput Sci","first-page":"468","volume-title":"Positive deduction modulo regular theories","author":"L. Vigneron","year":"1995","unstructured":"L. Vigneron. Positive deduction modulo regular theories. In Proceedings of Computer Science Logic, Paderborn (Germany), pages 468\u2013485. LNCS 1092, Springer-Verlag, 1995. 131, 152, 152"},{"key":"10_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-48660-7_34","volume-title":"Towards an automatic analysis of security protocols","author":"C. Weidenbach","year":"1999","unstructured":"C. Weidenbach. Towards an automatic analysis of security protocols. In Proceedings of the 16th International Conference on Automated Deduction, pages 378\u2013382. LNCS 1632, Springer-Verlag, 1999. 131"},{"key":"10_CR35","unstructured":"U. Wertz. First-Order Theorem Proving Modulo Equations. Technical Report MPI-I-92-216, MPI Informatik, April 1992. 153"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"T. Woo and S. Lam. A semantic model for authentication protocols. In IEEE Symposium on Research in Security and Privacy, pages 178\u2013194. IEEE Computer Society, 1993. 134, 147","DOI":"10.1109\/RISP.1993.287633"}],"container-title":["Lecture Notes in Artificial Intelligence","Logic for Programming and Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44404-1_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T08:06:44Z","timestamp":1737533204000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44404-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540412854"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-44404-1_10","relation":{},"subject":[]}}