Schnorr protocol in Jasmin

Denis Firsov; Tiago Oliveira; Dominique Unruh

Paper 2023/752

Schnorr protocol in Jasmin

Denis Firsov

, Tallinn University of Technology, Guardtime

Tiago Oliveira

, Max Planck Institute for Security and Privacy

Dominique Unruh

, University of Tartu

Abstract

We implement the Schnorr proof system in assembler via the Jasmin toolchain, and prove the security (proof-of-knowledge property) and the absence of leakage through timing side-channels of that implementation in EasyCrypt. In order to do so, we show how leakage-freeness of Jasmin programs can be proven for probabilistic programs (that are not constant-time). We implement and verify algorithms for fast constant-time modular multiplication and exponentiation (using Barrett reduction and Montgomery ladder). We implement and verify 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: cryptography formal methods EasyCrypt Jasmin Schnorr protocol
Contact author(s): denis firsov @ gmail com
tiago oliveira @ mpi-sp org
unruh @ ut ee
History: 2023-05-25: approved; 2023-05-24: received; See all versions
Short URL: https://ia.cr/2023/752
License: CC BY

BibTeX

@misc{cryptoeprint:2023/752,
      author = {Denis Firsov and Tiago Oliveira and Dominique Unruh},
      title = {Schnorr protocol in Jasmin},
      howpublished = {Cryptology ePrint Archive, Paper 2023/752},
      year = {2023},
      note = {\url{https://eprint.iacr.org/2023/752}},
      url = {https://eprint.iacr.org/2023/752}
}