A rollercoaster ride on the formal analysis of attested TLS

Transport Layer Security (TLS) is a widely used protocol for secure channel establishment. However, it lacks any inherent mechanism for validating the security state of the endpoint software and its platform. To overcome this limitation, there have been recent proposals to combine remote attestation and TLS, named as attested TLS. The most common attested TLS protocol for confidential computing is Intel's RA-TLS, which is used in multiple open-source industrial projects.  By using the state-of-the-art symbolic security analysis tool ProVerif, we found a potential issue in RA-TLS, namely attestation evidence can be replayed from an old session without the verifier noticing. We finally reflect on the challenges and lessons learned in the formalization process, including the discovery of crucial issues in the earlier formalization of TLS.

(Joint work with Arto Niemi, Hannes Tschofenig, and Thomas Fossati)