Article Title]{Algebraic Cryptanalysis of Reduced-Round International Data Encryption Algorithm

Abstract SMT stands for Satisfiability Modulo Theories. SMT framework for addressing first-order logic-based constraint fulfillment problems. The following cryptographic procedures have used SMT solvers: SMT solver tools are used for differential cryptanalysis, collision attack, pre-image attack, modular root-finding, and cryptographic primitives verification. We demonstrate the effectiveness of SMT solvers for solving block cipher cryptanalysis constraints. During a cryptanalytic attack, we transform the boolean equations representing a block cipher into a more suitable format (Z3py). The performance of the IDEA cipher is evaluated utilizing the proposed cryptanalysis method. This technique uses plaintext and ciphertext pairs, partial key bits to recover the partial secret key and a predetermined number of rounds.