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.
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.
@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{\"i}ve
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)},
OPTDOI = {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},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}