On Thu, Apr 30, 2026 at 10:27:58PM +0200, Muhammad Usama Sardar wrote: > Hi Ilari, > > > In addition, I was a bit surprised to see the word 'dangerous' for which I > have a related formal analysis based on which FWIW, I deem what Scott has > described to be secure at the /symbolic/ (not /computational/) level. So I > would like to understand what I have got wrong in my analysis.
Sure, it is secure under some assumptions. However: - Do the assumptions hold in practice? - Is the RP implementing the required policy correctly? > I acknowledge that symbolic analysis has limitations. Has 'dangerous' got > something to do with cryptography? Do you recommend getting confirmation via > computational proof in tools like CryptoVerif? or do you have an intuition > where the proof will break at the computational level? It does not have anything to do with cryptography itself. It is practical design and implementation stuff. Continuing the "poorly thought out or risky designs" comment, those are almost never stuff protocol-level formal analysis would be expected to catch. -Ilari _______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
