Commenced in January 2007
Frequency: Monthly
Edition: International
Paper Count: 1

Publications

1 A Computer Proven Application of the Discrete Logarithm Problem

Authors: Markus Kaiser, Sebastian Kusch

Abstract:

In this paper we analyze the application of a formal proof system to the discrete logarithm problem used in publickey cryptography. That means, we explore a computer verification of the ElGamal encryption scheme with the formal proof system Isabelle/HOL. More precisely, the functional correctness of this algorithm is formally verified with computer support. Besides, we present a formalization of the DSA signature scheme in the Isabelle/HOL system. We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic signature scheme.

Keywords: formal verification, formal proof system, higher-order logic, cryptographic signature scheme

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1190