Hi,I fully understand that the subject draft itself is no longer relevant to this WG. But I want to share it for a few reasons:
1. I made some claims in February (cf. email below) and I want to substantiate those with formal artifacts. 2. I believe from a formal analysis perspective, some of the proposed solutions are still relevant to this WG for hybrid PQ stuff (e.g., composite, like draft-reddy-tls-composite-mldsa and parallel, like draft-yusef-tls-pqt-dual-certs). For example, thinking of one key as traditional and the other one as PQ, I believe it can provide a starting point for formal analysis of hybrid PQ proposals, with some additional PQ considerations. 3. Inria's artifacts for TLS 1.3 come with absolutely no comments in the main processes. I have added extensive comments and I hope you will find them useful for understanding the TLS 1.3 model or for extending it for the formal analysis of your drafts. In a separate work, we are working on baseline modular formal model of pure TLS 1.3 (RFC8446bis) in ProVerif and explanation of properties for authors to get started with formal analysis of their own extensions of TLS 1.3.So our paper (accepted at AsiaCCS) is here [A] and the formal artifacts are here [B]. We (i.e., I, Mariam Moustafa and Tuomas Aura) would like to thank folks from this WG, in particular Ekr, Hannes, Yaron, Chris P, Jonathan and Richard Barnes for their valuable contributions.
I welcome any feedback or thoughts, particularly on points 2 and 3 above. -Usama[A] https://www.researchgate.net/publication/398839141_Identity_Crisis_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS
[B] https://github.com/CCC-Attestation/formal-spec-id-crisis On 26.02.25 23:22, Muhammad Usama Sardar wrote:
Hi all, *Context*:At IETF 121, Hannes presented draft-fossati-tls-attestation [1] mentioning Confidential Computing as the priority (slide 3 in [2]) and asked for adoption (slide 4 in [2]).*Findings of Formal Analysis*:In collaboration with the /active/ editors of the draft, we have been doing the formal analysis of this draft and we believe that the protocol as applied to Confidential Computing (Sec. 9.1 in [1]) breaks the very fundamental property namely "Server Authentication" even under ideal conditions (i.e., assuming all remote attestation mechanisms to be perfect [See Attack 1 below]).*Background on Remote Attestation (RA): *See RFC 9334 [3]. Disclaimer: Don't worry if you find it very ambiguous, because it definitely is :) RATS WG defines vague terminology as the characteristic of the WG [8]. This has been part of the challenge for me for the last 5 years or so.*Threat model of Confidential Computing: *Cloud Service Provider (CSP) is fully untrusted. Only the hardware (CPU) and guest VM is trusted.*Overview of formal model*:Figure 13 in [1] shows TLS Handshake mysteriously covering all the entities namely Client, Verifier, Server and Attestation Service. An issue [4] requesting clarification on that is celebrating its first anniversary today. Since that remains a mystery, as agreed with the editors, as a starting point, we model Client and Verifier as one entity calling it Verifying Relying Party. Please note that this leads to only a subset of the attacks which are actually possible on the proposed protocol.In short, the case we have modeled is: * TLS Server as Attester * TLS Client as Verifying Relying Party (where Verifying Relying Party = combination of Verifier and Relying Party roles of RATS) *Fundamental Issue: *The proposed protocol /replaces/ authentication with attestation rather than /augmenting/ authentication with attestation.*Overview of Attack 1: */High-level idea/: If a client wants to connect to www.deutsche-bank.de for example, the protocol no longer provides this guarantee that it is actually connecting to the desired bank. What the client is instead provided with is that the computing environment and platform is as expected. What would a client do that?/Technical details/: Rather than using long-term identity (ID, e.g., hostname) and its corresponding long-term key (LTK) signed by the Certification Authority (CA), the protocol uses measurements (m) and Ephemeral Key (EK) signed by the Attestation Key (AK). That is, ID is now completely gone from the protocol leading to MITM.*Overview of Attack 2: */High-level idea: /Server authentication fails if there is even a single compromised Confidential Computing machine in the world (i.e., AK is compromised) whose certificate has not yet been revoked. Transient execution attacks like Foreshadow [5] have already shown the compromise to be practical. Moreover, with the confidential computing threat model, a hostile adversary (e.g., CSP) has no incentive to announce to the world to revoke the key of compromised machine./Technical details/: The adversary can divert the TLS connection to the compromised machine which then impersonates the server. Since the adversary has AK on compromised machine, it can sign any desired measurements which are acceptable by the client, while it may run the VM of its own in order to get the secrets from the client (e.g., the login credentials of the client).*Recommendation:*We recommend combining web PKI and RA rather than replacing one with another.In short: * Web PKI cert provides (ID,pubLTK) signed by CA. * RA provides (m,pubEK) signed by AK/Attack1/: Using Web PKI cert (in combination with RA) covers the first attack./Attack2/: Combining web PKI with RA ensures that the adversary has to break that specific machine rather than any machine in the world.However, this seems to be a challenge since the CertificateVerify message is not extensible and can provide Proof-of-Possession of only one key. ** *Paper:*A paper covering this is currently under submission. We will make it public later on.*Alternative solutions:* * We have explored alternative protocols. We have also formally analyzed a widely used Interoperable RA-TLS protocol [6] and it is vulnerable to the same attacks mentioned above. * According to my notes of IETF 120, Chris Patton proposed to look in to RFC 9261. Hannes kindly put together an initial draft [7] on this. While not yet formally analyzed, we believe it is apparently vulnerable to both attacks. *Open Questions:* A couple of challenges to augment authentication with attestation are: 1. What is the "long-term identity" of Virtual Machine (VM)-based Trusted Execution Environments (TEEs)? Which entity provisions (and signs) this "long-term identity"? How is that provisioning entity trusted? 2. How is CA-certified Long-Term Key (LTK) injected in the Confidential Computing workload in the first place? *Discussion/Question to WG: *Is it acceptable to make significant changes to the messages in the TLS handshake protocol?*Clarification: *The formal model has been analyzed under Confidential Computing threat model. The attacks may or may not apply to other scenarios (e.g., IoT). I just don't know yet. I will happily give the chance to others to get their hands (and bodies) dirty with muddy RATS on non-confidential computing scenarios.Thanks, Usama * * [1] https://www.ietf.org/archive/id/draft-fossati-tls-attestation-08.html[2] https://datatracker.ietf.org/meeting/121/materials/slides-121-tls-tls-and-attestation-00.pdf[3] https://www.rfc-editor.org/rfc/rfc9334.html [4] https://github.com/tls-attestation/draft-tls-attestation/issues/40 [5] https://foreshadowattack.eu/ [6] https://github.com/CCC-Attestation/interoperable-ra-tls[7] https://hannestschofenig.github.io/exported-attestation/draft-fossati-rats-exported-attestation.html[8] https://mailarchive.ietf.org/arch/msg/rats/PIuGlghjjuysRUFjxYq9SdOV37A/
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
