Abstract
We examine some known attacks on the PIN verification framework, based on weaknesses of the security API for the tamper-resistant Hardware Security Modules used in the network. We specify this API in an imperative language with cryptographic primitives, and show how its flaws are captured by a notion of robustness that extends the one of Myers, Sabelfeld and Zdancewic to our cryptographic setting. We propose an improved API, give an extended type system for assuring integrity and for preserving confidentiality via randomized and non-randomized encryptions, and show our new API to be type-checkable.
Work partially supported by Miur’07 Project SOFT.
Chapter PDF
Similar content being viewed by others
Keywords
- Message Authentication Code
- Integrity Level
- Typing Rule
- Integrity Representative
- Cryptographic Primitive
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Hackers crack cash machine PIN codes to steal millions, http://www.timesonline.co.uk/tol/money/consumer_affairs/article4259009.ece
PIN Crackers Nab Holy Grail of Bank Card Security. Wired Magazine Blog ’Threat Level’, http://blog.wired.com/27bstroke6/2009/04/pins.html
Abadi, M.: Secrecy by typing in security protocols. JACM 46(5), 749–786 (1999)
Abadi, M., Jurjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 82–94. Springer, Heidelberg (2001)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). JCRYPTOL 15(2), 103–127 (2002)
Adão, P., Bana, G., Herzog, J., Scedrov, A.: Soundness of formal encryption in the presence of key-cycles. In: de Capitani di Vimercati, S., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 374–396. Springer, Heidelberg (2005)
Askarov, A., Hedin, D., Sabelfeld, A.: Cryptographically-masked flows. Theoretical Computer Science 402(2-3), 82–101 (2008)
Berkman, O., Ostrovsky, O.: The unbearable lightness of PIN cracking. In: Dietrich, S., Dhamija, R. (eds.) FC 2007 and USEC 2007. LNCS, vol. 4886, pp. 224–238. Springer, Heidelberg (2007)
Bond, M., Zielinski, P.: Decimalization table attacks for PIN cracking. Technical Report UCAM-CL-TR-560, University of Cambridge, Computer Laboratory (2003)
Clulow, J.: The design and analysis of cryptographic APIs for security devices. Master’s thesis, University of Natal, Durban (2003)
Courant, J., Ene, C., Lakhnech, Y.: Computationally sound typing for non-interference: The case of deterministic encryption. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 364–375. Springer, Heidelberg (2007)
Delaune, S., Kremer, S., Steel, G.: Formal analysis of PKCS#11. In: IEEE Computer Security Foundations Symposium, June 23-25 2008, pp. 331–344 (2008)
Focardi, R., Centenaro, M.: Information flow security of multi-threaded distributed programs. In: ACM SIGPLAN PLAS 2008, June 8, 2008, pp. 113–124 (2008)
Focardi, R., Centenaro, M., Luccio, F., Steel, G.: Type-based analysis of PIN processing APIs (full version). Technical Report CS-2009-6, Università Ca’ Foscari, Venezia, Italy (2009), http://www.unive.it/nqcontent.cfm?a_id=5144
Focardi, R., Luccio, F.L., Steel, G.: Improving pin processing api security. In: Workshop on Analysis of Security APIs, July 10-11 (to appear, 2009)
Fournet, C., Rezk, T.: Cryptographically sound implementations for typed information-flow security. In: POPL 2008, pp. 323–335. ACM Press, New York (2008)
Gordon, A., Jeffrey, A.: Authenticity by typing for security protocols. Technical Report MSR-2001-49, Microsoft Research (2001)
I. Inc. CCA Basic Services Reference and Guide for the IBM 4758 PCI and IBM 4764 PCI-X Cryptographic Coprocessors. Technical report, 2006. Rel. 2.53–3.27 (2006)
Keighren, G., Aspinall, A., Steel, G.: Towards a type system for security APIs. In: ARSPA-WITS 2009, York, UK, March 28-29, 2009, pp. 173–192 (2009)
Laud, P.: On the computational soundness of cryptographically masked flows. In: POPL 2008, pp. 337–348. ACM Press, New York (2008)
Longley, D., Rigby, S.: An automatic search for security flaws in key management schemes. Computers and Security 11(1), 75–89 (1992)
Mannan, M., van Oorschot, P.: Reducing threats from flawed security APIs: The banking PIN case. Computers & Security 28(6), 410–420 (2009)
Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification and qualified robustness. Journal of Computer Security 14(2), 157–196 (2006)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. Journal of Computer Security (to appear)
Steel, G.: Formal Analysis of PIN Block Attacks. TCS 367(1-2), 257–270 (2006)
Vaughan, J.A., Zdancewic, S.: A cryptographic decentralized label model. In: IEEE Symposium on Security and Privacy, pp. 192–206. IEEE Computer Society, Los Alamitos (2007)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(2/3), 167–187 (1996)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Centenaro, M., Focardi, R., Luccio, F.L., Steel, G. (2009). Type-Based Analysis of PIN Processing APIs. In: Backes, M., Ning, P. (eds) Computer Security – ESORICS 2009. ESORICS 2009. Lecture Notes in Computer Science, vol 5789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04444-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-04444-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04443-4
Online ISBN: 978-3-642-04444-1
eBook Packages: Computer ScienceComputer Science (R0)