Cryptology ePrint Archive: Report 2020/028

Verified Security of BLT Signature Scheme

Denis Firsov and Ahto Buldas and 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.

Category / Keywords: cryptographic protocols / digital signatures, EasyCrypt, formalized cryptography, timestamping

Original Publication (in the same form): ACM SIGPLAN CPP 2020
DOI:
10.1145/3372885.3373828

Date: received 10 Jan 2020

Contact author: denis firsov at guardtime com

Available format(s): PDF | BibTeX Citation

Version: 20200113:102813 (All versions of this report)

Short URL: ia.cr/2020/028


[ Cryptology ePrint archive ]