{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T15:55:18Z","timestamp":1761580518392},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540712084"},{"type":"electronic","value":"9783540712091"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_42","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"538-552","source":"Crossref","is-referenced-by-count":18,"title":["Automatic Analysis of the Security of XOR-Based Key Management Schemes"],"prefix":"10.1007","author":[{"given":"V\u00e9ronique","family":"Cortier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gavin","family":"Keighren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graham","family":"Steel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"42_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-55602-8_155","volume-title":"Automated Deduction - CADE-11","author":"F. Baader","year":"1992","unstructured":"Baader, F., Schulz, K.: Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 50\u201365. Springer, Heidelberg (1992)"},{"key":"42_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-44709-1_19","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2001","author":"M. Bond","year":"2001","unstructured":"Bond, M.: Attacks on cryptoprocessor transaction sets. In: Ko\u00e7, \u00c7.K., Naccache, D., Paar, C. (eds.) CHES 2001. LNCS, vol.\u00a02162, pp. 220\u2013234. Springer, Heidelberg (2001)"},{"key":"42_CR3","unstructured":"CCA Basic Services Reference and Guide (October 2006), Available online at \n                    \n                      http:\/\/www-03.ibm.com\/security\/cryptocards\/pdfs\/bs327.pdf"},{"key":"42_CR4","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., et al.: An NP decision procedure for protocol insecurity with XOR. In: Proc. of 18th Annual IEEE Symposium on Logic in Computer Science (LICS \u201903), pp. 261\u2013270 (2003)","DOI":"10.1109\/LICS.2003.1210066"},{"key":"42_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-44881-0_12","volume-title":"Rewriting Techniques and Applications","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: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 148\u2013164. Springer, Heidelberg (2003)"},{"key":"42_CR6","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proc. of 18th Annual IEEE Symposium on Logic in Computer Science (LICS \u201903), pp. 271\u2013280 (2003)","DOI":"10.1109\/LICS.2003.1210067"},{"key":"42_CR7","unstructured":"Cortier, V., Keighren, G., Steel, G.: Automatic analysis of the security of XOR-based key management schemes. Inf.\u00a0Research Report EDI-INF-RR-0863, U. of Edinburgh (2006)"},{"key":"42_CR8","unstructured":"Courant, J., Monin, J.-F.: Defending the bank with a proof assistant. In: Proceedings of Workshop on Issues in the Theory of Security (WITS \u201906), Vienna (March 2006)"},{"key":"42_CR9","unstructured":"IBM Comment on \u201cA Chosen Key Difference Attack on Control Vectors\u201d (January 2001) Available from \n                    \n                      http:\/\/www.cl.cam.ac.uk\/~mkb23\/research.html"},{"key":"42_CR10","unstructured":"Keighren, G.: Model checking IBM\u2019s common cryptographic architecture API. Informatics Research Report EDI-INF-RR-0862, University of Edinburgh (2006)"},{"key":"42_CR11","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","year":"2005","unstructured":"Nieuwenhuis, R. (ed.): CADE 2005. LNCS (LNAI), vol.\u00a03632. Springer, Heidelberg (2005)"},{"key":"42_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/11532231_24","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Steel","year":"2005","unstructured":"Steel, G.: Deduction with XOR constraints in security API modelling. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 322\u2013336. Springer, Heidelberg (2005)"},{"key":"42_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/11805618_21","volume-title":"Term Rewriting and Applications","author":"M. Turuani","year":"2006","unstructured":"Turuani, M.: The CL-Atse Protocol Analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 277\u2013286. Springer, Heidelberg (2006)"},{"key":"42_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/11532231_25","volume-title":"Automated Deduction \u2013 CADE-20","author":"K.N. Verma","year":"2005","unstructured":"Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational Horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 337\u2013352. Springer, Heidelberg (2005)"},{"key":"42_CR15","unstructured":"Youn, P., et al.: Robbing the bank with a theorem prover. Technical Report UCAM-CL-TR-644, University of Cambridge (August 2005)"},{"key":"42_CR16","unstructured":"AVISPA Tool Set. Available from \n                    \n                      http:\/\/www.avispa-project.org\/"},{"key":"42_CR17","unstructured":"AVISPA User Manual, version 1.1 (June 2006) Available online at \n                    \n                      http:\/\/www.avispa-project.org\/package\/user-manual.pdf"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_42.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:51Z","timestamp":1605763011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_42","relation":{},"subject":[]}}