ITTC Project

Trusted Platform Module (TPM) Verification

Project Award Date: 04-16-2012


If the Trusted Platform Module (TPM) is to form the trusted root of secure computing systems, validation, verification, and certification are essential. Without these assurances, there is no trust in the system. With millions of TPMs fielded, it becomes critical to remove ambiguities and inconsistencies in the current TPM specification.

ITTC researchers will provide a formal TPM specification, verification of the specification, and a verified TPM implementation. A verified TPM - the ultimate research goal - will dramatically simplify certification.

Model the TPM state and command execution - Using monadic techniques develop a model of the TPM internal state and a framework for command execution.

Model and Verify the attestation subset - Using the TPM state model, specify and verify the TPM command subset for PCR management and quote generation. Extend existing verification of PCR extension results.

Model and Verify the key management subset - Using the TPM state model, specify and verify the TPM command subset for generating and managing keys.

Verify common TPM command sequences - Using the new monadic model to expand previously performed verification of various TPM processes including boot


Faculty Investigator(s): Perry Alexander (PI)

Student Investigator(s): Brigid Halling

Project Sponsors

Primary Sponsor(s): Battelle Memorial Institute

Partner with ITTC

The Information and Telecommunication Technology Center at the University of Kansas has developed several assistance policies that enhance interactions between the Center and local, Kansas, or national companies. 

ITTC assistance includes initial free consulting (normally one to five hours). If additional support is needed, ITTC will offer one of the following approaches: 

Sponsored Research Agreement

Individuals and organizations can enter into agreements with KUCR/ITTC and provide funds for sponsored research to be performed at ITTC with the assistance of faculty, staff and students.

Licensing and Royalty/Equity Agreement

An ITTC goal is the development of investment-grade technologies for transfer to, and marketing by, local, Kansas, and national businesses. To enhance this process, the Center has developed flexible policies that allow for licensing, royalty, and equity arrangements to meet both the needs of ITTC and the company.

Commercialization Development

Companies with a technology need that can be satisfied with ITTC's resources can look to us for assistance. We can develop a relationship with interested partners that will provide for the development of a technology suited for commercialization.

ITTC Resource Access

ITTC resources, including computers and software systems, may be made available to Kansas companies in accordance with the Center's mission and applicable Regents and University policies.

ITTC Calendar
There are no upcoming events at this time.