Abstract
Key management is the Achilles heel of cryptography. In recent years, several attacks have been identified due to poor key management or too liberal APIs, which do not provide a policy that precisely determines the intended use of cryptographic keys. In this paper, we have taken advantage of the expressiveness and simplicity of strand spaces, first introduced in 1998 by Joshua Guttman et al., to specify a significant subset of key management APIs. We used the automatic CPSA tool to rediscover, in an extremely clear and effective way, some known attacks. We have therefore defined a generic key management policy model and proved a key secrecy theorem for a typed version of the API. The proof highlighted the necessary requirements of the policy that we formalized through a closure property that, in fact, computes which types a key can take at runtime.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
CPSA: A cryptographicprotocol shapes analyzer. In: Hackage. The MITRE Corporation (2009). http://hackage.haskell.org/package/cpsa
Completeness of CPSA: The MITRE Corporation (2011). https://www.mitre.org/sites/default/files/pdf/12_0038.pdf
Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: ProVerif 2.02pl1: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial (2020). https://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf
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–269. ACM Press, October 2010. https://doi.org/10.1145/1866307.1866337
Caleiro, C., Viganó, L., Basin, D.: Relating strand spaces and distributed temporal logic for security protocol analysis. Logic J. IGPL 13, 637–663 (2005)
Centenaro, M., Focardi, R., Luccio, F.: Type-based analysis of key management in PKCS#11 cryptographic devices. J. Comput. Secur. 21(6), 971–1007 (2013)
Centenaro, M., Focardi, R., Luccio, F., Steel, G.: Type-based analysis of PIN processing APIs. In: Springer (ed.) Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS 09), vol. 5789, pp. 53–68 (2009). https://doi.org/10.1007/978-3-642-04444-1_4
Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: A comparison between strand spaces and multiset rewriting for security protocol analysis. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 356–383. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36532-X_22
Clulow, J.: The Design and Analysis of Cryptographic APIs for Security Devices. Master’s thesis, University of Natal, Durban (2003)
Clulow, J.: On the security of PKCS#11. In: Proceedings of the 5th Int. Workshop on Cryptographic Hardware and Embedded Systems (CHES 2003). LNCS, vol. 2779, pp. 411–425. Springer (2003). https://doi.org/10.1007/978-3-540-45238-6_32
Dax, A., Künnemann, R., Tangermann, S., Backes, M.: How to wrap it up - a formally verified proposal for the use of authenticated wrapping in PKCS#11. In: 2019 IEEE 32nd Computer Security Foundations Symposium (CSF 2019), pp. 62–6215 (2019). https://doi.org/10.1109/CSF.2019.00012
Delaune, S., Kremer, S., Steel, G.: Formal analysis of PKCS#11 and proprietary extensions. J. Comput. Secur. 18(6), 1211–1245 (2010). https://doi.org/10.3233/JCS-2009-0394
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29, 198–208 (1983)
Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, pp. 1–50. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03829-7_1
Fabrega, F., Herzog, J., Guttman, J.: Strand spaces: why is a security protocol correct? In: Proceedings. 1998 IEEE Symposium on Security and Privacy, pp. 160–171 (1998). https://doi.org/10.1109/SECPRI.1998.674832
Focardi, R., Luccio, F.L.: A formally verified configuration for hardware security modules in the cloud. In: Vigna, G., Shi, E. (eds.) The ACM Conference on Computer and Communications Security (CCS), 2021. ACM (2021). (to appear)
Focardi, R., Luccio, F.L., Steel, G.: An introduction to security API analysis. In: Foundations of Security Analysis and Design VI - FOSAD Tutorial Lectures, pp. 35–65 (2011)
Fröschle, S., Sommer, N.: Concepts and proofs for configuring PKCS#11. In: Formal Aspects of Security and Trust - 8th International Workshop, (FAST 2011), Revised Selected Papers. LNCS, vol. 7140, pp. 131–147. Springer (2011). https://doi.org/10.1007/978-3-642-29420-4_9
González-Burgueño, A., Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: Analysis of the PKCS#11 API using the Maude-NPA tool. In: Chen, L., Matsuo, S. (eds.) SSR 2015. LNCS, vol. 9497, pp. 86–106. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27152-1_5
Guttman, J.: State and progress in strand spaces: proving fair exchange. J. Autom. Reasoning 48, 159–195 (2012)
Halpern, Y., Pucella, J.R.: On the relationship between strand spaces and multi-agent systems. ACM Trans. Inf. Syst. Secur. 61, 43–70 (2003)
Kamil, A., Lowe, G.: Understanding abstractions of secure channels. In: Degano, P., Etalle, S., Guttman, J.D. (eds.) Formal Aspects of Security and Trust - 7th International Workshop, FAST 2010. Revised Selected Papers. Lecture Notes in Computer Science, vol. 6561, pp. 50–64. Springer (2010). https://doi.org/10.1007/978-3-642-19751-2_4
Künnemann, R.: Automated backward analysis of PKCS#11 v2.20. In: Principles of Security and Trust - 4th International Conference (POST 2015). LNCS, vol. 9036, pp. 219–238. Springer (2015). https://doi.org/10.1007/978-3-662-46666-7_12
Lanus, E., Zieglar, E.: Analysis of a forced-latency defense against man-in-the-middle attacks. J. Inf. Warfare 16(2), 66–78 (2017)
Liskov, M., Ramsdell, J., Guttman, J., Rowe, P.: The Cryptographic Protocol Shapes Analyzer: A Manual. The MITRE Corporation. CPSA Version 3. Available at https://hackage.haskell.org/package/cpsa-3.3.2/src/doc/cpsamanual.pdf (2016)
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–701. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_48
OASIS: PKCS #11 Cryptographic Token Interface Base Specification Version 3.0, June 2020. Accessed May 2021. https://docs.oasis-open.org/pkcs11/pkcs11-base/v3.0/pkcs11-base-v3.0.html
Ramsdell, J., Guttman, J.D., Millen, J.K., O’Hanlon, B.: An Analysis of the CAVES Attestation Protocol using CPSA. eprint arXiv:1207.0418 (2012). https://arxiv.org/abs/1207.0418
Ramsdell, J.D., Dougherty, D.J., Guttman, J.D., Rowe, P.D.: A hybrid analysis for security protocols with state. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 272–287. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10181-1_17
Sherman, A., et al.: Formal methods analysis of the secure remote password protocol. In: Logic, Language, and Security, vol. 12300. Springer (2020). https://doi.org/10.1007/978-3-030-62077-6_9
Stanley-Oakes, R.: A provably secure PKCS#11 configuration without authenticated attributes. In: Financial Cryptography and Data Security, pp. 145–162. Springer International Publishing (2017). https://doi.org/10.1007/978-3-319-70972-7_8
Steel, G.: Proposal: Authenticated Attributes for Key Wrap in PKCS#11 (2014). https://lists.oasis-open.org/archives/pkcs11/201408/msg00006/pkcs11-authenticated-encryption-key-transport.pdf
Yang, F., Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Strand spaces with choice via a process algebra semantics. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016, pp. 76–89. ACM (2016). https://doi.org/10.1145/2967973.2968609
Acknowledgments
We would like to thank the anonymous reviewers for their very interesting and insightful comments. This work has been partially supported by the European Regional Development Fund project SAFE PLACE: Sistemi IoT per ambienti di vita salubri e sicuri (POR FESR 2014–2020 AZIONE 1.1.4 DGR 822/2020—ID 10288513).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Focardi, R., Luccio, F.L. (2021). Secure Key Management Policies in Strand Spaces. In: Dougherty, D., Meseguer, J., Mödersheim, S.A., Rowe, P. (eds) Protocols, Strands, and Logic. Lecture Notes in Computer Science(), vol 13066. Springer, Cham. https://doi.org/10.1007/978-3-030-91631-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-91631-2_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-91630-5
Online ISBN: 978-3-030-91631-2
eBook Packages: Computer ScienceComputer Science (R0)