{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T19:13:09Z","timestamp":1768158789323,"version":"3.49.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,9,20]],"date-time":"2017-09-20T00:00:00Z","timestamp":1505865600000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["645865-SPOOC"],"award-info":[{"award-number":["645865-SPOOC"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-11-JS02-006"],"award-info":[{"award-number":["ANR-11-JS02-006"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"name":"European Sectorial Operational Programme Human Resource Development","award":["POSDRU\/159\/1.5\/S\/137750"],"award-info":[{"award-number":["POSDRU\/159\/1.5\/S\/137750"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1314338"],"award-info":[{"award-number":["1314338"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2016,11,15]]},"abstract":"<jats:p>Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality, and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryptographic protocols. As in the applied pi calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory that allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence, which can therefore be automatically verified for such processes. When protocols are not determinate, our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory is generated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool Active Knowledge in Security Protocols and has been effectively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.<\/jats:p>","DOI":"10.1145\/2926715","type":"journal-article","created":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T10:18:28Z","timestamp":1474366708000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":58,"title":["Automated Verification of Equivalence Properties of Cryptographic Protocols"],"prefix":"10.1145","volume":"17","author":[{"given":"Rohit","family":"Chadha","sequence":"first","affiliation":[{"name":"University of Missouri, MO, USA"}]},{"given":"Vincent","family":"Cheval","sequence":"additional","affiliation":[{"name":"University of Kent"}]},{"given":"\u015etefan","family":"Ciob\u00e2c\u0103","sequence":"additional","affiliation":[{"name":"\u201cAlexandru Ioan Cuza\u201d University, Ia\u015fi, Romania"}]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[{"name":"Inria Nancy--Grand-Est"}]}],"member":"320","published-online":{"date-parts":[[2016,9,20]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2015. French expats vote online in 2012 legislative elections. (2015). http:\/\/www.parliament.uk\/documents\/speaker\/digital-democracy\/FR_Successcase.pdf."},{"key":"e_1_2_2_2_1","unstructured":"2015. Statistics about Internet Voting in Estonia. (2015). http:\/\/www.vvk.ee\/voting-methods-in-estonia\/engindex\/statistics."},{"key":"e_1_2_2_3_1","first-page":"1","article-title":"Deciding knowledge in security protocols under equational theories","volume":"387","author":"Abadi Mart\u00edn","year":"2006","unstructured":"Mart\u00edn Abadi and V\u00e9ronique Cortier. 2006. Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 387, 1--2 (November 2006), 2--32. 10.l016\/j.tcs.2006.08.032","journal-title":"Theor. Comput. Sci."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.12.023"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_2_2_7_1","volume-title":"Formal to Practical Security. LNCS, State-of-the-Art Survey","author":"Affeldt Reynald","unstructured":"Reynald Affeldt and Hubert Comon-Lundh. 2009. Verification of security protocols with a bounded number of sessions based on resolution for rigid variables. In Formal to Practical Security. LNCS, State-of-the-Art Survey, Vol. 5458. Springer, 1--20."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779782.1779786"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.15"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36830-1_2"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_7"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/280474"},{"key":"e_1_2_2_14_1","volume-title":"Handbook of Automated Reasoning","author":"Baader Franz","unstructured":"Franz Baader and Wayne Snyder. 2001. Unification theory. In Handbook of Automated Reasoning, Volume I, Chapter 8. Elsevier Science, 445--532."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.26"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102125"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_11"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/882488.884178"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2004.1301317"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.8"},{"key":"e_1_2_2_22_1","unstructured":"Johannes Borgstr\u00f6m. 2008. Equivalences and Calculi for Formal Verifiation of Cryptographic Protocols. PhD thesis. EPFL Switzerland."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_11"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.15"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_6"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","unstructured":"Vincent Cheval and Bruno Blanchet. 2013. Proving more observational equivalences with proverif. In Principles of Security and Trust\u2014Second International Conference POST. 226--246. 10.1007\/978-3-642-36830-1_12","DOI":"10.1007\/978-3-642-36830-1_12"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_35"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046744"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9199-5"},{"key":"e_1_2_2_30_1","unstructured":"Andrew Cholewa Jos\u00e9 Meseguer and Santiago Escobar. 2014. Variants of Variants and the Finite Variant Property. Research report. University of Illinois at Urbana-Champaign. 13 pages. http:\/\/hdl.handle.net\/2142\/47117."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1776656.1776682"},{"key":"e_1_2_2_32_1","unstructured":"\u015etefan Ciob\u00e2c\u0103. 2011. Computing finite variants for subterm convergent rewrite systems. Research Report LSV-11-06. Laboratoire Sp\u00e9cification et V\u00e9rification ENS Cachan France. 16 pages. http:\/\/www.lsv.ens-cachan.fr\/Publis\/RAPPORTS_LSV\/PDF\/rr-lsv-2011-06.pdf."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_27"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9197-7"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779419.1779435"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.9"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1888881.1888886"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27375-9_6"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2009.2316"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0340"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1804632.1804637"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-09428-1_17"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1981.32"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/941566.941570"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/647091.713943"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2005.04.007"},{"key":"e_1_2_2_51_1","volume-title":"The new south wales ivote system: Security failures and verification flaws in a live online election. CoRR abs\/1504.05646","author":"Alex Halderman J.","year":"2015","unstructured":"J. Alex Halderman and Vanessa Teague. 2015. The new south wales ivote system: Security failures and verification flaws in a live online election. CoRR abs\/1504.05646 (2015). http:\/\/arxiv.org\/abs\/1504.05646"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v9i25.21741"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/b107380"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11266-9_46"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/646480.693776"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275552"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/647215.720390"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11851-2_11"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.28"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753480"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2926715","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2926715","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2926715","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:47:18Z","timestamp":1763459238000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2926715"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,20]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,11,15]]}},"alternative-id":["10.1145\/2926715"],"URL":"https:\/\/doi.org\/10.1145\/2926715","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,20]]},"assertion":[{"value":"2015-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-04-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-09-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}