Analysing PKCS\11 Key Management APIs with Unbounded Fresh Data (bibtex)
by Sibylle Fröschle, Graham Steel
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 (Sibylle Fröschle, Graham Steel), 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) (Pierpaolo Degano, Luca Viganò, 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},
}
Powered by bibtexbrowser