**Commenced**in January 2007

**Frequency:**Monthly

**Edition:**International

**Paper Count:**5

# higher-order logic Related Publications

##### 5 A Formal Approach for Proof Constructions in Cryptography

**Authors:**
Markus Kaiser,
Johannes Buchmann

**Abstract:**

**Keywords:**
prime numbers,
primality tests,
formal proof system,
higher-order logic,
Bayes' Formula,
Miller-Rabin primality test,
(conditional) probabilitydistributions,
formalverification

##### 4 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,
formal verification,
primality tests,
(conditional) proba¬bility distributions,
formal proof system,
higher-order logic,
Bayes' Formula,
Miller-Rabin primality test

##### 3 Formal Analysis of a Public-Key Algorithm

**Authors:**
Markus Kaiser,
Johannes Buchmann

**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.

**Keywords:**
Public-Key Encryption,
formal verification,
higher-order logic,
Rabin public-key scheme,
formalproof system

##### 2 A Computer Proven Application of the Discrete Logarithm Problem

**Authors:**
Sebastian Kusch,
Markus Kaiser

**Abstract:**

In this paper we analyze the application of a formal proof system to the discrete logarithm problem used in publickey cryptography. That means, we explore a computer verification of the ElGamal encryption scheme with the formal proof system Isabelle/HOL. More precisely, the functional correctness of this algorithm is formally verified with computer support. Besides, we present a formalization of the DSA signature scheme in the Isabelle/HOL system. We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic signature scheme.

**Keywords:**
formal verification,
formal proof system,
higher-order logic,
cryptographic signature scheme

##### 1 Computer Proven Correctness of the Rabin Public-Key Scheme

**Authors:**
Johannes Buchmann,
Markus Kaiser

**Abstract:**

**Keywords:**
Public-Key Encryption,
formal verification,
higher-order logic,
Rabin public-key scheme,
formalproof system