@article{(Open Science Index):https://publications.waset.org/pdf/13059,
	  title     = {Computer Proven Correctness of the Rabin Public-Key Scheme},
	  author    = {Johannes Buchmann and  Markus Kaiser},
	  country	= {},
	  institution	= {},
	  abstract     = { 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.},
	    journal   = {International Journal of Computer and Information Engineering},
	  volume    = {1},
	  number    = {3},
	  year      = {2007},
	  pages     = {625 - 630},
	  ee        = {https://publications.waset.org/pdf/13059},
	  url   	= {https://publications.waset.org/vol/3},
	  bibsource = {https://publications.waset.org/},
	  issn  	= {eISSN: 1307-6892},
	  publisher = {World Academy of Science, Engineering and Technology},
	  index 	= {Open Science Index 3, 2007},
	}