Transactions on Symmetric Cryptology, Volume 2024
On Impossible Boomerang Attacks
README
(Impossible) Boomerang distinguishers
This repository contains the source code associated to the articles On Boomerang Attacks on Quadratic Feistel Ciphers published in ToSC Volume 2023, Issue 3 and On Impossible Boomerang Attacks published in ToSC Volume 2024, Issue 2.
SMT models in ./SMT:
- SMT models are generated by katanSMTpython.py and simonSMTpython.py
- katanSMTpython.py only supports katan32. Usage
python3 katanSMTpython.py E0_rounds Em_rounds E1_rounds probability
- simonSMTpython supports all Simon versions and impossible boomerangs. See
--help
for details. - Raw outputs of the SMT solver can be found in ./SMT/out
- find_quartet_simon.py looks for quartets with some constraints. It can be used to find impossible boomerangs or check whether the output of simonSMTpython.py is instanciable. See
--help
for details. - All SMT models were solved using Bitwuzla
- SMT outputs can be pretty-printed using
python3 [parse_katan.py|parse_simon.py] <output_file>
- Pretty-printer also generates code snippets for C verification
MiniZinc models in ./minizinc:
- skinnyee.mzn contains an impossible boomerang model for MiniZinc. It was solved using OR-tools.
Details on the models can be found in the articles.
Code for experimental tests in ./verification:
- Compile with
make
. Requires OpenMP. - katan.c contains optimized C code adapted from the reference implementation of Katan's designers (https://www.cs.haifa.ac.il/~orrd/KATAN/katan.c). It checks boomerang distinguishers.
- Simon functions are adapted from the NSA reference implementation.
- simon_rk.c checks related-key boomerang distinguishers,
- simon_rx.c checks rotational-xor boomerang distinguishers,
- simon_rxd.c checks rotational-xor-differential boomerang distinguishers.