Proposing an MILP-based method for the experimental verification of difference-based trails: application to SPECK, SIMECK

Searching for the right pairs of inputs in difference-based distinguishers is an important task for the experimental verification of the distinguishers in symmetric-key ciphers. In this paper, we develop an MILP-based approach to verify the possibility of difference-based distinguishers and extract the right pairs. We apply the proposed method to some published difference-based trails (Related-Key Differentials (RKD), Rotational-XOR (RX)) of block ciphers SIMECK, and SPECK. As a result, we show that some of the reported RX-trails of SIMECK and SPECK are incompatible, i.e. there are no right pairs that follow the expected propagation of the differences for the trail. Also, for compatible trails, the proposed approach can efficiently speed up the search process of finding the exact value of a weak key from the target weak key space. For example, in one of the reported 14-round RX trails of SPECK, the probability of a key pair to be a weak key is $$2^{-94.91}$$ when the whole key space is $$2^{96}$$ ; our method can find a key pair for it in a comparatively short time. It is worth noting that it was impossible to find this key pair using a traditional search. As another result, we apply the proposed method to SPECK block cipher, to construct longer related-key differential trails of SPECK which we could reach 15, 16, 17, and 19 rounds for SPECK32/64, SPECK48/96, SPECK64/128, and SPECK128/256, respectively. It should be compared with the best previous results which are 12, 15, 15, and 20 rounds, respectively, that both attacks work for a certain weak key class. It should be also considered as an improvement over the reported result of rotational-XOR cryptanalysis on SPECK.