{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,12]],"date-time":"2025-08-12T22:02:11Z","timestamp":1755036131333,"version":"3.41.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319271514"},{"type":"electronic","value":"9783319271521"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-27152-1_5","type":"book-chapter","created":{"date-parts":[[2015,12,9]],"date-time":"2015-12-09T04:55:10Z","timestamp":1449636910000},"page":"86-106","source":"Crossref","is-referenced-by-count":6,"title":["Analysis of the PKCS#11 API Using the Maude-NPA Tool"],"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","published-online":{"date-parts":[[2015,12,9]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur. 10(3) (2007). doi: 10.1145\/1266977.1266978 . http:\/\/dblp.uni-trier.de\/rec\/bib\/journals\/tissec\/AbadiBF07","DOI":"10.1145\/1266977.1266978"},{"key":"5_CR2","unstructured":"Anderson, R.J.: Security Engineering: A Guide to Building Dependable Distributed Systems, 2nd edn. Wiley Publishing (2008). http:\/\/dblp.uni-trier.de\/rec\/bib\/books\/daglib\/0020262"},{"issue":"3","key":"5_CR3","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. J. Inf. Secur. 4(3), 181\u2013208 (2005)","journal-title":"Int. J. Inf. Secur."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, pp. 82\u201396. IEEE Computer Society, June 2001","DOI":"10.1109\/CSFW.2001.930138"},{"key":"5_CR5","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. 2162, pp. 220\u2013234. Springer, Heidelberg (2001)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and fixing pkcs# 11 security tokens. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, pp. 260\u2013269. ACM (2010)","DOI":"10.1145\/1866307.1866337"},{"key":"5_CR7","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A formal analysis of some properties of kerberos 5 using msr. In: CSFW, p. 175. IEEE Computer Society (2002)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-28641-4_19","volume-title":"Principles of Security and Trust","author":"M Centenaro","year":"2012","unstructured":"Centenaro, M., Focardi, R., Luccio, F.L.: Type-based analysis of PKCS#11 key management. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 349\u2013368. Springer, Heidelberg (2012)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/978-3-540-45238-6_32","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2003","author":"J Clulow","year":"2003","unstructured":"Clulow, J.: On the security of PKCS #11. In: Walter, C.D., Ko\u00e7, \u00c7.K., Paar, C. (eds.) CHES 2003. LNCS, vol. 2779, pp. 411\u2013425. Springer, Heidelberg (2003)"},{"key":"5_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. 5789, pp. 605\u2013620. Springer, Heidelberg (2009)"},{"key":"5_CR11","unstructured":"Cryptosense. Cryptosense Web Page. https:\/\/cryptosense.com\/"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Delaune, S., Kremer, S., Steel, G.: Formal analysis of pkcs#11. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, 23\u201325 June 2008, Pittsburgh, Pennsylvania, pp. 331\u2013344. IEEE Computer Society (2008)","DOI":"10.1109\/CSF.2008.16"},{"key":"5_CR13","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., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Effective symbolic protocol analysis via equational irreducibility conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 73\u201390. Springer, Heidelberg (2012)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, J., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009)"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.ic.2014.07.007","volume":"238","author":"S Escobar","year":"2014","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL Protocol Analyzer. Inf. Comput. 238, 157\u2013186 (2014)","journal-title":"Inf. Comput."},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"FJ Thayer Fabrega","year":"1999","unstructured":"Thayer Fabrega, F.J., Herzog, J., Guttman, J.: Strand spaces: what makes a security protocol correct? J. Comput. Secur. 7, 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-23082-0_2","volume-title":"Foundations of Security Analysis and Design VI","author":"R Focardi","year":"2011","unstructured":"Focardi, R., Luccio, F.L., Steel, G.: An introduction to security API analysis. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol. 6858, pp. 35\u201365. Springer, Heidelberg (2011)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-03459-6_7","volume-title":"Foundations and Applications of Security Analysis","author":"S Fr\u00f6schle","year":"2009","unstructured":"Fr\u00f6schle, S., Steel, G.: Analysing PKCS#11 key management APIs with unbounded fresh data. In: Degano, P., Vigan\u00f2, L. (eds.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 92\u2013106. Springer, Heidelberg (2009)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-319-14054-4_8","volume-title":"Security Standardisation Research","author":"A Gonz\u00e1lez-Burgue\u00f1o","year":"2014","unstructured":"Gonz\u00e1lez-Burgue\u00f1o, A., Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: Analysis of the IBM CCA security API protocols in Maude-NPA. In: Chen, L., Mitchell, C. (eds.) SSR 2014. LNCS, vol. 8893, pp. 111\u2013130. Springer, Heidelberg (2014)"},{"key":"5_CR20","unstructured":"IBM. CCA basic services reference and guide: CCA basic services reference and guide for the IBM 4758 PCI and IBM 4764 (2008). http:\/\/www-03.ibm.com\/security\/cryptocards\/pdfs\/bs327.pdf."},{"key":"5_CR21","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"},{"key":"5_CR22","unstructured":"Kremer, S., K\u00fcnnemann, R.: Automated analysis of security protocols with global state. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, 18\u201321 May, 2014, Berkeley, CA, USA, pp. 163\u2013178 (2014)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-3-662-46666-7_12","volume-title":"Principles of Security and Trust","author":"R K\u00fcnnemann","year":"2015","unstructured":"K\u00fcnnemann, R.: Automated backward analysis of PKCS#11 v2.20. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 219\u2013238. Springer, Heidelberg (2015)"},{"key":"5_CR24","unstructured":"RSA Laboratories. PKCS#11: Cryptographic token interface standard. https:\/\/www.emc.com\/emc-plus\/rsa-labs\/standards-initiatives\/pkcs-11-cryptographic-token-interface-standard.htm"},{"issue":"1","key":"5_CR25","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. Comput. Secur. 11(1), 75\u201389 (1992)","journal-title":"Comput. Secur."},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Applying formal methods to the analysis of a key management protocol. J. Comput. Secur. 1(1) (1992)","DOI":"10.3233\/JCS-1992-1102"},{"issue":"6","key":"5_CR27","doi-asserted-by":"publisher","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. J. Comput. Secur. 12(6), 893\u2013932 (2004)","journal-title":"J. Comput. Secur."},{"issue":"6","key":"5_CR28","doi-asserted-by":"publisher","first-page":"893","DOI":"10.3233\/JCS-2004-12604","volume":"12","author":"C Meadows","year":"2004","unstructured":"Meadows, C., Syverson, P.F., Cervesato, I.: Formal specification and analysis of the group domain of interpretation protocol using NPATRL and the NRL protocol analyzer. J. Comput. Secur. 12(6), 893\u2013931 (2004)","journal-title":"J. Comput. Secur."},{"key":"5_CR29","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":"5_CR30","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 analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"key":"5_CR31","unstructured":"OASIS. OASIS PKCS 11 TC. OASIS PKCS 11 TC Home Page. https:\/\/www.oasis-open.org\/committees\/tc_home.php?wg_abbrev=pkcs11"},{"key":"5_CR32","unstructured":"Tsalapati, E.: Analysis of PKCS#11 using AVISPA tools. Master\u2019s thesis, University of Edinburgh (2007)"}],"container-title":["Lecture Notes in Computer Science","Security Standardisation Research"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27152-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T18:05:18Z","timestamp":1748714718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27152-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319271514","9783319271521"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27152-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}