Veriﬁed non-recursive calculation of Beneš networks applied to Classic McEliece

Wrenna Robson; Samuel Kelly

Paper 2026/107

Veriﬁed non-recursive calculation of Beneš networks applied to Classic McEliece

Wrenna Robson

, University of Bristol

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.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Preprint.
Keywords: Computer aided cryptography formal methods efficient soft- ware implementation permutation networks
Contact author(s): wrenna robson @ bristol ac uk
sam j kelly 2020 @ bristol ac uk
History: 2026-01-25: approved; 2026-01-23: received; See all versions
Short URL: https://ia.cr/2026/107
License: CC BY

BibTeX

@misc{cryptoeprint:2026/107,
      author = {Wrenna Robson and Samuel Kelly},
      title = {Veriﬁed 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}
}