Version 1.0.5: Lean 4 formalization of Theorem 3.1 (class bridge), Corollary 3.2 (class fingerprint invariance), and Section 5 bad-index set; Appendix A.2 correspondence corrected. Exhaustive GF(2^8) checks remain in Python. The Mobius Bridge of Nasr and Carlini removes one guessed key byte from meet-in-the-middle attacks on 7-round AES by constructing a fingerprint invariant under the group action that survives the S-box. This note shows the construction holds for every S-box of the form S = L2 ˆ Frobj ˆ inv ˆ L1, with the Frobenius exponent as the only degree of freedom. ARIA's four substitution-layer maps (S1, S2, S1−1, S2−1 at exponents 0, 3, 0, 5) are instantiated with the published affine maps and constants (a = 0x63, b = 0xE2). Bad indices relocate to L1−1(0). Identities verified exhaustively over GF(28) and formalized in Lean 4. No attack complexities for ARIA are claimed. Source: github.com/chokmah-me/aria-moebius. This record is the paper PDF only.
ARIA · block cipher · meet-in-the-middle · Mobius Bridge · GF(2^8) · Frobenius · Lean 4 · S-box · cryptanalysis