Understanding Attestation: Analyzing Protocols that Use Quotes

Presented as part of the 2019 HCSS conference.

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 or Trusted Platform Modules. Conclusions about attestations thus require reasoning about protocols, relevant hardware services, and possible behaviors of programs jointly.

This paper presents a mechanized approach to modeling these properties. The Cryptographic Protocol Shapes Analyzer CPSA now combines protocol analysis with axioms or rules, allowing formalizing hardware and software conclusions.

We use CPSA to model aspects of Intel's SGX mechanism. We model underlying manufacturer-provided protocols, and build modular layers of attestation above this basis. User-level protocols can make trust decisions based on the results of attestation.

A full version may be found at: https://web.cs.wpi.edu/~guttman/pubs/att_lncs.pdf

Dr. Joshua Guttman is a Senior Principal Scientist at the MITRE Corporation, and Research Professor at Worcester Polytechnic Institute. He has focused on security foundations and applications, including cryptographic protocol analysis and design, network security, operating systems security, and information flow. Dr. Guttman has written extensively, with about 75 academic publications, and regularly serves on program committees and proposal evaluations. He was educated at Princeton and the University of Chicago.