Root-of-trust abstractions for symbolic analysis: application to attestation protocols

A key component in building trusted computing services is a highly secure anchor that serves as a Root-of-Trust (RoT). There are several works that conduct formal analysis on the security of such commodity RoTs (or parts of it), and also a few ones devoted to verifying the trusted computing service as a whole. However, most of the existing schemes try to verify security without differentiating the internal cryptography mechanisms of the underlying hardware token from the client application cryptography. This approach limits, to some extent, the reasoning that can be made about the level of assurance of the overall system by automated reasoning tools. In this work, we present a methodology that enables the use of formal verification tools towards verifying complex protocols using trusted computing. The focus is on reasoning about the overall application security, provided from the integration of the RoT services, and how these can translate to larger systems when the underlying cryptographic engine is considered perfectly secure. Using the Tamarin prover, we demonstrate the feasibility of our approach by instantiating it for a TPM-based remote attestation service, which is one of the core security services needed in today's increased attack landscape.