A Computer Proven Application of the Discrete Logarithm Problem
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.
Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1332058Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1257
 FIPS-PUB 186-2. Digital Signature Standard, January 27, 2000. United States Department of Commerce/National Institute of Standads and Technology.
 Claudia Eckert. IT-Sicherheit. Oldenbourg Wissenschaftsverlag, 2 edition, 2003.
 Taher ElGamal. A Public-Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms. In Advances in Cryptology - CRYPTO 84, pages 10-18. Springer-Verlag, 1984/1985. IEEE Transaction of Information Technology, v. IT-31, n.4, 1985.
 Joe Hurd. Elliptic Curve Cryptography. A case study.
 Markus Kaiser and Johannes Buchmann. Computer Verification in Cryptography. In International Conference of Computer Science, Vienna, Austria, volume 12, 2006.
 Markus Kaiser, Johannes Buchmann, and Tsuyoshi Takagi. A Framework for Machinery Proofs in Probability Theory for Use in Cryptography, 2005. Kryptotag in Darmstadt.
 Sebastian Kusch. Formalizing the DSA Signature Scheme in Isabelle/ HOL. Diplomarbeit, Technische Universit┬¿at Darmstadt, 2007.
 Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002.
 Michael Rabin. Digitalized signatures and public key functions as intractable as factorization, 1979. Massachusetts Institute of Technology, Laboratory for Computer Science, Cambridge, Massachusetts.