{"title":"Formal Analysis of a Public-Key Algorithm","authors":"Markus Kaiser, Johannes Buchmann","volume":9,"journal":"International Journal of Computer and Information Engineering","pagesStart":2761,"pagesEnd":2769,"ISSN":"1307-6892","URL":"https:\/\/publications.waset.org\/pdf\/6288","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.<\/p>\r\n","references":"[1] Martin Abadi and Jan J\u252c\u00bfurjens. Formal Eavesdropping and its Computational\r\nInterpretation, 2001.\r\n[2] Johannes Buchmann. Einf\u252c\u00bfuhrung in die Kryptographie. Springer-Verlag, 2 edition, 2001.\r\n[3] Johannes Buchmann and Markus Kaiser. Computer Verification in\r\nCryptography. In International Conference of Computer Science, Vienna,\r\nAustria, volume 12, 2006.\r\n[4] Johannes Buchmann, Tsuyoshi Takagi, and Markus Kaiser. A Framework\r\nfor Machinery Proofs in Probability Theory for Use in Cryptography,\r\n2005. Kryptotag in Darmstadt.\r\n[5] http:\/\/www.verisoft.de.\r\n[6] Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle\/HOL\r\n- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture\r\nNotes in Computer Science. Springer-Verlag, 2002.\r\n[7] Michael Rabin. Digitalized signatures and public key functions as\r\nintractable as factorization, 1979. Massachusetts Institute of Technology,\r\nLaboratory for Computer Science, Cambridge, Massachusetts.\r\n[8] Nigel Smart. Cryptography: An Indroduction. McGraw-Hill Education,\r\n2003.\r\n[9] Christoph Sprenger, Michael Backes, Birgit Pfitzmann, and Michael\r\nWaidner. Cryptographically Sound Theorem Proving, 2006.\r\n[10] http:\/\/isabelle.in.tum.de.","publisher":"World Academy of Science, Engineering and Technology","index":"Open Science Index 9, 2007"}