| dc.contributor.advisor | Alexander, Perry | |
| dc.contributor.author | Halling, Brigid Rose | |
| dc.date.accessioned | 2013-09-30T18:45:03Z | |
| dc.date.available | 2013-09-30T18:45:03Z | |
| dc.date.issued | 2013-05-31 | |
| dc.date.submitted | 2013 | |
| dc.identifier.other | http://dissertations.umi.com/ku:12994 | |
| dc.identifier.uri | http://hdl.handle.net/1808/12299 | |
| dc.description.abstract | The Trusted Platform Module (TPM) serves as the root-of-trust in a trusted computing environment, and therefore warrants formal specification and verification. This thesis 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 use it. TPM commands are specified as state transformations and sequenced to represent protocols using a state monad. Preconditions, postconditions, and invariants are specified for individual commands and validated. All specifications are written and verified automatically using the PVS decision procedures and rewriting system. | |
| dc.format.extent | 166 pages | |
| dc.language.iso | en | |
| dc.publisher | University of Kansas | |
| dc.rights | This item is protected by copyright and unless otherwise specified the copyright of this thesis/dissertation is held by the author. | |
| dc.subject | Computer science | |
| dc.subject | Formal verification | |
| dc.subject | Tpm | |
| dc.subject | Trusted computing | |
| dc.title | Towards a Formal Verification of the Trusted Platform Module | |
| dc.type | Thesis | |
| dc.contributor.cmtemember | Alexander, Perry | |
| dc.contributor.cmtemember | Gill, Andrew | |
| dc.contributor.cmtemember | Li, Fengjun | |
| dc.thesis.degreeDiscipline | Electrical Engineering & Computer Science | |
| dc.thesis.degreeLevel | M.S. | |
| kusw.oastatus | na | |
| kusw.oapolicy | This item does not meet KU Open Access policy criteria. | |
| kusw.bibid | 8086303 | |
| dc.rights.accessrights | openAccess | |
