Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem
François Dupressoir, Sara Zain · 2021
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.