Stéphanie Delaune, Steve Kremer, and Graham Steel. Formal Analysis of PKCS#11. In Proceedings of the 4th Taiwanese-French Conference on Information Technology (TFIT'08), pp. 267–278, Taipei, Taiwan, March 2008.
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.
@inproceedings{DKS-TFIT2008,
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.},
address = {Taipei, Taiwan},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Steel, Graham},
booktitle = {{P}roceedings of the 4th {T}aiwanese-{F}rench
{C}onference on {I}nformation {T}echnology
({TFIT}'08)},
editor = {Kuo, Tei-Wei and Cruz-Lara, Samuel},
month = mar,
pages = {267-278},
title = {Formal Analysis of {PKCS}\#11},
year = {2008},
acronym = {{TFIT}'08},
nmonth = {3},
lsv-category = {auti},
wwwpublic = {labo and ccsb},
}