I have consolidated my current analysis of the TLS 1.3 key schedule in this pre-print [0]. I have organized it as one section (1.3) independent of ProVerif and the other section (1.4) maps to it such that those with no knowledge of ProVerif can also see how intuitive the mapping is.

Some of the PSK part is still a mystery to me. That needs a careful review.

I welcome any thoughts or comments on how it can be improved, such that it can serve as reference formal artifacts for TLS 1.3 key schedule.

I started work on provision of functionality of ExtendedKeyUpdate in my model but that is subject to precise clarifications [1]. In my understanding, ProVerif alone will be insufficient. I think it additionally needs a computational analysis, but I have no experience with that.

-Usama

[0] https://www.researchgate.net/publication/396245726_Perspicuity_of_Attestation_Mechanisms_in_Confidential_Computing_Validation_of_TLS_13_Key_Schedule

[1] https://github.com/tlswg/tls-key-update/issues/59

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]

Reply via email to