Formal Analysis of a Public-Key Algorithm

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.

• Markus Kaiser
• Johannes Buchmann

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

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