Formal analysis of a TPM-based secrets distribution and storage scheme
conference contributionposted on 17.12.2009 by Ronald Toegl, Georg Hofferek, Karin Greimel, Adrian Leung, Raphael C.-W. Phan, Roderick Bloem
Any type of content contributed to an academic conference, such as papers, presentations, lectures or proceedings.
Trusted computing introduces the Trusted Platform Module (TPM) as a root of trust on an otherwise untrusted computer. The TPM can be used to restrict the use of cryptographic keys to trusted states, i.e., to situations in which the computer runs trusted software. This allows for the distribution of intellectual property or secrets to a remote party with a reasonable security that such secrets will not be obtained by a malicious or compromised client. We model a specific protocol for the distribution of secrets proposed by Sevine et al. A formal analysis using the NuSMV model checker shows that the protocol allows an intruder to give the client an arbitrary secret, without the client noticing. We propose an alternative that prevents this scenario.
- Mechanical, Electrical and Manufacturing Engineering