Block cipher algorithms use shared secret keys to cipher texts. The aim of the related-key attack is to evaluate if it is possible to find out the key by studying difference propagations. To this aim, cryptanalysts need to compute maximum differential paths. This problem is solved in two steps :
Some abstract solutions may not accept concrete solutions and our goal is to limit as much as possible the number of inconsistent abstract solutions at the concrete level. These inconsistencies mainly come from the fact that ciphering massively relies on XOR operations (bitwise exclusive or), and this operation is poorly abstracted during the first step. To improve that, we introduce a constraint for propagating a set of XORs in a global way.
First we study the complexity of the problem aiming at deciding if a XOR set accepts a concrete solution. We show that if the problem is polynomial when variables are not constrained, it becomes NP-complete if we constrain some variables to take values between 1 and a given upper bound. Then, we introduce the global constraint abstractXOR which is satisfied if there exists an abstract solution that can be concretized in the case where variables are not constrained by an upper bound and we introduce polynomial algorithms to propagate this constraint. We show how to use this global constraint to model a maximal differential path problem for Midori and we compare the performance of the model using this global constraint with other models.