Paper 2023/1721 Original: eprint.iacr.org/2023/1721 ↗

Optimizing S-box Implementations Using SAT Solvers: Revisited

Abstract

We propose a new method to encode the problems of optimizing S-box implementations into SAT problems. By considering the inputs and outputs of gates as Boolean functions, the fundamental idea of our method is representing the relationships between these inputs and outputs according to their algebraic normal forms. Based on this method, we present several encoding schemes for optimizing S-box implementations according to various criteria, such as multiplicative complexity, bitslice gate complexity, gate complexity, and circuit depth complexity. The experimental results of these optimization problems show that, compared to the encoding method proposed in FSE 2016, which represents these relationships between Boolean functions by their truth tables, our new encoding method can significantly reduce accelerate the subsequent solving process by 2-100 times for the majority of instances. To further improve the solving efficiency, we propose several strategies to eliminate the redundancy of the derived equation system and break the symmetry of the solution space. We apply our method in the optimizations of the S-boxes used in Ascon, ICEPOLE, PRIMATEs, Keccak/Ketje/Keyak, Joltik/Piccolo, LAC, Minalpher, Prøst, and RECTANGLE. We achieve some new improved implementations and narrow the range of the optimal values for different optimization criteria of these S-boxes.