[Ufmrg] Re: [Seat] Artifacts for formal proofs of insecurity of RA-TLS and draft-fossati-tls-attestation

[Muhammad Usama Sardar <[e-mail]>]

Hi UFMRG and SEAT,

Following up, the pre-print is available at [3]. We (i.e., I, Mariam 
Moustafa and Tuomas Aura) would once again like to thank the folks 
mentioned below for their valuable contributions.

We welcome any feedback/questions from the WG/RG.

-Usama

On 28.11.25 17:01, Muhammad Usama Sardar wrote:
>
> Hi UFMRG and SEAT,
>
> In line with the scope of SEAT charter, we (i.e., I, Mariam Moustafa 
> and Tuomas Aura) would like to share our formal analysis [0] of 
> attested TLS protocols for your review and feedback, and for further 
> research and development.
>
> We formally analyzed two of the most prominent attested TLS protocols:
>
>  1. Interoperable RA-TLS [1] (pre-handshake attestation)
>  2. draft-fossati-tls-attestation (TLS-attest) [2] (intra-handshake
>     attestation)
>
> using ProVerif and proposed some solutions for discovered security 
> vulnerabilities.
>
> We would like to take this opportunity to specially thank Ionut 
> Mihalcea who has contributed significantly in the discussions to make 
> the formalization very thorough and close to systems view. We also 
> want to specially thank Jean-Marie Jacquet, Thomas Fossati, Eric 
> Rescorla, Hannes Tschofenig, Yaron Sheffer, Laurence Lundblade, 
> Giridhar Mandyam, Christopher Patton, Jonathan Hoyland and Richard 
> Barnes for their valuable input.
>
> Several other folks at IETF/IRTF have given feedback during the last 
> 2+ years, which has helped us improve the quality of the artifacts. 
> Thank you all!
>
> We submitted the artifacts at AsiaCCS (Core rank A security 
> conference) as part of the paper review process and the paper has been 
> accepted for publication with very good reviews (3xaccept, 1xweak 
> accept). We will share the pre-print of paper soon.
>
> -Usama
>
> [0] https://github.com/CCC-Attestation/formal-spec-id-crisis
>
> [1] https://github.com/ccc-attestation/interoperable-ra-tls
>
> [2] https://datatracker.ietf.org/doc/draft-fossati-tls-attestation/
>
[3] 
https://www.researchgate.net/publication/398839141_Identity_Crisis_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS