{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T23:40:30Z","timestamp":1740958830539,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642197505"},{"type":"electronic","value":"9783642197512"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19751-2_3","type":"book-chapter","created":{"date-parts":[[2011,2,24]],"date-time":"2011-02-24T10:55:17Z","timestamp":1298544917000},"page":"34-49","source":"Crossref","is-referenced-by-count":5,"title":["Efficient Decision Procedures for Message Deducibility and Static Equivalence"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Conchinha","sequence":"first","affiliation":[]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[]},{"given":"Carlos","family":"Caleiro","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/11690634_27","volume-title":"Foundations of Software Science and Computation Structures","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Baudet, M., Warinschi, B.: Guessing Attacks and the Computational Soundness of Static Equivalence. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 398\u2013412. Springer, Heidelberg (2006)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-27836-8_7","volume-title":"Automata, Languages and Programming","author":"M. Abadi","year":"2004","unstructured":"Abadi, M., Cortier, V.: Deciding Knowledge in Security Protocols Under Equational Theories. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 46\u201358. Springer, Heidelberg (2004)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cortier, V.: Deciding Knowledge in Security Protocols Under (Many More) Equational Theories. In: Proc. Workshop on Computer Security Foundations (CSFW 2005), pp. 62\u201376 (2005)","DOI":"10.1109\/CSFW.2005.14"},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/373243.360213","volume":"36","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., Fournet, C.: Mobile Values, New Names and Secure Communications. ACM SIGPLAN Notices\u00a036, 104\u2013115 (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P., He\u00e1m, P., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"issue":"3","key":"3_CR6","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D. Basin","year":"2005","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A Symbolic Model Checker for Security Protocols. Int. Journal of Information Security\u00a04(3), 181\u2013208 (2005)","journal-title":"Int. Journal of Information Security"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Baudet, M.: Deciding Security of Protocols against Off-line Guessing Attacks. In: Proc. 12th ACM Conf. on Computer and Communications Security, pp. 16\u201325 (2005)","DOI":"10.1145\/1102120.1102125"},{"key":"3_CR8","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":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/11523468_53","volume-title":"Automata, Languages and Programming","author":"M. Baudet","year":"2005","unstructured":"Baudet, M., Cortier, V., Kremer, S.: Computationally Sound Implementations of Equational Theories Against Passive Adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 652\u2013663. Springer, Heidelberg (2005)"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/CSFW.2001.930138","volume-title":"14th Computer Security Foundations Workshop (CSFW 2001)","author":"B. Blanchet","year":"2001","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th Computer Security Foundations Workshop (CSFW 2001), pp. 82\u201396. IEEE Computer Society, Los Alamitos (2001)"},{"key":"3_CR11","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 (2005); Journal of Logic and Algebraic Programming 75(1), 3\u201351","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"3_CR12","unstructured":"Bella, G., Paulson, L.C.: Using Isabelle to Prove Properties of the Kerberos Authentication System. In: DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Bellovin, S.M., Merritt, M.: Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks. In: IEEE Symposium on Research in Security and Privacy, pp. 72\u201384 (1992)","DOI":"10.1145\/168588.168618"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: An NP Decision Procedure for Protocol Insecurity with XOR. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 261\u2013270 (2003)","DOI":"10.1109\/LICS.2003.1210066"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-24597-1_11","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"Y. Chevalier","year":"2003","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 124\u2013135. Springer, Heidelberg (2003)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-02959-2_27","volume-title":"Automated Deduction \u2013 CADE-22","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.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 355\u2013370. Springer, Heidelberg (2009)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Shmatikov, V.: Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive Or. In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 271\u2013280 (2003)","DOI":"10.1109\/LICS.2003.1210067"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-39910-0_10","volume-title":"Verification: Theory and Practice","author":"H. Comon-Lundh","year":"2004","unstructured":"Comon-Lundh, H., Treinen, R.: Easy Intruder Deductions. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 225\u2013242. Springer, Heidelberg (2004)"},{"key":"3_CR19","unstructured":"Conchinha, B., Basin, D., Caleiro, C.: Efficient Algorithms for Deciding Deduction and Static Equivalence, Technical Reports 680 ETH Z\u00fcrich, Information Security Group D-INFK (2010), ftp:\/\/ftp.inf.ethz.ch\/pub\/publications\/tech-reports\/6xx\/680.pdf"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Corin, R., Doumen, J., Etalle, S.: Analyzing Password Protocol Security Against Off-line Dictionary Attacks. In: Proc. of the 12th ACM Conf. on Computer and Communications Security (CCS 2005). ENTCS, vol.\u00a0121, pp. 47\u201363 (2005)","DOI":"10.1016\/j.entcs.2004.10.007"},{"key":"3_CR21","doi-asserted-by":"publisher","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\u201343 (2006)","journal-title":"Journal of Computer Security"},{"key":"3_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-75560-9_16","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"V. Cortier","year":"2007","unstructured":"Cortier, V., Delaune, S.: Deciding Knowledge in Security Protocols for Monoidal Equational Theories. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 196\u2013210. Springer, Heidelberg (2007)"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1016\/j.ic.2007.07.005","volume":"206","author":"S. Delaune","year":"2009","unstructured":"Delaune, S., Lafourcade, P., Lugiez, D., Treinen, R.: Symbolic Protocol Analysis for Monoidal Equational Theories. Information and Computation\u00a0206, 312\u2013351 (2009)","journal-title":"Information and Computation"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"648","DOI":"10.1109\/49.223865","volume":"11","author":"L. Gong","year":"1993","unstructured":"Gong, L., Lomas, M.A., Needham, R.M., Saltzer, J.H.: Protecting Poorly Chosen Secrets From Guessing Attacks. IEEE Journal on Selected Areas in Communications\u00a011, 648\u2013656 (1993)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Lafourcade, P.: Intruder Deduction for the Equational Theory of Exclusive-or with Commutative and Distributive Encryption. In: Proc. 1st International Workshop on Security and Rewriting Techniques (SecReT 2006). ENTCS, vol.\u00a0171, pp. 37\u201357 (2007)","DOI":"10.1016\/j.entcs.2007.02.054"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"515","DOI":"10.3233\/JCS-2005-13306","volume":"13","author":"J. Millen","year":"2005","unstructured":"Millen, J., Shmatikov, V.: Symbolic Protocol Analysis With an Abelian Group Operator or Diffie\u2013Hellman Exponentiation. Journal of Computer Security\u00a013, 515\u2013564 (2005)","journal-title":"Journal of Computer Security"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19751-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T23:21:46Z","timestamp":1740957706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19751-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642197505","9783642197512"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19751-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}