Steve Kremer: Formal analysis of protocols based on TPM state registers

Formal analysis of protocols based on TPM state registers

Stéphanie Delaune, Steve Kremer, Mark D. Ryan, and Graham Steel. Formal analysis of protocols based on TPM state registers. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), pp. 66–82, IEEE Computer Society Press, Cernay-la-Ville, France, June 2011.
doi:10.1109/CSF.2011.12

Download

[PDF] [HTML]

Abstract

We present a Horn-clause-based framework for analysing security protocols that use platform configuration registers (PCRs), which are registers for maintaining state inside the Trusted Platform Module (TPM). In our model, the PCR state space is unbounded and our experience shows that a na\"ive analysis using ProVerif or SPASS does not terminate. To address this, we extract a set of instances of the Horn clauses of our model, for which ProVerif does terminate on our examples. We prove the soundness of this extraction process: no attacks are lost, that is, any query derivable in the more general set of clauses is also derivable from the extracted instances. The effectiveness of our framework is demonstrated in two case studies: a simplified version of Microsoft Bitlocker, and a digital envelope protocol that allows a user to choose whether to perform a decryption, or to verifiably renounce the ability to perform the decryption.

BibTeX

@inproceedings{DKRS-csf11,
  abstract =      {We present a Horn-clause-based framework for
                  analysing security protocols that use platform
                  configuration registers (PCRs), which are registers
                  for maintaining state inside the Trusted Platform
                  Module (TPM). In our model, the PCR state space is
                  unbounded  and our experience shows that a na\"ive
                  analysis using ProVerif or SPASS does not terminate.
                  To address this, we extract a set of instances of
                  the Horn clauses of our model, for which ProVerif
                  does terminate on our examples. We prove the
                  soundness of this extraction process: no attacks are
                  lost, that is, any query derivable in the more
                  general set of clauses is also derivable from the
                  extracted instances. The effectiveness of our
                  framework is demonstrated in two case studies: a
                  simplified version of Microsoft Bitlocker, and a
                  digital envelope protocol that allows a user to
                  choose whether to perform a decryption, or to
                  verifiably renounce the ability to perform the
                  decryption.},
  address =       {Cernay-la-Ville, France},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve and
                   Ryan, Mark D. and Steel, Graham},
  booktitle =     {{P}roceedings of the 24th {IEEE} {C}omputer
                   {S}ecurity {F}oundations {S}ymposium ({CSF}'11)},
  DOI =           {10.1109/CSF.2011.12},
  month =         jun,
  pages =         {66-82},
  publisher =     {{IEEE} Computer Society Press},
  title =         {Formal analysis of protocols based on {TPM} state
                   registers},
  year =          {2011},
  acronym =       {{CSF}'11},
  nmonth =        {6},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf},
}