Abstract
PKCS#11 is a widely adopted standard that defines a security API for accessing devices such as smartcards and hardware security modules. Motivated by experiments on several devices we develop an approach that allows us to formally establish security properties of keys stored on such devices. We use first-order linear time logic extended by past operators. The expressiveness of a first-order language allows us to model the security API and its features close to how it is specified while the past operators enable proof by backwards analysis. We apply this approach to prove that keys that initially have the attribute extractable set to false are secure.
This work is partially supported by DFG SFB/TR14 AVACS and the BMBF/DAAD project 50725248.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Borgström, J.: Monotonicity for multiple key managment tokens (2009); presentation at ASA 2009
Castellini, C.: Automated Reasoning in Quantified Modal and Temporal Logic. Ph.D. thesis, University of Edinburgh (2004)
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)
D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J.: Handbook of Tableau Methods. Kluwer Academic Publishers, Dordrecht (1999)
Delaune, S., Kremer, S., Steel, G.: Formal analysis of PKCS#11. In: CSF 2008, pp. 331–344. IEEE Computer Society Press, Los Alamitos (2008)
Fröschle, S., 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)
Gabbay, D.M.: Labelled Deductive Systems, vol. 1. Oxford Science Publications (1996)
Kröger, F., Merz, S.: Temporal Logic and State Systems. Springer, Heidelberg (2008)
RSA Laboratories: PKCS#11: Cryptographic Token Interface Standard, vol. v2.30, Draft 4. RSA Security Inc. (July 2009)
Thayer, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: IEEE Symposium on Security and Privacy, pp. 160–171 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fröschle, S., Sommer, N. (2011). Reasoning with Past to Prove PKCS#11 Keys Secure. In: Degano, P., Etalle, S., Guttman, J. (eds) Formal Aspects of Security and Trust. FAST 2010. Lecture Notes in Computer Science, vol 6561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19751-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-19751-2_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19750-5
Online ISBN: 978-3-642-19751-2
eBook Packages: Computer ScienceComputer Science (R0)