Modern Boolean Satisﬁability Problem (SAT) solvers utilise a ”smart” brute force search. This means that SAT solvers can ﬁnd ”smart” solutions to Boolean Satisﬁability problems. Hence, any problem that can be converted into a SAT problem can be solved in an unexpected manner by a SAT solver. In order to understand the satisﬁability problem, we must ﬁrst deﬁne the language in which the problem is phrased. The language is propositional logic. Hence they are sometimes called propositional satisfiability problem solvers. SAT is the first problem that was proven to be NP-complete. Thinking of all the problems in the outside world you could attack with SAT technology like
The potentials of the technology is obvious. Finding if a problem is solvable is of huge interest in the industry. Especially cryptographic problems can be reduced to their hardness. That is why we used them to tackle improving modern SAT solvers to even better performance.
Performing hundreds of test runs and a source-code analysis, we empirically identified improved parameter configurations for CryptoMiniSat (CMS) 5 for solving cryptographic CNF instances originating from algebraic known-plaintext attacks on 3 rounds encryption of the Small AES-64 model cipher SR(3, 4, 4, 4). We finally became able to reconstruct 64-bit long keys in under an hour real time which, to our knowledge, has never been achieved so far.
The outcomes are summarized in a paper “CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances” (https://easychair.org/smart-program/FLoC2018/POS-2018-07-07.html#talk:72772) . We are now proud of being invited to present our findings at this year’s “Federated Logic Conference 2018” in Oxford, UK. We that is Anastasia Leventi-Peetz, Oliver Zendel, Werner Lennartz and Kai Weber.
#SAT, #FLoC2018, #Industry4.0, #AI, #Inducto, #Werusys