{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:26:31Z","timestamp":1774837591238,"version":"3.50.1"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,9,1]],"date-time":"2010-09-01T00:00:00Z","timestamp":1283299200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,2]]},"DOI":"10.1007\/s10817-010-9197-7","type":"journal-article","created":{"date-parts":[[2010,8,31]],"date-time":"2010-08-31T05:15:44Z","timestamp":1283231744000},"page":"219-262","source":"Crossref","is-referenced-by-count":14,"title":["Computing Knowledge in Security Protocols Under Convergent Equational Theories"],"prefix":"10.1007","volume":"48","author":[{"given":"\u015etefan","family":"Ciob\u00e2c\u0103","sequence":"first","affiliation":[]},{"given":"St\u00e9phanie","family":"Delaune","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,9,1]]},"reference":[{"issue":"1\u20132","key":"9197_CR1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"387","author":"M Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comp. Sci. 387(1\u20132), 2\u201332 (2006)","journal-title":"Theor. Comp. Sci."},{"key":"9197_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th ACM Symposium on Principles of Programming Languages (POPL\u201901). ACM (2001)","DOI":"10.1145\/360204.360213"},{"key":"9197_CR3","unstructured":"Anantharaman, S., Narendran, P., Rusinowitch, M.: Intruders with caps. In: Proc. 18th International Conference on Term Rewriting and Applications (RTA\u201907). LNCS, vol. 4533. Springer (2007)"},{"key":"9197_CR4","doi-asserted-by":"crossref","unstructured":"Armando, A., et\u00a0al.: The AVISPA Tool for the automated validation of internet security protocols and applications. In: Proc. 17th Int. Conference on Computer Aided Verification (CAV\u201905). LNCS, vol. 3576, pp. 281\u2013285. Springer (2005)","DOI":"10.1007\/11513988_27"},{"key":"9197_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-540-74621-8_7","volume-title":"Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS\u201907)","author":"M Arnaud","year":"2007","unstructured":"Arnaud, M., Cortier, V., Delaune, S.: Combining algorithms for deciding knowledge in security protocols. In: Wolter, F. (ed.) Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS\u201907). Lecture Notes in Artificial Intelligence, vol. 4720, pp. 103\u2013117. Springer, Liverpool, UK (2007)"},{"key":"9197_CR6","doi-asserted-by":"crossref","unstructured":"Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: Proc. 21st IEEE Computer Security Foundations Symposium (CSF\u201908) (2008)","DOI":"10.1109\/CSF.2008.26"},{"key":"9197_CR7","doi-asserted-by":"crossref","unstructured":"Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: Proc. IEEE Symposium on Security and Privacy (S&P\u201908). IEEE Computer Society Press (2008)","DOI":"10.1109\/SP.2008.23"},{"key":"9197_CR8","doi-asserted-by":"crossref","unstructured":"Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: 12th ACM Conference on Computer and Communications Security (CCS\u201905) (2005)","DOI":"10.1145\/1102120.1102125"},{"key":"9197_CR9","unstructured":"Baudet, M.: YAPA (Yet Another Protocol Analyzer). http:\/\/www.lsv.ens-cachan.fr\/~baudet\/yapa\/index.html (2008)"},{"key":"9197_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-642-02348-4_11","volume-title":"Proc. 20th International Conference on Rewriting Techniques and Applications (RTA\u201909)","author":"M Baudet","year":"2009","unstructured":"Baudet, M., Cortier, V., Delaune, S.: YAPA: a generic tool for computing intruder knowledge. In: Proc. 20th International Conference on Rewriting Techniques and Applications (RTA\u201909), Lecture Notes in Computer Science, vol. 5595, pp. 148\u2013163. Springer, Bras\u00edlia, Brazil (2009)"},{"key":"9197_CR11","unstructured":"Berrima, M., Ben Rajeb, N., Cortier, V.: Deciding knowledge in security protocols under some e-voting theories. Research Report RR-6903, INRIA (2009)"},{"key":"9197_CR12","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th Computer Security Foundations Workshop (CSFW\u201901), pp. 82\u201396. IEEE Computer Society Press (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"9197_CR13","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Symposium on Logic in Computer Science, pp. 331\u2013340. IEEE Computer Society Press (2005)","DOI":"10.1109\/LICS.2005.8"},{"key":"9197_CR14","unstructured":"Chevalier, Y.: R\u00e9solution de probl\u00e8mes d\u2019 accessibilit\u00e9 pour la compilation et la validation de protocoles cryptographiques. Ph.D. thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy, France (2003)"},{"key":"9197_CR15","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Kourjieh, M.: Key substitution in the symbolic analysis of cryptographic protocols. In: Proc. 27th International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS\u201907), pp.\u00a0121\u2013132 (2007)","DOI":"10.1007\/978-3-540-77050-3_10"},{"key":"9197_CR16","unstructured":"Ciob\u00e2c\u0103, \u015e.: KiSs. http:\/\/www.lsv.ens-cachan.fr\/~ciobaca\/kiss (2009)"},{"key":"9197_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-642-02959-2_27","volume-title":"Proceedings of the 22nd International Conference on Automated Deduction (CADE\u201909)","author":"\u015e Ciob\u00e2c\u0103","year":"2009","unstructured":"Ciob\u00e2c\u0103, \u015e., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. In: Schmidt, R. (ed.) Proceedings of the 22nd International Conference on Automated Deduction (CADE\u201909). Lecture Notes in Artificial Intelligence, pp.\u00a0355\u2013370, Springer, Montreal, Canada (2009)"},{"key":"9197_CR18","unstructured":"Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. In: Proc. 2nd International Workshop on Security Issues with Petri Nets and Other Computational Models (WISP\u201904), ENTCS (2004)"},{"key":"9197_CR19","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S.: Deciding knowledge in security protocols for monoidal equational theories. In: Proc. 14th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201907). LNAI. Springer (2007)","DOI":"10.1007\/978-3-540-75560-9_16"},{"issue":"1","key":"9197_CR20","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. J. Comput. Secur. 14(1), 1\u201343 (2006)","journal-title":"J. Comput. Secur."},{"issue":"4","key":"9197_CR21","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. J. Comput. Secur. 17(4), 435\u2013487 (2009)","journal-title":"J. Comput. Secur."},{"key":"9197_CR22","doi-asserted-by":"crossref","unstructured":"Kremer, S., Ryan, M.D.: Analysis of an electronic voting protocol in the applied pi-calculus. In: 14th European Symposium on Programming (ESOP\u201905). LNCS, vol. 3444, pp. 186\u2013200. Springer (2005)","DOI":"10.1007\/978-3-540-31987-0_14"},{"issue":"4","key":"9197_CR23","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1016\/j.ic.2006.10.008","volume":"205","author":"P Lafourcade","year":"2007","unstructured":"Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for the equational theory of Abelian groups with distributive encryption. Inf. Comput. 205(4), 581\u2013623 (2007)","journal-title":"Inf. Comput."},{"key":"9197_CR24","doi-asserted-by":"crossref","unstructured":"Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. 8th ACM Conference on Computer and Communications Security (CCS\u201901) (2001)","DOI":"10.1145\/502006.502007"},{"key":"9197_CR25","doi-asserted-by":"crossref","unstructured":"Okamoto, T.: Receipt-free electronic voting schemes for large scale elections. In: Proc. 5th Int. Security Protocols Workshop, LNCS, vol. 1361. Springer (1997)","DOI":"10.1007\/BFb0028157"},{"key":"9197_CR26","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1016\/S0304-3975(02)00490-5","volume":"299","author":"M Rusinowitch","year":"2003","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions and composed keys is NP-complete. Theor. Comp. Sci. 299, 451\u2013475 (2003)","journal-title":"Theor. Comp. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9197-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9197-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9197-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T07:47:50Z","timestamp":1740469670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9197-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,1]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["9197"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9197-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,9,1]]}}}