Towards a Verified Reference Implementation of a Trusted Platform Module

(Transcript of Discussion)
  • Aybek Mukhamedov
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7028)


This work was done jointly with Andrew Gordon and Mark Ryan. A TPM is a trusted platform module. The trusted platform is supposed to provide two main functions: integrity measurement, report and storage. And the trusted platform relies on a security chip called a TPM to realise two of those functions, trusted storage and reporting. The TPM defines more than 90 commands with its API. Manual inspection of them is not feasible, and clearly product recalls are expensive because TPM is bound to the computer. So there’s a need for formal analysis of the API, and protocol verification tools seem to be suitable for the task.

There are a number of successful frameworks for protocol verification, for example, specialised ones like ProVerif, or general purpose tools like FDR. There has been an effort to do an API analysis previously, but a common feature of the previous work was that it did the analysis of the abstract model, and there was no clear connection between the verified model and the implementation.


Shared Secret Trust Platform Module Threat Model Reference Implementation Product Recall 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Aybek Mukhamedov
    • 1
  1. 1.University of BirminghamUK

Personalised recommendations