HACL* implementation of Curve25519, verified in F*, made it into NSS! https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/ … Bonus: 20% faster on 64-bit architectures.
-
Show this thread
-
Reciprocal in C (not so different from handwritten C): https://github.com/mitls/hacl-star/blob/master/snapshots/hacl-c/Curve25519.c#L353 … Decomposed and proved in F*:https://github.com/mitls/hacl-star/blob/master/code/curve25519/Hacl.Bignum.Crecip.fst#L424 …
1 reply 1 retweet 2 likesShow this thread
Replying to @xEFFFFFFF
You're comparing it to DJB-style C code, which is hard to decipher. Better compare to https://github.com/briansmith/ring/issues/500#issuecomment-300939066 … or the C equivalent instead.
0 replies
0 retweets
2 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.