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

François Dupressoir; Sara Zain

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

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	IEEE Computer Security Foundations Symposium
Editors	Ralf Küsters, David A. Naumann
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Publication status	Accepted/In press - 8 Dec 2020

Handle.net

Persistent link

Cite this

@inproceedings{7504e383c16e43a48caa07232218a2da,

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

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.",

author = "Fran{\c c}ois Dupressoir and Sara Zain",

year = "2020",

month = dec,

day = "8",

language = "English",

editor = "Ralf K{\"u}sters and Naumann, {David A.}",

booktitle = "IEEE Computer Security Foundations Symposium",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

}

Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem. / Dupressoir, François ; Zain, Sara.
IEEE Computer Security Foundations Symposium. ed. / Ralf Küsters; David A. Naumann. Institute of Electrical and Electronics Engineers (IEEE), 2020.

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

TY - GEN

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

AU - Dupressoir, François

AU - Zain, Sara

PY - 2020/12/8

Y1 - 2020/12/8

N2 - 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.

AB - 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.

M3 - Conference Contribution (Conference Proceeding)

BT - IEEE Computer Security Foundations Symposium

A2 - Küsters, Ralf

A2 - Naumann, David A.

PB - Institute of Electrical and Electronics Engineers (IEEE)

ER -

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

Abstract

Handle.net

Fingerprint

Cite this