ATTENTION: The software behind KU ScholarWorks is being upgraded to a new version. Starting July 15th, users will not be able to log in to the system, add items, nor make any changes until the new version is in place at the end of July. Searching for articles and opening files will continue to work while the system is being updated.
If you have any questions, please contact Marianne Reed at mreed@ku.edu .
Towards a Formal Verification of the Trusted Platform Module
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 |
Files in this item
This item appears in the following Collection(s)
-
Engineering Dissertations and Theses [1055]
-
Theses [4088]