[Lake] From formal analysis of attested TLS to attested EDHOC

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

Hi all,

In Montreal, I had very interesting discussions with Marco and Göran on 
how to make my formal analysis more flexible and useful for EDHOC. 
Following up on these discussions, we (i.e., I, Mariam Moustafa and 
Tuomas Aura) would like to share our paper [0] and formal analysis [1] 
of attested TLS protocols for your review and feedback, and for further 
research and development towards attested EDHOC. In particular, our 
approach takes security goals of remote attestation and TLS separately 
(cf. Sec. 5.1 in [0]), such that TLS security goals can be replaced by 
EDHOC security goals in the future. We are thinking on the lines of 
making the protocol model modular as well, such that TLS protocol model 
can be replaced by EDHOC protocol model. We are particularly interested 
in feedback in this direction. This approach also seems well-aligned 
with lake charter stating:

  *

    Remote attestation of EDHOC peers, reusing as much as possible available
    work from the RATS and TLS working groups.

Perhaps we should add SEAT WG there as well.

In our paper [0], we formally analyzed two of the most prominent 
attested TLS protocols:

 1. Interoperable RA-TLS [2] (pre-handshake attestation)
 2. draft-fossati-tls-attestation (TLS-attest) [3] (intra-handshake
    attestation)

Analysis of [3] may be particularly interesting for this WG because 
draft-ietf-lake-ra has been following this draft (except for the 
post-handshake part). Several slides and videos/recordings are already 
available in README in [1].

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). So we are 
pretty confident that our approach will provide a firm basis for formal 
analysis of attested EDHOC.

One limitation is that it currently has Server as Attester. Analysis for 
Client as Attester is planned, and that should then be directly useful 
for attested EDHOC (Initiator as Attester).

We welcome any feedback/questions related to the paper, artifacts and 
the overall plan to move towards attested EDHOC.

-Usama

[0] 
https://www.researchgate.net/publication/398839141_Identity_Crisis_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS

[1] https://github.com/CCC-Attestation/formal-spec-id-crisis

[2] https://github.com/ccc-attestation/interoperable-ra-tls

[3] https://datatracker.ietf.org/doc/draft-fossati-tls-attestation/

PS: For any follow-up, please keep me explicitly in To/CC. I am 
currently overwhelmed with SEAT work and currently not following this list.