Formal Analysis of a Public-Key Algorithm

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article, a formal specification and verification of the Rabin public-key scheme in a formal proof system is presented. The idea is to use the two views of cryptographic verification: the computational approach relying on the vocabulary of probability theory and complexity theory and the formal approach based on ideas and techniques from logic and programming languages. A major objective of this article is the presentation of the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Moreover, we explicate a (computer-proven) formalization of correctness as well as a computer verification of security properties using a straight-forward computation model in Isabelle/HOL. The analysis uses a given database to prove formal properties of our implemented functions with computer support. The main task in designing a practical formalization of correctness as well as efficient computer proofs of security properties is to cope with the complexity of cryptographic proving. We reduce this complexity by exploring a light-weight formalization that enables both appropriate formal definitions as well as efficient formal proofs. Consequently, we get reliable proofs with a minimal error rate augmenting the used database, what provides a formal basis for more computer proof constructions in this area.

Keywords: public-key encryption, Rabin public-key scheme, formalproof system, higher-order logic, formal verification.

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

References:

[1] Martin Abadi and Jan J¨urjens. Formal Eavesdropping and its Computational Interpretation, 2001.
[2] Johannes Buchmann. Einf¨uhrung in die Kryptographie. Springer-Verlag, 2 edition, 2001.
[3] Johannes Buchmann and Markus Kaiser. Computer Verification in Cryptography. In International Conference of Computer Science, Vienna, Austria, volume 12, 2006.
[4] Johannes Buchmann, Tsuyoshi Takagi, and Markus Kaiser. A Framework for Machinery Proofs in Probability Theory for Use in Cryptography, 2005. Kryptotag in Darmstadt.
[5] http://www.verisoft.de.
[6] 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.
[7] Michael Rabin. Digitalized signatures and public key functions as intractable as factorization, 1979. Massachusetts Institute of Technology, Laboratory for Computer Science, Cambridge, Massachusetts.
[8] Nigel Smart. Cryptography: An Indroduction. McGraw-Hill Education, 2003.
[9] Christoph Sprenger, Michael Backes, Birgit Pfitzmann, and Michael Waidner. Cryptographically Sound Theorem Proving, 2006.
[10] http://isabelle.in.tum.de.