@article{(Open Science Index):https://publications.waset.org/pdf/6288, title = {Formal Analysis of a Public-Key Algorithm}, author = {Markus Kaiser and Johannes Buchmann}, country = {}, institution = {}, 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. }, journal = {International Journal of Computer and Information Engineering}, volume = {1}, number = {9}, year = {2007}, pages = {2761 - 2768}, ee = {https://publications.waset.org/pdf/6288}, url = {https://publications.waset.org/vol/9}, bibsource = {https://publications.waset.org/}, issn = {eISSN: 1307-6892}, publisher = {World Academy of Science, Engineering and Technology}, index = {Open Science Index 9, 2007}, }