Papers With

← All papers
First page of On a conjecture on the Kasami APN function: reductions, structure theorems, a proof for $k\bmod n\in\{1,2,n{-}2,n{-}1\}$, and exhaustive verification for $n\le 13$

On a conjecture on the Kasami APN function: reductions, structure theorems, a proof for $k\bmod n\in\{1,2,n{-}2,n{-}1\}$, and exhaustive verification for $n\le 13$

Gábor P. Nagy, Attila Vajda

math.CO Aug 19, 2026 · v2 math.NT
formalization combinatorics cryptography ai-agents
Read PDF arXiv abstract Code
TL;DR
Results formally verified in Lean 4 by Aristotle (Harmonic), building on a companion Lean repository proving APN/AB properties of the Kasami function.
Abstract
We study Carlet's cyclic-additive conjecture for the Kasami almost perfect nonlinear (APN) function $F(x)=x^{4^k-2^k+1}$ on $GF(2^n)$, $\gcd(k,n)=1$: for the $2^{n-1}$-element set $Δ=\{F(b)+F(b+1)+1: b\in GF(2^n)\}$ and all distinct nonzero $v_1,v_2\in GF(2^n)$, \[ \bigl|\{(x,y,z)\inΔ^3 : v_1x+v_2y+(v_1+v_2)z=0\}\bigr| \;=\; 2^{2n-3}. \] This exact triple-count condition was first formulated by Carlet in his 2018 cyclic-additive difference-set framework; the Kasami instance was subsequently posed as an open problem at the NSUCRYPTO 2019 cryptographic olympiad, whose individual proposer was not publicly disclosed. We prove the conjecture for $k\bmod n\in\{1,2,n-2,n-1\}$, in particular a complete proof for $k=2$ ($d=13$) via a quadratic-form theory and an exact root-count reduction, and we verify it exhaustively by computer for every admissible $(n,k)$ with $n\le13$.
Problem

Carlet's cyclic-additive conjecture for the Kasami APN function x^{4^k-2^k+1} on GF(2^n) asserts that a triple count over the set Δ of shifted derivative values always equals 2^{2n-3}. The Kasami instance was posed as an open problem at NSUCRYPTO 2019.

Approach

The count is reduced via additive characters to the vanishing of a character sum Z(ρ). This is reformulated as a balancedness statement for the derivative and then as an exact statement about the inverse of the Müller–Cohen–Matthews permutation, using a Frobenius transfer to reduce to odd k. Quadratic-form theory and exact root counts settle the special cases, and exhaustive computation covers small n. Proofs were produced by an AI assistant, built on a companion Lean 4 repository, and later formally verified in Lean 4 by Aristotle.

Results

The conjecture is proved for k mod n in {1, 2, n−2, n−1}, including a complete proof for k=2 (d=13). It is verified exhaustively for all admissible (n,k) with n ≤ 13. A natural termwise-vanishing mechanism is shown to fail, and a hypothesis missing from the background facts (MCM is a permutation only for odd k) is corrected.