Paper 2026/107

Verified non-recursive calculation of Beneš networks applied to Classic McEliece

Samuel Kelly, University of Bristol

Abstract

The Beneš network can be utilised to apply a single permutation to different inputs repeatedly. We present novel generalisations of Bernstein's formulae for the control bits of a Beneš network and from them derive an iterative control bit setting algorithm. We provide verified proofs of our formulae and prototype a a provably correct implementation in the Lean language and theorem prover. We develop and evaluate portable and vectorised implementations of our algorithm in the C programming language. Our implementation utilising Intel's Advanced Vector eXtensions 2 feature reduces execution latency by 25% compared to the equivalent implementation in the libmceliece software library.

Note: A supplementary repository (https://github.com/bristolcrypto/controlbits) of relevant artifacts is available as an adjunct to this paper.

@misc{cryptoeprint:2026/107,
      author = {Wrenna Robson and Samuel Kelly},
      title = {Verified non-recursive calculation of Beneš networks applied to Classic {McEliece}},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/107},
      year = {2026},
      url = {https://eprint.iacr.org/2026/107}
}