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
cryptographyformal methodsEasyCryptJasminSchnorr 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
Creative Commons Attribution
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}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.