[Seat] Re: Comments on formal analysis of relay attacks in attested TLS (CVE-2026-33697)

[camilo ayerbe <[e-mail]>]

Hi all,

I'd like to add one point from an independent angle, and be clear about
what it does and doesn't claim. For disclosure, I'm a co-author of TRIP
<https://datatracker.ietf.org/doc/draft-ayerbe-trip-protocol/>, which is
post-handshake, so I have a stake here.

The CVE stands on its own — the relay on the self-asserted-key binders is
real, and the response to it was right. From the timeline shared
<https://github.com/muhammad-usama-sardar/intra-handshake.fail#detailed-vulnerability-disclosure-timeline>,
I see that all the relevant stakeholders have acknowledged the relay
attacks:

   -

   Cocos AI created the security advisory
   <https://github.com/ultravioletrs/cocos/security/advisories/GHSA-vfgg-mvxx-mgg7>
   and acknowledged the formal analysis
   -

   CCC Intra-handshake attestation implementation
   <https://github.com/ccc-attestation/attested-tls-poc> has been
declared vulnerable
   to relay attacks,
   <https://github.com/CCC-Attestation/attested-tls-poc/pull/58>and the
   repository has been archived.
   -

   Vulnerable intra-handshake draft draft-fossati-tls-attestation
   <https://datatracker.ietf.org/doc/draft-fossati-tls-attestation/10/> has
   been withdrawn by authors.
   -

   Edgeless Systems has created the security advisory
   <https://github.com/edgelesssys/contrast/security/advisories/GHSA-hjgc-jc5v-fw7h>
   and acknowledged the formal analysis.



On the question the thread is actually asking —whether a hybrid intra+post
design gives a security property post-handshake alone cannot — I modeled
the specified §5.1.1 (CA-backed TIK) of
draft-fossati-seat-early-attestation-05 binder independently and landed
where Usama and all others in the thread have: I couldn't find a property
achievable in intra-handshake that a post-handshake step right after secure
channel establishment couldn't also achieve. So I'm not offering a
counter-example — if anything, my look supports the "no separation"
reading, and it leaves the open question where Songbo has put it: what does
the intra-handshake version establish that post alone doesn't? If there is
no such property, the complexity of intra-handshake is unnecessary, which
is itself a security problem that I would like to avoid for my draft. I'd
also agree the symbolic security analysis doesn't settle the computational
questions raised here — proof-of-possession for a key placed in report
data, and cryptographic key-separation for reusing TLS-derived secrets both
need more than symbolic security analysis. I'd leave those open.

The dimension I'd add is *continuity*, as an architectural requirement
rather than a formal property. An intra-handshake binder attests once, at
setup; for use cases where the peer's measured state can change over the
life of the connection, that single attestation goes stale, and only
post-handshake — repeated or interval — attestation keeps it fresh. This is
the case TRIP is built around, and a one-shot intra-handshake binder
structurally can't provide it. I raise it because it points the same way as
the thread: post-handshake is the load-bearing mechanism, and for these use
cases it isn't optional.


Thanks, Camilo


On Thu, Jul 30, 2026 at 11:48 AM Songbo Bu <[e-mail]> wrote:

> Hi all,
>
> I agree with the clarifications in Usama's message. The question is
> not whether a modified construction can satisfy selected correlation
> properties under its own assumptions. My question was whether a hybrid
> intra- and post-handshake design establishes a specific security
> property that post-handshake attestation alone cannot establish.
>
> The public artifact separates three correlation goals: Evidence with
> the DH shared secret (G1), the client handshake traffic key (G2), and
> the client application traffic key (G3). It shows that its proposed
> intra-handshake construction establishes G1 and G2 but not G3. The
> artifact does not model a hybrid design against a post-handshake-only
> baseline, so it does not demonstrate a hybrid-over-post separation.
>
> For that reason, I think a claimed counter-example should state:
>
> 1. the exact property satisfied by hybrid but not post-only;
> 2. the identical adversary, trust, and deployment assumptions under
> which both are compared;
> 3. the exact statement in Section 9 that the result contradicts; and
> 4. the endpoint events and correspondence query used to establish the
> separation.
>
> Without that separation, changing the construction may still produce a
> useful design, but it does not answer the question I posed. It also
> leaves the additional intra-handshake machinery—Evidence availability
> during the handshake, interaction with transcript and key state, new
> failure paths, and implementation burden—without a demonstrated
> security benefit over post-handshake attestation alone.
>
> I also agree that two questions should be evaluated separately from
> symbolic equality. Placing an infrastructure public key or identity in
> signed report data does not by itself prove possession of the
> corresponding private key. Reusing TLS-derived traffic keys for
> another purpose also needs an explicit key-separation and
> computational-security justification. These questions are not settled
> merely because a symbolic model can express an equality.
>
> This does not rule out operational reasons for a hybrid design. It
> asks that operational motivation be separated from the claimed
> security property, and that the latter be stated in a form that can be
> formally verified. ProVerif code is never wired up in real
> implementations.
>
> On Tue, 28 Jul 2026 15:37:02 -0600, Nathanael Ritz <[e-mail]>
> wrote:
> > Top posting. It appears I have been asked to set aside falsifiable
> formal analysis effort or to suggest that such work is itself
> unfalsifiable. While that may or may not be true, I believe this thread has
> truly run its course.
> >
> > Sincerely,
> >
> > Nathanael
> >
> > On Tue, 28 Jul 2026 at 14:37, Muhammad Usama Sardar <
> [e-mail]> wrote:
> >
> > Hi Nathanael,
> >
> > Markus kindly clarified what he would like to see in more detail.
> > Could you please do the same to help keep this discussion more
> > focused? Here is my understanding of the points where you
> > disagree:
> >
> > - While the paper [6] claims it 'may not be possible' to achieve
> > level 3 binding in intra-handshake attestation, you believe it
> > is possible. Setting aside what you model and prove is correct
> > or not, I don't see how this contradicts the claim 'may not be
> > possible' in the paper.
> >
> > - We haven't yet seen a property that the hybrid construction
>
> > (intra- + post-handshake attestation) can satisfy, but
> > post-handshake attestation alone cannot satisfy, unless
> > you are implicitly implying that level-3 binding cannot be
> > achieved by post-handshake attestation. Please clarify
> > explicitly.
> >
> > Is there something I have missed? As mentioned before to Markus,
> > I believe it is much more organized to have them answered in
> > detailed technical report. So more important than the discussion
> > below is the correction/addition/edits in above statements.
> >
> > Also, I believe it will be more constructive to respond point by
> > point to [5] where you disagree, so we can do further working to
> > share with the WG/RG.
> >
> > We will then work on it and share with the WG/RG.
> >
> > On 28.07.26 20:51, Nathanael Ritz
> > wrote:
> >
> > On Tue, 28 Jul 2026 at
> > 10:00, Muhammad Usama Sardar <[e-mail]>
> > wrote:
> >
> > This does not address any of the questions in [5]
> > where your working was shown to be not correct, and
> > these inaccuracies still remain here too.
> >
> > [NR}: I disagree, but the authors are welcome to cite
> > my work and my words directly in relationship to any
> > questions that are, in their opinion, left unanswered so
> > that I can address them directly rather than guessing.
> >
> > For example, our responses to your #2 in [5].
> >
> > For clarity, nothing has changed in the key schedule
> > of TLS 1.3 for quite long time (I think draft-20 which
> > became RFC8446). Saying that RFC9846 is "new work" for
> > key schedule is almost surely wrong. Maybe Ekr can
> > confirm.
> >
> > [NR]: If it is being stated that I am suggesting
> > RFC9846 includes 'new work for key schedule', please quote
> > me directly, as I am currently unclear to what context and
> > statements are being referenced to right now.
> >
> > Thanks for clarifying. 'non-conformant Key Schedule' and then
> > mention of RFC 9846 §7.5 was unclear for #2 in [5]; it has stayed
> > the same for pretty much a decade. We believe that both points in
> > your #2 about key schedule are not valid and we justified it
> > technically in [5], to which we have seen no response.
> >
> > Best regards,
> >
> > Usama, Slava, and Jean-Marie
> >
> > [5]
> https://mailarchive.ietf.org/arch/msg/seat/dKVqaL8RJSQLonIEmtzrDYEXEAU/
> >
> > [6]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS
>
> _______________________________________________
> Seat mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>