@article{(Open Science Index):https://publications.waset.org/pdf/4326, title = {A Computer Proven Application of the Discrete Logarithm Problem}, author = {Sebastian Kusch and Markus Kaiser}, country = {}, institution = {}, 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. }, journal = {International Journal of Computer and Information Engineering}, volume = {1}, number = {5}, year = {2007}, pages = {1302 - 1306}, ee = {https://publications.waset.org/pdf/4326}, url = {https://publications.waset.org/vol/5}, bibsource = {https://publications.waset.org/}, issn = {eISSN: 1307-6892}, publisher = {World Academy of Science, Engineering and Technology}, index = {Open Science Index 5, 2007}, }