Verifiable Security of Prefix-free Merkle-Damgård

In recent years, an increasingly popular approach to the game-playing technique in cryptographic proofs is to rigorously specify games as pieces of well-defined program code; this irons out potential ambiguities in their specification, and enables a formal analysis of those games and proofs with the help of automated tools, as envisioned by Halevi [49]. Barthe et al. recently developed EasyCrypt [13], a tool which comes with a fully-specified programming language suitable for the formalization of cryptographic games, as well as an associated probabilistic relational Hoare logic and built-in program verification techniques. EasyCrypt can automatically generate proof obligations arising within a game-playing proof, and solve these mechanically using state-of-the-art automated tools. In this thesis, we use EasyCrypt to formally verify the indifferentiability of the prefix-free Merkle-Damgård construction, following a seminal proof by Coron et al. [39]. Merkle-Damgård is a cryptographic construction ubiquitously used to implement hash functions: These have received considerable attention from the cryptographic community in the last few years, motivated by the ongoing SHA-3 competition. Indifferentiability is a powerful and non-trivial security notion that yields many implications, and certainly constitutes a desirable security property to achieve when designing a modern cryptographic hash function. More concretely, we specify a sensible sequence of games in EasyCrypt’s language, and discuss the arguments that were needed for machine-checking the validity of the transitions relating those games. We focus in particular on the underlying axiomatization and derived lemmas used to justify the validity of side-conditions that arose when proving invariants of those games. Our results provide a first, but significant step towards a machine-checked verification of the indifferentiability of the finalists of the SHA-3 competition