Formal Analysis of PKCS#11
- 1 January 2008
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 331-344
- https://doi.org/10.1109/csf.2008.16
Abstract
PKCS#11 defines an API for cryptographic devices that has been widely adopted in industry. However, it has been shown to be vulnerable to a variety of attacks that could, for example, compromise the sensitive keys stored on the device. In this paper, we set out a formal model of the operation of the API, which differs from previous security API models notably in that it accounts for non-monotonic mutable global state. We give decidability results for our formalism, and describe an implementation of the resulting decision procedure using a model checker. We report some new attacks and prove the safety of some configurations of the API in our model.Keywords
This publication has 11 references indexed in Scilit:
- Robbing the Bank with a Theorem ProverLecture Notes in Computer Science, 2010
- Automatic Analysis of the Security of XOR-Based Key Management SchemesPublished by Springer Science and Business Media LLC ,2007
- A Formal Theory of Key Conjuring20th IEEE Computer Security Foundations Symposium (CSF'07), 2007
- Applying protocol analysis to security device interfacesIEEE Security & Privacy, 2006
- Deduction with XOR Constraints in Security API ModellingLecture Notes in Computer Science, 2005
- Multiset rewriting and the complexity of bounded security protocolsJournal of Computer Security, 2004
- Multiset Rewriting and Security Protocol AnalysisLecture Notes in Computer Science, 2002
- API-level attacks on embedded systemsComputer, 2001
- An automatic search for security flaws in key management schemesComputers & Security, 1992
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983