{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T22:22:21Z","timestamp":1780352541111,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,7,20]],"date-time":"2011-07-20T00:00:00Z","timestamp":1311120000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2011,7,20]]},"DOI":"10.1145\/2003476.2003488","type":"proceedings-article","created":{"date-parts":[[2011,7,20]],"date-time":"2011-07-20T12:34:54Z","timestamp":1311165294000},"page":"65-76","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Protocol analysis in Maude-NPA using unification modulo homomorphic encryption"],"prefix":"10.1145","author":[{"given":"Santiago","family":"Escobar","sequence":"first","affiliation":[{"name":"Universidad Polit\u00e9cnica de Valencia, Valencia, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[{"name":"University of New Mexico, Albuquerque, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christopher","family":"Lynch","sequence":"additional","affiliation":[{"name":"Clarkson University, Potsdam, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[{"name":"Naval Research Laboratory, Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[{"name":"University at Albany-SUNY, Albany, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ralf","family":"Sasse","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2011,7,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.l016\/j.tcs.2006.08.032"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755688.1755713"},{"key":"e_1_3_2_1_3_1","series-title":"LNCS","first-page":"20","volume-title":"Proc. RTA","author":"Anantharaman S.","year":"2007","unstructured":"S. Anantharaman , P. Narendran , and M. Rusinowitch . Intruders with caps . In Proc. RTA 2007 , volume 4533 of LNCS , pages 20 -- 35 . Springer , 2007. S. Anantharaman, P. Narendran, and M. Rusinowitch. Intruders with caps. In Proc. RTA 2007, volume 4533 of LNCS, pages 20--35. Springer, 2007."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/288090.288097"},{"key":"e_1_3_2_1_6_1","series-title":"LNCS","first-page":"50","volume-title":"CADE","author":"Baader F.","year":"1992","unstructured":"F. Baader and K. U. Schulz . Unification in the union of disjoint equational theories: Combining decision procedures . In CADE , volume 607 of LNCS , pages 50 -- 65 . Springer , 1992 . F. Baader and K. U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In CADE, volume 607 of LNCS, pages 50--65. Springer, 1992."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39650-5_15"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_11"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.05.030"},{"key":"e_1_3_2_1_11_1","volume-title":"APM Report","author":"Bull J.","year":"1997","unstructured":"J. Bull . The authentication protocol . APM Report , 1997 . J. Bull. The authentication protocol. APM Report, 1997."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_10"},{"key":"e_1_3_2_1_13_1","first-page":"181","volume-title":"LPAR, LNCS","author":"Chevalier Y.","year":"2007","unstructured":"Y. Chevalier , D. Lugiez , and M. Rusinowitch . Verifying cryptographic protocols with subterms constraints . In LPAR, LNCS vol. 4790 , pages 181 -- 195 . Springer , 2007 . Y. Chevalier, D. Lugiez, and M. Rusinowitch. Verifying cryptographic protocols with subterms constraints. In LPAR, LNCS vol. 4790, pages 181--195. Springer, 2007."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.10.022"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_27"},{"key":"e_1_3_2_1_16_1","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"Clavel M.","year":"2007","unstructured":"M. Clavel , F. Dur\u00e0n , S. Eker , P. Lincoln , N. Mart\u00ed-Oliet , J. Meseguer , and C. L. Talcott . All About Maude - A High-Performance Logical Framework , volume 4350 of Lecture Notes in Computer Science . Springer , 2007 . M. Clavel, F. Dur\u00e0n, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, and C. L. Talcott. All About Maude - A High-Performance Logical Framework, volume 4350 of Lecture Notes in Computer Science. Springer, 2007."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"e_1_3_2_1_18_1","first-page":"271","volume-title":"LICS","author":"Comon-Lundh H.","unstructured":"H. Comon-Lundh and V. Shmatikov . Intruder deductions, constraint solving and insecurity decision in presence of exclusive or . In LICS , pages 271 --. IEEE Computer Society, 2003. H. Comon-Lundh and V. Shmatikov. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In LICS, pages 271--. IEEE Computer Society, 2003."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1239376.1239377"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.035"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1927806.1927813"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/353594.353603"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.11.010"},{"key":"e_1_3_2_1_26_1","first-page":"318","volume-title":"CADE, LNCS","author":"Hullot J.-M.","year":"1980","unstructured":"J.-M. Hullot . Canonical forms and unification. In CADE, LNCS vol. 87 , pages 318 -- 334 . Springer , 1980 . J.-M. Hullot. Canonical forms and unification. In CADE, LNCS vol. 87, pages 318--334. Springer, 1980."},{"key":"e_1_3_2_1_27_1","series-title":"LNCS","first-page":"361","volume-title":"Proc. ICALP","author":"Jouannaud J.-P.","year":"1983","unstructured":"J.-P. Jouannaud , C. Kirchner , and H. Kirchner . Incremental construction of unification algorithms in equational theories . In Proc. ICALP , volume 154 of LNCS , pages 361 -- 373 . Springer , 1983 . J.-P. Jouannaud, C. Kirchner, and H. Kirchner. Incremental construction of unification algorithms in equational theories. In Proc. ICALP, volume 154 of LNCS, pages 361--373. Springer, 1983."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32254-2_25"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.11.043"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.17"},{"key":"e_1_3_2_1_31_1","volume-title":"Journal of Automated Reasoning","author":"K\u00fcsters R.","year":"2010","unstructured":"R. K\u00fcsters and T. Truderung . Reducing protocol analysis with xor to the xor-free case in the Horn theory based approach . Journal of Automated Reasoning , 2010 . To appear. R. K\u00fcsters and T. Truderung. Reducing protocol analysis with xor to the xor-free case in the Horn theory based approach. Journal of Automated Reasoning, 2010. To appear."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/646480.693776"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.05.018"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/794196.795054"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00095-X"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9000-6"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(03)00211-4"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788822"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1150577.1150581"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(97)00180-4"},{"key":"e_1_3_2_1_41_1","volume-title":"Proc. STM 2010","author":"Sasse R.","year":"2010","unstructured":"R. Sasse , S. Escobar , J. Meseguer , and C. Meadows . Protocol analysis modulo combination of theories: A case study in Maude-NPA . In Proc. STM 2010 . Springer , 2010 . R. Sasse, S. Escobar, J. Meseguer, and C. Meadows. Protocol analysis modulo combination of theories: A case study in Maude-NPA. In Proc. STM 2010. Springer, 2010."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80022-7"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80026-3"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_21"}],"event":{"name":"PPDP '11: Symposium on Principles and Practices of Declarative Programming","location":"Odense Denmark","acronym":"PPDP '11","sponsor":["University of Southern Denmark","Danish Agency for Science Technology and Innovation DASTI","SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2003476.2003488","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2003476.2003488","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:06:22Z","timestamp":1750244782000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2003476.2003488"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,20]]},"references-count":44,"alternative-id":["10.1145\/2003476.2003488","10.1145\/2003476"],"URL":"https:\/\/doi.org\/10.1145\/2003476.2003488","relation":{},"subject":[],"published":{"date-parts":[[2011,7,20]]},"assertion":[{"value":"2011-07-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}