Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

Abstract

Digital signatures based on the Discrete Logarithm (DL) problem often suffer from long signature sizes, and reductions made loose by the use of Pointcheval and Stern's Forking Lemma.
At EUROCRYPT 2003, Goh and Jarecki provided the first forking-free proof of unforgeability for a DL-based signature scheme—rooting its security in the hardness of the Computational Diffie-Hellman problem in the random oracle model.
In this paper, we present and discuss the first machine-checked proofs for DL-based signature schemes reducing tightly to CDH, produced using EasyCrypt. We craft our proofs around a shim which reduces the local proof effort, and helps us identify patterns that can be easily adapted to similar tightly-secure DL-based schemes.
Original languageEnglish
Title of host publicationIEEE Computer Security Foundations Symposium
EditorsRalf Küsters, David A. Naumann
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Publication statusAccepted/In press - 8 Dec 2020

Fingerprint Dive into the research topics of 'Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem'. Together they form a unique fingerprint.

Cite this