A Computer Proven Application of the Discrete Logarithm Problem

Authors: Sebastian Kusch, Markus Kaiser

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.

Keywords: Formal proof system, higher-order logic, formal verification, cryptographic signature scheme.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1332058

References:

[1] FIPS-PUB 186-2. Digital Signature Standard, January 27, 2000. United States Department of Commerce/National Institute of Standads and Technology.
[2] Claudia Eckert. IT-Sicherheit. Oldenbourg Wissenschaftsverlag, 2 edition, 2003.
[3] 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.
[4] Joe Hurd. Elliptic Curve Cryptography. A case study.
[5] Markus Kaiser and Johannes Buchmann. Computer Verification in Cryptography. In International Conference of Computer Science, Vienna, Austria, volume 12, 2006.
[6] Markus Kaiser, Johannes Buchmann, and Tsuyoshi Takagi. A Framework for Machinery Proofs in Probability Theory for Use in Cryptography, 2005. Kryptotag in Darmstadt.
[7] Sebastian Kusch. Formalizing the DSA Signature Scheme in Isabelle/ HOL. Diplomarbeit, Technische Universit¨at Darmstadt, 2007.
[8] 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.
[9] Michael Rabin. Digitalized signatures and public key functions as intractable as factorization, 1979. Massachusetts Institute of Technology, Laboratory for Computer Science, Cambridge, Massachusetts.
[10] http://isabelle.in.tum.de.