Steve Kremer: Formal Analysis of PKCS#11

Formal Analysis of PKCS#11

Stéphanie Delaune, Steve Kremer, and Graham Steel. Formal Analysis of PKCS#11. In Proceedings of the 4th Taiwanese-French Conference on Information Technology (TFIT'08), pp. 267–278, Taipei, Taiwan, March 2008. Invited talk.

Download

[PDF]

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-TFIT2008,
  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 =       {Taipei, Taiwan},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve and
                   Steel, Graham},
  booktitle =     {{P}roceedings of the 4th {T}aiwanese-{F}rench
                   {C}onference on {I}nformation {T}echnology
                   ({TFIT}'08)},
  editor =        {Kuo, Tei-Wei and Cruz-Lara, Samuel},
  month =         mar,
  pages =         {267-278},
  title =         {Formal Analysis of {PKCS}\#11},
  year =          {2008},
  acronym =       {{TFIT}'08},
  nmonth =        {3},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-tfit08.pdf},
  note =          {Invited talk},
}