Formal Analysis of PKCS\11 (bibtex)
by Stéphanie Delaune, Steve Kremer, Graham Steel
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.
Reference:
Formal Analysis of PKCS\11 (Stéphanie Delaune, Steve Kremer, Graham Steel), In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), IEEE Computer Society Press, 2008.
Bibtex Entry:
@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},
  PDF =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-csf08.pdf},
  LONGPDF =       {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-04.pdf},
  LONGPS =        {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2008-04.ps},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}
Powered by bibtexbrowser