A Formal Approach for Proof Constructions in Cryptography
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 (σ-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 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.
[1] Heinz Bauer. Wahrscheinlichkeitstheorie. Walter de Gruyter Verlag, 5
edition, 2001.
[2] M. Bellare and P. Rogaway. Random oracles are practical: a paradigm
for designing efficient protocols. In proceedings of the First ACM
Conference on Computer and Communication Security, 1993.
[3] Johannes Buchmann. Einf¨uhrung in die Kryptographie. Springer-Verlag,
2 edition, 2001.
[4] E. Fujisaki, T. Okamoto, D. Pointcheval, and J. Stern. RSA-OAEP is
secure under the RSA assumption. In proceedings of CRYPTO 2001,
2001.
[5] Hans-Otto Georgii. Stochastik. Walter de Gruyter Verlag, 1 edition,
2002.
[6] B.W. Gnedenko. Lehrbuch der Wahrscheinlichkeitstheorie. Verlag Harri
Deutsch, 10 edition, 1997.
[7] Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL
- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture
Notes in Computer Science. Springer-Verlag, 2002.
[8] V. Shoup. OAEP Reconsidered. In Advances in Cryptology - CRYPTO
2001, volume 2139 of Lecture Notes of Computer Science, pages 239-
259. Springer-Verlag, 2001.
[9] http://isabelle.in.tum.de.
[10] Dietmar W¨atjen. Kryptographie - Grundlagen, Algorithmen, Protokolle.
Spektrum Akademischer Verlag, 2004.
[1] Heinz Bauer. Wahrscheinlichkeitstheorie. Walter de Gruyter Verlag, 5
edition, 2001.
[2] M. Bellare and P. Rogaway. Random oracles are practical: a paradigm
for designing efficient protocols. In proceedings of the First ACM
Conference on Computer and Communication Security, 1993.
[3] Johannes Buchmann. Einf¨uhrung in die Kryptographie. Springer-Verlag,
2 edition, 2001.
[4] E. Fujisaki, T. Okamoto, D. Pointcheval, and J. Stern. RSA-OAEP is
secure under the RSA assumption. In proceedings of CRYPTO 2001,
2001.
[5] Hans-Otto Georgii. Stochastik. Walter de Gruyter Verlag, 1 edition,
2002.
[6] B.W. Gnedenko. Lehrbuch der Wahrscheinlichkeitstheorie. Verlag Harri
Deutsch, 10 edition, 1997.
[7] Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL
- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture
Notes in Computer Science. Springer-Verlag, 2002.
[8] V. Shoup. OAEP Reconsidered. In Advances in Cryptology - CRYPTO
2001, volume 2139 of Lecture Notes of Computer Science, pages 239-
259. Springer-Verlag, 2001.
[9] http://isabelle.in.tum.de.
[10] Dietmar W¨atjen. Kryptographie - Grundlagen, Algorithmen, Protokolle.
Spektrum Akademischer Verlag, 2004.
@article{"International Journal of Information, Control and Computer Sciences:54753", author = "Markus Kaiser and Johannes Buchmann", title = "A Formal Approach for Proof Constructions in Cryptography", 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 (σ-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 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.", keywords = "prime numbers, primality tests, (conditional) probabilitydistributions, formal proof system, higher-order logic, formalverification, Bayes' Formula, Miller-Rabin primality test.", volume = "2", number = "2", pages = "389-8", }