Open Access

Muhammad Usama Sardar, Arto Niemi, Hannes Tschofenig, Thomas Fossati

• Transport Layer Security (TLS) is a widely used protocol for secure channel establishment. However, TLS lacks any inherent mechanism for validating the security state of the endpoint software and its platform. To overcome this limitation, recent works have combined remote attestation (RA) and TLS, named attested TLS. The most popular attested TLS protocol for confidential computing is Intel’s RA-TLS, which is used in multiple open-source industrial projects. However, there is no formal reasoning for security of attested TLS for confidential computing in general and RA-TLS in particular. Using the state-of-the-art symbolic security analysis tool ProVerif, we found vulnerabilities in RA-TLS at both RA and TLS layers, which have been acknowledged by Intel. We also propose mitigations for the vulnerabilities. During the process of formalization, we found that despite several formal verification efforts for TLS to ensure its security, the validation of corresponding formal models has been largely overlooked. This work demonstrates that a simple validation framework could discover crucial issues in state-of-the-art formalization of TLS 1.3 key schedule. These issues have been acknowledged and fixed by the authors. Finally, we provide recommendations for protocol designers and the formal verification community based on the lessons learned in the formal verification and validation.