%0 Journal Article
	%A Sebastian Kusch and  Markus Kaiser
	%D 2007
	%J International Journal of Computer and Information Engineering
	%B World Academy of Science, Engineering and Technology
	%I Open Science Index 5, 2007
	%T A Computer Proven Application of the Discrete Logarithm Problem
	%U https://publications.waset.org/pdf/4326
	%V 5
	%X 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.

	%P 1302 - 1306