A short piece of machine-checked cybersecurity analysis. ARADI is a 2024 NSA lightweight block cipher; for its six-round differential behaviour the automated analysis CLAASPing ARADI prints weight 84 in bold in its Table 4, meaning optimal. Inside the authors' own CLAASP model the optimum is 82: a weight-82 trail exists, and no trail of weight 81 or less does. The hard half -- that nothing lighter exists -- is 945 cube-and-conquer subproblems, every one UNSAT with a DRAT certificate an independent checker re-verifies. This is a single corrected table cell with a reproducible certificate, not a break of the cipher.
The open value
CLAASPing ARADI (Bellini et al., INDOCRYPT 2024) analyses the NSA cipher ARADI automatically with the CLAASP framework. Its Table 4 lists, per round count, the weight of the best single-key differential trail found, with the entries claimed optimal printed in bold; for six rounds it prints 84. Whether 84 is really the optimum has a checkable answer inside CLAASP's own model.
How it was shown
Upper bound: a trail of weight 82 exists in CLAASP's S-box model, with per-round S-box weights 18-6-18-16-8-16. Its weight is confirmed by re-fixing it in CLAASP, by the designers' round-function formula, and by Monte-Carlo estimation. Lower bound: that no trail of weight 81 or less exists is proved by a hybrid CNF — CLAASP's own clauses for trail validity, a bidirectional sequential-counter bound on the weight, and Matsui-style window pruning — split by cube-and-conquer into 945 subproblems, every one UNSAT; all 945 UNSAT results, and the Matsui bounds they rely on, carry a DRAT certificate checked by drat-trim. So the six-round optimum is exactly 82. The same weight-82 trail is also optimal in CLAASP's bit-sliced (AND-gate) model, so 84 is not optimal under either weight definition. The seven- and eight-round values 106 and 122 of Table 4 are reproduced and confirmed.
Check it yourself
This re-scores the weight-82 trail by the designers' round-function formula, with no solver and no heavy dependencies, confirming the upper bound: a trail of weight 82 exists. The hard half — that nothing lighter exists — is the DRAT certificate, which an independent checker (drat-trim) re-verifies; the 945 certificate summaries with per-proof SHA-256 and the scripts are in the code and preprint below.
Status
The trail, the search, the certificates and the reproduction scripts were released on 7 Nov 2026 and archived on Zenodo. The note proposes no new construction and claims no attack; it corrects a single table cell and gives the first machine-checked lower bound for round-reduced ARADI. Corrections are welcome at the address in the footer.
Links
Cite as
Nobuo Otoi (ba-cybersecurity.com). The six-round differential optimum of ARADI is 82: a machine-checked lower bound. 2026. https://doi.org/10.5281/zenodo.24025026.
@misc{otoi2026aradi,
author = {Otoi, Nobuo},
title = {The six-round differential optimum of ARADI is 82: a machine-checked lower bound},
year = {2026},
doi = {10.5281/zenodo.24025026},
publisher = {Zenodo},
howpublished = {\url{https://ba-cybersecurity.com/research/aradi-6r-optimum/}},
note = {Preprint. Artifacts and DRAT certificates: https://github.com/otoinobuo/aradi-6r-optimum}
}
Preprint published 7 Nov 2026 · This page: updated 7 Nov 2026 · Permanent address: https://ba-cybersecurity.com/research/aradi-6r-optimum/