[CFRG] Re: Formal artifacts for attested TLS binding analysis

[Songbo Bu <[e-mail]>]

Hi CFRG,

I fully support the results and the technical direction of this work.

I have also participated in the related SEAT and UFMRG discussions, so
I have been following the broader question of what security properties
different attested TLS constructions are intended to provide.

My reading of the public artifacts is that their main value is to make
the cryptographic binding question more precise. Instead of treating
"attestation is bound to the connection" as a single undifferentiated
property, the artifacts separate different levels of binding and make
clear which properties can be obtained.

I think this is relevant to CFRG because these questions are
fundamentally about cryptographic binding: what is bound into the
attestation evidence, what is bound to TLS exporter-derived material,
what the verifier is required to check, and what security property
follows from those checks. This seems especially important when
comparing intra-handshake, post-handshake, and hybrid attestation
designs, because the comparison depends on the exact cryptographic
property being claimed, not only on where the protocol messages
appear.

I also have a few README-level suggestions that may make the artifacts
easier for new readers to follow:

- Add a short "what this repository shows" summary at the beginning.
- Add a reader guide explaining which files to inspect first.
- Add a table mapping each binding level to the corresponding security
goal, model file, and expected result.
- Add a minimal reproduction path with the main commands and expected outputs.
- Define the binding-level terminology before comparing it with
related work or draft mechanisms.

Overall, I think the artifacts are valuable because they turn a vague
discussion about attested TLS binding into concrete cryptographic
properties, assumptions, and review questions.

Best regards,
Songbo