The ITB project is presented, developing a symmetric cryptographic isolator designed to wrap standard pseudo-random functions (PRFs) and hash primitives (AES, BLAKE2/3, Areion and others) in a coupled combinatorial and topological barrier. Unlike classical block and stream encryption modes, the ITB architecture aims to structurally isolate the internal primitive, preventing the propagation of differential and linear characteristics, algebraic linearization, and direct encodings for SAT/SMT and MILP solvers across the barrier boundaries. The code is written in Go with low-level optimizations in assembly language for x86_64 and ARM64 (Aarch64) architectures and distributed under the Apache 2.0 license.
Data conversion in ITB is divided into two concatenated levels (Interlocked Barrier, controlled by eight isolated key seeds (8-seed isolation) with local key evolution through a feed-forward cascade (ChainHash). At the first level, the Rank Barrier performs a key combinatorial permutation of each 48-bit block (or 168-bit block for 512-bit primitives), distributing the plaintext bits across three independent regions based on a two-step combination by its number (the space of balanced partitions C(48, 16) * C(32, 16) is about 2^70.20, and in 168-bit mode C(168, 56) * C(112, 56) – about 2^258.60). At the second level, the Pixel Barrier maps data onto a grid of 8-byte elements (8 channels of 7 bits of data and 1 bit of pseudo-random noise in each byte) with a per-pixel key 7-bit cyclic shift, masking of 7-bit channels and selection of the position of the noise bit.
Main features of the project:
- Experimental testing of insulating properties for known non-cryptographic functions (stress test with weak primitives). The repository includes a laboratory bench that inserts the usual FNV-1a hash function inside the barrier. Due to nonlinear combinadic ranking, splitting bytes along the boundaries of 7-bit channels (GCD(7, 8) = 1) and injection of noise bits into each byte, practical inversion or construction of a solvable SAT/SMT model using plaintext and ciphertext is blocked already at the stage of formulating the system of equations.
- Machine-verified formal verification in Lean 4. All 12 basic mathematical, combinatorial and bit-vector theorems of the design (as well as an application scheme for hybrid 3-to-8 key agreement from three independent KEM channels in APPS.md), described in the document PROOFS.md, are fully proven in Lean 4 without using axioms or skipping proofs.