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.
Keywords
- Trust Platform Module
- Direct Anonymous Attestation
- Remote Attestation
- Command Execution
- Attestation Protocol
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This work was sponsored in part by the Battelle Memorial Institute under PO US001-0000328568.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Trusted Computing Group, 3885 SW 153rd Drive, Beaverton, OR 97006: TCG TPM Specification, version 1.2 revision 103 edn. (July 2007), https://www.trustedcomputinggroup.org/resources/tpm_main_specification/
Brickell, E., Camenisch, J., Chen, L.: Direct anonymous attestation. In: Proceedings of the 11th ACM Conference on Computer and Communications Security, pp. 132–145. ACM (2004)
Challener, D., Yoder, K., Catherman, R., Stafford, D., Doorn, L.V.: A Practical Guide to Trusted Computing. IBM Press (2007)
Coker, G., Guttman, J., Loscocco, P., Herzog, A., Millen, J., O’Hanlon, B., Ramsdell, J., Segall, A., Sheehy, J., Sniffen, B.: Principles of remote attestation. International Journal of Information Security 10(2), 63–81 (2011)
Coker, G., Guttman, J., Loscocco, P., Sheehy, J., Sniffen, B.: Attestation: Evidence and trust. In: Chen, L., Ryan, M.D., Wang, G. (eds.) ICICS 2008. LNCS, vol. 5308, pp. 1–18. Springer, Heidelberg (2008)
Datta, A., Franklin, J., Garg, D., Kaynar, D.: A logic of secure systems and its application to trusted computing. In: 2009 30th IEEE Symposium on Security and Privacy, pp. 221–236. IEEE (2009)
Delaune, S., Kremer, S., Ryan, M., Steel, G.: Formal analysis of protocols based on tpm state registers. In: Proceedings of the 24th IEEE Computer Security Foundations Workshop, CSF 2011, pp. 66–82 (2011)
Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: A formal analysis of authentication in the TPM. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 111–125. Springer, Heidelberg (2011)
Goldreich, O., Oren, Y.: Definitions and properties of zero-knowledge proof systems. Journal of Cryptology 7, 1–32 (1994), http://dx.doi.org/10.1007/BF00195207 , doi:10.1007/BF00195207
Gürgens, S., Rudolph, C., Scheuermann, D., Atts, M., Plaga, R.: Security evaluation of scenarios based on the TCG’s TPM specification. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 438–453. Springer, Heidelberg (2007)
Haldar, V., Chandra, D., Franz, M.: Semantic remote attestation – a virtual machine directed approach to trusted computing. In: Proceedings of the Third Virtual Machine Research and Technology Symposium, San Jose, CA (May 2004)
Lin, A.H.: Automated analysis of security APIs. Ph.D. thesis, Massachusetts Institute of Technology (2005)
Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991), citeseer.nj.nec.com/moggi89notions.html
Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Ryan, M.: Introduction to the tpm 1.2 (March 2009), ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/08-intro-TPM.pdf (draft Report)
Sailer, R., Zhang, X., Jaeger, T., van Doorn, L.: Design and implementatation of a tcg-based integrity measurement architecture. In: Proceedings of the 13th USENIX Security Symposium. USENIX Association, Berkeley (2004)
Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2012)
Wadler, P.: The essence of functional programming. In: Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albequerque, New Mexico, pp. 1–14 (1992), citeseer.nj.nec.com/wadler92essence.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Halling, B., Alexander, P. (2013). Verifying a Privacy CA Remote Attestation Protocol. In: Brat, G., Rungta, N., Venet, A. (eds) NASA Formal Methods. NFM 2013. Lecture Notes in Computer Science, vol 7871. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38088-4_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-38088-4_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38087-7
Online ISBN: 978-3-642-38088-4
eBook Packages: Computer ScienceComputer Science (R0)