Paper 2020/1493 Original: eprint.iacr.org/2020/1493 ↗
Verified fast formulas for control bits for permutation networks
Abstract
This paper presents detailed and computer-verified proofs of formulas that, given a permutation pi of 2^m indices with m>=1, produce control bits for a standard permutation network that uses 2^m(m-1/2) swaps to apply pi to a list. The formulas match the control bits computed by a serial algorithm of Stone (1968) and a parallel algorithm of Nassimi–Sahni (1982). The proofs are a step towards computer-verified correctness proofs for efficient implementations of these algorithms.
Metadata
- Available format(s)
PDF
- Category
- Implementation
- Publication info
- Preprint.
- History
- 2020-11-29: last updated
- 2020-11-29: published
- Short URL
- https://ia.cr/2020/1493
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2020/1493,
author = {Daniel J. Bernstein},
title = {Verified fast formulas for control bits for permutation networks},
howpublished = {Cryptology {ePrint} Archive, Paper 2020/1493},
year = {2020},
url = {https://eprint.iacr.org/2020/1493}
}