Inverting Thanks to SAT Solving - An Application on Reduced-step MD*

Florian Legendre, Gilles Dequen, Michaël Krajecki

2012

Abstract

The SATisfiability Problem is a core problem in mathematical logic and computing theory. The last decade progresses have led it to be a great and competitive approach to practically solve a wide range of industrial and academic problems. Thus, the current SAT solving capacity allows the propositional formalism to be an interesting alternative to tackle cryptanalysis problems. This paper deals with an original application of the SAT problem to cryptanalysis. We thus present a principle, based on a propositional modeling and solving, and provide details on logical inferences, simplifications, learning and pruning techniques used as a preprocessor with the aim of reducing the computational complexity of the SAT solving and hence weakening the associated cryptanalysis. As cryptographic hash functions are central elements in modern cryptography we choose to illustrate our approach with a dedicated attack on the second preimage of the well-known MD⋆ hash functions. We finally validate this reverse-engineering process, thanks to a generic SAT solver achieving a weakening of the inversion of MD⋆. As a result, we present an improvement of the current limit of best practical attacks on step-reduced MD4 and MD5 second preimage, respectively up to 39 and 28 inverted rounds.

Paper Citation

in Harvard Style

Legendre F., Dequen G. and Krajecki M. (2012). Inverting Thanks to SAT Solving - An Application on Reduced-step MD* . In Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012) ISBN 978-989-8565-24-2, pages 339-344. DOI: 10.5220/0004077603390344

in Bibtex Style

@conference{secrypt12,
author={Florian Legendre and Gilles Dequen and Michaël Krajecki},
title={Inverting Thanks to SAT Solving - An Application on Reduced-step MD*},
booktitle={Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012)},
year={2012},
pages={339-344},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004077603390344},
isbn={978-989-8565-24-2},
}

in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012)
TI - Inverting Thanks to SAT Solving - An Application on Reduced-step MD*
SN - 978-989-8565-24-2
AU - Legendre F.
AU - Dequen G.
AU - Krajecki M.
PY - 2012
SP - 339
EP - 344
DO - 10.5220/0004077603390344