Stéphanie Delaune, Steve Kremer, and Graham Steel. Formal Analysis of PKCS#11. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), pp. 331–344, IEEE Computer Society Press, Pittsburgh, Pennsylvania, USA, June 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-csf08,
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 = {Pittsburgh, Pennsylvania, USA},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Steel, Graham},
booktitle = {{P}roceedings of the 21st {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'08)},
OPTDOI = {10.1109/CSF.2008.16},
month = jun,
pages = {331-344},
publisher = {{IEEE} Computer Society Press},
title = {Formal Analysis of {PKCS}\#11},
year = {2008},
acceptrate = {21/115},
acronym = {{CSF}'08},
nmonth = {6},
OPTLONGPDF = {https://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
rr-lsv-2008-04.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}