Paper 2023/752

Schnorr protocol in Jasmin

José Bacelar Almeida, Universidade do Minho, Braga, Portugal, INESC TEC, Porto, Portugal
Denis Firsov, Tallinn University of Technology, Guardtime
Tiago Oliveira, Max Planck Institute for Security and Privacy
Dominique Unruh, University of Tartu

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).

Available format(s)
Publication info
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
2023-06-16: revised
2023-05-24: received
See all versions
Short URL
Creative Commons Attribution


      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},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.