{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T07:04:32Z","timestamp":1763017472388,"version":"3.40.5"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319140537"},{"type":"electronic","value":"9783319140544"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-14054-4_8","type":"book-chapter","created":{"date-parts":[[2014,12,10]],"date-time":"2014-12-10T03:39:19Z","timestamp":1418182759000},"page":"111-130","source":"Crossref","is-referenced-by-count":7,"title":["Analysis of the IBM CCA Security API Protocols in Maude-NPA"],"prefix":"10.1007","author":[{"given":"Antonio","family":"Gonz\u00e1lez-Burgue\u00f1o","sequence":"first","affiliation":[]},{"given":"Sonia","family":"Santiago","sequence":"additional","affiliation":[]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur.\u00a010(3) (2007)","DOI":"10.1145\/1266977.1266978"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW 2014), Cape Breton, Nova Scotia, Canada, June 2001, pp. 82\u201396. IEEE Computer Society (2014)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"8_CR3","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":"8_CR4","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A formal analysis of some properties of kerberos 5 using msr. In: CSFW, pp. 175\u20131790. IEEE Computer Society (2002)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Cachin, C., Chandran, N.: A secure cryptographic token interface. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, pp. 141\u2013153 (2009)","DOI":"10.1109\/CSF.2009.7"},{"key":"8_CR6","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: 18th Annual IEEE Symposium on Logic in Computer Science, LICS 2003 (2003)"},{"key":"8_CR7","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":"8_CR8","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":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/978-3-540-71209-1_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. Cortier","year":"2007","unstructured":"Cortier, V., Keighren, G., Steel, G.: Automatic analysis of the aecurity of XOR-based key management schemes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 538\u2013552. Springer, Heidelberg (2007)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/978-3-642-04444-1_37","volume-title":"Computer Security \u2013 ESORICS 2009","author":"V. Cortier","year":"2009","unstructured":"Cortier, V., Steel, G.: A generic security API for symmetric key management on cryptographic devices. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol.\u00a05789, pp. 605\u2013620. Springer, Heidelberg (2009)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-33167-1_5","volume-title":"Computer Security \u2013 ESORICS 2012","author":"S. Erbatur","year":"2012","unstructured":"Erbatur, S., et al.: Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol.\u00a07459, pp. 73\u201390. Springer, Heidelberg (2012)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol.\u00a05705, pp. 1\u201350. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-642-15497-3_19","volume-title":"Computer Security \u2013 ESORICS 2010","author":"S. Escobar","year":"2010","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Sequential Protocol Composition in Maude-NPA. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol.\u00a06345, pp. 303\u2013318. Springer, Heidelberg (2010)"},{"key":"8_CR14","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J. Thayer Fabrega","year":"1999","unstructured":"Thayer Fabrega, F.J., Herzog, J., Guttman, J.: Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security\u00a07, 191\u2013230 (1999)","journal-title":"Journal of Computer Security"},{"key":"8_CR15","unstructured":"Gonz\u00e1lez-Burgue\u00f1o, A.: Protocol Analysis Modulo Exclusive-Or Theories: A Case study in Maude-NPA. Master\u2019s thesis, Universitat Polit\u00e8cnica de Val\u00e8ncia (March 2014), https:\/\/angonbur.webs.upv.es\/Previous_work\/Master_Thesis.pdf"},{"key":"8_CR16","unstructured":"IBM. Comment on Mike\u2019s Bond paper A Chosen Key Difference Attack on Control Vectors (2001), http:\/\/www.cl.cam.ac.uk\/~mkb23\/research\/CVDif-Response.pdf"},{"key":"8_CR17","unstructured":"IBM. CCA basic services reference and guide: CCA basic services reference and guide for the IBM 4758 PCI and IBM 4764 (2001), http:\/\/www-03.ibm.com\/security\/cryptocards\/pdfs\/bs327.pdf.2008"},{"key":"8_CR18","unstructured":"Keighren, G.: Model Checking IBM\u2019s Common Cryptographic Architecture API. Technical Report 862, University of Edinburgh (October 2006)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Kemmerer, R.A.: Using formal verification techniques to analyze encryption protocols. In: IEEE Symposium on Security and Privacy, pp. 134\u2013139. IEEE Computer Society (1987)","DOI":"10.1109\/SP.1987.10005"},{"issue":"3-4","key":"8_CR20","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":"8_CR21","doi-asserted-by":"crossref","unstructured":"Linn, J.: Generic security service application program interface version 2, update 1. IETF RFC 2743 (2000), https:\/\/datatracker.ietf.org\/doc\/rfc2743","DOI":"10.17487\/rfc2743"},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0167-4048(92)90222-D","volume":"11","author":"D. Longley","year":"1992","unstructured":"Longley, D., Rigby, S.: An automatic search for security flaws in key management schemes. Computers & Security\u00a011(1), 75\u201389 (1992)","journal-title":"Computers & Security"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Applying formal methods to the analysis of a key management protocol. Journal of Computer Security\u00a01(1) (1992)","DOI":"10.3233\/JCS-1992-1102"},{"issue":"2","key":"8_CR24","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming\u00a026(2), 113\u2013131 (1996)","journal-title":"Journal of Logic Programming"},{"issue":"6","key":"8_CR25","doi-asserted-by":"crossref","first-page":"893","DOI":"10.3233\/JCS-2004-12604","volume":"12","author":"C. Meadows","year":"2004","unstructured":"Meadows, C., Cervesato, I., Syverson, P.: Specification and Analysis of the Group Domain of Interpretation Protocol using NPATRL and the NRL Protocol Analyzer. Journal of Computer Security\u00a012(6), 893\u2013932 (2004)","journal-title":"Journal of Computer Security"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Analysis of the internet key exchange protocol using the nrl protocol analyzer. In: IEEE Symposium on Security and Privacy, pp. 216\u2013231. IEEE Computer Society (1999)","DOI":"10.21236\/ADA465466"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S. Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic snalysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-36213-2_11","volume-title":"Security Protocols XVII","author":"A. Mukhamedov","year":"2013","unstructured":"Mukhamedov, A., Gordon, A.D., Ryan, M.: Towards a verified reference implementation of a trusted platform module. In: Christianson, B., Malcolm, J.A., Maty\u00e1\u0161, V., Roe, M. (eds.) Security Protocols 2009. LNCS, vol.\u00a07028, pp. 69\u201381. Springer, Heidelberg (2013)"},{"key":"8_CR29","unstructured":"National Institute of Standards and Technology. FIPS PUB 46-3: Data Encryption Standard (DES), supersedes FIPS 46-2 (October 1999)"},{"key":"8_CR30","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":"8_CR31","doi-asserted-by":"crossref","unstructured":"Steel, G.: Deduction with xor constraints in security api modelling. In: Nieuwenhuis (ed.) [30], pp. 322\u2013336","DOI":"10.1007\/11532231_24"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis (ed.) [30], pp. 337\u2013352","DOI":"10.1007\/11532231_25"}],"container-title":["Lecture Notes in Computer Science","Security Standardisation Research"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-14054-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T00:15:40Z","timestamp":1747181740000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-14054-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319140537","9783319140544"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-14054-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}