Paper 2023/752
Schnorr protocol in Jasmin
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
-
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} }