Modeling of algebraic analysis of PRESENT cipher by SAT solvers

Abstract Paper presents approaches to algebraic analysis of the reliability of symmetric block ciphers by solving Boolean satisfiability (SAT) problem. A description of the application of decision search algorithms by the DPLL method is given. The principle of formation of the SAT problem for algebraic analysis of PRESENT cipher is proposed, as well as the parameters of the obtained SAT problems for a different number of cipher rounds and plaintexts.