In this talk, I will briefly present both the EasyCrypt interactive proof assistant—whose focus is on the formalization of game-based cryptographic security proofs, before discussing its application to the SHA-3 standard. In combination with the Jasmin language—an "assembly-in-the-head" language with formalized semantics and a certified compiler—our proof is used to produce a complete high-assurance standard, with machine-checked proofs, verified reference implementations, and a verified optimized implementation for a specific platform.
I will discuss some of the challenges encountered in formalizing the security proof, and discuss the techniques afforded by the combined use of "interactive first" technologies such as Jasmin and EasyCrypt, which allow us to produce highly-efficient, yet fully verified, implementations. Some future perspectives may be discussed
I am a Senior Lecturer in the Cryptography Group and Department of Computer Science at the University of Bristol (UK). My research revolves around proving cryptographic and side-channel security properties of concrete realizations and implementations of cryptographic primitives and protocols, sometimes in the presence of partial compromise. This involves tackling problems in modelling adversaries and systems, designing and applying proof methodologies and verification tools, and generally finding less tedious ways of verifying complex properties of large (but not vast) systems and code bases.