Verified cryptography for Firefox 57

Posted Sep 14, 2017 22:42 UTC (Thu) by roc (subscriber, #30627)
In reply to: Verified cryptography for Firefox 57 by ms
Parent article: Verified cryptography for Firefox 57

It's not just verified to be free of large classes of bugs, but it's verified to be a correct implementation (of Curve25519 in this case), i.e. it produces the correct answers for all inputs.

People who are interested should read about the overarching project: https://project-everest.github.io/

"Verified as unbreakable" is not yet present in this case, but it's a realistic goal for the future, for the right definition of the term. We are able to verify that various cryptographic protocols are "unbreakable", in the sense that if the endpoints implement those protocols correctly and certain algorithmic hardness results hold, then an adversary who can only observe and manipulate what's on the wire learns nothing about certain data (e.g. the contents of packets). Work like Everest can prove the correctness of the endpoint implementations. The hardness assumptions can only be defeated by an adversary who makes mathematical breakthroughs --- we're talking Fields Medal-worthy work --- or if you use too-small key sizes. Against verified crypto, plausible attacks will be either direct attacks against endpoints, or attacks that learn something other than what the protocol was protecting (e.g. packet timing instead of packet contents).

finally someone who knows what he's talking about

Posted Sep 14, 2017 23:20 UTC (Thu) by HelloWorld (guest, #56129) [Link] (1 responses)

Thank you for this interesting comment!

finally someone who knows what he's talking about

Posted Sep 15, 2017 8:35 UTC (Fri) by Wol (subscriber, #4433) [Link]

This is what I moan about when I say Science isn't Maths.

The whole point of a proof in maths is that it shows your assumptions are self-consistent.

The whole point of a proof in science is that it shows your assumptions are in line with reality.

And a lot of the comments here show that people have difficulty grasping the difference (yes, that seems to be the norm :-(

That's why, when you're presenting a proof like this, it's important to state all your assumptions (like the grandparent post does), but it's also why peoples' eyes glaze over because it's all maths and so many people seem to be scared of maths :-(

Cheers,
Wol

Verified cryptography for Firefox 57

Posted Sep 15, 2017 11:07 UTC (Fri) by ballombe (subscriber, #9523) [Link] (2 responses)

There is a big asymmetry here:
If you prove that ECDL cannot be solved in polynomial time in general, you will probably get the Field medal if you are young enough.
However, if you prove that ECDL can be solved in subexponential time, chance are you will not be awarded the Field medal.

Why ? because there a precedent for breaking similar algorithms, while there is no precedent for negative proofs
(this is an instance of the P=NP problem).

The truth is a large number of mathematicians expect ECDL to be solvable in subexponential time, so are unlikely to work toward proving the opposite.

Verified cryptography for Firefox 57

Posted Sep 15, 2017 13:34 UTC (Fri) by Wol (subscriber, #4433) [Link] (1 responses)

And how many of these things turn out to be solved almost by accident?

I think it was Fermat's, but I'm sure there have been several, where some mathematician presented a proof of something completely unrelated and then added, almost in a footnote, "by the way, Fermat's is a trivial subset of this proof".

I think everyone knew a big announcement was coming, but really didn't expect a Fermat proof to be announced and dismissed in such a trivial manner!

Cheers,
Wol

Verified cryptography for Firefox 57

Posted Sep 19, 2017 14:09 UTC (Tue) by gowen (guest, #23914) [Link]

I think it was Fermat's, but I'm sure there have been several, where some mathematician presented a proof of something completely unrelated and then added, almost in a footnote, "by the way, Fermat's is a trivial subset of this proof".

This was Wiles and Fermat, but its worth noting that reducing FLT to a footnote was a jokey way by Wiles to bury the lede. He knew what the big story was here, and everyone in the room (who were basically the worlds foremost minds on modular forms) knew the best-known implication of the Taniyama-Shinmura Conjecture - and hence where Wiles was likely to end up - well before that point. FWIW - I believe the lectures ended "Corollary: Fermat's Last Theorem"