NDLI: Encoding Hash Functions as a SAT Problem

Content Provider	IEEE Xplore Digital Library
Author	Legendre, F. Dequen, G. Krajecki, M.
Copyright Year	2012
Description	Author affiliation: Univ. of Reims Champagne-Ardenne, Moulin de la Housse Reims, France (Legendre, F.; Krajecki, M.) \|\| MIS Amiens, Univ. of Picardie Jules Verne, Amiens, France (Dequen, G.)
Abstract	The SATisfiability Problem is a core problem in mathematical logic and computing theory. In the last years, 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 cryptographic problems, and particularly introduced a new field called logical cryptanalysis [15]. This paper deals with an original application of the SAT problem to encode the well-known MD? and SHA? hash functions algorithm in a generic DIMACS formula. As cryptographic hash functions are central elements in modern cryptography we choose to validate our modelisation with a dedicated attack on the inversion of these functions. This attack behaves like a reverse-engineering process, thanks to a state of the art SAT solver achieving a weakening of the second preimage of MD? and SHA?. As a result, we present our modelisation and an improvement of the current limit of best practical attacks on step-reduced MD4, MD5 and SHA? inversions, respectively up to 39, 28 and 23 broken steps. Finally, a brief analyse of our results allows to give an idea about logical cryptanalysis and hash functions.
Starting Page	916
Ending Page	921
File Size	372964
Page Count	6
File Format	PDF
ISBN	9781479902279
ISSN	10823409
DOI	10.1109/ICTAI.2012.128
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2012-11-07
Publisher Place	Greece
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Encoding Ciphers Runtime Mathematical model Silicon hash functions satisfiability logical cryptanalysis
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Libarray of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

From a logical approach to internal states of Hash functions how SAT problem can help to understand SHA-⋆ and MD⋆

Logical cryptanalysis as a SAT-problem: Encoding and analysis (2000)

Logical reasoning to detect weaknesses about sha-1 and md4/5 (2014).

Differential cryptanalysis of hash functions based on block ciphers

Cryptanalysis of Block Ciphers and Hash Functions

Logical Cryptanalysis as a SAT Problem: the Encoding of the Data Encryption Standard (1999)

Complete SAT based Cryptanalysis of RC5 Cipher

How to fake an RSA signature by encoding modular root finding as a SAT problem (2003)

Security margin evaluation of sha-3 contest finalists through sat-based attacks (extension).

Encoding Hash Functions as a SAT Problem

Similar Documents

From a logical approach to internal states of Hash functions how SAT problem can help to understand SHA-⋆ and MD⋆

Logical cryptanalysis as a SAT-problem: Encoding and analysis (2000)

Logical reasoning to detect weaknesses about sha-1 and md4/5 (2014).

Differential cryptanalysis of hash functions based on block ciphers

Cryptanalysis of Block Ciphers and Hash Functions

Logical Cryptanalysis as a SAT Problem: the Encoding of the Data Encryption Standard (1999)

Complete SAT based Cryptanalysis of RC5 Cipher

How to fake an RSA signature by encoding modular root finding as a SAT problem (2003)

Security margin evaluation of sha-3 contest finalists through sat-based attacks (extension).

Encoding Hash Functions as a SAT Problem