Hmm. I didn't expect this announcement this soon - at least on the public mailing list, the notion of a winner still seemed very far away. Just 18 days ago: <a href="https://groups.google.com/forum/#!searchin/crypto-competitions/phc$20winners/crypto-competitions/E99ZyJATo6E/plkmr4sQQ8QJ" rel="nofollow">https://groups.google.com/forum/#!searchin/crypto-competitio...</a><p>Anyway, as best as I could tell, the consensus on the public mailing list was that the best case for a singular winner would be an amalgamation of four finalists: Argon2, Lyra2, Catena, and yescrypt. Each of them has some properties that are desirable. I'm curious to what extent Argon2 will be modified - and especially curious if the final spec will have tunable parameters / multiple modes or be a one-size-fits-all deal.<p>Edit: If you're interested in more information, a decent starting place is this paper: <a href="https://eprint.iacr.org/2014/881.pdf" rel="nofollow">https://eprint.iacr.org/2014/881.pdf</a> If you folks want more reading material, I can pull some emails from the mailing list
Here is the spec for the winner: <a href="https://password-hashing.net/submissions/specs/Argon-v2.pdf" rel="nofollow">https://password-hashing.net/submissions/specs/Argon-v2.pdf</a>
For those like me that weren't aware of this competition here's their website with more info <a href="https://password-hashing.net/" rel="nofollow">https://password-hashing.net/</a>
Impressive stuff. One of the features of the winner is that you can offload the expensive computation to a client and still maintain the security you would have if it were done on the server. This should hopefully persuade people to use slow hash functions where they otherwise would not due to performance concerns.
What tools are typically used to develop these algorithms? The site has <a href="https://password-hashing.net/faq.html#qd" rel="nofollow">https://password-hashing.net/faq.html#qd</a> which mentions attempts to formally define the security of a good algorithm though a quick scan of the two papers indicates the definitions are mathematical properties described in English. However, when it comes to implementations is there a generally accepted language/framework in which correctness can be proven? Haskell comes to mind as one such language which its proponents tout as ensuring correctness, though I lack the experience to determine whether this means "your broken algorithm runs 100% correctly" vs. "a broken algorithm will not compile".