Formal Analysis of PKCS#11
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, PA, USA, June 2008.
doi:10.1109/CSF.2008.16
Download
[PDF] [PDF (long version)] [PS (long version)] [HTML]
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.
BibTeX
@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, PA, 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)},
DOI = {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},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-csf08.pdf},
}