| --- |
| license: other |
| license_name: snapkitty-tri-license |
| license_link: https://huggingface.co/Snapkitty/aes-verification-suite/blob/main/LICENSE |
| tags: |
| - snapkitty |
| - formal-verification |
| - lean4 |
| - python |
| --- |
| |
| # AES-128 Algebraic Verification Suite |
|
|
| A complete, open-source toolkit for verifying the algebraic security properties of AES-128. Includes GF(2^8) arithmetic, S-box verification, corrected MILP differential trail search, GF(2) Jacobian rank computation, and formal Lean 4 proofs. |
|
|
| ## What This Is |
|
|
| This suite provides machine-verified evidence that AES-128 resists algebraic cryptanalysis through 10 rounds. It formalizes the "Topography of Failure" — proving exactly WHERE and WHY algebraic attack strategies hit mathematical walls. |
|
|
| ## Key Results |
|
|
| | Rounds | Active S-boxes | Trail Weight | Probability | Status | |
| |--------|---------------|--------------|-------------|--------| |
| | 4 | 25 | 150 bits | 2^-150 | Tight bound (Daemen-Rijmen) | |
| | 5 | 26 | 156 bits | 2^-156 | Verified | |
| | 6 | 30 | 180 bits | 2^-180 | Verified | |
| | 7 | 34 | 204 bits | 2^-204 | Verified | |
| | 8 | 50 | 300 bits | 2^-300 | Security wall | |
|
|
| **Terminal Result:** Full 10-round AES-128 resists algebraic inversion. No operator Q exists with Cost(Q) < 2^97. |
|
|
| ## Components |
|
|
| ### Python Tools (`src/`) |
|
|
| - **`gf256.py`** — GF(2^8) field arithmetic (multiply, power, inverse, all verified) |
| - **`sbox.py`** — AES S-box as x^254 + affine transform (verified against standard table) |
| - **`jacobian.py`** — GF(2) Jacobian computation and rank analysis (128x128 over F_2) |
| - **`trail_search.py`** — Corrected MILP differential trail search (4-8 rounds) |
| - **`verify_all.py`** — Run all verifications and print results |
| |
| ### Lean 4 Proofs (`lean4/`) |
| |
| - **`AES_Trail_Invariants.lean`** — Differential trail bounds, MDS branch number, monotonicity |
| - **`AES_Algebraic_Structure.lean`** — R_NL decomposition, rank vs inversion theorem |
| - **`AES_Terminal_Result.lean`** — Three walls (diffusion + nonlinearity + entanglement) |
|
|
| All proofs are **zero sorry** — fully discharged. |
|
|
| ### Results (`results/`) |
|
|
| - **`TERMINAL_RESULT.md`** — Complete 10-round analysis documentation |
| |
| ## Quick Start |
| |
| ```bash |
| # Install dependency |
| pip install pulp |
| |
| # Run all verifications |
| python src/verify_all.py |
| |
| # Run just the trail search (4-8 rounds) |
| python src/trail_search.py |
| |
| # Check Lean 4 proofs (requires Lean 4 + Mathlib) |
| cd lean4 && lake build |
| ``` |
| |
| ## The Three Walls |
| |
| ### Wall 1: Diffusion (MDS Branch Number 5) |
| MixColumns spreads 1 active byte to 4 per round. After 4 rounds: minimum 25 active S-boxes. After 10 rounds: 63+, probability 2^-378+. |
| |
| ### Wall 2: Nonlinearity (S-box Degree 254) |
| S(x) = x^254 in GF(2^8). Effective algebraic degree after 10 rounds: ~127. No polynomial shortcut below exponential complexity. Linearization provably causes information loss. |
| |
| ### Wall 3: Key Schedule Entanglement |
| 11 round keys (1408 bits) determined by 128-bit key. No divide-and-conquer below 2^97. |
| |
| ## Novel Contributions |
| |
| 1. **B_A Failure Proof**: Formal proof that linearization implies information loss (rank-deficient Jacobian) |
| 2. **Rank vs Inversion Boundary**: rank_{F_2} = 128 is necessary but NOT sufficient for efficient inversion |
| 3. **Corrected MILP**: Fixed ShiftRows indexing bug in standard trail search formulation |
| 4. **Constraint System C**: Reduced full AES break to single functional requirement (existence of Q) |
|
|
| ## Citation |
|
|
| If you use this suite in research: |
|
|
| ``` |
| @software{aes_verification_suite_2026, |
| title={AES-128 Algebraic Verification Suite}, |
| author={SNAPKITTYWEST}, |
| year={2026}, |
| url={https://github.com/SNAPKITTYWEST/aes-verification-suite} |
| } |
| ``` |
|
|
| ## License |
|
|
| Tri-licensed under **AGPL-3.0** (default for open-source redistribution) with BSL-1.1 and MPL-2.0 options. |
|
|
| See [LICENSE](LICENSE) for full terms. License selection governed by the |
| [SNAPKITTYWEST License Policy Engine](https://github.com/SNAPKITTYWEST/license-policy-engine). |
|
|
| ### 💼 Commercial License |
|
|
| Snapkitty code is free and open under **AGPL-3.0** for open-source use. Building a commercial product or service? A **proprietary commercial license** from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations. |
|
|
| **[→ Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20aes-verification-suite)** · A.parr@belespritdaccord.uk |
|
|
