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

[Steve <[e-mail]>]

Dear all,

>From cloud-security industry perspective, Cloud Security Alliance (CSA-GCR)
community reviewed and discussed the paper and its supporting open-source
code at commit f8b14af70a021fcfef5ebca683185f89b9d8f27a, and strongly
supports both. We also followed the recent exchange on list and watched
some videos and explored slides in repo and draft-intra-handshake-fail.

As several other WG/RG members have implied, I found concerns of Nathanael
lacking substance and I completely agree with the explanations provided by
the authors:

1. Handshake Secret and server/client_handshake_traffic_secret are two
different keys (see Figure 5 of RFC9846).
2. Removing `CV_Ext` results in diversion attacks due to lack of
proof-of-cloud. Putting `pubLTK` and `ID_S` does not help because both are
public and hence known to the adversary.
3. Reusing keys, such as Handshake Secret, from TLS 1.3 key schedule
directly in `rdata` is highly dangerous because it needs to expose TLS 1.3
keys. Same applies to the proposal for using `kch` and `ksh`. I agree TLS
1.3 computational proofs would almost surely break here.
4. ProVerif is abstract symbolic modeling and never "wired up in real
implementations".
5. Additional Derive-Secret stage for proposed exporter is required for
isolation. This is well-proved via formal analysis of TLS 1.3.
6. Standard exporter of RFC9846 is irrelevant for formal analysis of
intra-handshake attestation.
7. `kdf_es` is correctly modeled, including both `exp0` and `ems0`.
early_exporter_secret `ems0` is not discarded. early_exporter_secret `ems0`
has absolutely nothing to do with the standard exporter.
8. Correlation properties do not need any assumption. Their unique purpose
is to check binding and not correspondence.

However, there is a potential ambiguity. I suggest the authors clarify
explicitly in paper/repo that:
1. The current formal analysis is only for non-PSK-based handshake. For
checking correlations as defined by the authors, considering PSK-based
handshake is not necessary but should be explicit. Section 3 of ID-Crisis
paper mentions this explicitly but intra-handshake.fail paper and
supporting repo does not appear to explicitly mention it.

As several other WG/RG members have implied, I suggest Nathanael to:
1. not reinvent the wheel from scratch, rather build on top of well-vetted
and battle-tested code of AsiaCCS and ESORICS.
2. Maybe work collaboratively with Usama's team rather than nitpicking.
Formal models are abstract and not bit-by-bit compatible with the code.
There is no doubt of the immense value this paper and supporting code has
brought to the WG. What can be more convincing than the fact that all
stakeholders of intra-handshake attestation have acknowledged
vulnerabilities and created security advisories, CVE, or declared repo
vulnerable and archived and withdrawn draft?
3. Clearly show one exact value of `rdata` and do a computational proof for
his proposal on `hs` or `kch` and `ksh` in `rdata` and share with the
WG/RG. Symbolic analysis is obviously insufficient for this.
4. Identify a security property in ProVerif that hybrid intra- and
post-handshake attestation can satisfy, but post-handshake attestation
alone cannot satisfy before considering adding the complexity in handshake
when post-handshake attestation is required for continuous attestation
anyway. Formally, model and security property are two separate things. The
question on security property in ProVerif cannot be resolved by modifying
the model. That question is still open and crucial to answer.

I strongly support using the paper and code as a reference point for
further SEAT discussion. Congratulations on the excellent work and thank
you for giving the WG a rock-solid foundation to formally evaluate the
proposals rather than handwaving!

Looking forward to the paper on CVEs of 9.1 ;)

Best regards,

Steve

Research Analyst, Cloud Security Alliance (CSA-GCR)

Chengxin Huang <[e-mail]> 于2026年8月3日周一 23:02写道：

> Hello everyone,
>
> Following the discussion, I strongly support the analysis by Sardar et al.
> as before. I would like to add that it's not only Confidential Computing
> Consortium, Sardar et al. seem to have gone to every part of the world
> except China and to every relevant forum known to me to discuss the topic
> and the formal models:
> https://github.com/CCC-Attestation/formal-spec-id-crisis#upcoming-and-recent-talks-and-research-visits
> and
> https://github.com/muhammad-usama-sardar/intra-handshake.fail#upcoming-and-recent-talks-and-research-visits.
> AsiaCCS and ESORICS are top security conferences that I trust as well. We
> should definitely benefit from their several years of effort and various
> attacks that they have discovered. Starting from scratch is not a good use
> of WG time.
>
> I reviewed Sardar et al.'s artifacts at commit
> f8b14af70a021fcfef5ebca683185f89b9d8f27a. As of now, there is no technical
> change after this commit. The only changes are in README on presentation
> and clarification. I am pretty confident that the models accurately model
> TLS, attestation and the confidential computing threat model and explain it
> nicely in their paper. As I mentioned previously, I found the binding
> levels as the most useful insight in the paper. The modularity and
> flexibility of the artifacts is the key advantage. I could easily try out
> different binders by trying out different values of rdata, all failing to
> achieve level-3 binding.
>
> Similar to Haowen and others, I also agree with all the clarifications
> provided by Sardar et al. Handshake secret and handshake traffic secret are
> indeed different in TLS 1.3 key schedule and they have correctly modeled
> both. Removing proof-of-possession of cloud provider owned key leads to
> diversion attacks to anywhere in the world, as already demonstrated in
> AsiaCCS paper. They are correct that reusing same keys for multiple
> contexts is a cryptographic problem that can be demonstrated by
> computational tools, like EasyCrypt. I have never seen ProVerif code wired
> up in real implementation and would like to see a concrete reference. I
> don't see any technical problem in authors' proposed derivation of
> cryptographic exporter, except that it is not allowed by the charter.
> Standard exporters of RFC9846 are surely out of scope of intra-handshake
> attestation. The derivation of early_exporter_secret ems0 and early
> exporter value exp0 is correct in ProVerif. The paper's conclusion 'may not
> be possible' is not refuted by completely modifying the model and showing
> that it is possible. Hence, I don't view it as a genuine counter-example.
> In my view, paper stands correct in its entirety, and all claims are
> justified.
>
> I agree with Haowen and the following acknowledgments of intra-handshake
> attestation maintainers and proponents are more than sufficient evidence
> for me on the credibility of the work:
>
>    -
>
>    Meta: https://www.cve.org/CVERecord?id=CVE-2026-33697
>    -
>
>    Cocos AI:
>    https://github.com/ultravioletrs/cocos/security/advisories/GHSA-vfgg-mvxx-mgg7
>    and https://www.cve.org/CVERecord?id=CVE-2026-33697
>    -
>
>    Edgeless Systems:
>    https://github.com/edgelesssys/contrast/security/advisories/GHSA-hjgc-jc5v-fw7h
>    -
>
>    Confidential Computing Consortium reference implementation of
>    intra-handshake attestation declared vulnerable and archived:
>    https://github.com/CCC-Attestation/attested-tls-poc/pull/58
>    -
>
>    Vulnerable draft-fossati-tls-attestation withdrawn:
>    https://datatracker.ietf.org/doc/draft-fossati-tls-attestation/10/
>
> I would like to add an implementation-oriented observation. Moving
> Evidence into the handshake is not merely a change in message placement. It
> requires Evidence to be available while the handshake is in progress and
> introduces interactions with transcript state, key state, failure handling,
> retransmission or retry behavior, and implementation-specific handshake
> logic. In particular, signature is costly and this adds additional
> handshake completion time, which is clearly a security problem in itself.
>
> That additional machinery may be justified for some specific use cases,
> but the benefit should be stated concretely. As many other fellows have
> asked, my ask for Nathanael is a security *property* that:
>
>    -
>
>    the hybrids can satisfy
>    -
>
>    post-handshake attestation alone cannot satisfy If there is no such
>    property, taking a risk of high-severity vulnerabilities appears to be
>    unjustified only useful for some niche use cases. I am pretty confident
>    that post-handshake attestation can achieve level-3 binding if EKM is
>    included in the binder.
>
> One suggestion I have for authors is that cryptographic proof in S. 6.4 of
> paper is a good starting point for cryptographic strength, but it is
> nothing more than that. In particular, a computational proof of security
> needs more work. The future work in S.9 of paper mentions 'computational
> analysis' but it falls short of discussing what tools would be used. Would
> it be paper-and-pen proof? I suggest to use computerized tools, such that
> the community can build on top of that.
>
> I also eagerly look forward to the claimed CVEs of CVSS 9.1 whenever the
> responsible disclosure concludes. Maybe they are in this weird situation
> that they want to help the WG but they can't yet disclose all what they
> want to say. This is understandable and I have sympathies with them. But
> the evidence that they have already provided is much more than sufficient
> for the WG as a pretty solid foundation.
>
> Best regards, Chengxin Huang
>
>
> On Mon, Aug 3, 2026 at 8:46 PM Song Haowen <[e-mail]>
> wrote:
>
>> Dear all,
>>
>> It's surely helpful for the WG to use Usama's artifacts which have been
>> deeply discussed in the Confidential Computing Consortium (I have watched
>> the recordings mentioned in the GitHub repository:
>> https://github.com/muhammad-usama-sardar/intra-handshake.fail#upcoming-and-recent-talks-and-research-visits and
>> CCC list archives) and have gone through reviews from several top security
>> conferences that I trust, such as AsiaCCS and ESORICS. It is surely an
>> untiring effort of several years to go to the nitty gritty details of the
>> key schedule. Thus, I do not see value in Nathanael's artifacts to reinvent
>> the wheel from scratch.
>>
>> I have reviewed Usama's paper and artifacts in thorough detail. ProVerif
>> artifacts provide the WG a concrete security property as a baseline for
>> evaluation of proposals. The system model and threat model are justified
>> for the confidential computing scenario, which is the fundamental use case
>> of attested TLS and which is where I would like to use it. All useful
>> binding mechanisms are considered. Other binding mechanisms will give
>> similar results, because intra-handshake is fundamentally limited unless we
>> change TLS 1.3 drastically. If someone disagrees, one has to show the
>> concrete value of rdata that I can put in ProVerif and check myself on
>> Usama's artifacts. I appreciate the flexibility of Usama's artifacts that
>> doing such an analysis is quite easy.
>>
>> From the GitHub repository, it is clear that all vendors and proponents
>> of intra-handshake have acknowledged vulnerabilities highlighted in the
>> paper:
>>
>>    - Ultraviolet Cocos AI:
>>    https://github.com/ultravioletrs/cocos/security/advisories/GHSA-vfgg-mvxx-mgg7
>>     and https://www.cve.org/CVERecord?id=CVE-2026-33697
>>    - Edgeless Systems:
>>    https://github.com/edgelesssys/contrast/security/advisories/GHSA-hjgc-jc5v-fw7h
>>    - Meta: https://www.cve.org/CVERecord?id=CVE-2026-33697
>>    - Confidential Computing Consortium reference implementation of
>>    intra-handshake attestation:
>>    https://github.com/CCC-Attestation/attested-tls-poc/pull/58
>>    - Vulnerable draft-fossati-tls-attestation withdrawn:
>>    https://datatracker.ietf.org/doc/draft-fossati-tls-attestation/10/
>>
>> It is also clear that it is the most severe vulnerability, crossing all
>> other vulnerabilities in the literature of confidential computing, and
>> requiring no physical access:
>> https://github.com/muhammad-usama-sardar/intra-handshake.fail#comparison-with-other-vulnerabilities-in-confidential-computing-literature
>>
>> I also agree with all the clarifications provided by Usama et al. The
>> distinction between handshake secret and handshake traffic secrets is
>> indeed critical in TLS 1.3 key schedule. Certificate is public information.
>> Anyone can have it. You can use my certificate. The private information
>> must be used to create proof-of-possession. Removing this, we have no
>> guarantee on the cloud provider and diversion attacks of AsiaCCS paper by
>> Usama et al. apply. Reuse of keys for multiple contexts is a well-studied
>> cryptographic problem and can only be seen in a computational analysis
>> tool. So I am completely unconvinced by Nathanael's proposal of using
>> secrets from key schedule directly in the binder. As authors clarified,
>> ProVerif code is not wired up in real implementation at all. Authors'
>> derivation of cryptographic exporter is cryptographically correct. As
>> others pointed out, we have used similar derivation for early and standard
>> exporters in TLS 1.3 for a decade, and no CVE is yet known to my knowkedge.
>> Nathanael has to show a concrete attack trace if he sees one. I haven't
>> seen that yet. Reading the paper title should make clear that the paper is
>> about intra-handshake, and thus Nathanael's point on standard exporters in
>> RFC9846 is moot. I confirm that early_exporter_secret ems0 is correctly
>> generated in ProVerif, and the authors' choice for the macro to return
>> early exporter value exp0 is perfectly valid because ems0 is never
>> required other than simply generating exp0. PSK input is indeed always
>> there in the key schedule of TLS 1.3 (Figure 5 of RFC9846), regardless of
>> whether it is PSK-based handshake or not. Of course, early_exporter_secret
>> ems0 has nothing to do with the standard exporter at all. Presenting a
>> weird "counter-example" to the paper's conclusion of 'may not be possible'
>> does not falsify the 'may' and is thus not a counter-example at all.
>> Drastically changing the system model and the threat model will surely lead
>> to different results. Authors are making claims in the context of
>> confidential computing.
>>
>>
>> Muhammad Usama Sardar <[e-mail]>
>> 于2026年7月29日周三 04:37写道：
>>
>>> 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:
>>>
>>>    1. 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.
>>>    2. 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]
>>>
>> _______________________________________________
>> Seat mailing list -- [e-mail]
>> To unsubscribe send an email to [e-mail]
>>
> --
> Ufmrg mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>