Cryptanalysis of a Reduced-Round IDEA Cipher Using Z3 Solver

Abstract

We formulate key recovery for the International Data Encryption Algorithm (IDEA) as a quantifier-free bit-vector satisfiability problem. The IDEA is a 64-bit block cipher with a 128-bit key whose round function combines multiplication modulo 2^16+1, addition modulo 2^16, and XOR. The model includes the 25-bit cyclic key schedule, all round transformations, and the final output layer and is solved with Z3 through its Python API. We evaluate reduced-round instances using one all-zero plaintext-ciphertext pair and disclose 112 of the 128 key bits, leaving 16 bits to infer. Across the solved round counts, repeated runs recover the planted key and provide median wall-clock measurements on the stated platform. A legacy series with 96 disclosed bits is retained solely for comparison because its raw logs are unavailable. We also examine unconstrained key search at the smallest round counts. The result is a reproducible measurement of reduced-round SMT performance, not a practical break of full-round IDEA.