2008 · 48 citations · 10 references
ComputingComputer ScienceCybersecurityComputer SecurityCryptographyFormal MethodsApi SecurityDeductive VerificationProtocol AnalysisProtocol VerificationSecure Key StorageSecurity Protocol VerificationDecidabilityDecidability ProblemsFormal Methods For Security ProtocolsFormal Security AnalysisFormal Verification Of Cryptographic ProtocolsFormal Verification Tools For Cryptographic ProtocolsModel Checking Of Security ProtocolsSecure Interface Verification
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.
10
On the security of public key protocols
Danny Dolev, A. Yao · IEEE Transactions on Information Theory · 1983 · 5.7K citations
Multiset rewriting and the complexity of bounded security protocols
Nancy Durgin, Patrick Lincoln, John C. Mitchell et al. · Journal of Computer Security · 2004 · 166 citations
API-level attacks on embedded systems
Mike Bond, Ross Anderson · Computer · 2001 · 109 citations