The goal of the Verified TPM is specifying and verifying the TPM 1.2 formally in PVS. We specify the TPM as a state transformation system with each instruction modifying the TPM state. We then use a state monad to sequence instruction execution, threading state through a sequence of instructions.
The System-Level Design Group is a part of The Information and Telecommunication Technology Center at The University of Kansas.
Verified TPM is supported by