Write a Blog >>
Tue 21 Jan 2020 12:07 - 12:30 at Maurepas - Verified cryptography Chair(s): Adam Chlipala

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

Displayed time zone: Saskatchewan, Central America change

11:45 - 12:30
Verified cryptographyCPP at Maurepas
Chair(s): Adam Chlipala Massachusetts Institute of Technology
Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
David Butler Alan Turing Institute, David Aspinall University of Edinburgh, Adria Gascon Alan Turing Institute
DOI Pre-print Media Attached
Verified Security of BLT Signature Scheme
Denis Firsov Guardtime AS, Ahto Buldas Tallinn University of Technology, Ahto Truu Guardtime AS, Risto Laanoja Guardtime AS
DOI Pre-print Media Attached File Attached