Computer Proven Correctness of the Rabin Public-Key Scheme

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.

Authors:

• Johannes Buchmann
• Markus Kaiser

Keywords:

• public-key encryption
• Rabin public-key scheme
• formalproof system
• higher-order logic
• formal verification.

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.