Tools for proofs

Security proof  for even simple cryptographic systems are dangerous and ugly beasts. Luckily, they are only rarely seen: they are usually safely kept in the confines of ``future full-versions'' of papers, or only appear in cartoon-ish form, generically labelled as ... ``proof sketch". 

The following two quotes frame the problem in less metaphorical terms. 

``In our opinion, many proofs in cryptography have become essentially  unverifiable. Our field may be approaching a crisis of rigor".

                                              Bellare and Rogaway (cca 2004)

``Do we have a problem with cryptographic proofs? Yes, we

do [...] We generate more proofs than we carefully verify

(and as a consequence some of our published proofs are

incorrect)". 

       
                                                                     Halevi (cca 2005)


Solutions developed by cryptographers e.g. compositional reasoning and the game-hopping technique, help to structure proofs and reduce their complexity and therefore alleviate to some extent the pain of having to develop rigorous proofs. Yet, more often than not proofs are still sketchy and shady.

There is help that comes from the programming languages community which has a long experience with developing tools for proving that programs work correctly and...cryptographic systems are just programs. Recent progress,  e.g. automated verification of parts of TLS, fully verified security proofs of implementation masking schemes to defeat leakage, is impressive and exciting.  More work is under way. 

If you want to learn more about how can you get someone else to do the proofs for you or, more realistically, learn about what existent tools can currently do, what they could do in the future, and discuss what is needed and which way to go, then you should attend the 

Workshop on Models and Tools for Security Analysis and Proofs
 -- Paris, 29th of April; co-located with EuroSnP and Eurocrypt --

which the Bristol Crypto group helps organize. The workshop features as speakers some of the most prominent researchers that are contributing to this direction. You can register for the workshop HERE. Early registration ends March 31st!


But wait...there is more. If you want to explore this area beyond what a one-day workshop allows, then you should consider attending the

Summer School on Models and Tools for Proofs 

-- Nancy, France, July 10th - 13th --

See you all in Paris and/or Nancy!