Paper 2026/107 Original: eprint.iacr.org/2026/107 ↗
Verified non-recursive calculation of Beneš networks applied to Classic McEliece
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.
Metadata
- Available format(s)
PDF- Category
- Implementation
- Publication info
- Preprint.
- History
- 2026-09-24: last updated
- 2026-01-23: published
- Short URL
- https://ia.cr/2026/107
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@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}
}