On 18 Jul 2021, at 07:00, Hugo V.C. <[email protected]> wrote: > > This sounds even better... Thanks Alex. > > El sáb., 17 jul. 2021 22:57, Axel Heider <[email protected]> escribió: > >> Hugo, >> >> last year Leonard Blazevic did his master thesis at Hensoldt Cyber >> about this, see >> https://tumanager.ei.tum.de/service.php?token=lifecycle_sec_tueilnt&mode=pdfdownload&tId=330&language=en >> I've put him in CC.
Just keep in mind that for crypto, while functional correctness is one (very strong) property, it isn’t the whole story. The other important parts are cryptographic safety (which for AES is well understood) and security from side-channel attacks, which depend on implementation choices and is much harder to prove. Having a functional correctness proof of a well-understood crypto scheme is definitely something extremely desirable, I’m just trying to raise awareness to the limitations to avoid disappointment and reputational damage – just imagine the headlines “‘proved secure’ crypto code hacked”. Gernot _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
