POPL 2020 (series) / CPP 2020 (series) / The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs /
Verified Security of BLT Signature Scheme
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.
Slides (slides.pdf) | 149KiB |
Tue 21 Jan Times are displayed in time zone: Saskatchewan, Central America change
Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change
11:45 - 12:30: Verified cryptographyCPP at Maurepas Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
11:45 - 12:07 Talk | Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL CPP David ButlerAlan Turing Institute, David AspinallUniversity of Edinburgh, Adria GasconAlan Turing Institute DOI Pre-print Media Attached | ||
12:07 - 12:30 Talk | Verified Security of BLT Signature Scheme CPP Denis FirsovGuardtime AS, Ahto BuldasTallinn University of Technology, Ahto TruuGuardtime AS, Risto LaanojaGuardtime AS DOI Pre-print Media Attached File Attached |