Abstract
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. © 2013 Springer-Verlag.
Cite
CITATION STYLE
Halling, B., & Alexander, P. (2013). Verifying a privacy CA remote attestation protocol. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7871 LNCS, pp. 398–412). https://doi.org/10.1007/978-3-642-38088-4_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
