@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},
	}