Computer Proven Correctness of the Rabin Public-Key Scheme

The authors describe a formal specification and verification of the Rabin public-key scheme in the formal proof system Isabelle/ 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 their implemented functions with computer support. The main task in designing a practical formalization of correctness as well as security properties is to cope with the complexity of cryptographic proving.