---
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