Hi all,
# *Context*At the expat BoF [0], some questions were raised about my claims of insecurity of intra-handshake attestation (draft-fossati-tls-attestation). We previously shared our ProVerif artifacts [8] for review. We did follow-up work and found more attacks. As supporting public evidence, *Cocos AI has publicly acknowledged [9]* the new attacks this Friday (see section "#Cocos AI acknowledgment of attacks" below). As helpful context, Cocos AI [4] claimed their attested TLS to be the "best in the world" in the Confidential Computing Consortium and despite we having informed them repeatedly about the attacks after our formal analysis, they were continuing to misguide the community on social media. Anyway, we now respect their honesty and transparency, and we remain fully committed to helping them towards secure solutions.
We would like to hear the thoughts of folks about this work. Some of the work is being done at SEAT WG, and I -- as author of use cases draft (draft-mihalcea-seat-use-cases) and protocol design draft (draft-fossati-seat-expat) -- would like to know more about the requirements of this community from protocol design perspective to see how we can securely satisfy those requirements.
# *Summary*We (i.e., I, Dr. Viacheslav Dubeyko [IBM], and Prof. Jean-Marie Jacquet [University of Namur]) extensively explored binding mechanisms in intra-handshake attestation for confidential agentic AI systems. The way we define agentic AI system includes agent to agent (A2A) and agent to orchestrator (A2O) communication.
We did formal analysis in state-of-the-art tool ProVerif and we would like to share a summary of our findings from our formal analysis with the hope to get some feedback and share some questions for which folks may have some insights to share.
# *Key Finding*/All/ analyzed binding mechanisms and implementations are ad-hoc and /all/ of them result in relay attacks.
Please note that this includes Meta's AI [1] for which a thorough security assessment [2] was carried out by /Trail of Bits/ and they were unable to capture the relay attacks but as kindly clarified by Tjaden Hess, no formal methods were used in their review process. Our analysis shows the value of formal methods in the review process.
# *Fundamental Issue*Basically, there is no binding of Evidence to the TLS connection in all of these implementations.
# *TEE-agnostic System Model* * Layered Attester (e.g., Intel TDX) * Composite Attester (e.g., Arm CCA) # *Scope of Attested TLS* * Intra-handshake attestation # *Formalization Approach* * Symbolic security analysis # *Formalization Tool* * ProVerif # *Binding Mechanisms**A*. We considered the following values for user-defined field "rdata" in TEEs
1. Client's TLS nonce 2. Client's Attestation nonce 3. Early exporter 4. (Hash of) Server's public key/Question for discussion/: Is someone aware of any other value that folks use in "rdata"? If possible, please share a link to specification and/or implementation.
*B*. Combinations: We considered the following combinations of binding mechanisms from *A*: 1. Hash (Client's TLS nonce || Server's public key) 2. Hash (Client's Attestation nonce || Server's public key) 3. Hash (Client's Attestation nonce || Server's public key || Early exporter)/Question//for //discussion/: Is someone aware of any other combination that folks use in "rdata"? If possible, please share a link to specification and/or implementation.
# *Prominent Industrial Implementations* 1. Edgeless Systems Contrast [3]: uses binding mechanism *B2* 2. Cocos AI [4] 3. CCC proof-of-concept [5]: uses binding mechanism *B2* (Implementation of draft-fossati-tls-attestation) 4. Meta’s AI [1]: uses binding mechanism *A1*/Question//for //discussion/: Is someone aware of any other intra-handshake attestation implementation? If possible, please share a link to specification and/or implementation.
# *Binding Levels* 1. Shared DH secret (g^xy) 2. Client's handshake traffic key (htsc) 3. Client's application traffic key (atsc) # *Correlation Properties* * G1: Correlation of Evidence to Shared DH Secret * G2: Correlation of Evidence to Client’s Handshake Traffic Key (htsc) * G3: Correlation of Evidence to Client’s Application Traffic Key (atsc) # *Results* We proved the proposition: G3 => G2 => G1We discovered relay attacks in all above proposals for binding mechanisms as well as all implementations analyzed. We provide a formal proof of insecurity that all above binding mechanisms and implementations fail to even achieve G1 property (Level 1 binding).
Any binding that involves server's public key needs additional assumption that server's private key does not leak.
In general, all solutions fail when server's private key is leaked. In other words, extension of TLS with attestation in these implementations is not really bringing much benefit from a security perspective and rather giving a false sense of security.
We believe that it is not possible to achieve level 3 binding for intra-handshake attestation alone without breaking other TLS properties.
# *Implementation Issues* * Meta's AI uses client's TLS nonce (instead of attestation nonce), and hence does not provide Evidence freshness. * Cocos AI abuses the SNI extension to convey attestation nonce. * Edgeless Systems Contrast was abusing the SNI extension to convey attestation nonce, and currently abusing the ALPN extension to convey attestation nonce. # *Proposed Mitigation* * We propose a cryptographic binder and modify CertificateVerify message, which achieves level 2 binding. # *Paper and Artifacts*A paper is under submission and artifacts are well-documented. We will make the paper and artifacts public later on.
# *Cocos AI acknowledgment of attacks*This Friday Cocos AI (one of the implementers of the protocol) has publicly acknowledged [9] our email and the relay attacks we highlighted on their design and implementation in our email. Particularly, see the sections "Limitations and the Relay Attack" and "The Relay Attack Scenario" in [9]. Note that their description is almost a paraphrase of our email. There are some nits that we disagree with them but that doesn't matter much. They have essentially acknowledged the attacks and shared a short-term, medium-term and long-term plan for roadmap for the attacks. We believe this alone is sufficient supporting evidence.
# *Contributors*We thank Eric Rescorla, Juho Forsén, Markus Rudy, Mariam Moustafa, Tjaden Hess, Yuning Jiang, Pavel Nikonorov, Casey Wilson, and Martin Thomson for sharing their insights and providing valuable feedback.
# *Other related implementations within IETF* * Attested EDHOC: Our intuition (no formal proof yet) is that the attacks should apply to attested EDHOC protocol in intra-handshake attestation [6] as well -- at least for the case of Responder as Attester. We have informed LAKE WG [7] about these attacks. # *Feedback/Ideas*We look forward to your thoughts and ideas on how we can mutually progress this work forward towards secure solutions.
Best regards, Usama, Slava (Viacheslav), and Jean-Marie[0] https://datatracker.ietf.org/doc/bofreq-fossati-tls-exported-attestation-expat/
[1] https://ai.meta.com/static-resource/private-processing-technical-whitepaper
[2] https://github.com/trailofbits/publications/blob/master/reviews/2025-08-meta-whatsapp-privateprocessing-securityreview.pdf
[3] https://github.com/CCC-Attestation/meetings/blob/main/materials/MarkusRudy.contrast-atls-ccc-attestation.pdf
[4] https://docs.cocos.ultraviolet.rs/atls [5] https://github.com/ccc-attestation/attested-tls-poc [6] https://datatracker.ietf.org/doc/draft-ietf-lake-ra/ [7] https://mailarchive.ietf.org/arch/msg/lake/Tovtl7wgvzwJWT2I2ZwnhoIOnYQ/ [8] https://github.com/CCC-Attestation/formal-spec-id-crisis[9] https://web.archive.org/web/20260227160554/https://www.ultraviolet.rs/blog/tee-tls-privacy/
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
