Application of SAT-Solvers to the Problem of Finding Vectorial Boolean Functions with Required Cryptographic Properties

Abstract: We propose a method for finding an almost perfect nonlinear (APN) function. It is basedon translation into SAT-problem and using SAT-solvers. We construct several formulas definingthe conditions for finding an APN function and introduce two representations of the function,sparse and dense, which are used to describe the problem of finding one-to-one vectorial Booleanfunctions and APN functions. We also propose a new method for finding a vector APN functionwith additional properties. It is based on the idea of representing the unknown vectorial Booleanfunction as a sum of a known APN function and two unknown Boolean functions,(Formula presented.), where F is a known APN function. It is shown that this method is more efficient thanthe direct construction of APN function using SAT for dimensions 6 and 7. As a result, themethod described in the paper can prove the nonexistence of cubic APN functions in dimension 7representable in the form of the sum described above. © 2022, Pleiades Publishing, Ltd.