As the hardware root-of-trust in a trusted computing environment, the Trusted Platform Module (TPM) warrants formal specification and verification. This work presents results of an effort to specify and verify an abstract TPM 1.2 model using PVS that is useful for understanding the TPM and verifying protocols that utilize it. TPM commands are specified as state transformations and sequenced to represent protocols using a state monad. Postconditions and invariants are specified for individual commands and validated by verifying a Privacy CA attestation protocol. All specifications are written and verified automatically using the PVS decision procedures and rewriting system.
展开▼
