Abstract
PKCS#11, is a security API for cryptographic tokens. It is known to be vulnerable to attacks which can directly extract, as cleartext, the value of sensitive keys. In particular, the API does not impose any limitation on the different roles a key can assume, and it permits to perform conflicting operations such as asking the token to wrap a key with another one and then to decrypt it. Fixes proposed in the literature, or implemented in real devices, impose policies restricting key roles and token functionalities. In this paper we define a simple imperative programming language, suitable to code PKCS#11 symmetric key management, and we develop a type-based analysis to prove that the secrecy of sensitive keys is preserved under a certain policy. We formally analyse existing fixes for PKCS#11 and we propose a new one, which is type-checkable and prevents conflicting roles by deriving different keys for different roles.
Work partially supported by the RAS Project “TESLA: Techniques for Enforcing Security in Languages and Applications”.
Chapter PDF
Similar content being viewed by others
Keywords
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
Anderson, R.: The Correctness of Crypto Transaction Sets. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2000. LNCS, vol. 2133, pp. 125–127. Springer, Heidelberg (2001), http://www.cl.cam.ac.uk/ftp/users/rja14/protocols00.pdf
Bond, M.: Attacks on Cryptoprocessor Transaction Sets. In: Koç, Ç.K., Naccache, D., Paar, C. (eds.) CHES 2001. LNCS, vol. 2162, pp. 220–234. Springer, Heidelberg (2001)
Bond, M., Anderson, R.: API level attacks on embedded systems. IEEE Computer Magazine 34(10), 67–75 (2001)
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), pp. 260–269. ACM (2010)
Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: CryptokiX: a cryptographic software token with security fixes. In: Proceedings of the 4th International Workshop on Analysis of Security APIs (ASA), Edinburgh, UK (July 2010)
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. 5789, pp. 53–68. Springer, Heidelberg (2009)
Clayton, R., Bond, M.: Experience Using a Low-Cost FPGA Design to Crack DES Keys. In: Kaliski Jr., B.S., Koç, Ç.K., Paar, C. (eds.) CHES 2002. LNCS, vol. 2523, pp. 579–592. Springer, Heidelberg (2003)
Clulow, J.: On the Security of PKCS #11. In: Walter, C.D., Koç, Ç.K., Paar, C. (eds.) CHES 2003. LNCS, vol. 2779, pp. 411–425. Springer, Heidelberg (2003)
Delaune, S., Kremer, S., Steel, G.: Formal analysis of PKCS#11. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), Pittsburgh, PA, USA, pp. 331–344. IEEE Computer Society Press (June 2008)
Delaune, S., Kremer, S., Steel, G.: Formal analysis of PKCS#11 and proprietary extensions. Journal of Computer Security 18(6), 1211–1245 (2010)
Focardi, R., Luccio, F.L.: Secure Recharge of Disposable RFID Tickets. In: Barthe, G. (ed.) FAST 2011. LNCS, vol. 7140, pp. 85–99. Springer, Heidelberg (2012)
Fröschle, S.B., Sommer, N.: Reasoning with Past to Prove PKCS#11 Keys Secure. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 96–110. Springer, Heidelberg (2011)
Fröschle, S., Sommer, N.: Concepts and Proofs for Configuring PKCS#11. In: Barthe, G. (ed.) FAST 2011. LNCS, vol. 7140, pp. 131–147. Springer, Heidelberg (2012)
Fröschle, S.B., Steel, G.: Analysing PKCS#11 Key Management APIs with Unbounded Fresh Data. In: Degano, P., Viganò, L. (eds.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 92–106. Springer, Heidelberg (2009)
Keighren, G., Aspinall, D., Steel, G.: Towards a Type System for Security APIs. In: Degano, P., Viganò, L. (eds.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 173–192. Springer, Heidelberg (2009)
Longley, D., Rigby, S.: An automatic search for security flaws in key management schemes. Computers and Security 11(1), 75–89 (1992)
openCryptoki, http://sourceforge.net/projects/opencryptoki/
RSA Security Inc., v2.20. PKCS #11: Cryptographic Token Interface Standard (June 2004)
RSA Security Inc., Draft v2.30. PKCS #11: Cryptographic Token Interface Standard (July 2009), http://www.rsa.com/rsalabs/node.asp?id=2133
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Centenaro, M., Focardi, R., Luccio, F.L. (2012). Type-Based Analysis of PKCS#11 Key Management. In: Degano, P., Guttman, J.D. (eds) Principles of Security and Trust. POST 2012. Lecture Notes in Computer Science, vol 7215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28641-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-28641-4_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28640-7
Online ISBN: 978-3-642-28641-4
eBook Packages: Computer ScienceComputer Science (R0)