Soundness of Symbolic Equivalence for Modular Exponentiation

Yassine Lakhnech 1 Laurent Mazare 1 Bogdan Warinschi 2
1 VERIMAG - IMAG - VERIMAG
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper, we study the Dynamic Decisional Diffie-Hellman (3DH) problem, a powerful generalization of the Decisional Diffie-Hellman (DDH) problem. Our main result is that DDH implies 3DH. This result leads to significantly simpler proofs for protocols by relying directly on the more general problem. Our second contribution is a computationally sound symbolic technique for reasoning about protocols that use symmetric encryption and modular exponentiation. We show how to apply our results in the case of the Burmester & Desmedt protocol.
Keywords : Diffie-Hellman assumptions soundness of formal encryption provable security
Document type :
Conference papers
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download
https://hal.inria.fr/inria-00080673
Contributor : Véronique Cortier <>
Submitted on : Tuesday, June 20, 2006 - 3:03:19 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM
Long-term archiving on : Monday, April 5, 2010 - 11:06:34 PM

File

paper4.pdf

Identifiers

  • HAL Id : inria-00080673, version 1

Collections

INRIA | FCC2006 | IMAG | UNIV-FCOMTE | UGA | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | LORIA | UNIV-LORRAINE | VERIMAG

Citation

Yassine Lakhnech, Laurent Mazare, Bogdan Warinschi. Soundness of Symbolic Equivalence for Modular Exponentiation. Workshop on Formal and Computational Cryptography - FCC 2006, Véronique Cortier et Steve Kremer, Jul 2006, Venice/Italy. ⟨inria-00080673⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

341

Files downloads

156

Contact


archive-ouverte@inria.fr