Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Security and Trust Management

STM 2019: Security and Trust Management pp 89–106Cite as

Understanding Attestation: Analyzing Protocols that Use Quotes

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 11738))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Since an out-of-order execution attack falsifies this claim [7], the current SGX does not satisfy our axioms.

References

  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. 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. Bhargavan, K., Corin, R., Fournet, C., Gordon, A.D.: Secure sessions for web services. ACM Trans. Inf. Syst. Secur. 10(2), 8 (2007)

    Article  Google Scholar 

  4. Blanchet, B.: An efficient protocol verifier based on prolog rules. In: IEEE CSFW, pp. 82–96. IEEE CS Press, June 2001

    Google Scholar 

  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). https://doi.org/10.1007/11818175_32

    Chapter  Google Scholar 

  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. 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. 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)

    Article  MathSciNet  Google Scholar 

  9. Coker, G., et al.: Principles of remote attestation. IJIS 10(2), 63–81 (2011)

    Article  Google Scholar 

  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. Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-540-78636-8

    Book  MATH  Google Scholar 

  12. Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29, 198–208 (1983)

    Article  MathSciNet  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-98938-9_8

    Chapter  Google Scholar 

  14. Dyckhoff, R., Negri, S.: Geometrisation of first-order logic. Bull. Symb. Logic 21(2), 123–163 (2015)

    Article  MathSciNet  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-03829-7_1

    Chapter  MATH  Google Scholar 

  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). https://doi.org/10.1007/978-3-540-31987-0_11

    Chapter  Google Scholar 

  17. Gollamudi, A., Chong, S.: Automatic enforcement of expressive security policies using enclaves. In: OOPSLA, pp. 494–513 (2016)

    Article  Google Scholar 

  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. Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201–267 (2014)

    Article  Google Scholar 

  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). https://doi.org/10.1007/11580850_8

    Chapter  Google Scholar 

  21. Guttman, J.D., Ramsdell, J.D.: CPSA inputs for understanding attestation, April 2019. https://web.cs.wpi.edu/~guttman/pubs/understanding_attestation_example/

  22. Intel. Intel® Software Guard Extensions (Intel® SGX) (2016). https://software.intel.com/en-us/sgx

  23. Intel. Intel® Software Guard Extensions (Intel® SGX) data center attestation primitives: ECDSA quote library API, November 2018. https://download.01.org/intel-sgx/dcap-1.0.1/docs/Intel_SGX_ECDSA_QuoteGenReference_DCAP_API_Linux_1.0.1.pdf

  24. Kaplan, D., Powell, J., Woller, T.: AMD memory encryption, April 2016. https://developer.amd.com/wordpress/media/2013/12/AMD_Memory_Encryption_Whitepaper_v7-Public.pdf

  25. Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. J. Comput. Secur. 24(5), 583–616 (2016)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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 2002

    Google Scholar 

  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). https://doi.org/10.1007/978-3-030-19052-1_10

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-39799-8_48

    Chapter  Google Scholar 

  30. Murray, T., van Oorschot, P.C.: Formal proofs, the fine print and side effects. In: IEEE SecDev, September 2018

    Google Scholar 

  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)

    Article  Google Scholar 

  32. Ramsdell, J.D., Guttman, J.D.: CPSA4: a cryptographic protocol shapes analyzer with geometric rules. The MITRE Corporation (2018). https://github.com/ramsdell/cpsa

  33. Ramsdell, J.D., Guttman, J.D., Liskov, M.: CPSA: A cryptographic protocol shapes analyzer (2016). http://hackage.haskell.org/package/cpsa

  34. Rescorla, E., Ray, M., Dispensa, S., Oskov, N.: Transport Layer Security (TLS) Renegotiation Indication Extension. RFC 5746 (Proposed Standard) (2010)

    Google Scholar 

  35. Rowe, P.D., Guttman, J.D., Liskov, M.D.: Measuring protocol strength with security goals. Int. J. Inf. Secur. (2016). https://doi.org/10.1007/s10207-016-0319-z. http://web.cs.wpi.edu/~guttman/pubs/ijis_measuring-security.pdf

    Article  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-21401-6_30

    Chapter  Google Scholar 

  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. Sinha, R., et al.: A design and verification methodology for secure isolated regions. In: PLDI (2016)

    Google Scholar 

  39. Sinha, R., Rajamani, S., Seshia, S., Vaswani, K.: Moat: verifying confidentiality of enclave programs. In: ACM CCS, Moat (2015)

    Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. The MITRE Corporation, Bedford, MA, USA

    Joshua D. Guttman & John D. Ramsdell

Authors
  1. Joshua D. Guttman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John D. Ramsdell
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Joshua D. Guttman .

Editor information

Editors and Affiliations

  1. University of Luxembourg, Esch-sur-Alzette, Luxembourg

    Sjouke Mauw

  2. University of Padua, Padua, Italy

    Mauro Conti

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Guttman, J.D., Ramsdell, J.D. (2019). Understanding Attestation: Analyzing Protocols that Use Quotes. In: Mauw, S., Conti, M. (eds) Security and Trust Management. STM 2019. Lecture Notes in Computer Science(), vol 11738. Springer, Cham. https://doi.org/10.1007/978-3-030-31511-5_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31511-5_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31510-8

  • Online ISBN: 978-3-030-31511-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation