Verifiable Security of Prefix-free Merkle-Damgård
Master Thesis Saarland University, 2012.
(
Abstract
|
BibTeX
| Links:
)
@mastersthesis{skor_12:master,
title = {Verifiable Security of Prefix-free Merkle-Damgård},
author = {Malte Skoruppa},
url = {https://www-intern.cispa.uni-saarland.de/wordpress/wp-content/uploads/2016/04/master_thesis_final_skoruppa.pdf},
year = {2012},
date = {2012-01-01},
school = {Saarland University},
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.},
keywords = {}
}
title = {Verifiable Security of Prefix-free Merkle-Damgård},
author = {Malte Skoruppa},
url = {https://www-intern.cispa.uni-saarland.de/wordpress/wp-content/uploads/2016/04/master_thesis_final_skoruppa.pdf},
year = {2012},
date = {2012-01-01},
school = {Saarland University},
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.},
keywords = {}
}
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.
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.