<?xml version="1.0" encoding="UTF-8"?> <article key="pdf/5664" mdate="2008-02-21 00:00:00"> <author>Markus Kaiser and Johannes Buchmann</author> <title>A Formal Approach for Proof Constructions in Cryptography</title> <pages>587 - 594</pages> <year>2008</year> <volume>2</volume> <number>2</number> <journal>International Journal of Computer and Information Engineering</journal> <ee>https://publications.waset.org/pdf/5664</ee> <url>https://publications.waset.org/vol/14</url> <publisher>World Academy of Science, Engineering and Technology</publisher> <abstract>In this article we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (&amp;sigma;algebras, probability spaces and conditional probabilities). These are given in the formal language of the formal proof system IsabelleHOL. Moreover, we computer prove Bayes Formula. Besides, we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this article shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in cryptographic research, if the corresponding basic mathematical knowledge is available in a database.</abstract> <index>Open Science Index 14, 2008</index> </article>