Article

Applications of SAT solvers to cryptanalysis of hash functions

Authors:

Lintao ZhangAuthors Info & Claims

SAT'06: Proceedings of the 9th international conference on Theory and Applications of Satisfiability Testing

Pages 102 - 115

https://doi.org/10.1007/11814948_13

Published: 12 August 2006 Publication History

Abstract

Several standard cryptographic hash functions were broken in 2005. Some essential building blocks of these attacks lend themselves well to automation by encoding them as CNF formulas, which are within reach of modern SAT solvers. In this paper we demonstrate effectiveness of this approach. In particular, we are able to generate full collisions for MD4 and MD5 given only the differential path and applying a (minimally modified) off-the-shelf SAT solver. To the best of our knowledge, this is the first example of a SAT-solver-aided cryptanalysis of a non-trivial cryptographic primitive. We expect SAT solvers to find new applications as a validation and testing tool of practicing cryptanalysts.

References

[1]

Eli Biham and Rafi Chen. Near-collisions of SHA-0. In Matthew K. Franklin, editor, Advances in Cryptology--CRYPTO 2004, volume 3152 of Lecture Notes in Computer Science, pages 290-305. Springer, 2004.

[2]

John Black, Martin Cochran, and Trevor Highland. A study of the MD5 attacks: Insights and improvements. In Fast Software Encryption 2006, 2006.

Digital Library

[3]

Eli Biham, Rafi Chen, Antoine Joux, Patrick Carribault, Christophe Lemuet, and William Jalby. Collisions of SHA-0 and reduced SHA-1. In Cramer {Cra05}, pages 36-57.

Digital Library

[4]

Gilles Brassard, editor. Advances in Cryptology--CRYPTO '89, 9th Annual International Cryptology Conference, Santa Barbara, California, USA, August 20-24, 1989, Proceedings, volume 435 of Lecture Notes in Computer Science. Springer, 1990.

[5]

Florent Chabaud and Antoine Joux. Differential collisions in SHA-0. In Hugo Krawczyk, editor, CRYPTO, volume 1462 of Lecture Notes in Computer Science, pages 56-71. Springer, 1998.

Digital Library

[6]

Ronald Cramer, editor. Advances in Cryptology--EUROCRYPT 2005, 24th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Aarhus, Denmark, May 22-26, 2005, Proceedings, volume 3494 of Lecture Notes in Computer Science. Springer, 2005.

Digital Library

[7]

Ivan Damgård. Collision free hash functions and public key signature schemes. In David Chaum and Wyn L. Price, editors, Advances in Cryptology--EUROCRYPT '87, volume 304 of Lecture Notes in Computer Science, pages 203-216. Springer, 1988.

Digital Library

[8]

Ivan Damgård. A design principle for hash functions. In Brassard {Bra90}, pages 416-427.

Digital Library

[9]

Magnus Daum. Cryptanalysis of Hash Functions of the MD4-Family. PhD thesis, Ruhr-Universität Bochum, 2005.

[10]

Bert den Boer and Antoon Bosselaers. Collisions for the compressin function of MD5. In Tor Helleseth, editor, Advances in Cryptology-- EUROCRYPT '93, volume 765 of Lecture Notes in Computer Science, pages 293-304. Springer, 1994.

Digital Library

[11]

Hans Dobbertin. Cryptanalysis of MD4. In Dieter Gollmann, editor, Fast Software Encryption '96, volume 1039 of Lecture Notes in Computer Science, pages 53-69. Springer, 1996.

Digital Library

[12]

Hans Dobbertin. The status of MD5 after a recent attack. CryptoBytes, 2(2):1-6, 1996.

[13]

Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Proceedings of the International Symposium on the Theory and Applications of Satisfiability Testing (SAT), pages 61-75, 2005.

Digital Library

[14]

Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Proceedings of the International Symposium on the Theory and Applications of Satisfiability Testing (SAT), 2003.

[15]

Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into SAT. J. Satisfiability, Boolean Modeling and Computation, 2:1-26, 2006.

[16]

Claudia Fiorini, Enrico Martinelli, and Fabio Massacci. How to fake an RSA signature by encoding modular root finding as a SAT problem. Discrete Applied Mathematics, 130(2):101-127, 2003.

Digital Library

[17]

Evgueni Goldberg and Yakov Novikov. BerkMin: A fast and robust Satsolver. In DATE, pages 142-149, 2002.

Digital Library

[18]

Philip Hawkes, Michael Paddon, and Gregory G. Rose. Musings on the Wang et al. MD5 collision. Cryptology ePrint Archive, Report 2004/264, 2004. http://eprint.iacr.org/.

[19]

Dejan Jovanovic and Predrag Janičic. Logical analysis of hash functions. In Bernhard Gramlich, editor, Frontiers of Combining Systems (FroCoS), volume 3717 of Lecture Notes in Artificial Intelligence, pages 200-215. Springer Verlag, 2005.

Digital Library

[20]

Arthur Evans Jr., William Kantrowitz, and Edwin Weiss. A user authentication scheme not requiring secrecy in the computer. Commun. ACM, 17(8):437-442, 1974.

Digital Library

[21]

Vlastimil Klima. Finding MD5 collisions on a notebook PC using multimessage modifications. Cryptology ePrint Archive, Report 2005/102, 2005. http://eprint.iacr.org/.

[22]

Leslie Lamport. Constructing digital signatures from a one-way function. Technical Report CSL-98, SRI International, October 1979.

[23]

Fabio Massacci. Using Walk-SAT and Rel-SAT for cryptographic key search. In International Joint Conference on Artificial Intelligence, IJCAI 99, pages 290-295, 1999.

Digital Library

[24]

Ralph C. Merkle. One way hash functions and DES. In Brassard {Bra90}, pages 428-446.

Digital Library

[25]

Fabio Massacci and Laura Marraro. Logical cryptanalysis as a SAT problem. Journal of Automated Reasoning, 24:165-203, 2000.

Digital Library

[26]

Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference (DAC), June 2001.

Digital Library

[27]

João P. Marques-Silva and Karem A. Sakallah. GRASP--a search algorithm for propositional satisfiability. IEEE Transactions in Computers, 48(5):506-521, May 1999.

Digital Library

[28]

Alfred J. Menezes, Paul C. van Oorschot, and Scott A. Vanstone. Handbook of Applied Cryptography. CRC Press, 1996.

Digital Library

[29]

NIST. Secure hash standard. FIPS PUB 180, National Institute of Standards and Technology, May 1993.

[30]

NIST. Secure hash standard. FIPS PUB 180-1, National Institute of Standards and Technology, April 1995.

[31]

Ronald L. Rivest. The MD4 message digest algorithm. In Alfred Menezes and Scott A. Vanstone, editors, Advances in Cryptology--CRYPTO '90, volume 537 of Lecture Notes in Computer Science, pages 303-311. Springer, 1991.

Digital Library

[32]

Ronald L. Rivest. The MD5 message-digest algorithm. RFC 1321, The Internet Engineering Task Force, April 1992.

[33]

Ronald L. Rivest, Adi Shamir, and Leonard M. Adleman. A method for obtaining digital signatures and public-key cryptosystems. Commun. ACM, 21(2):120-126, 1978.

Digital Library

[34]

Lawrence Ryan. Efficient algorithms for clause-learning SAT solvers. M.Sc. Thesis, Simon Fraser University, February 2004.

[35]

Victor Shoup, editor. Advances in Cryptology--CRYPTO 2005: 25th Annual International Cryptology Conference, Santa Barbara, California, USA, August 14-18, 2005, Proceedings, volume 3621 of Lecture Notes in Computer Science. Springer, 2005.

Digital Library

[36]

Martin Schläffer and Elisabeth Oswald. Searching for differential paths in MD4. In Fast Software Encryption 2006, 2006.

Digital Library

[37]

Gregory Tseytin. On the complexity of derivation in propositional calculus., pages 115-125. Consultant Bureau, New York-London, 1968.

[38]

Xiaoyun Wang, Xuejia Lai, Dengguo Feng, Hui Chen, and Xiuyuan Yu. Cryptanalysis of the hash functions MD4 and RIPEMD. In Cramer {Cra05}, pages 1-18.

Digital Library

[39]

Markus Wedler, Dominik Stoffel, and Wolfgang Kunz. Arithmetic reasoning in DPLL-based SAT solving. In DATE, pages 30-35, 2004.

Digital Library

[40]

Xiaoyun Wang and Hongbo Yu. How to break MD5 and other hash functions. In Cramer {Cra05}, pages 19-35.

[41]

Xiaoyun Wang, Yiqun Lisa Yin, and Hongbo Yu. Finding collisions in the full SHA-1. In Shoup {Sho05}, pages 17-36.

Digital Library

[42]

Xiaoyun Wang, Hongbo Yu, and Yiqun Lisa Yin. Efficient collision search attacks on SHA-0. In Shoup {Sho05}, pages 1-16.

Digital Library

Cited By

Shi JLiu GLi CLi Y(2024)Automated-Based Rebound Attacks on ACE PermutationTopics in Cryptology – CT-RSA 202410.1007/978-3-031-58868-6_4(78-111)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.1007/978-3-031-58868-6_4
Li YLiu FWang G(2024)New Records in Collision Attacks on SHA-2Advances in Cryptology – EUROCRYPT 202410.1007/978-3-031-58716-0_6(158-186)Online publication date: 26-May-2024
https://dl.acm.org/doi/10.1007/978-3-031-58716-0_6
Li YChen XGuo WLi XLuo WHuang JZhen HYuan MYan JSingh ASun YAkoglu LGunopulos DYan XKumar ROzcan FYe J(2023)HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware BaselineProceedings of the 29th ACM SIGKDD Conference on Knowledge Discovery and Data Mining10.1145/3580305.3599837(4414-4425)Online publication date: 6-Aug-2023
https://dl.acm.org/doi/10.1145/3580305.3599837
Show More Cited By

Recommendations

CDCL(Crypto) SAT solvers for cryptanalysis
CASCON '19: Proceedings of the 29th Annual International Conference on Computer Science and Software Engineering

Over the last two decades we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers on industrial problems from a variety of domains. The availability of such a powerful general-...
Cryptanalysis of hash functions based on blockciphers suitable for IoT service platform security

It is well-known that blockcipher-based hash functions may be attacked when adopting blockciphers having related-key differential properties. However, all forms of related-key differentials are not always effective to attack them. In this paper we ...
Cryptanalysis of Hash Functions with Structures
Selected Areas in Cryptography

Hash function cryptanalysis has acquired many methods, tools and tricks from other areas, mostly block ciphers. In this paper another trick from block cipher cryptanalysis, the structures, is used for speeding up the collision search. We investigate the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SAT'06: Proceedings of the 9th international conference on Theory and Applications of Satisfiability Testing

August 2006

437 pages

ISBN:3540372067

Editors:
Armin Biere
Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria
,
Carla P. Gomes
Department of Computer Science, Cornell University, Ithaca, NY

Sponsors

NEC
cadence: cadence
Microsoft Research: Microsoft Research
IBM: IBM

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 12 August 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

31
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shi JLiu GLi CLi Y(2024)Automated-Based Rebound Attacks on ACE PermutationTopics in Cryptology – CT-RSA 202410.1007/978-3-031-58868-6_4(78-111)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.1007/978-3-031-58868-6_4
Li YLiu FWang G(2024)New Records in Collision Attacks on SHA-2Advances in Cryptology – EUROCRYPT 202410.1007/978-3-031-58716-0_6(158-186)Online publication date: 26-May-2024
https://dl.acm.org/doi/10.1007/978-3-031-58716-0_6
Li YChen XGuo WLi XLuo WHuang JZhen HYuan MYan JSingh ASun YAkoglu LGunopulos DYan XKumar ROzcan FYe J(2023)HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware BaselineProceedings of the 29th ACM SIGKDD Conference on Knowledge Discovery and Data Mining10.1145/3580305.3599837(4414-4425)Online publication date: 6-Aug-2023
https://dl.acm.org/doi/10.1145/3580305.3599837
Liu FWang GSarkar SAnand RMeier WLi YIsobe T(2023)Analysis of RIPEMD-160: New Collision Attacks and Finding Characteristics with MILPAdvances in Cryptology – EUROCRYPT 202310.1007/978-3-031-30634-1_7(189-219)Online publication date: 23-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30634-1_7
Liu MLi P(2022)SATMargin: Practical Maximal Frequent Subgraph Mining via Margin Space SamplingProceedings of the ACM Web Conference 202210.1145/3485447.3512196(1495-1505)Online publication date: 25-Apr-2022
https://dl.acm.org/doi/10.1145/3485447.3512196
Ebrahimi ARegazzoni FPalmieri P(2022)Reducing the Cost of Machine Learning Differential Attacks Using Bit Selection and a Partial ML-DistinguisherFoundations and Practice of Security10.1007/978-3-031-30122-3_8(123-141)Online publication date: 12-Dec-2022
https://dl.acm.org/doi/10.1007/978-3-031-30122-3_8
Edwards JVishkin U(2021)Study of Fine-grained Nested Parallelism in CDCL SAT SolversACM Transactions on Parallel Computing10.1145/34706398:3(1-18)Online publication date: 20-Sep-2021
https://dl.acm.org/doi/10.1145/3470639
Beck GZinkus MGreen MCapkun SRoesner F(2020)Automating the development of chosen ciphertext attacksProceedings of the 29th USENIX Conference on Security Symposium10.5555/3489212.3489315(1821-1837)Online publication date: 12-Aug-2020
https://dl.acm.org/doi/10.5555/3489212.3489315
Indrøy JCostes NRaddum H(2020)Boolean Polynomials, BDDs and CRHS Equations - Connecting the Dots with CryptaPathSelected Areas in Cryptography10.1007/978-3-030-81652-0_9(229-251)Online publication date: 21-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-81652-0_9
Hu XLi YJiao LTian SWang M(2020)Mind the Propagation of StatesAdvances in Cryptology – ASIACRYPT 202010.1007/978-3-030-64837-4_14(415-445)Online publication date: 7-Dec-2020
https://dl.acm.org/doi/10.1007/978-3-030-64837-4_14
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents