(2012) Verifiable Security of Prefix-free Merkle-Damgård.
|
Text
master_thesis_final_skoruppa.pdf - Published Version Download (935kB) | Preview |
Abstract
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.
| Item Type: | Thesis (Masters) |
|---|---|
| Additional Information: | pub_id: 812 Bibtex: skor_12:master URL date: None |
| Uncontrolled Keywords: | master |
| Divisions: | Michael Backes (InfSec) |
| Depositing User: | Sebastian Weisgerber |
| Date Deposited: | 26 Jul 2017 10:33 |
| Last Modified: | 18 Jul 2019 12:08 |
| Primary Research Area: | NRA1: Trustworthy Information Processing |
| URI: | https://publications.cispa.saarland/id/eprint/1061 |
Actions
Actions (login required)
 |
View Item |