Sciweavers

Share
IFIP
2010
Springer

A Formal Analysis of Authentication in the TPM

8 years 7 months ago
A Formal Analysis of Authentication in the TPM
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.
Stéphanie Delaune, Steve Kremer, Mark Dermo
Added 18 May 2011
Updated 18 May 2011
Type Journal
Year 2010
Where IFIP
Authors Stéphanie Delaune, Steve Kremer, Mark Dermot Ryan, Graham Steel
Comments (0)
books