Optimizing S-box Implementations Using SAT Solvers: Revisited

Fuxin Zhang; Zhenyu Huang

Paper 2023/1721

Optimizing S-box Implementations Using SAT Solvers: Revisited

Fuxin Zhang, State Key Laboratory of Information Security, Institute of Information Engineering, Chinese Academy of Sciences, Beijing, China, School of Cyber Security, University of Chinese Academy of Sciences, Beijing, China

Zhenyu Huang, State Key Laboratory of Information Security, Institute of Information Engineering, Chinese Academy of Sciences, Beijing, China, School of Cyber Security, University of Chinese Academy of Sciences, Beijing, China

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.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Preprint.
Keywords: S-box SAT solver Circuit optimization Algebraic normal form
Contact author(s): zhangfuxin @ iie ac cn
huangzhenyu @ iie ac cn
History: 2023-11-13: approved; 2023-11-07: received; See all versions
Short URL: https://ia.cr/2023/1721
License: CC BY

BibTeX

@misc{cryptoeprint:2023/1721,
      author = {Fuxin Zhang and Zhenyu Huang},
      title = {Optimizing S-box Implementations Using {SAT} Solvers: Revisited},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/1721},
      year = {2023},
      url = {https://eprint.iacr.org/2023/1721}
}