2019.04.06 13:17:53 (1114487386191343617) from Daniel J. Bernstein:
Another example of how easy it's becoming to deploy cryptographic software formally verified to be bug-free: https://www.microsoft.com/en-us/research/blog/evercrypt-cryptographic-provider-offers-developers-greater-security-assurances/ As in NaCl, the only public-key option is ECC, and the only curve is Curve25519. Asking for RSA-2048 for "algorithm agility" = asking for bugs.
2019.04.06 13:32:43 (1114491119763693568) from Daniel J. Bernstein:
It's unfortunate that Microsoft's EverCrypt advertising doesn't highlight the impact of design choices in cryptographic functions. (They even pick a picture with special cases that 25519 eliminates!) This is even more important for verifying more complex post-quantum software.