Optimal SAT Solver Synthesis of Quantum Circuits Representing Cryptographic Nonlinear Functions

In this article we present a procedure that allows to synthesize optimal circuit representing any reversible function within reasonable size limits. The procedure allows to choose either the NCT or the MCT gate set and specify any number of ancillary qubits to be used in the circuit. We will explore efficacy of this procedure by synthesizing various sources of nonlinearity used in contemporary symmetric ciphers and draw conclusions about properties of those transformations in quantum setting. In particular we will try to synthesize optimal circuit representing ASCON cipher SBOX which recently won NIST competition for Lightweight Cryptography standard.