[Seat] Regarding symbolic analysis of draft-fossati-seat-early-attestation-06

[Nathanael Ritz <[e-mail]>]

## Early take-away:

Based on Usama's models and the draft's specifications in section 5.1.1,
ProVerif demonstrates comprehensive resilience against any compromising key
leak, indicates strong injective-agreement between honest parties and does
not provide any indication of an exploitable path for relay, replay or
divergent attacks. The binding mechanism proposed by
draft-fossati-seat-early-attestation-06 appears to be a success.

---

Hi everyone,

Apologies to anyone who might have otherwise been looking, but I neglected
to include the footnotes for my last message. I've included them below.

Incidentally, while reviewing the repository for the artifacts that Usama
has shared, I noticed that the README was updated to suggest that
draft-fossati-seat-early-attestation-06 is represented by what the page
labels as "binder 7" [*].

There appears to be some confusion here: as "binder 7" composes the Early
Exporter Secret (`exp0`), an attestation nonce from the client (`ar`), and
the public half of the server's ephemeral signing key (`pubEK`) -> `rdata =
(ar,exp0,pubEK)`. This is not what draft-fossati-seat-early-attestation-06
specifies, as the draft calls for the value gathered from the
ClientHello...ServerHello checkpoint in section 5.1.1.

Fortunately, on line 671 of the symbolic model for "binder 7", we can see a
variable assigned to the same checkpoint that
draft-fossati-seat-early-attestation-06 calls for.

The useful variable is labelled as "Log_SH" with an annotation that reads:
(* after this step, log_SH contains sent ClientHello || received
ServerHello *) [2]. That makes updating the binder value to represent the
correct specification dramatically easy -> `rdata = (Log_SH,pubEK)`.

---

Now, as it turns out, I learned we can get isomorphic results in this model
by updating the original construction in "binder 7" from "(ar,exp0,pubEK)"
-> "(sr,exp0,mode,pubEK)" -- maybe that's why the README was updated in
this way. Regardless, since we have two interesting binding mechanisms to
explore, I have saved them as unique copies.

In either case, the queries from 'other-props.pvl' indicate that the
attestation signing key provides "compound authentication". That means that
even if both the long term "LTK" or even the TEE-bound ephemeral "EK"
signing keys are completely compromised, the model still demonstrates that
the protocol's expected security properties still hold under AK.

Since the original queries did not anticipate such systematic success
across the various security properties, I have gone ahead and updated the
other-props.pvl to individually examine the security properties for each
key in isolation.

---

That being said, the most recent model has a couple of structural
discrepancies from what draft-fossati-seat-early-attestation-06 specifies.

1. Namely, the draft only calls for a single key and recommends that it be
authenticated by a trusted 3rd party such as with a webPKI mechanism
2. The symbolic models introduce a dual CertificateVerify message to the
state machine that has no parallel in the individual I-D
3. The model includes an unchecked parameter in the Certificate (CRT)
message called `selfsign` that introduces a modeling artifact.

While the unchecked `selfsign` parameter is generally harmless, it
introduces a modeling artifact that affects the so-called "G3 (level 3)"
binding property. As such, I have duplicated the first two models and
introduced a change that removes that parameter from the CRT message. To
some, this may be interpreted as a structural change, which is why the
models are saved separately.

Finally, the models are configured to generate the ephemeral TLS signing
keys before they can be asserted by a trusted 3rd party. This causes all
queries that check for the security properties of EK to fail. However,
under normal day-to-day operations, one might expect that the ephemeral
signing keys would have been attested at least once and could be retained
in an existing cached AR.

Because a cached AR is signed by the Verifier's Attestation Results signing
key (ARK), it acts as a trusted 3rd party root-of-trust, much like webPKI.
As such, I have yet another model saved which demonstrates the practical
use of ephemeral signing keys beyond initial provisioning.

---

To make it easy to diff on gh, the original has been saved to
'broken_orig', while the initial files alongside the readme reflect the
"(sr,exp0,mode,pubEK)" construction, duplicated also in its own folder. The
binder actually specified by the -06 revision is found in 'ch-sh/...'. Each
model has light variations, but they all run the same identical expanded
query file other-props.pvl, with consistent and expected results from each.

I have included a README.md in the "binder7/ folder which illustrates the
success of the protocol design based on the listed specifications within
the models [3]. Note that I am not endorsing the original model's structure
but merely using it as an avenue to evaluate the binder mechanism proposed
by draft-fossati-seat-early-attestation-06. I hope this information is
helpful, and happy to follow-up with any questions.

Cheers,
Nathanael


[*]
https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/819bb7f20ac458b27c9be2c91cce1e72b8b5f4f7/README.md?plain=1#L32

[0] Original academic framing:
https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/f8b14af70a021fcfef5ebca683185f89b9d8f27a/README.md?plain=1#L82

[1] Complexity talking point from -04 announcement:
https://mailarchive.ietf.org/arch/msg/seat/2HfF4JjZbJhw-HJo1GbVTkUmeVU/

[2] The useful variable:
https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/f8b14af70a021fcfef5ebca683185f89b9d8f27a/binder7/tls-lib-simple.pvl#L671

[3] Formal analysis of Early Attestation -06
https://github.com/nathanaelritz/intra-handshake-paper/tree/early-binder7-patch/binder7


---------- Forwarded message ---------
From: Nathanael Ritz <[e-mail]>
Date: Fri, 7 Aug 2026 at 11:32
Subject: Re: [Seat] Re: FW: New Version Notification for
draft-fossati-seat-early-attestation-06.txt
To: [e-mail] <[e-mail]>


Hi, some comments are available inline with [NR]:

On Fri, 7 Aug 2026 at 02:46, Songbo Bu <[e-mail]> wrote:

> Hello Nathanael,
>
> Ironically, the approach to keep working on the solution without knowing
> the property is ad-hoc approach. As clarified before, the constructive
> purpose is to judge whether the complexity of intra-handshake attestation
> is required to satisfy some property. If we do not know the goal we are
> trying to achieve, how can we ever achieve it? So property is critical to
> SEAT success and this is surely a technical approach. Several members have
> supported this approach.
>

[NR]: I'm afraid this idea and the question which Usama introduced back
from the -04 announcement [0] assumes the premise. We have yet to establish
a baseline for what complexity means relative to any other approach, so the
premise has not been established. Regardless, I do not think there is some
zero-sum game here between attestation timing windows.

[NR]:  For example, I see viable use cases for both approaches as long as
the appropriate session binding value is selected and the appropriate care
is taken in applying the Evidence and Attestation Results appraisal
policies. Personally, I have identified the same potential pitfalls if
binding is misconfigured or if you rely on the ephemeral signing key for
CertificateVerify without a trusted 3rd party root of trust.


>
> Formally, attestation binder in section 5.1.1 of the draft-06 does not
> introduce anything new that needs a new formal analysis.
> Intra-handshake.fail and CVE-2026-33697 apply as is.
>

[NR]: This assertion is not supported by the statement offered in the
camera ready repository for the paper which merely suggests "that it may
not be possible to achieve strong application-traffic (level 3) binding
using intra-handshake attestation alone" [1]. It may be helpful for the WG
to understand why such careful language is now being set aside if nothing
new has been released to explain the change in approach.


>
> The fundamental misunderstanding you are having is that the book by Boneh
> and Shoup does not talk about attestation at all. The threat model for
> attestation is different from traditional authentication mechanisms. Part
> of the server is untrusted in attestation, which is not the case in
> traditional authentication mechanisms and hence your citation of the book
> and protocol 'AKE4' is completely irrelevant to this technical discussion.
>

[NR]:  I do not believe we are trying to (nor would we need to) weild any
new crypto ideas here. Instead, we are applying standard cryptographic
assumptions established by well studied mechanisms found in authenticated
key exchange mechanisms such as those used by TLS and composing remote
attestation on top of it with channel binding. Of which, provides a
concrete set of well understood properties. If a concrete attack against
such well-understood mechanisms exists, I would hope to see the technical
details shared.


>
> Both papers ID-Crisis and intra-handshake.fail present concrete
> counter-examples with complete technical details with open-source code,
> which apply to this draft.
>

[NR]: Again, this statement is completely unestablished. There is no
demonstration of failed injective-agreement in the subsequent transfer of
application data in either of these drafts, nor any demonstration that
would show that an attacker may have access to the application traffic keys
by way of the mechanisms proposed in the Early Attestation draft.
Furthermore, any security considerations and caveats I would apply
(including the importance of validating the TLS signing key via a trusted
third party) apply the same way regardless of the attestation timing
window, based on my own studies.


> Would we like to design a protocol that breaks if any single machine in
> the whole world breaks?
>

[NR]:  It seems this is a non-sequitor.


> It is unclear what you are trying to achieve by raising these questions.
>

[NR]: I hope the above makes the earlier feedback more clear.

Cheers,
Nathanael

[0]
https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/f8b14af70a021fcfef5ebca683185f89b9d8f27a/README.md?plain=1#L82

[1] https://mailarchive.ietf.org/arch/msg/seat/2HfF4JjZbJhw-HJo1GbVTkUmeVU/


>
>
> Best,
> Songbo
>
> Ionut Mihalcea <[e-mail]> 于2026年8月6日周四 18:49写道：
>
>> Hi,
>>
>> Agree with Tiru, quoting from the CVE: "Because the attestation evidence
>> is bound to the ephemeral key *but not to the TLS channel*, possession of
>> that key is sufficient to relay or divert the attested TLS session"
>> (emphasis mine), and also from Tiru's initial email: "the resulting binder
>> is unique to the connection (two-sided uniqueness). Evidence generated in
>> one connection therefore cannot be replayed in another."
>>
>> I also continue to disagree with the assumption that binding to or
>> correlation with the application traffic secret is the only possible secure
>> construction.
>>
>> Thanks,
>> Ionut
>>
>> *From: *tirumal reddy <[e-mail]>
>> *Date: *Thursday, 6 August 2026 at 10:27
>> *To: *Muhammad Usama Sardar <[e-mail]>
>> *Cc: *[e-mail] <[e-mail]>
>> *Subject: *[Seat] Re: FW: New Version Notification for
>> draft-fossati-seat-early-attestation-06.txt
>>
>> Hi Usama,
>>
>> CVE-2026-33697 was not established against this draft. The binders
>> analyzed in your paper differ from the one specified in Section 5.1.1 of
>> this draft, and the models in your paper seem to add a dual
>> CertificateVerify that this draft does not specify. The CVE is therefore
>> not demonstrated against draft-fossati-seat-early-attestation.
>>
>> If you maintain that it applies, please demonstrate the relay attack
>> against the binder as specified in Section 5.1.1: the
>> ClientHello...ServerHello transcript checkpoint plus the hash of the public
>> key of the attester's end-entity certificate used for authentication with a
>> standard CertificateVerify specified in TLS 1.3.
>>
>> We will review any concrete demonstration.
>>
>> Best Regards,
>> -Tiru
>> _______________________________________________
>> 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]
>