Formal Analysis of Secure Bootstrap in Trusted Computing

  • Shuyi Chen
  • Yingyou Wen
  • Hong Zhao
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4610)


The stated goal of the trusted computing is to redesign PC hardware for providing protection against software attack. Trust platform is key technology of trusted computing. However, the security of trusted platform should be verified in theory, and the model of trusted platform should be further improved. In this paper, a formal method for verifying the security of trusted platform is presented. The vulnerability of secure bootstrap is analyzed based on the proposed formal semantics. Moreover, an improved model of secure bootstrap is proposed. The semantics presented here also can be used to reasoning about other applications of trusted computing, which provides a general and effective method for analyzing security of trusted computing applications.


Formal Semantic Predicate Logic Integrity Measurement Trust Level Trusted Platform Module 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
    Microsoft. Next-Generation Secure Computing Base home page (2006),
  3. 3.
    Peinado, M., Chen, Y., England, P., et al.: NGSCB: A trusted open system. In: Wang, H., Pieprzyk, J., Varadharajan, V. (eds.) ACISP 2004. LNCS, vol. 3108, pp. 86–97. Springer, Heidelberg (2004)Google Scholar
  4. 4.
    Intel. LaGrande Technology Architectural Overview (2006),
  5. 5.
    Alan, Z.: Coming soon to VMware, Microsoft, and Xen: AMD Virtualization Technology Solves Virtualization Challenges (2006),
  6. 6.
    Lie, D., Thekkath, C., Mitchell, M., et al.: Architectural support for copy and tamper resistant software. In: William, E., et al. (eds.) ASPLOS-IX 2000[C]. Operating Systems Review, vol. 34, pp. 168–177. ACM Press, New York (2000)Google Scholar
  7. 7.
    Garfinkel, T., Pfaff, B., Chow, J., et al.: Terra: A virtual machine-based platform for trusted computing. In: Birman, K., et al. (eds.) SOSP 2003 [C]. Operating Systems Review, vol. 37, pp. 193–206. ACM Press, New York (2003)Google Scholar
  8. 8.
    Abadi, M., Wobber, T.: A Logical Account of NGSCB. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 1–12. Springer, Heidelberg (2004)Google Scholar
  9. 9.
    Patel, J., Teacy, W.T., Jennings, N.R., et al.: A Probabilistic Trust Model for Handling Inaccurate Reputation Sources. In: Herrmann, P., Issarny, V., Shiu, S.C.K. (eds.) iTrust 2005. LNCS, vol. 3477, pp. 193–209. Springer, Heidelberg (2005)Google Scholar
  10. 10.
    Beth, T., Borcherding, M., Klein, B.: Valuation of Trust in Open Network. In: Gollmann, D. (ed.) Computer Security - ESORICS 1994. LNCS, vol. 875, pp. 509–522. Springer, Heidelberg (1994)Google Scholar
  11. 11.
    Bondavalli, A., Chiaradonna, S., Giandomenico, F.D., et al.: Dependability Modeling and Evaluation of Multiple Phased Systems Using DEEM. In: IEEE Transactions on Reliability, vol. 53, pp. 23–26. IEEE Press, New York (2000)Google Scholar
  12. 12.
    Maurer, U.: Modelling a public-key infrastructure. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) Computer Security - ESORICS 1996. LNCS, vol. 1146, pp. 325–350. Springer, Heidelberg (1996)Google Scholar
  13. 13.
    Bakkali, H.E., Kaitouni, B.I.: Predicate calculus logic for the PKI trust model analysis. In: IEEE International Symposium on Network Computing and Applications (NCA 2001), pp. 368–371. IEEE Press, New York (2001)CrossRefGoogle Scholar
  14. 14.

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Shuyi Chen
    • 1
  • Yingyou Wen
    • 1
  • Hong Zhao
    • 1
  1. 1.School of Information Science and Engineering, Northeastern University, 110004, ShenyangChina

Personalised recommendations