by Fröschle, Sibylle and Steel, Graham
Abstract:
We extend Delaune, Kremer and Steel's framework for analysis of PKCS11-based APIs from bounded to unbounded fresh data. We achieve this by: formally defining the notion of an \emphattribute policy; showing that a well-designed API should have a certain class of policy we call \emphcomplete; showing that APIs with complete policies may be safely abstracted to APIs where the attributes are fixed; and proving that these \emphstatic APIs can be analysed in a small bounded model such that security properties will hold for the unbounded case. We automate analysis in our framework using the SAT-based security protocol model checker SATMC. We show that a symmetric key management subset of the Eracom PKCS11 API, used in their ProtectServer product, preserves the secrecy of sensitive keys for unbounded numbers of fresh keys and \emphhandles, i.e. pointers to keys. We also show that this API is not robust: if an encryption key is lost to the intruder, SATMC finds an attack whereby all the keys may be compromised.
Reference:
Analysing PKCS\#11 Key Management APIs with Unbounded Fresh Data (Fröschle, Sibylle and Steel, Graham), In Revised Selected Papers of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09) (Degano, Pierpaolo, Viganò, Luca, eds.), Springer, volume 5511, 2009.
Bibtex Entry:
@inproceedings{FS-arspawits09,
abstract = {We extend Delaune, Kremer and Steel's framework for
analysis of PKCS#11-based APIs from bounded to
unbounded fresh data. We achieve this by: formally
defining the notion of an \emph{attribute policy};
showing that a well-designed API should have a
certain class of policy we call \emph{complete};
showing that APIs with complete policies may be
safely abstracted to APIs where the attributes are
fixed; and proving that these \emph{static} APIs can
be analysed in a small bounded model such that
security properties will hold for the unbounded case.
We automate analysis in our framework using the
SAT-based security protocol model checker SATMC. We
show that a symmetric key management subset of the
Eracom PKCS#11 API, used in their ProtectServer
product, preserves the secrecy of sensitive keys for
unbounded numbers of fresh keys and \emph{handles},
i.e.~pointers to keys. We also show that this API is
not robust: if~an encryption key is lost to the
intruder, SATMC finds an attack whereby all the keys
may be compromised.},
address = {York, UK},
author = {Fr{\"o}schle, Sibylle and Steel, Graham},
booktitle = {{R}evised {S}elected {P}apers of the {J}oint
{W}orkshop on {A}utomated {R}easoning for {S}ecurity
{P}rotocol {A}nalysis and {I}ssues in the {T}heory of
{S}ecurity ({ARSPA-WITS}'09)},
DOI = {10.1007/978-3-642-03459-6_7},
editor = {Degano, Pierpaolo and Vigan{\`o}, Luca},
month = aug,
pages = {92-106},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Analysing {PKCS}\#11 Key Management {API}s with
Unbounded Fresh Data},
volume = {5511},
year = {2009},
acronym = {{ARSPA-WITS}'09},
nmonth = {8},
conf-year = {2009},
conf-month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf},
PDF = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}