Sebastian Kusch and Markus Kaiser
A Computer Proven Application of the Discrete Logarithm Problem
1302 - 1306
2007
1
5
International Journal of Computer and Information Engineering
https://publications.waset.org/pdf/4326
https://publications.waset.org/vol/5
World Academy of Science, Engineering and Technology
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 IsabelleHOL. 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 IsabelleHOL system. We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic signature scheme.
Open Science Index 5, 2007