{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T23:14:32Z","timestamp":1763507672456},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642230813"},{"type":"electronic","value":"9783642230820"}],"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-23082-0_2","type":"book-chapter","created":{"date-parts":[[2011,8,9]],"date-time":"2011-08-09T04:24:32Z","timestamp":1312863872000},"page":"35-65","source":"Crossref","is-referenced-by-count":10,"title":["An Introduction to Security API Analysis"],"prefix":"10.1007","author":[{"given":"Riccardo","family":"Focardi","sequence":"first","affiliation":[]},{"given":"Flaminia L.","family":"Luccio","sequence":"additional","affiliation":[]},{"given":"Graham","family":"Steel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Hackers crack cash machine PIN codes to steal millions. The Times online, http:\/\/www.timesonline.co.uk\/tol\/money\/consumer_affairs\/article4259009.ece"},{"key":"2_CR2","unstructured":"Mastermind, http:\/\/commons.wikimedia.org\/wiki\/File:Mastermind.jpg"},{"key":"2_CR3","unstructured":"PIN Crackers Nab Holy Grail of Bank Card Security. Wired Magazine Blog \u2019Threat Level\u2019, http:\/\/blog.wired.com\/27bstroke6\/2009\/04\/pins.html"},{"key":"2_CR4","unstructured":"The EMV Standard, http:\/\/www.emvco.com\/"},{"key":"2_CR5","unstructured":"Anderson, R.: The correctness of crypto transaction sets. In: 8th International Workshop on Security Protocols (April 2000), http:\/\/www.cl.cam.ac.uk\/ftp\/users\/rja14\/protocols00.pdf"},{"key":"2_CR6","first-page":"288","volume-title":"Security Protocols","author":"R. Anderson","year":"2003","unstructured":"Anderson, R.: What we can learn from API security (transcript of discussion). In: Security Protocols, pp. 288\u2013300. Springer, Heidelberg (2003)"},{"key":"2_CR7","volume-title":"Security Engineering","author":"R. Anderson","year":"2007","unstructured":"Anderson, R.: Security Engineering, 2nd edn. Wiley, Chichester (2007)","edition":"2"},{"key":"2_CR8","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.A., Boichut, Y., Chevalier, Y., Compagna, L., Cu\u00e9llar, J., Hankes Drielsma, P., H\u00e9am, 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":"1","key":"2_CR9","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10207-007-0041-y","volume":"7","author":"A. Armando","year":"2008","unstructured":"Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. Int. J. Inf. Sec.\u00a07(1), 3\u201332 (2008), Software available at http:\/\/www.ai-lab.it\/satmc , Currently developed under the AVANTSSAR project, http:\/\/www.avantssar.eu","journal-title":"Int. J. Inf. Sec."},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-540-77366-5_20","volume-title":"Financial Cryptography and Data Security","author":"O. Berkman","year":"2007","unstructured":"Berkman, O., Ostrovsky, O.M.: The unbearable lightness of PIN cracking. In: Dietrich, S., Dhamija, R. (eds.) FC 2007 and USEC 2007. LNCS, vol.\u00a04886, pp. 224\u2013238. Springer, Heidelberg (2007)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45789-5_25","volume-title":"Static Analysis","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B.: From secrecy to authenticity in security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 342\u2013359. Springer, Heidelberg (2002)"},{"key":"2_CR12","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)"},{"issue":"10","key":"2_CR13","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1109\/2.955101","volume":"34","author":"M. Bond","year":"2001","unstructured":"Bond, M., Anderson, R.: API level attacks on embedded systems. IEEE Computer Magazine\u00a034(10), 67\u201375 (2001)","journal-title":"IEEE Computer Magazine"},{"key":"2_CR14","unstructured":"Bond, M., Clulow, J.: Encrypted? randomised? compromised (when cryptographically secured data is not secure). In: Cryptographic Algorithms and their Uses, pp. 140\u2013151 (2004)"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.entcs.2004.09.036","volume":"125","author":"M. Bond","year":"2005","unstructured":"Bond, M., Clulow, J.: Extending security protocol analysis: New challenges. Electronic Notes in Theoretical Computer Science\u00a0125(1), 13\u201324 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2_CR16","unstructured":"Bond, M., Zielinski, P.: Decimalization table attacks for pin cracking. Technical Report UCAM-CL-TR-560, University of Cambridge, Computer Laboratory (2003), http:\/\/www.cl.cam.ac.uk\/TechReports\/UCAM-CL-TR-560.pdf"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/1866307.1866337","volume-title":"Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS 2010)","author":"M. Bortolozzo","year":"2010","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 (CCS 2010), pp. 260\u2013269. ACM Press, Chicago (2010)"},{"issue":"4","key":"2_CR18","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/MSP.2010.124","volume":"8","author":"C. Cachin","year":"2010","unstructured":"Cachin, C., Camenisch, J.: Encrypting keys securely. IEEE Security & Privacy\u00a08(4), 66\u201369 (2010)","journal-title":"IEEE Security & Privacy"},{"key":"2_CR19","first-page":"141","volume-title":"Computer Security Foundations (CSF-22)","author":"C. Cachin","year":"2009","unstructured":"Cachin, C., Chandran, N.: A secure cryptographic token interface. In: Computer Security Foundations (CSF-22), pp. 141\u2013153. IEEE Computer Society Press, Long Island (2009)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-04444-1_4","volume-title":"Computer Security \u2013 ESORICS 2009","author":"M. Centenaro","year":"2009","unstructured":"Centenaro, M., Focardi, R., Luccio, F.L., Steel, G.: Type-based analysis of PIN processing APIs. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol.\u00a05789, pp. 53\u201368. Springer, Heidelberg (2009)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/3-540-36400-5_42","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2002","author":"R. Clayton","year":"2003","unstructured":"Clayton, R., Bond, M.: Experience using a low-cost FPGA design to crack DES keys. In: Kaliski Jr., B.S., Ko\u00e7, \u00c7.K., Paar, C. (eds.) CHES 2002. LNCS, vol.\u00a02523, pp. 579\u2013592. Springer, Heidelberg (2003)"},{"key":"2_CR22","unstructured":"Clulow, J.: The design and analysis of cryptographic APIs for security devices. Master\u2019s thesis, University of Natal, Durban (2003)"},{"key":"2_CR23","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.\u00a02779, pp. 411\u2013425. Springer, Heidelberg (2003)"},{"key":"2_CR24","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":"2_CR25","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1109\/CSF.2008.16","volume-title":"Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008)","author":"S. Delaune","year":"2008","unstructured":"Delaune, S., Kremer, S., Steel, G.: Formal analysis of PKCS#11. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 331\u2013344. IEEE Computer Society Press, Pittsburgh (2008)"},{"issue":"6","key":"2_CR26","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.3233\/JCS-2009-0394","volume":"18","author":"S. Delaune","year":"2010","unstructured":"Delaune, S., Kremer, S., Steel, G.: Formal analysis of PKCS#11 and proprietary extensions. Journal of Computer Security\u00a018(6), 1211\u20131245 (2010)","journal-title":"Journal of Computer Security"},{"issue":"29","key":"2_CR27","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"2","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions in Information Theory\u00a02(29), 198\u2013208 (1983)","journal-title":"IEEE Transactions in Information Theory"},{"issue":"4","key":"2_CR28","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1145\/363516.363532","volume":"9","author":"A. Durante","year":"2000","unstructured":"Durante, A., Focardi, R., Gorrieri, R.: A compiler for analyzing cryptographic protocols using noninterference. ACM Transactions on Software Engineering and Methodology\u00a09(4), 488\u2013528 (2000)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"2","key":"2_CR29","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"N.A. Durgin","year":"2004","unstructured":"Durgin, N.A., Lincoln, P., Mitchell, J.C.: Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security\u00a012(2), 247\u2013311 (2004)","journal-title":"Journal of Computer Security"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-16074-5_7","volume-title":"Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security","author":"R. Focardi","year":"2010","unstructured":"Focardi, R., Luccio, F.L.: Secure upgrade of hardware security modules in bank networks. In: Armando, A., Lowe, G. (eds.) ARSPA-WITS 2010. LNCS, vol.\u00a06186, pp. 95\u2013110. Springer, Heidelberg (2010)"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Focardi, R., Luccio, F.L.: Guessing bank pins by winning a mastermind game. Theory of Computing Systems (to appear, 2011)","DOI":"10.1007\/s00224-011-9340-9"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-04766-4_7","volume-title":"Identity and Privacy in the Internet Age","author":"R. Focardi","year":"2009","unstructured":"Focardi, R., Luccio, F.L., Steel, G.: Blunting differential attacks on PIN processing APIs. In: J\u00f8sang, A., Maseng, T., Knapskog, S.J. (eds.) NordSec 2009. LNCS, vol.\u00a05838, pp. 88\u2013103. Springer, Heidelberg (2009)"},{"key":"2_CR33","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.\u00a05511, pp. 92\u2013106. Springer, Heidelberg (2009)"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"issue":"4","key":"2_CR35","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/MSP.2006.85","volume":"4","author":"J. Herzog","year":"2006","unstructured":"Herzog, J.: Applying protocol analysis to security device interfaces. IEEE Security & Privacy Magazine\u00a04(4), 84\u201387 (2006)","journal-title":"IEEE Security & Privacy Magazine"},{"key":"2_CR36","unstructured":"IEEE 1619.3 Technical Committee. IEEE storage standard 1619.3 (key management) (draft), https:\/\/siswg.net\/"},{"key":"2_CR37","unstructured":"International Organization\u00a0for Standardization. ISO 9564-1: Banking personal identification number (PIN) management and security, 30 pages"},{"key":"2_CR38","unstructured":"Keighren, G.: Model checking security APIs. Master\u2019s thesis, University of Edinburgh (2007)"},{"key":"2_CR39","first-page":"1","volume":"9","author":"D. Knuth","year":"1976","unstructured":"Knuth, D.: The Computer as a Master Mind. Journal of Recreational Mathematics\u00a09, 1\u20136 (1976)","journal-title":"Journal of Recreational Mathematics"},{"key":"2_CR40","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1109\/CSF.2011.25","volume-title":"Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF 2011)","author":"S. Kremer","year":"2011","unstructured":"Kremer, S., Steel, G., Warinschi, B.: Security for key management interfaces. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF 2011), Cernay-la-Ville, France, pp. 266\u2013280. IEEE Computer Society Press, Los Alamitos (2011)"},{"issue":"1","key":"2_CR41","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 and Security\u00a011(1), 75\u201389 (1992)","journal-title":"Computers and Security"},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"2","key":"2_CR43","doi-asserted-by":"publisher","first-page":"157","DOI":"10.3233\/JCS-2006-14203","volume":"14","author":"A.C. Myers","year":"2006","unstructured":"Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification and qualified robustness. Journal of Computer Security\u00a014(2), 157\u2013196 (2006)","journal-title":"Journal of Computer Security"},{"key":"2_CR44","unstructured":"OASIS Key Management Interoperability Protocol (KMIP) Technical Committee. KMIP \u2013 key management interoperability protocol (February 2009), http:\/\/xml.coverpages.org\/KMIP\/"},{"key":"2_CR45","unstructured":"openCryptoki, http:\/\/sourceforge.net\/projects\/opencryptoki\/"},{"key":"2_CR46","unstructured":"Pickover, C.A.: The Math Book: From Pythagoras to the 57th Dimension, 250 Milestones in the History of Mathematics. Sterling (2009)"},{"key":"2_CR47","unstructured":"RSA Security Inc., v2.20. PKCS #11: Cryptographic Token Interface Standard (June 2004)"},{"key":"2_CR48","volume-title":"Applied Cryptography","author":"B. Schneier","year":"1996","unstructured":"Schneier, B.: Applied Cryptography, 2nd edn. John Wiley and Sons, Chichester (1996)","edition":"2"},{"issue":"1-2","key":"2_CR49","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.tcs.2006.08.042","volume":"367","author":"G. Steel","year":"2006","unstructured":"Steel, G.: Formal Analysis of PIN Block Attacks. Theoretical Computer Science\u00a0367(1-2), 257\u2013270 (2006)","journal-title":"Theoretical Computer Science"},{"key":"2_CR50","first-page":"25","volume":"5","author":"J. Stuckman","year":"2006","unstructured":"Stuckman, J., Zhang, G.: Mastermind is NP-Complete. INFOCOMP Journal of Computer Science\u00a05, 25\u201328 (2006)","journal-title":"INFOCOMP Journal of Computer Science"},{"key":"2_CR51","unstructured":"Tsalapati, E.: Analysis of PKCS#11 using AVISPA tools. Master\u2019s thesis, University of Edinburgh (2007)"},{"key":"2_CR52","unstructured":"Youn, P., Adida, B., Bond, M., Clulow, J., Herzog, J., Lin, A., Rivest, R., Anderson, R.: Robbing the bank with a theorem prover. Technical Report UCAM-CL-TR-644, University of Cambridge (August 2005)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design VI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23082-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T18:47:53Z","timestamp":1560451673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23082-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642230813","9783642230820"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23082-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}