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.

• Sebastian Kusch
• Markus Kaiser

• Formal proof system
• higher-order logic
• formal verification
• cryptographic signature scheme.

[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.