Computer Verification in Cryptography

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

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 (o--algebras, probability spaces and condi¬tional 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 crypto-graphic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) proba¬bility distributions, formal proof system, higher-order logic, formal verification, Bayes' Formula, Miller-Rabin primality test.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1330123

References:

[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 HarriDeutsch, 10 edition, 1997.
[7] Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL– A Proof Assistant for Higher-Order Logic, volume 2283 of LectureNotes in Computer Science. Springer-Verlag, 2002.
[8] V. Shoup. OAEP Reconsidered. In Advances in Cryptology – CRYPTO2001, 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.