Formal security analysis of PKCS#11 and proprietary extensions

Issue title: 21st IEEE Computer Security Foundations Symposium (CSF'08)

Guest editors: Andrei SabelfeldGuest Editor

Article type: Research Article

Authors: Delaune, Stéphanie | Kremer, Steve | Steel, Graham^{; *}

Affiliations: LSV, ENS Cachan & CNRS & INRIA, France

Correspondence: [*] Corresponding author: Graham Steel, 61, avenue du Président Wilson, 94235 Cachan Cedex, France. Tel.: +33 1 47 40 77 80; Fax: +33 1 47 40 75 21; E-mail: [email protected].

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 the model checker NuSMV. We report some new attacks and prove the safety of some configurations of the API in our model. We also analyse proprietary extensions proposed by nCipher (Thales) and Eracom (Safenet), designed to address the shortcomings of PKCS#11.

Keywords: Security APIs, PKCS#11, cryptographic devices, decidability, model checking

DOI: 10.3233/JCS-2009-0394

Journal: Journal of Computer Security, vol. 18, no. 6, pp. 1211-1245, 2010