Wrenna Robson
University of Bristol, Bristol, UK

Samuel Kelly
University of Bristol, Bristol, UK

Keywords: Computer aided cryptography, formal methods, efficient software implementation, permutation networks

Abstract

The Beneš network can be utilised to apply a single permutation to different inputs repeatedly. We present novel generalisations of Bernstein’s [Ber20] 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 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 29% compared to the equivalent implementation in the libmceliece software library on the Intel Ultra 7 165U CPU.