Paper 2023/752
Schnorr protocol in Jasmin
, Universidade do Minho, Braga, Portugal, INESC TEC, Porto, Portugal, Tallinn University of Technology, Guardtime, Max Planck Institute for Security and Privacy, University of TartuAbstract
We implement the Schnorr protocol in assembler via the Jasmin toolchain, and prove the security (proof-of-knowledge and zero-knowledge properties) and the absence of leakage through timing side-channels of that implementation in EasyCrypt. In order to do so, we provide a semantic characterization of leakage-freeness for probabilistic Jasmin programs (that are not constant-time). We design a library for multiple-precision integer arithmetic in Jasmin -- the "libjbn'' library. Among others, we implement and verify algorithms for fast constant-time modular multiplication and exponentiation (using Barrett reduction and Montgomery ladder). We also implement and verify correctness and leakage-freeness of the rejection sampling algorithm. And finally, we put it all together and show the security of the overall implementation (end-to-end verification) of the Schnorr protocol, by connecting our implementation to prior security analyses in EasyCrypt (Firsov, Unruh, CSF~2023).
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- cryptographyformal methodsEasyCryptJasminSchnorr protocolmultiple-precision integer arithmetic
- Contact author(s)
-
jba @ di uminho pt
denis firsov @ gmail com
tiago oliveira @ mpi-sp org
unruh @ ut ee - History
- 2023-06-16: revised
- 2023-05-24: received
- See all versions
- Short URL
- https://ia.cr/2023/752
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2023/752,
author = {José Bacelar Almeida and Denis Firsov and Tiago Oliveira and Dominique Unruh},
title = {Schnorr protocol in Jasmin},
howpublished = {Cryptology {ePrint} Archive, Paper 2023/752},
year = {2023},
url = {https://eprint.iacr.org/2023/752}
}
