{"title":"A Computer Proven Application of the Discrete Logarithm Problem","authors":"Sebastian Kusch, Markus Kaiser","volume":5,"journal":"International Journal of Computer and Information Engineering","pagesStart":1302,"pagesEnd":1307,"ISSN":"1307-6892","URL":"https:\/\/publications.waset.org\/pdf\/4326","abstract":"<p>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>\r\n","references":"[1] FIPS-PUB 186-2. Digital Signature Standard, January 27, 2000. United\r\nStates Department of Commerce\/National Institute of Standads and\r\nTechnology.\r\n[2] Claudia Eckert. IT-Sicherheit. Oldenbourg Wissenschaftsverlag, 2\r\nedition, 2003.\r\n[3] Taher ElGamal. A Public-Key Cryptosystem and a Signature Scheme\r\nBased on Discrete Logarithms. In Advances in Cryptology - CRYPTO\r\n84, pages 10-18. Springer-Verlag, 1984\/1985. IEEE Transaction of\r\nInformation Technology, v. IT-31, n.4, 1985.\r\n[4] Joe Hurd. Elliptic Curve Cryptography. A case study.\r\n[5] Markus Kaiser and Johannes Buchmann. Computer Verification in\r\nCryptography. In International Conference of Computer Science, Vienna,\r\nAustria, volume 12, 2006.\r\n[6] Markus Kaiser, Johannes Buchmann, and Tsuyoshi Takagi. A Framework\r\nfor Machinery Proofs in Probability Theory for Use in Cryptography,\r\n2005. Kryptotag in Darmstadt.\r\n[7] Sebastian Kusch. Formalizing the DSA Signature Scheme in Isabelle\/\r\nHOL. Diplomarbeit, Technische Universit\u252c\u00bfat Darmstadt, 2007.\r\n[8] Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle\/HOL\r\n- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture\r\nNotes in Computer Science. Springer-Verlag, 2002.\r\n[9] Michael Rabin. Digitalized signatures and public key functions as\r\nintractable as factorization, 1979. Massachusetts Institute of Technology,\r\nLaboratory for Computer Science, Cambridge, Massachusetts.\r\n[10] http:\/\/isabelle.in.tum.de.","publisher":"World Academy of Science, Engineering and Technology","index":"Open Science Index 5, 2007"}