Understanding Attestation: Analyzing Protocols that Use Quotes

  • Joshua D. GuttmanEmail author
  • John D. Ramsdell
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11738)


Attestation protocols use digital signatures and other cryptographic values to convey evidence of hardware state, program code, and associated keys. They require hardware support such as Trusted Execution Environments. Conclusions about attestations thus depend jointly on protocols, hardware services, and program behavior.

We present a mechanized approach to modeling these properties, combining protocol analysis with axioms, that formalize hardware and software properties. Here, we model aspects of Intel’s SGX mechanism. Above the underlying manufacturer-provided protocols, we build a modular user-level that uses its attestations to make trust decisions.


  1. 1.
    Barbosa, M., Portela, B., Scerri, G., Warinschi, B.: Foundations of hardware-based attested computation and application to SGX. In: IEEE EuroS&P, pp. 245–260 (2016)Google Scholar
  2. 2.
    Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: IEEE Computer Security Foundations Symposium (2009)Google Scholar
  3. 3.
    Bhargavan, K., Corin, R., Fournet, C., Gordon, A.D.: Secure sessions for web services. ACM Trans. Inf. Syst. Secur. 10(2), 8 (2007)CrossRefGoogle Scholar
  4. 4.
    Blanchet, B.: An efficient protocol verifier based on prolog rules. In: IEEE CSFW, pp. 82–96. IEEE CS Press, June 2001Google Scholar
  5. 5.
    Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 537–554. Springer, Heidelberg (2006). Scholar
  6. 6.
    Brickell, E., Li, J.: Enhanced privacy ID: a direct anonymous attestation scheme with enhanced revocation capabilities. In: ACM Workshop on Privacy in the Electronic Society, pp. 21–30. ACM (2007)Google Scholar
  7. 7.
    Van Bulck, J., et al.: Foreshadow: extracting the keys to the intel SGX kingdom with transient out-of-order execution. In: USENIX Security, pp. 991–1008 (2018)Google Scholar
  8. 8.
    Chadha, R., Cheval, V., Ciobâc, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1–23:32 (2016)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Coker, G., et al.: Principles of remote attestation. IJIS 10(2), 63–81 (2011)CrossRefGoogle Scholar
  10. 10.
    Costan, V., Lebedev, I.A., Devadas, S.: Sanctum: minimal hardware extensions for strong software isolation. In: USENIX Security Symposium, pp. 857–874 (2016)Google Scholar
  11. 11.
    Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012). Scholar
  12. 12.
    Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29, 198–208 (1983)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Dougherty, D.J., Guttman, J.D., Ramsdell, J.D.: Security protocol analysis in context: computing minimal executions using SMT and CPSA. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 130–150. Springer, Cham (2018). Scholar
  14. 14.
    Dyckhoff, R., Negri, S.: Geometrisation of first-order logic. Bull. Symb. Logic 21(2), 123–163 (2015)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009). Scholar
  16. 16.
    Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 141–156. Springer, Heidelberg (2005). Scholar
  17. 17.
    Gollamudi, A., Chong, S.: Automatic enforcement of expressive security policies using enclaves. In: OOPSLA, pp. 494–513 (2016)CrossRefGoogle Scholar
  18. 18.
    Guttman, J.D.: Shapes: surveying crypto protocol runs. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series. IOS Press (2011)Google Scholar
  19. 19.
    Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201–267 (2014)CrossRefGoogle Scholar
  20. 20.
    Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming cryptographic protocols. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 116–145. Springer, Heidelberg (2005). Scholar
  21. 21.
    Guttman, J.D., Ramsdell, J.D.: CPSA inputs for understanding attestation, April 2019.
  22. 22.
    Intel. Intel® Software Guard Extensions (Intel® SGX) (2016).
  23. 23.
    Intel. Intel® Software Guard Extensions (Intel® SGX) data center attestation primitives: ECDSA quote library API, November 2018.
  24. 24.
    Kaplan, D., Powell, J., Woller, T.: AMD memory encryption, April 2016.
  25. 25.
    Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. J. Comput. Secur. 24(5), 583–616 (2016)CrossRefGoogle Scholar
  26. 26.
    Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in distributed systems: theory and practice. ACM Trans. Comput. Syst. 10(4), 265–310 (1992)CrossRefGoogle Scholar
  27. 27.
    Li, N., Mitchell, J.C., Winsborough, W.H.: Design of a role-based trust management framework. In: Proceedings, 2002 IEEE Symposium on Security and Privacy, pp. 114–130. IEEE CS Press, May 2002Google Scholar
  28. 28.
    Liskov, M.D., Guttman, J.D., Ramsdell, J.D., Rowe, P.D., Thayer, F.J.: Enrich-by-need protocol analysis for Diffie-Hellman. In: Guttman, J.D., Landwehr, C.E., Meseguer, J., Pavlovic, D. (eds.) Foundations of Security, Protocols, and Equational Reasoning. LNCS, vol. 11565, pp. 135–155. Springer, Cham (2019). Scholar
  29. 29.
    Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013). Scholar
  30. 30.
    Murray, T., van Oorschot, P.C.: Formal proofs, the fine print and side effects. In: IEEE SecDev, September 2018Google Scholar
  31. 31.
    Noorman, J., et al.: Sancus 2.0: a low-cost security architecture for IoT devices. ACM Trans. Priv. Secur. 20(3), 7:1–7:33 (2017)CrossRefGoogle Scholar
  32. 32.
    Ramsdell, J.D., Guttman, J.D.: CPSA4: a cryptographic protocol shapes analyzer with geometric rules. The MITRE Corporation (2018).
  33. 33.
    Ramsdell, J.D., Guttman, J.D., Liskov, M.: CPSA: A cryptographic protocol shapes analyzer (2016).
  34. 34.
    Rescorla, E., Ray, M., Dispensa, S., Oskov, N.: Transport Layer Security (TLS) Renegotiation Indication Extension. RFC 5746 (Proposed Standard) (2010)Google Scholar
  35. 35.
    Rowe, P.D., Guttman, J.D., Liskov, M.D.: Measuring protocol strength with security goals. Int. J. Inf. Secur. (2016). Scholar
  36. 36.
    Saghafi, S., Danas, R., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 434–449. Springer, Cham (2015). Scholar
  37. 37.
    Schuster, F., et al.: VC3: trustworthy data analytics in the cloud using SGX. In: 2015 IEEE S&P, pp. 38–54 (2015)Google Scholar
  38. 38.
    Sinha, R., et al.: A design and verification methodology for secure isolated regions. In: PLDI (2016)Google Scholar
  39. 39.
    Sinha, R., Rajamani, S., Seshia, S., Vaswani, K.: Moat: verifying confidentiality of enclave programs. In: ACM CCS, Moat (2015)Google Scholar
  40. 40.
    Subramanyan, P., Sinha, R., Lebedev, I.A. Devadas, S., Seshia, S.A.: A formal foundation for secure remote execution of enclaves. In: ACM CCS (2017)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.The MITRE CorporationBedfordUSA

Personalised recommendations