aria-moebius: Lean formalization and class-bridge verifier

Sketchnote for the software catalog (CC BY 4.0). Full-size PNG.

Abstract

This deposit is the Lean 4 and Python companion to Mobius Bridges for the Invert-and-Affine S-box Class, with the Four ARIA Instantiations (paper v1.0.5). The Nasr–Carlini Möbius Bridge is not specific to the AES S-box: it holds for every S-box of the form S = L₂ ∘ Frob^j ∘ inv ∘ L₁, with the Frobenius exponent j as the only degree of freedom. ARIA instantiates four members of that class at once (S1, S2, S1⁻¹, S2⁻¹ at j = 0, 3, 0, 5).

The v1.0.4 zip contains Bridge.lean / AriaMobius.lean (Lean 4.32.2, mathlib v4.32.2) formalizing Theorem 3.1, Corollary 3.2, and the §5 bad-index set, plus verify_bridge_class.py, which runs five exhaustive GF(2⁸) checks (0/64770 mismatches per ARIA Table 1 row with published A, B, a=0x63, b=0xE2). Axiom set: propext, Classical.choice, Quot.sound; no sorry. Independent kernel: con-leche --verified accepted the Bridge export (CHECK_EXIT=0). Prefer the software concept DOI for the always-latest zip. Cite the paper for the theorem. No attack complexities for ARIA are claimed.

Keywords

ARIA · block cipher · Mobius Bridge · GF(2^8) · Frobenius · Lean 4 · S-box · formal verification · mathlib · invert-and-affine · class bridge · fingerprint invariance · meet-in-the-middle · cryptanalysis · axiom audit · con-leche · independent kernel

← All research