are extremely useful in cryptanalysis, are an extension of square attack
(also called saturation attack or integral cryptanalysis). Given their im-
portance, a large number of works tried to offer automatic tools to find
division properties, primarily based on MILP or SAT/SMT. This paper
studies better modeling techniques for finding division properties using
the Constraint Programming and SAT/SMT-based automatic tools. We
use the fact that the Quine-McCluskey algorithm produces a concise
CNF representation corresponding to the division trail table of an Sbox.
As a result, we can offer significantly more compact models, which allow
SAT and Constraint Programming tools to outperform previous results.
To show the strength of our new approach, we look at the NIST lightweight
candidate KNOT and Ascon. We show several new distinguishers with
a lower data complexity for 17-round KNOT-256, KNOT-384 and 19-
round KNOT-512. In addition, for the 5-round Ascon, we get a lower
data distinguisher than the previous division-based results.
Finally, we revisit the method to extend the integral distinguisher by
composing linear layers at the input and output. We provide a formu-
lation to find the optimal number of linear combinations that need to
be considered. As a result of this new formulation, we prove that 18-
round KNOT-256 and KNOT-384 have no integral distinguisher using
conventional division property and we show this more efficiently than
the previous methods.