The security of communications heavily relies on cryptography. For decades, mathematicians have invested an immense effort in providing cryptography that is built on firm mathematical foundations. This has lead to a collection of cryptographic primitives whose correctness can be proved by drawing on results from branches of mathematics such as complex analysis, algebraic geometry, representation theory and number theory. A stated goal of recent competitions for cryptographic standards is to gain trust from the broad cryptography community through open and transparent processes. These processes generally involve open-source reference and optimized implementations for performance evaluation, rigorous security analyses for provable security evaluation and, often, informal evaluation of security against side-channel attacks. These artefacts contribute to building trust in candidates, and ultimately in the new standard. However, the disconnect between implementations and security analyses is a major cause for concern.

In this talk, I will present the Jasmin-EasyCrypt project that explores how formal approaches could eliminate this disconnect and bring together implementations (most importantly, efficient implementations) and software artefacts, in particular machine-checked proofs, supporting security analyses.