期刊名称：International Journal of Computer Systems Science and Engineering
印刷版ISSN：1307-430X
出版年度：2007
卷号：03
期号：02
页码：60-60
出版社：World Academy of Science, Engineering and Technology
摘要：In this paper 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 (σ-algebras, probability spaces and conditional
probabilities). These are given in the formal language of the
formal proof system Isabelle/HOL. Moreover, we computer prove
Bayes¡¯ Formula. Besides we describe an application of the presented
formalized probability distributions to cryptography. Furthermore,
this paper 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.
Loading...
