Computer Proven Correctness of the Rabin Public-Key Scheme

Authors: Johannes Buchmann, Markus Kaiser

Abstract:

We decribe a formal specification and verification of the Rabin public-key scheme in the formal proof system Is-abelle/HOL. 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. The analysis presented uses a given database to prove formal properties of our implemented functions with computer support. Thema in task in designing a practical formalization of correctness as well as 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 eficient formal proofs. This yields the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Consequently, we get reliable proofs with a minimal error rate augmenting the used database. This 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.1080422

References:

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