[Seat] Re: SEAT Architecture: Community models for intra- and post- TLS 1.3 handshake attestation using symbolic formal analysis

[Chengxin Huang <[e-mail]>]

Dear all,

In response to Mr. Ritz's formal models, every single time he has shared a
formal proof of [draft-intra], Sardar et al. have proved it to be wrong by
practically demonstrating it with a concrete attack path and certified by a
GHSA/CVE. Therefore, before I spend my precious time reviewing these
models, this raises the question that what is the guarantee that these
formal proofs will not be broken this time or what validation method has
been used to ensure that formal models are practically representative of
reality?

Adding "insecureSkipVerify" variant, Mr. Ritz provides a practical proof
that Usama and Songbo have made a [valuable-contribution] to his formal
models. It is not too late for Mr. Ritz to acknowledge their contribution
and write a public apology to them for the [paradox].

Can Mr. Ritz please share the diff of his proof from ESORICS-certified
[intra-handshake.fail] for review?

Best regards,
Chengxin Huang

[draft-intra]
https://datatracker.ietf.org/doc/draft-fossati-seat-early-attestation/06/
[intra-handshake.fail]
https://github.com/muhammad-usama-sardar/intra-handshake.fail
[valuable-contribution]
https://mailarchive.ietf.org/arch/msg/seat/BgPbNyx2HhQlUpQ6LHy9wXW3esw/
[paradox]
https://mailarchive.ietf.org/arch/msg/seat/upV8i1kPT-3jHTAYkUOjUA92sZE/

Nathanael Ritz <[e-mail]>于2026年9月3日 周四01:31写道：

> Hi SEATizens,
>
> A set of baseline models for the two prominent approaches to attested TLS
> 1.3 based on draft-early [INTRA] and draft-expat [POST], has been prepared
> and is available for review in the SEAT Architecture repository associated
> with the editor's copy of the individual Internet-Draft.
>
> Key verification highlights across both models:
>
> -  **Standard Key Schedule Compatibility (draft-early [0]):**
> Intra-handshake attestation maintains the standard RFC 8446 key schedule
> without custom HKDF labels or modified extractors. Handshake binding is
> established via public transcript integration of CH...SH (`log_SH`) and the
> TLS public key (`pubEK`), providing unconditional session correlation and
> demonstrating that altering the TLS 1.3 key schedule is completely
> unnecessary for formal session integrity.
>
> -  **Post-Handshake Binding Guarantees (draft-expat [1] with ALTEA
> [2,*] ):** Attestation binding via exported key material formally proves
> mutual agreement on Diffie-Hellman secrets (`gxy`), handshake keys (`kch`),
> and application traffic keys (`kc`). Full session correlation `(kc, ev)`
> holds under client-side validation against degenerate key share elements
> (`BadElement`).
>
> -  **Orthogonal Trust-Root Redundancy:** Server identity and platform
> attestation operate as independent trust paths.
>
>    ==> *No Degradation to Standard TLS 1.3 Guarantees:* Confidentiality,
> authenticity,
>            and session key secrecy remain strictly intact and decoupled
> from the Remote
>            Attestation trust boundary, ensuring standard channel security
> even upon complete
>            attestation collapse.
>
>    ==> *Remote Attestation Adds Compound Assurance:* When Remote
> Attestation
>            is valid and the TLS client rejects degenerate key shares
> (BadElement), aTLS
>            provides end-to-end transport confidentiality, key secrecy, and
> data authenticity
>            guarantees independent of any requirement for traditional
> WebPKI CA trust chains.
>
> - **Hostile Host Threat Modeling:** Verifies resilience against untrusted
> hypervisors, adversary-driven quotes, and multi-tenant credential
> substitution, enforcing parameter boundaries strictly through client-side
> validation.
>
> - **Negative testing via "insecureSkipVerify" variant.** A dedicated
> configuration for both major models strips out the attestation binder
> (`rdata = zero`) and omits reference measurement verification (e.g.,
> `dev_status1 = dev_statusRef`), modeling an insecure verification bypass
> implementation errors, debugging, or testing. These variants specifically
> serve as a contextual sanity check, proving the validity of the other
> associated model variants and their verified properties.
>
> - **Resilience Under Handshake Key Exposure:** Client application key
> confidentiality (`kc`) and session binding hold across both timing models
> even when handshake traffic keys (`kch`, `ksh`) are directly leaked to an
> active adversary.
>
> ==> Full results is available at [EARLY-Verification] and
> [EXPAT-Verification].
>
> ---
>
> Feedback or questions on the approach for both major models and their
> variants are welcome.
>
> Cheers,
> Nathanael
>
> [INTRA]
> https://github.com/tls-attestation/seat-architecture/tree/main/symbolic-models/aTLS/intra
>
> [POST]
> https://github.com/tls-attestation/seat-architecture/tree/main/symbolic-models/aTLS/post
>
> [EARLY-Verification]
> https://raw.githubusercontent.com/tls-attestation/seat-architecture/refs/heads/main/symbolic-models/aTLS/intra/draft-early/verification_results-early.log
>
> [EXPAT-Verification]
> https://raw.githubusercontent.com/tls-attestation/seat-architecture/refs/heads/main/symbolic-models/aTLS/post/draft-expat/verification_results_expat.log
>
> [0]
> https://datatracker.ietf.org/doc/draft-fossati-seat-early-attestation/06/
> [1] https://datatracker.ietf.org/doc/draft-fossati-seat-expat/03/
> [2] https://datatracker.ietf.org/doc/draft-reddy-seat-expat-transport/02/
> [3]
> https://www.ietf.org/archive/id/draft-reddy-seat-expat-transport-02.html#shim-mode
>
> p.s. For those curious about the properties of secure evidence and
> attestation transport over (other) secure transport channels, such as
> light-weight authenticated key exchange (LAKE), the symbolic models for
> LAKE RA have also been mirrored to the repository:
> https://github.com/tls-attestation/seat-architecture/tree/main/symbolic-models/LAKE-RA
> _______________________________________________
> Seat mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>