Paper 2020/028
Verified Security of BLT Signature Scheme
Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja
Abstract
The majority of real-world applications of digital signatures use timestamping to ensure non-repudiation in face of possible key revocations. This observation led Buldas, Laanoja, and Truu to a server-assisted digital signature scheme built around cryptographic timestamping. In this paper, we report on the machine-checked proofs of existential unforgeability under the chosen-message attack (EUF-CMA) of some variations of BLT digital signature scheme. The proofs are developed and verified using the EasyCrypt framework, which provides interactive theorem proving supported by the state-of-the-art SMT solvers.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. ACM SIGPLAN CPP 2020
- DOI
- 10.1145/3372885.3373828
- Keywords
- digital signaturesEasyCryptformalized cryptographytimestamping
- Contact author(s)
- denis firsov @ guardtime com
- History
- 2020-01-30: revised
- 2020-01-13: received
- See all versions
- Short URL
- https://ia.cr/2020/028
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2020/028,
author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja},
title = {Verified Security of {BLT} Signature Scheme},
howpublished = {Cryptology {ePrint} Archive, Paper 2020/028},
year = {2020},
doi = {10.1145/3372885.3373828},
url = {https://eprint.iacr.org/2020/028}
}
