Hi Usama, > On Nov 16, 2025, at 4:20 AM, Muhammad Usama Sardar > <[email protected]> wrote: > > If I understood correctly in the meeting, the authors have some ongoing > formal analysis but I could not find anything in the repo [0]. Could you > please point me to the repo where the formal analysis is being done?
We initiated analysis by extending the base TLS 1.3 model in ProVerif that was used for analyzing ECH. It requires some polish before putting on GitHub, though I’ve not had capacity to do that work. When it’s done, I will update this thread. > From the formal analysis perspective, is there something specific other than > the open issue mentioned in section 8.4 that you need help with? Yes, that is the primary property we need to confirm through analysis. Best, Chris > > -Usama > > [0] https://github.com/tlswg/tls-pake > > _______________________________________________ > TLS mailing list -- [email protected] > To unsubscribe send an email to [email protected] _______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
