WASET
	@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},
	}