Formal analysis of protocols based on TPM state registers (bibtex)
by Stéphanie Delaune, Steve Kremer, Mark D. Ryan, Graham Steel
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\EFve 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.
Reference:
Formal analysis of protocols based on TPM state registers (Stéphanie Delaune, Steve Kremer, Mark D. Ryan, Graham Steel), In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), IEEE Computer Society Press, 2011.
Bibtex Entry:
@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\EFve
                   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)},
  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},
  PDF =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf},
  lsv-category =  {intc},
  lsv-status =    {apar},
  wwwpublic =     {public},
}
Powered by bibtexbrowser