{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T19:40:02Z","timestamp":1742758802761,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642286407"},{"type":"electronic","value":"9783642286414"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28641-4_10","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T21:10:46Z","timestamp":1332450646000},"page":"169-188","source":"Crossref","is-referenced-by-count":6,"title":["Reduction of Equational Theories for Verification of Trace Equivalence: Re-encryption, Associativity and Commutativity"],"prefix":"10.1007","author":[{"given":"Myrto","family":"Arapinis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergiu","family":"Bursuc","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark D.","family":"Ryan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1-2","key":"10_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science\u00a0367(1-2), 2\u201332 (2006)","journal-title":"Theoretical Computer Science"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104\u2013115 (January 2001)","DOI":"10.1145\/373243.360213"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Information and Computation\u00a0148(1) (1999)","DOI":"10.1006\/inco.1998.2740"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: CSF, pp. 107\u2013121. IEEE Computer Society (2010)","DOI":"10.1109\/CSF.2010.15"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS 2005), Alexandria, Virginia, USA, pp. 16\u201325. ACM Press (November 2005)","DOI":"10.1145\/1102120.1102125"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-02348-4_11","volume-title":"Rewriting Techniques and Applications","author":"M. Baudet","year":"2009","unstructured":"Baudet, M., Cortier, V., Delaune, S.: YAPA: A Generic Tool for Computing Intruder Knowledge. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 148\u2013163. Springer, Heidelberg (2009)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: IEEE Symposium on Security and Privacy, pp. 86\u2013100 (2004)","DOI":"10.1109\/SECPRI.2004.1301317"},{"issue":"1","key":"10_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","volume":"75","author":"B. Blanchet","year":"2008","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming\u00a075(1), 3\u201351 (2008)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-14203-1_35","volume-title":"Automated Reasoning","author":"V. Cheval","year":"2010","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Automating Security Analysis: Symbolic Equivalence of Constraint Systems. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 412\u2013426. Springer, Heidelberg (2010)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: Negative tests and non-determinism. In: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011), Chicago, Illinois, USA. ACM Press (October 2011)","DOI":"10.1145\/2046707.2046744"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Ciob\u00e2c\u0103, \u015e., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. Journal of Automated Reasoning (2011)","DOI":"10.1007\/s10817-010-9197-7"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-36575-3_8","volume-title":"Programming Languages and Systems","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: Security Properties: Two Agents Are Sufficient. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 99\u2013113. Springer, Heidelberg (2003)"},{"key":"10_CR13","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":"10_CR14","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.entcs.2004.10.007","volume":"121","author":"R. Corin","year":"2005","unstructured":"Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. Electr. Notes Theor. Comput. Sci.\u00a0121, 47\u201363 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S.: A method for proving observational equivalence. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF 2009), Port Jefferson, NY, USA, pp. 266\u2013276. IEEE Computer Society Press (July 2009)","DOI":"10.1109\/CSF.2009.9"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S.: Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning (2011)","DOI":"10.1007\/s10817-010-9208-8"},{"issue":"1","key":"10_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/JCS-2006-14101","volume":"14","author":"V. Cortier","year":"2006","unstructured":"Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security\u00a014(1), 1\u201343 (2006)","journal-title":"Journal of Computer Security"},{"issue":"3-4","key":"10_CR18","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s10817-010-9187-9","volume":"46","author":"V. Cortier","year":"2010","unstructured":"Cortier, V., Kremer, S., Warinschi, B.: A\u00a0survey of symbolic methods in computational analysis of cryptographic systems. Journal of Automated Reasoning\u00a046(3-4), 225\u2013259 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Cortier, V., Smyth, B.: Attacking and fixing helios: An analysis of ballot secrecy. In: Proc. of the 24th IEEE Computer Security Foundations Symposium, pp. 297\u2013311 (2011)","DOI":"10.1109\/CSF.2011.27"},{"issue":"4","key":"10_CR20","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S. Delaune","year":"2009","unstructured":"Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security\u00a017(4), 435\u2013487 (2009)","journal-title":"Journal of Computer Security"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 243\u2013309. North-Holland (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"2","key":"10_CR22","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1145\/941566.941570","volume":"12","author":"L. Durante","year":"2003","unstructured":"Durante, L., Sisto, R., Valenzano, A.: Automatic testing equivalence verification of spi calculus specifications. ACM Trans. Softw. Eng. Methodol.\u00a012(2), 222\u2013284 (2003)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Kremer, S., Mercier, A., Treinen, R.: Reducing equational theories for the decision of static equivalence. Journal of Automated Reasoning (2011)","DOI":"10.1007\/s10817-010-9203-0"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Using proverif to analyze protocols with Diffie-Hellman exponentiation. In: CSF, pp. 157\u2013171. IEEE Computer Society (2009)","DOI":"10.1109\/CSF.2009.17"},{"issue":"3-4","key":"10_CR25","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10817-010-9188-8","volume":"46","author":"R. K\u00fcsters","year":"2011","unstructured":"K\u00fcsters, R., Truderung, T.: Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. J. Autom. Reasoning\u00a046(3-4), 325\u2013352 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-30191-2_21","volume-title":"Information and Communications Security","author":"C. Lynch","year":"2004","unstructured":"Lynch, C., Meadows, C.: Sound Approximations to Diffie-Hellman Using Rewrite Rules. In: L\u00f3pez, J., Qing, S., Okamoto, E. (eds.) ICICS 2004. LNCS, vol.\u00a03269, pp. 262\u2013277. Springer, Heidelberg (2004)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S.: Diffie-Hellman without difficulty. In: FAST (2011)","DOI":"10.1007\/978-3-642-29420-4_14"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/11863908_20","volume-title":"Computer Security \u2013 ESORICS 2006","author":"P.Y.A. Ryan","year":"2006","unstructured":"Ryan, P.Y.A., Schneider, S.A.: Pr\u00eat \u00e0 Voter with Re-encryption Mixes. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 313\u2013326. Springer, Heidelberg (2006)"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Tiu, A., Dawson, J.E.: Automating open bisimulation checking for the spi calculus. In: Proc. of the 23rd IEEE Computer Security Foundations Symposium, pp. 307\u2013321 (2010)","DOI":"10.1109\/CSF.2010.28"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28641-4_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:58:39Z","timestamp":1742756319000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28641-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642286407","9783642286414"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28641-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}