Steve Kremer: A Formal Analysis of Authentication in the TPM

A Formal Analysis of Authentication in the TPM

Stéphanie Delaune, Steve Kremer, Mark D. Ryan, and Graham Steel. A Formal Analysis of Authentication in the TPM. In Revised Selected Papers of the 7th International Workshop on Formal Aspects in Security and Trust (FAST'10), pp. 111–125, Lecture Notes in Computer Science 6561, Springer, Pisa, Italy, September 2010.
doi:10.1007/978-3-642-19751-2_8

Download

[PDF] [PS] [HTML]

Abstract

The Trusted Platform Module (TPM) is a hardware chip designed to enable computers to achieve a greater level of security than is possible in software alone. To this end, the TPM provides a way to store cryptographic keys and other sensitive data in its shielded memory. Through its API, one can use those keys to achieve some security goals. The TPM is a complex security component, whose specification consists of more than \(700\) pages.
We model a collection of four TPM commands, and we identify and formalise their security properties. Using the tool ProVerif, we rediscover some known attacks and some new variations on them. We propose modifications to the API and verify our properties for the modified API.

BibTeX

@inproceedings{DKRS-fast10,
  abstract =      {The Trusted Platform Module~(TPM) is a hardware chip
                   designed to enable computers to achieve a greater
                   level of security than is possible in software alone.
                   To this end, the TPM provides a way to store
                   cryptographic keys and other sensitive data in its
                   shielded memory. Through its API, one can use those
                   keys to achieve some security goals. The TPM is a
                   complex security component, whose specification
                   consists of more than \(700\)~pages.\par We model a
                   collection of four TPM commands, and we identify and
                   formalise their security properties. Using the tool
                   ProVerif, we rediscover some known attacks and some
                   new variations on them. We propose modifications to
                   the API and verify our properties for the modified
                   API.},
  address =       {Pisa, Italy},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve and
                   Ryan, Mark D. and Steel, Graham},
  booktitle =     {{R}evised {S}elected {P}apers of the 7th
                   {I}nternational {W}orkshop on {F}ormal {A}spects in
                   {S}ecurity and {T}rust ({FAST}'10)},
  DOI =           {10.1007/978-3-642-19751-2_8},
  editor =        {Degano, Pierpaolo and Etalle, Sandro and
                   Guttman, Joshua},
  month =         sep,
  pages =         {111-125},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {A~Formal Analysis of Authentication in the {TPM}},
  volume =        {6561},
  year =          {2010},
  acronym =       {{FAST}'10},
  nmonth =        {9},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-fast10.pdf},
}