Cryptanalysis of a Reduced-Round IDEA Cipher Using Z3 Solver
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 ke...