Automated Verification of Dynamic Root of Trust Protocols

  • Sergiu Bursuc
  • Christian JohansenEmail author
  • Shiwei Xu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10204)


Automated verification of security protocols based on dynamic root of trust, typically relying on protected hardware such as TPM, involves several challenges that we address in this paper. We model the semantics of trusted computing platforms (including CPU, TPM, OS, and other essential components) and of associated protocols in a classical process calculus accepted by ProVerif. As part of the formalization effort, we introduce new equational theories for representing TPM specific platform states and dynamically loaded programs.

Formal models for such an extensive set of features cannot be readily handled by ProVerif, due especially to the search space generated by unbounded extensions of TPM registers. In this context we introduce a transformation of the TPM process, that simplifies the structure of the search space for automated verification, while preserving the security properties of interest. This allows to run ProVerif on our proposed models, so we can derive automatically security guarantees for protocols running in a dynamic root of trust context.



We would like to thank Cas Cremers and several reviewers for helping improve this work.


  1. 1.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115, January 2001Google Scholar
  2. 2.
    Arapinis, M., Bursuc, S., Ryan, M.D.: Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity. In: Degano and Guttman [11], pp. 169–188Google Scholar
  3. 3.
    Arapinis, M., Ritter, E., Ryan, M.D.: StatVerif: verification of stateful processes. In: CSF, pp. 33–47. IEEE Computer Society (2011)Google Scholar
  4. 4.
    Arthur, W., Challener, D., Goldman, K.: A Practical Guide to TPM 2.0. APress, Berkeley (2015)Google Scholar
  5. 5.
    Barbosa, M., Portela, B., Scerri, G., Warinschi, B.: Foundations of hardware-based attested computation and application to SGX. In: IEEE European Symposium on Security and Privacy, EuroS&P, Saarbrücken, Germany, 21–24 March 2016, pp. 245–260. IEEE (2016)Google Scholar
  6. 6.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW 2001) (2001)Google Scholar
  7. 7.
    Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4), 363–434 (2009)CrossRefGoogle Scholar
  8. 8.
    Blanchet, B., Chaudhuri, A.: Automated formal analysis of a protocol for secure file sharing on untrusted storage. In: IEEE Symposium on Security and Privacy, pp. 417–431. IEEE Computer Society (2008)Google Scholar
  9. 9.
    Cortier, V., Degrieck, J., Delaune, S.: Analysing routing protocols: four nodes topologies are sufficient. In: Degano and Guttman [11], pp. 30–50Google Scholar
  10. 10.
    Datta, A., Franklin, J., Garg, D., Kaynar, D.: A logic of secure systems and its application to trusted computing. In: 30th IEEE Symposium on Security and Privacy, pp. 221–236. IEEE (2009)Google Scholar
  11. 11.
    Degano, P., Guttman, J.D. (eds.): POST 2012. LNCS, vol. 7215. Springer, Heidelberg (2012)Google Scholar
  12. 12.
    Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF 2011), Cernay-la-Ville, France, pp. 66–82. IEEE Computer Society Press, June 2011Google Scholar
  13. 13.
    Duflot, L., Grumelard, O., Levillain, O., Morin, B.: ACPI and SMI handlers: some limits to trusted computing. J. Comput. Virol. 6(4), 353–374 (2010)CrossRefGoogle Scholar
  14. 14.
    Fournet, C., Planul, J.: Compiling information-flow security to minimal trusted computing bases. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 216–235. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-19718-5_12 CrossRefGoogle Scholar
  15. 15.
    Franklin, J., Chaki, S., Datta, A., McCune, J.M., Vasudevan, A.: Parametric verification of address space separation. In: Degano and Guttman [11], pp. 51–68Google Scholar
  16. 16.
    Franklin, J., Chaki, S., Datta, A., Seshadri, A.: Scalable parametric verification of secure systems: how to verify reference monitors without worrying about data structure size. In: IEEE Symposium on Security and Privacy, pp. 365–379. IEEE Computer Society (2010)Google Scholar
  17. 17.
    Garay, J.A., Jakobsson, M., MacKenzie, P.: Abuse-free optimistic contract signing. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 449–466. Springer, Heidelberg (1999). doi: 10.1007/3-540-48405-1_29 CrossRefGoogle Scholar
  18. 18.
    Grawrock, D.: Dynamics of a Trusted Platform: A Building Block Approach. Intel Press, Hillsboro (2009)Google Scholar
  19. 19.
    Trusted Computing Group. TCG Architecture Overview, Specification revision 1.4 (2007).
  20. 20.
    Trusted Computing Group. TPM main specification (2011).
  21. 21.
    Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. In: IEEE Symposium on Security and Privacy, pp. 163–178. IEEE Computer Society (2014)Google Scholar
  22. 22.
    Küsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: 22nd IEEE Computer Security Foundations Symposium (CSF), pp. 157–171. IEEE Computer Society (2009)Google Scholar
  23. 23.
    Meier, S.: Advancing automated security protocol verification. PhD Thesis, ETH Zürich (2013)Google Scholar
  24. 24.
    Mödersheim, S.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Al-Shaer, E., Keromytis, A.D., Shmatikov, V. (eds.) ACM Conference on Computer and Communications Security, pp. 351–360. ACM (2010)Google Scholar
  25. 25.
    Paiola, M., Blanchet, B.: Verification of security protocols with lists: from length one to unbounded length. In: Degano and Guttman [11], pp. 69–88Google Scholar
  26. 26.
    RSA Security Inc., v2.20. PKCS #11: Cryptographic token interface standard, June 2004Google Scholar
  27. 27.
    Ryan, M.D., Smyth, B.: Applied pi calculus. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series. IOS Press (2011)Google Scholar
  28. 28.
    Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium (CSF), pp. 78–94. IEEE Computer Society (2012)Google Scholar
  29. 29.
    Wojtczuk, R., Rutkowska, J.: Attacking INTEL trusted execution technology. In: Black Hat DC (2009)Google Scholar
  30. 30.
    Wojtczuk, R., Rutkowska, J.: Attacking INTEL TXT via SINIT code execution hijacking. Invisible Things Lab (2009)Google Scholar
  31. 31.
    Wojtczuk, R., Rutkowska, J., Tereshkin, A.: Another way to circumvent INTEL trusted execution technology. Invisible Things Lab (2009)Google Scholar
  32. 32.
    Yubico, A.B.: Kungsgatan 37, 111 56 Stockholm Sweden. The YubiKey manual - Usage, configuration and introduction of basic concepts (version 2.2) (2010)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  1. 1.University of BristolBristolUK
  2. 2.University of OsloOsloNorway
  3. 3.Wuhan Digital Engineering InstituteWuhanChina

Personalised recommendations