{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T19:32:23Z","timestamp":1757705543634,"version":"3.37.3"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2010,7,13]],"date-time":"2010-07-13T00:00:00Z","timestamp":1278979200000},"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":[[2011,4]]},"DOI":"10.1007\/s10817-010-9188-8","type":"journal-article","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T11:54:46Z","timestamp":1278935686000},"page":"325-352","source":"Crossref","is-referenced-by-count":18,"title":["Reducing Protocol Analysis with XOR to the XOR-Free Case in the Horn Theory Based Approach"],"prefix":"10.1007","volume":"46","author":[{"given":"Ralf","family":"K\u00fcsters","sequence":"first","affiliation":[]},{"given":"Tomasz","family":"Truderung","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,7,13]]},"reference":[{"issue":"1","key":"9188_CR1","doi-asserted-by":"crossref","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 75(1), 3\u201351 (2008)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"9188_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14), pp. 82\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"9188_CR3","unstructured":"Bull, J.A., Otway, D.J.: The authentication protocol. Technical Report. DRA\/CIS3\/PROJ\/CORBA\/SC\/1\/CSM\/436-04\/03 , Defence Research Agency, Malvern, UK (1997)"},{"key":"9188_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/3-540-44709-1_19","volume-title":"Cryptographic Hardware and Embedded Systems\u2014CHES 2001. Third International Workshop","author":"M Bond","year":"2001","unstructured":"Bond, M.: Attacks on cryptoprocessor transaction sets. In: Cryptographic Hardware and Embedded Systems\u2014CHES 2001. Third International Workshop. Lecture Notes in Computer Science, vol. 2162, pp. 220\u2013234. Springer, Heidelberg (2001)"},{"key":"9188_CR5","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S., Steel, G.: A formal theory of key conjuring. In: 20th IEEE Computer Security Foundations Symposium (CSF\u201907), pp. 79\u201393. IEEE Comp. Soc. Press (2007)","DOI":"10.1109\/CSF.2007.5"},{"key":"9188_CR6","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 261\u2013270. IEEE Computer Society Press (2003)","DOI":"10.1109\/LICS.2003.1210066"},{"key":"9188_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1007\/978-3-540-71209-1_42","volume-title":"Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007)","author":"V Cortier","year":"2007","unstructured":"Cortier, V., Keighren, G., Steel, G.: Automatic analysis of the security of XOR-based key management schemes. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007). Lecture Notes in Computer Science, vol. 4424, pp. 538\u2013552. Springer, Heidelberg (2007)"},{"key":"9188_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/3-540-44881-0_12","volume-title":"Proceedings of the 14th Internatioinal Conference on Rewriting Techniques and Applications (RTA 2003)","author":"H Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Proceedings of the 14th Internatioinal Conference on Rewriting Techniques and Applications (RTA 2003). Lecture Notes in Computer Science, vol. 2706, pp. 148\u2013164. Springer, Heidelberg (2003)"},{"issue":"1\u20133","key":"9188_CR9","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.scico.2003.12.002","volume":"50","author":"H Comon-Lundh","year":"2004","unstructured":"Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Sci. Comput. Program. 50(1\u20133), 51\u201371 (2004)","journal-title":"Sci. Comput. Program."},{"key":"9188_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications, 16th International Conference, RTA 2005","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: Term Rewriting and Applications, 16th International Conference, RTA 2005. Lecture Notes in Computer Science, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"9188_CR11","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive OR. In: Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 271\u2013280. IEEE Computer Society Press (2003)","DOI":"10.1109\/LICS.2003.1210067"},{"key":"9188_CR12","unstructured":"Clulow, J.: The Design and Analysis of Cryptographic APIs for Security Devices. Master\u2019s thesis, University of Natal, Durban (2003)"},{"key":"9188_CR13","unstructured":"CCA Basic Services Reference and Guide: CCA Basic Services Reference and Guide. Available at http:\/\/www-03.ibm.com\/security\/cryptocards\/pdfs\/bs327.pdf (2003)"},{"key":"9188_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"646","DOI":"10.1007\/978-3-540-70918-3_55","volume-title":"Proceedings of the 24th Symposium on Theoretical Aspects of Computer Science (STACS 2007)","author":"R K\u00fcsters","year":"2007","unstructured":"K\u00fcsters, R., Truderung, T.: On the automatic analysis of recursive security protocols with XOR. In: Thomas, W., Weil, P. (eds.) Proceedings of the 24th Symposium on Theoretical Aspects of Computer Science (STACS 2007). Lecture Notes in Computer Science, vol. 4393, pp. 646\u2013657. Springer, Heidelberg (2007)"},{"key":"9188_CR15","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/1455770.1455788","volume-title":"Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS 2008)","author":"R K\u00fcsters","year":"2008","unstructured":"K\u00fcsters, R., Truderung, T.: Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach. In: Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS 2008), pp. 129\u2013138. ACM, New York (2008)"},{"key":"9188_CR16","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn theory Based Approach. Implementation. Available at http:\/\/infsec.uni-trier.de\/software\/KuestersTruderung-XORPROVERIF-2008.zip (2008)","DOI":"10.1145\/1455770.1455788"},{"key":"9188_CR17","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie\u2013Hellman exponentiation. In: Proceedings of the 22th IEEE Computer Security Foundations Symposium (CSF 2009), pp. 157\u2013171. IEEE Computer Society (2009)","DOI":"10.1109\/CSF.2009.17"},{"key":"9188_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/3-540-68339-9_28","volume-title":"Advances in Cryptology\u2014EUROCRYPT \u201996, International Conference on the Theory and Application of Cryptographic Techniques","author":"V Shoup","year":"1996","unstructured":"Shoup, V., Rubin, A.: Session key distribution using smart cards. In: Advances in Cryptology\u2014EUROCRYPT \u201996, International Conference on the Theory and Application of Cryptographic Techniques. Lecture Notes in Computer Science, vol. 1070, pp. 321\u2013331. Springer, Heidelberg (1996)"},{"key":"9188_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/11532231_24","volume-title":"Proceedings of the 20th International Conference on Automated Deduction (CADE 2005)","author":"G Steel","year":"2005","unstructured":"Steel, G.: Deduction with XOR constraints in security API modelling. In: Proceedings of the 20th International Conference on Automated Deduction (CADE 2005). Lecture Notes in Computer Science, vol. 3632, pp. 322\u2013336. Springer, Heidelberg (2005)"},{"key":"9188_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/978-3-642-02348-4_9","volume-title":"Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009)","author":"H Seidl","year":"2009","unstructured":"Seidl, H., Verma, K.N.: Flat and one-variable clauses for single blind copying protocols: the XOR case. In: Treinen, R. (ed.) Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009). Lecture Notes in Computer Science, vol. 55 pp. 118\u2013132. Springer, Heidelberg (2009)"},{"key":"9188_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/11532231_25","volume-title":"Proceedings of the 20th International Conference on Automated Deduction (CADE 2005)","author":"KN Verma","year":"2005","unstructured":"Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational Horn clauses. In: Proceedings of the 20th International Conference on Automated Deduction (CADE 2005). Lecture Notes in Computer Science, vol. 3328, pp. 337\u2013352. Springer, Heidelberg (2005)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9188-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9188-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9188-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T21:01:12Z","timestamp":1740258072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9188-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7,13]]},"references-count":21,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["9188"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9188-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2010,7,13]]}}}