Abstract
The Trusted Platform Module (TPM) is a hardware chip designed to enable computers to achieve a greater level of security than is possible in software alone. To this end, the TPM provides a way to store cryptographic keys and other sensitive data in its shielded memory. Through its API, one can use those keys to achieve some security goals. The TPM is a complex security component, whose specification consists of more than 700 pages.
We model a collection of four TPM commands, and we identify and formalise their security properties. Using the tool ProVerif, we rediscover some known attacks and some new variations on them. We propose modifications to the API and verify our properties for the modified API.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115. ACM Press, New York (2001)
Ables, K.: An attack on key delegation in the Trusted Platform Module (first semester mini-project in computer security). Master’s thesis, School of Computer Science, University of Birmingham (2009)
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Blanchet, B.: Automatic verification of correspondences for security protocols. Journal of Computer Security 17(4), 363–434 (2009)
Bruschi, D., Cavallaro, L., Lanzi, A., Monga, M.: Replay attack in TCG specification and solution. In: Proc. 21st Annual Computer Security Applications Conference (ACSAC 2005), pp. 127–137. IEEE Computer Society, Los Alamitos (2005)
Chen, L., Ryan, M.: Attack, solution and verification for shared authorisation data in TCG TPM. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 201–216. Springer, Heidelberg (2010)
Chen, L., Ryan, M.D.: Offline dictionary attack on TCG TPM weak authorisation data, and solution. In: Future of Trust in Computing, Vieweg & Teubner (2008)
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 (2010) (to appear)
Datta, A., Franklin, J., Garg, D., Kaynar, D.: A logic of secure systems and its application to trusted computing. In: Proc. 30th IEEE Symposium on Security and Privacy (S&P 2009), pp. 221–236 (2009)
Fröschle, S., Steel, G.: Analysing PKCS#11 key management aPIs with unbounded fresh data. In: Degano, P., Viganò, L. (eds.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 92–106. Springer, Heidelberg (2009)
Gasmi, Y., Sadeghi, A.-R., Stewin, P., Unger, M., Asokan, N.: Beyond secure channels. In: Scalable Trusted Computing (STC 2007), pp. 30–40 (November 2007)
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)
ISO/IEC PAS DIS 11889: Information technology – Security techniques – Trusted Platform Module
Lin, A.H.: Automated Analysis of Security APIs. Master’s thesis, MIT (2005), http://sdg.csail.mit.edu/pubs/theses/amerson-masters.pdf
Sarmenta, L.: TPM/J developer’s guide. Massachussetts Institute of Technology
Trusted Computing Group. TPM Specification version 1.2. Parts 1–3, revision 103 (2007), http://www.trustedcomputinggroup.org/resources/tpm_main_specification
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delaune, S., Kremer, S., Ryan, M.D., Steel, G. (2011). A Formal Analysis of Authentication in the TPM. In: Degano, P., Etalle, S., Guttman, J. (eds) Formal Aspects of Security and Trust. FAST 2010. Lecture Notes in Computer Science, vol 6561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19751-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-19751-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19750-5
Online ISBN: 978-3-642-19751-2
eBook Packages: Computer ScienceComputer Science (R0)