Certifying cryptographic algorithms

using the Coq system

Sabrina Tarento

March 23, 2005

Report of Master’s Internship carried out to the INRIA Sophia Antipolis under the direction of Gilles BARTHE, Responsible for Research

Abstract Formal methods have been extensively applied to the certification of cryptographic protocols. However, most of these works make the perfect cryptography assumption, i.e. the hypothese that there is no way to obtain knowledge about the plain-text pertaining to a cipher-text without knowing the key. Yet recent work has shown that such an assumption is unrealistic in practice.

As a first step towards relaxing the perfect cryptography assumption in formal correctness proofs of cryptographic protocols, we study the problem of proving cryptographic algorithms secure. To this end, we follow the so-called generic model, developed by Nechaev, Shoup, and Schnorr, in which the safety of cryptosystems can be established directly, rather than by showing a reduction to computationally infeasible problems. More precisely, we develop within the Coq proof assistant a framework in which to reason about generic algorithms, and exploit this framework to prove the safety of the ElGamal cryptosystem against generic attacks. To our best knowledge, this is the first attempt to certify cryptosystems formally in a proof assistant.

Keywords: generic algorithm, generic group model, DL-cryptosystem ElGamal.

Résumé Les méthodes formelles ont été intensivement appliquées à la certification des protocoles cryptographiques. Cependant, la plupart de ces travaux font l’hypothése de cryptographie parfaite, c.a.d, l’hypothése qu’il est impossible d’obtenir des informations sur un texte clair à partir d’un texte chiffré sans connaitre la clef de chiffrement. Pourtant les travaux récents ont prouvé qu’une telle hypothése est peu réaliste dans la pratique.

Dans un premier temps en omettant l’hypothése de cryptographie parfaite dans les preuves formelles de vérification des protocoles cryptographiques, nous étudions le problème de preuves d’algorithmes cryptographiques sûrs. À cet effet, nous suivons le modèle générique, développé par Nechaev, Shoup, et Schnorr, dans lequel la sûreté des systèmes cryptographiques peut être établie directement, plutôt qu’en montrant une réduction aux problèmes informatique à complexité rédhibitoire. Plus précisemment, nous développons sous l’assitant de preuves Coq un cadre dans lequel nous raisonnons sur des algorithmes génériques, et exploitons ce cadre pour prouver la sûreté du système cryptographique d’ El-Gamal contre des attaques génériques. À notre connaissance, c’est la première tentative de certifier des cryptosystèmes formellement dans un assistant de preuves.

Mots-clé: algorithme générique, modèle de groupe générique, DL-cryptosystème ElGamal.

Contents

3

1 Introduction

1.1 Cryptography

Cryptography is the science aiming at ensuring the confidentiality of informations (protection being the object of coding). It is an old science which appears at the Egyptians and which was used by Jules Cesar (shift of 3 letters). The second world war started the expansion of cryptography, in particular with the deciphering of the German system Enigma by the English mathematician Alan Turing. Today, the exponential development of the communication networks, the electronic trade and numerical technologies in general make cryptography impossible to circumvent. Cryptography has several objectives:

Confidentiality: the communication between two parties must not have been seen by a third party and the material of the communication must remain secret.

Integrity: prevent an active adversary from modifying the data transmitted.

Authentification: the identity of the author/sender can be verified so that the receiver knows the message/information did indeed come from the proper source.

Non-repudiation: the sender cannot deny having sent the message nor can they have means to change any of the content (including currency amounts) within the message. This is critical to keeping agreements when time lag (between sending and receiving) sees market conditions change.

For cryptography, there are two major types of systems of coding: secret-key systems, like the AES, and public-key systems like ElGamal.

In secret-key cryptography, the sender and receiver of a message know and use the same secret key; the sender uses the secret key to encrypt the message, and the receiver uses the same secret key to decrypt the message. This method is known as secret key or symmetric cryptography. The main challenge is getting the sender and receiver to agree on the secret key without anyone else finding out. If they are in separate physical locations, they must trust a courier, a phone system, or some other transmission medium to prevent the disclosure of the secret key. Anyone who overhears or intercepts the key in transit can later read, modify, and forge all messages encrypted or authenticated using that key. The generation, transmission and storage of keys is called key management; all cryptosystems must deal with key management issues. Because all keys in a secret-key cryptosystem must remain secret, secret-key cryptography often has difficulty providing secure key management, especially in open systems with a large number of users. In public key cryptosystems, each person gets a pair of keys, a public key and a private key. The public key is published, while the private key is kept secret. The need for the sender and receiver to share secret information is eliminated; all communications involve only public keys, and no private key is ever transmitted or shared. In this system, it is no longer necessary to trust the security of some means of communications. The only requirement is that public keys to be associated with their users in a trusted (authenticated) manner (for instance, in a trusted directory). Anyone can send a confidential message by just using public information, but the message can only be decrypted with the right private key, which is in the sole possession of the intended recipient. Furthermore, publickey cryptography can be used not only for privacy (encryption), but also for authentication (digital signatures) and other various techniques. In a public key cryptosystem, the private key is always linked mathematically to the public key. Therefore, it is always possible to attack a public-key system by deriving the private key from the public key. The typical defense against this is to make the problem of deriving the private key from the public key as difficult as possible. For instance, some public-key cryptosystems are designed such that deriving the private key from the public key requires the attacker to factor a large number, in this case it is computationally infeasible to perform the derivation. This is the idea behind the RSA public-key cryptosystem.

Public-key cryptosystems have two primary uses, encryption and digital signatures.

Encryption When Alice wishes to send a secret message to Bob, she looks up Bob’s public key in a directory, uses it to encrypt the message and sends it off. Bob then uses his private key to decrypt the message and reads it. No-one listening can decrypt the message. Anyone can send an encrypted message to Bob, but only Bob can read it (because only Bob knows Bob’s private key)

Digital Signatures To sign a message, Alice does a computation involving both her private key and the message itself. The output is called a digital signature and is attached to the message. To verify the signature, Bob does a computation involving the message, the purported signature, and Alice’s public key. If the result is correct according to a simple, prescribed mathematical relation, the signature is verified to be genuine; otherwise, the signature is fraudulent, or the message may have been altered.

In cryptography, we often use hash functions and essentially for the provision of digital signatures.

Definition A hash function H is a transformation that takes a variable-size input m and returns a fixed-size string, which is called the hash value h (that is, h = H(m)).

Employed in cryptography the hash functions are usually chosen to have some additional properties. The basic requirements for a cryptographic hash function are:

• the input can be of any length,

• the output has a fixed length,

• H(x) is relatively easy to compute for any given x ,

• H(x) is one-way,

A hash function H is said to be one-way if it is hard to invert, where “hard to invert” means that given a hash value h, it is computationally infeasible to find some input x such that H(x) = h.

1.2 Key-exchange algorithm

This key-exchange algorithm was invented by Whitfield Diffie and Martin Hellman in 1976 [?]. It too was previously invented within GCHQ in Britain, by Malcolm Williamson in 1974. Although it is impossible to encrypt any message directly in the Diffie-Hellman system, it is still useful for sending secret messages. In general terms, it can be thought of as working like this: two parties, sharing a public key, each think of a number. Both parties perform a particular type of hash operations on their number using the public key, and give the result to the other party. This is useful, because there is a function of one original number and the special hash that was calculated of the other number that is the same, regardless of which one of the numbers you have in its original form, and so the two parties can use that product as a conventional encryption key for communicating. Note that the number each party thinks of can also be called a secret key, and the hashed version as a public key.

The Diffie-Hellman method, like RSA, also uses modulus arithmetic, but here the modulus is just a prime number, which we will call P. Exponentiation is involved as well. So, in Diffie-Hellman, the two parties each think of a secret random number, respectively x and y. Each transmits a number A to that power. So, one party knows x and A^{y}, and the other party knows y and A^{x}. Each party can calculate A^{x×y}, since that is (A^{y})^{x} and it is also (A^{x})^{y}, but an eavesdropper, only knowing A^{x} and A^{y}, cannot do this.

A potential danger when Diffie-Hellman is used is that one could, for some values of the modulus P, choose values of A such that A^{x} has only a small number of possible values, no matter what x is, which would make it easy to find for a value of x that was equivalent to the original value of x. This can be defended against by using a modulus P such that P − 1 is equal to twice another prime number. This second, smaller prime number is known as a Sophie Germain prime, after a noted mathematician who was able to prove Fermat’s Last Theorem in the case when the exponent is such a prime.

1.3 ElGamal encryption

The Diffie-Hellman key exchange algorithm is usually described as an active exchange of keys by two parties:

• one party A chooses x, and transmits A^{x} [P],

• A ⟶ B : A^{x} [P]

• the other party B chooses y, and transmits A^{y} [P],

• B ⟶ A : A^{y}[P]

• both parties communicate using A^{xy} [P] as their session key.

ElGamal could be considered to be a special case of this. In ElGamal, to send a message to a party whose public key is A^{y} [P], we send our own public key, A^{x} [P], and in addition the message is enciphered by multiplying it by A^{xy} [P], the multiplication also being modulo P.

1.4 Formal verification of cryptographic protocols

The aim of cryptographic protocols is to distribute keys, authenticate principals and data over a network. The network is usually hostile, it may contain intruders who can read, modify, delete messages, and who may have control of one or more networks principals. A cryptographic protocol must be able to achieve its goals in face of these hostile intruders. Several principals wish to exchange data securely, but are subject to attack by an intruder who can do any sequence of a finite set of operations such as intercepting data, concatening and deconcatening data, encrypting and decrypting data, and so forth.

A number of techniques based on logic theories have recently been developed to provide formal verification of security protocols. Many of these are based on logics of belief, which are considered useful in evaluating the trust which may be placed in a security protocol. Others techniques are based on logics of knowledge, which are suitable for proving protocol security. The formal verification comprises an analysis of automated testing techniques and the development of a new logic for formally analysing public-key protocols. The logic, which combines the logics of knowledge and belief, enables the analysis of the security and trustworthiness of a wide range of security protocols.

Most of Formal verification of cryptographic protocols make the perfect cryptography assumption, i.e. the hypothese that there is no way to obtain knowledge about the plain-text pertaining to a cipher-text without knowing the key. Yet recent work has shown that such an assumption is unrealistic in practice, that’s why we don’t make this assumption and so we need to define a generic algorithm that can guess informations about plain-text without knowing the key.

1.5 The generic Model

Let G be an ideal group of prime order q with generator g. Nechaev [?] proves that the discrete logarithm problem is hard in such a model. The generic model was further elaborated on by Shoup [?]. Schnorr [?] presents the Shoup model in a slightly simpler setup. Encryption are for the private/public key pair (x, h), where x is random in ℤ_{q} and h = g^{x}. In his presentation, Schnorr describe the generic model in detail, first focusing on non-interactive algorithms and thereafter on algorithms interacting with oracles for hashing and decryption. The data of a generic algorithm is partitioned into group elements in G and non-group data. The generic steps for group elements are multivariate exponentiations:

mex: ℤ_{q}^{d} × G^{d} → G
(a_{1}, …, a_{d}, g_{1}, …, g_{d}) ↦ ∏_{i} g_{i}^{a_{i}} with d ≥ 0

Definition 1 A (non-interactive) generic algorithm is a sequence of t generic steps

• f_{1}, …, f_{t′} ∈ G(inputs) 1 ≤ t′ < t,

• f_{i} = ∏_{j=1}^{i−1} f_{j}^{a_{j}} for i = t′ + 1, …, t; where (a_{1}, …, a_{i−1}) ∈ ℤ_{q}^{i−1} depends arbitrarily on i, the non-group input and the set CO_{i−1} := {(j, k)|f_{j} = f_{k}, 1 ≤ j < k ≤ i − 1} of previous collisions of group elements (a collision is an equality between two elements of G).

Typical non-group inputs are given elements in ℤ_{q}, contained in given ciphertexts or signatures. CO_{t} is the set of all collisions found by the algorithm. Some group input f_{i} depends on the random coin flips, e.g., the random public key h = g^{x} depends on the random secret key x ∈ ℤ_{q}. The probability space consists of the random group elements of the input. The logarithms log_{g}f_{i} of the random input f_{i} play the role of secret parameters. Information about secret parameters can only be releaved by collisions. We let the non-group input and the generator g not depend on random bits. The output of a generic algorithm consists of

• non-group data that depend arbitrarily on the non-group input and the set CO_{t} of all collisions,

• group elements f_{σ_{1}}, …, f_{σ_{d}} where the integers σ_{1}, …, σ_{d} ∈ {1, …, t} depend arbitrarily on the non-group input and on CO_{t}.

A generic adversary A, attacking an encryption scheme, is an interactive algorithm that interacts with a decryptor. It performs some t generic steps resulting in t′ ≤ t group elements f_{1}, …, f_{t′}. A iteratively selects the next generic step depending arbitrarily on the non-group input and on previous collisions of group elements.

The computed group elements f_{1}, …, f_{t′} are given as explicit multiplicative combinations of group elements in the input and from decryptor interactions. Let the group elements in the input and from decryptor interactions be g_{1}, …, g_{l}. By induction on j, a computed f_{j} ∈ G is of the form f_{j} = (g_{1})^{a_{j,1}} … (g_{l})^{a_{j,l}}, where the exponents a_{j,1}, …, a_{j,l} ∈ ℤ_{q} depend arbitrarily on given non-group data. A can arbitrarily use the coefficients a_{j,1}, …, a_{j,l} from this explicit representation of f_{j}. A generic adversary is deterministic. Trivial collisions. We call a collision (i, j) ∈ CO_{t} trivial if f_{i} = f_{j} holds with probability 1, i.e., if it holds for all choices of the secret data such as the secret key x and the random bits r of the encipherer. Trivial collisions don’t release any information about the secret data while non-trivial collisions can completely release some secret data. Trivial collisions can be ignored, and so, we can exclude them from CO_{t} so that CO_{t} consists only of non-trivial collisions.

Let us introduce some results for the Generic Model. The following refers to a generic, non-interactive adversary A that performs some t steps in attacking the indistinguishability of ElGamal encryption. Given q, the public key h = g^{x}, two messages m_{0}, m_{1} ∈ G and an ElGamal cipher-text cip_{b} = (g^{r}, m_{b}h^{r}) for random r, x ∈ ℤ_{q} and b ∈ {0, 1}, A guesses b. We show that A doesn’t succeed better than with probability \frac{1}{2} + \frac{2}{q} \binom{t}{2}. The probability space consists of the random group elements g^{r}, g^{x}, m_{b}g^{rx}, or equivalently of the random r, x ∈ ℤ_{q} and b ∈ {0, 1}. Let A compute the group elements f_{1}, …, f_{t}. We state some results and the proofs are given in section 4.1.

Lemma 1 Non-trivial collisions occur with no better probability than \frac{2}{q} \binom{t}{2}. The probability refers to the random b, r, x.

Lemma 2 If there are no non-trivial collisions of group elements then the random b, r, x are statistically independent of the computed non-group data except that the b, r, x leading to collisions are excluded.

Proposition 1 (Generic DL-complexity lower bound) Let A, upon input g and h = g^{r} ∈ G, output y ∈ ℤ_{q}. Then P r_{x}(y = log_{g} h) ≤ \frac{1}{q} \binom{t}{2} + \frac{1}{q}.

The larger q is, the smaller is this probability and the more secure is the cryptosystem.

2 The Proof-assistant Coq

The system Coq [?] is designed to write formal specifications, programs and to verify that programs are correct with respect to their specification. It provides a specification language named Gallina. Terms of Gallina can represent programs as well as properties of these programs and proofs of these properties. Using the so-called Curry-Howard isomorphism, programs, properties and proofs are formalized the same language called Calculus of Inductive Constructions, that is a λ-calculus with a rich type system. All logical judgments in Coq are typing judgments. The very heart of the Coq system is the type-checking algorithm that checks the correctness of proofs, in other words that checks that a program complies to its specification. Coq also provides an interactive proof assistant to build proofs using specific programs called tactics. Here, we essentially use inductive types and record types.

2.1 Inductive types

Let us explain how we formalize simple inductive types, the definition of it has the following form:

Inductive ident : sort :=
ident_{1} : type_{1}
|  …
| ident_{n} : type_{n}

The name ident is the name of the inductively defined type and sort is the universes where it lives. The names ident_{1}, …, ident_{n} are the names of its constructors and type_{1}, …, type_{n} their respective types.

A related non-dependent construct is the constructive sum {A} + {B} of two propositions A and B.

Inductive sumbool[A, B : P rop] : Set :=
left : A− > (sumbool A B)
|right : B− > (sumbool A B).

This sumbool construct may be used as a kind of indexed boolean data type.

2.2 Record types

The Record construction is a macro allowing the definition of records as done in most programming languages. The definition of such a record has the following form:

Record ident[params] : sort := ident_{0}{
ident_{1} : term_{1}
…
ident_{n} : term_{n}}

the identifier ident is the name of the defined record and sort is its type. The identifier ident_{0} is the name of its constructor. If ident_{0} is omitted, the default name Build ident is used. The identifiers ident_{1}, …, ident_{n} are the names of fields and term_{1}, …, term_{n} their respective types. Remark that the type of ident_{i} may depend on the previous ident_{j} (for j < i). Thus the order of the fields is important. Finally, params are the parameters of the record. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, Recordident[params] : sort := {ident_{1} : type_{1}; ident_{2} := term_{2}; ident_{3} : type_{3}} in which case the correctness of type_{3} may rely on the instance term_{2} of ident_{2} and term_{2} in turn may depend on ident_{1}.

Our proofs require some concepts of Algebra and Probability.

3 Concepts of Algebra

3.1 The commutative field ℤ_{q}

The secrets are random in ℤ_{q} which must be a field to make some operations over secrets.

3.1.1 Some definitions

Let us suppose q a prime number.

Definition A ring is an abelian group (R, +), together with a second binary operation ∗ such that for all a,b and c in R,

a ∗ (b ∗ c) = (a ∗ b) ∗ c  associativity
a ∗ (b + c) = (a ∗ b) + (a ∗ c) left distributivity
(a + b) ∗ c = (a ∗ c) + (b ∗ c) right distributivity

The ring is known as unitary if its multiplication admits a neutral element. This element is known as unit. It is known as commutative, if its multiplication is commutative. The neutral element of the group known as null and is often called zero by analogy with the ring (ℤ, +, ∗).The ring is known as integral domain if a null product requires that one of the factors is null (i.e. equal to the neutral element for the addition).

Definition A field is a ring in which any element except 0 admits an inverse for the multiplication. In particular, a field is a integral domain. If the multiplication (second law) is commutative, the field is known as commutative.

3.1.2 Formalization

Proof-assistants like Coq rely on powerful type systems and have been successfully used in the formalization of mathematics. Nevertheless, their underlying type theories fail to support extensional concepts such as quotients, which plays a fundamental role in mathematics. The current version of Coq doesn’t implement quotient types. Instead, mathematical formalizations usually rely on setoids, that is mathematical structures packaging a carrier, the “set”; its equality, the “book equality”; and a proof component ensuring that the book equality is well-behaved. A setoid is a constructor for the type of set with an equivalence relation on it. For all q ∈ ℕ we formalize ℤ_{q} in the Coq system like a setoid, we define the equivalence relation mod as being the relation on the setoid in which its elements are in ℤ.

mod := ∀q ∈ ℕ ∀a, b ∈ ℤ ∃k ∈ ℤ | a − b = k × q

We use the formalization of fields made by L.Pottier [?] in order to show that ℤ_{q} is a commutative field. This formalization is for a general setoid so we can apply it to the setoid in ℤ with the modular equality. First, we proved that ℤ_{q} is a ring, so we showed the ring axioms.

Then we proved that ℤ_{q} is a commutative ring, we thus have:

∀a, b ∈ ℤ_{q} a ∗ b ≡ b ∗ a [q]

Finally, to show that ℤ_{q} is a commutative field, we have defined the function that returns the multiplicative inverse :

Zq_{inv} := ℤ_{q} → ℤ_{q}
x ↦ Zmod(x, q)^{q−2}

where Zmod(x, q) is the remainder of the Euclidean division of x per q. And showed:

∀a ∈ ℤ_{q} ¬a ≡ 0 [q]  ⇒  a ∗ Zq_{inv}(a) ≡ 1 [q]
∀a ∈ ℤ_{q} ¬a ≡ 0 [q]  ⇒  Zq_{inv}(a) ∗ a ≡ 1 [q]
¬1 ≡ 0 [q]

3.2 Formalization of polynomials

We initially used the formalization of the polynomials of L.Pottier [?] but it made calculations and proofs of the degree of a polynomial very difficult. Instead we decided to formalize the polynomials in a such way that the calculation of the degree is feasible. We choosed to define a polynomial as a list of monomials with coefficients. A monomial over x_{1}, …, x_{k} is represented as a function of type V ar → ℕ that for each variables gives the exponent.

V ar := (x_{1}, …, x_{k})
Mon := V ar → ℕ
Mon_{wc} := (c_{1}, m_{1}) where c_{1} ∈ ℤ_{q} and m_{1} ∈ Mon
P oly := [(c_{1}, m_{1}), …, (c_{l}, m_{l})]

3.2.1 Equality between two polynomials

There can be several representations of a polynomial, and we do not exclude the possibility that a monomial can occur more than once in a list, and thus to check if two polynomials are equal would be to check that their coefficient corresponding to each monomial are equal. We define a function find coeff which given a polynomial and a monomial returns the result of the sum of all the coefficients corresponding to this monomial.

∀ p, q ∈ P oly

eq pol(p, q) = (∀ m ∈ Mon_{wc} find coeff(p, m) =_{ℤ_{q}} find coeff(q, m))

3.2.2 Addition of two polynomials

The addition of two polynomials is simply the concatenation of the two lists.

add_{pol} : P oly × P oly → P oly
(p, q) ↦ app(p, q)

where app is the function concatenating two lists.

3.2.3 Multiplication of two polynomials

The multiplication of two monomials is the addition of the application of variables to the two monomials:

mult_{mon} : Mon × Mon ⟶ Mon (:= V ar → ℕ)
(m, m′) ⟼ x ↦ m(x) + m′(x)

The multiplication of two monomials with coefficient is the multiplication of the two coefficients and the multiplication of the two monomials:

mult_{mon_{wc}} : Mon_{wc} × Mon_{wc} ⟶ Mon_{wc}
((c, m), (c′, m′)) ⟼ (c ∗ c′, mult_{mon}(m, m′))

The multiplication between a monomial with coefficient and a polynomial is the multiplication of each monomial with coefficient of the list by the monomial with coefficient. To do this we use the function:

∀A, B ∈ T ype
mapT : B^{A} × (list A) ⟶ (list B)
(f, nil) ⟼ nil
(f, cons(a, l)) ⟼ cons(f(a), mapT (f, l))

where nil is the empty list, cons is the function that adds an element to a list, and ∀A ∈ T ype (list A) is the type of lists of elements of A.

mult_{mon_{wc}pol} : Mon_{wc} × poly ⟶ poly
(m, p) ⟼ mapT (mult_{mon_{w}c}(m), p)

where the A and B of the definition of mapT are Mon_{wc}. Finally to formalize the multiplication of two polynomials, we use the function:

∀A, B ∈ T ype
flat mapT : (A → (list B)) × (list A) ⟶ (list B)
(f, nil) ⟼ nil
(f, cons(b, l)) ⟼ app(f(x), flat mapT (f, l))

mult_{pol pol} : poly × poly ⟶ poly
(p, q) ⟼ flat mapT (m ∈ Mon_{wc} ↦ mult_{mon_{wc}pol}(m, q), p)

where the A and B of the definition of mapT are Mon_{wc}.

3.2.4 Evaluation of a polynomial

To define the evaluation of a monomial, we use the fonction:

∀A ∈ Set
proj : ∀k ∈ ℕ (F inset(k + 1) → A) ⟶ (F inset(k) → A)

In our case, A = ℕ and proj is the function that takes a k + 1-variables monomial and returns a k-variables monomial. Now, we can define recursively the evaluation of a monomial.

eval mon : ∀k ∈ ℕ ℤ_{q}^{k} × Mon ⟶ ℤ_{q}
(0,_{,} m) ⟼ 1
(k ≠ 0, x_{1}, …, x_{k}, m) ⟼ x_{k}^{d_{k}} × eval mon(x_{1}, …, x_{k−1}, proj(m))

where d_{k} is the exponent of the kth variable of m It results from this the definition of the evaluation of a monomial with coefficient:

eval mon_{wc} : ℤ_{q}^{k} × Mon_{wc} ⟶ ℤ_{q}
(X, (c, m)) ⟼ c ∗ eval mon(X, m)

Finally, to define the evaluation of a polynomial we construct a function giving the list of the evaluation of her monomials with coefficient:

eval pol list : ℤ_{q}^{k} × poly ⟶ (listℤ_{q})
(X, p) ⟼ mapT (eval mon_{wc}(X), p)

and so:

eval pol : ℤ_{q}^{k} × poly ⟶ ℤ_{q}
(X, p) ⟼ list add(eval pol list(X, p))

where list add is the function takes a list of elements and returns the sum of this elements.

3.2.5 Degree of a polynomial

This formalization of the polynomials allows us to very easily define the degree of a monomial. Indeed, it is just necessary to add the exponent of each variable of the monomial. Thus, the degree of a monomial with coefficient is zero if the coefficient equals zero and the degree of the monomial otherwise. Then we define the list of all the degrees of the monomials with coefficient of the polynomial and the degree of it is thus the maximum element of this list.

Let define F inset(k), a set of k variables, as the simple inductive type.

Inductive F inset : ℕ → Set := fb : ∀n ∈ ℕ, F inset(n + 1)
|fs : ∀n ∈ ℕ, F inset(n) → F inset(n + 1)

To define the degree of a monomial we use the function:

∀A ∈ T ype ∀a ∈ A ∀f ∈ A → A → A

fold finset : ∀k ∈ ℕ (F inset(k) → A) ⟶ A
(0, h) ⟼ a
(n + 1, g) ⟼ (fold finset(n, proj(n, g)), g(fb))

Now we can formalize the degree of a monomial as:

deg mon : Mon ⟶ ℕ
m ⟼ fold finset(k, m)

where in the definition of proj A = ℕ and in fold finset, A = ℕ, a = 0, and

f = minus : ℕ × ℕ → ℕ
(a, b) ↦ a − b

deg mon_{wc} : Mon_{wc} ⟶ ℕ
(0, m) ⟼ 0
(n ≠ 0, m) ⟼ deg mon(m)

And finally, the degree of a polynomial

deg pol : P oly ⟶ ℕ
p ⟼ max(0, list deg(p))

where max is the function that returns the maximum element between 0 and a list of numbers and list deg is the function taking a polynomial and returning the list of the degree of the monomials.

4 Concepts of probability

As all results for the generic model involve probabilities and there is no work about probabilities in Coq, we formalized this in Coq as well.

4.1 Definition and some properties

Definition A law of probability, or probability distribution, is a function prob which given an event A associates a number prob(A), its probability.

The properties which one awaits from a probability are those of the experimental frequencies.

prop 1: for all events A, 0 ≤ prob(A) ≤ 1 prop 2: the probability of the empty event is 0. prob(∅) = 0 prop 3: if (A_{i})_{i∈ℕ} is a list of pairwise disjoint events, i.e, A_{i} and A_{j} can’t occur at the same time if i ≠ j, then

prob(⋃_{i∈ℕ} A_{i}) = ∑_{i∈ℕ} prob(A_{i})

An immediate consequence of these properties is the relation between an event and its contrary writing \overline{A}:

prob(\overline{A}) = 1 − prob(A)

The laws of probability that one handles in practice are of two types, the continuous laws (The whole of the possibilities W is ℝ. The events are the intervals, and all the subsets of ℝ which one can form while combining of the intervals by intersections and unions. In theory of measurement, one calls them borelian) and the discrete laws: the whole of the results is finished W = w_{1}, …, w_{n} and if no information makes it possible to distinguish the results, it is natural to associate each possibility the probability \frac{1}{n}. The probability of any event A is then \frac{Card(A)}{n} This probability particular is called the equiprobability. All calculations in this case are brought back to enumerations:

prob(A) = \frac{number of successful cases}{number of possible cases}

4.2 Formalization

For more readability on the level of the proofs, we showed the majority of the general lemmas without dividing by the cardinal of the universe W. We assume that all the elements of the universe belong to a set V and we see W like a list of elements of V.

W ∈ (list V)

We define an event as a predicate and a decidability on this predicate:

Record Event : T ype := {
event pred :> V → P rop
event dec : (dec pred event pred)}

where dec pred takes a predicate and returns a property of decidability of it:

dec pred : (V → P rop) ⟶ Set
P  ⟼ ∀ x ∈ V {(P x)} + {∼ (P x)}

We define the empty event with the predicate returns False for all elements belonging to V. We define the union of two events P and Q with the predicate returns P (x)∨Q(x) for all element x ∈ V and the intersection with the predicate returns P (x) ∧ Q(x) for all element x ∈ V. And we formalize the contrary event with the predicate returns ¬P (x) for all element x ∈ V. To remove the repetition of elements we define a function filter:

filter : Event × (list V) ⟶ (list V)
(P, nil) ⟼ nil
(P, cons(b, l)) ⟼ if P (b) = T rue then cons(b, filter(P, l))
else filter(P, l)

And now we can define the probability (without dividing by the cardinal of the universe W) of an event:

P roba : Event → ℕ
P ↦ length (filter (P, W))

where length is the function giving the length of a list. We proved the main properties for all events A, B:

0 ≤ P roba(A) ≤ length(W)
P roba(∅) = 0
P roba(A ∪ B) + P roba(A ∩ B) = P roba(A) + P roba(B)

And some properties that we need to prove some lemma over probability, like for all events A, B, C:

P roba(A ∩ B) ≤ P roba(A)
P roba(A) = P roba(A ∩ B) + P roba(A ∩ \overline{B})
P roba((A ∪ B) ∩ C) = P roba((A ∩ C) ∪ (B ∩ C))

And after all the proofs, we define the probability:

P roba : Event → ℝ
P ↦ \frac{P roba(P)}{length (W)}

5 Proofs on the Generic Model

5.1 Proofs about results for the Generic Model

Proof of the Lemma 1 The proof of this lemma uses the following lemma, that we state without proof.

Lemma 3 A multivariate polynomial p ∈ ℤ_{q}[X_{1}, …, X_{k}] of total degree d satisfies for random x_{1}, …, x_{k} ∈ ℤ_{q} that P r_{x_{1},...,x_{k}}[p(x_{1}, …, x_{k}) = 0] ≤ \frac{d}{q} if ¬(p ≡ 0).

First, show that for all i, j such that i < j, ¬f_{i} ≡ f_{j} and for a constant b and random r, x ∈ ℤ_{q}

P r_{r,x}(f_{i} = f_{j}) ≤ \frac{2}{q}

This implies that:

P r_{r,x}(CO_{t} ≠ ∅) = ∑_{1≤i<j≤t} P r_{r,x}(f_{i} = f_{j}) ≤ \frac{2}{q}\binom{t}{2}

where CO_{t} is the set of non-trivial collisions. The group elements in input are g, g^{r}, h, m_{b}h^{r}, m_{0}, m_{1}. All group elements computed are combinations of (g_{1}, g_{2}, g_{3}, g_{4}) = (g, g^{r}, h, m_{b}h^{r}), i.e:

f_{j} = ∏_{ν=1}^{4} g_{ν}^{a_{j,ν}}

where a_{j,ν} ∈ ℤ_{q} depend on non-group data but not on b, r, x. Let see r, x as formal variables of ℤ_{q}, log_{g} f_{j} is a polynomial in ℤ_{q}[r, x] on the form:

a_{j,1} + a_{j,2}r + a_{j,3}x + a_{j,4}(log_{g} m_{b} + rx)

log_{g} f_{i} − log_{g} f_{j} ∈ ℤ_{q}[r, x]

Let d be the degree of this polynomial, d ≥ 1 because trivial collisions were eliminated. We must pay attention to that trivial collisions don’t depend on b, log_{g} f_{i} − log_{g} f_{j} is on the form:

c_{1} + c_{2}r + c_{3}x + c_{4}(log_{g} m_{b} + rx)

where ∀ i ∈ 1, …, 4 c_{i} ∈ ℤ_{q} depends only on q and non-trivial collisions. If f_{i} ≡ f_{j} holds for some b ∈ {0, 1} then c_{4} = 0 and f_{i} ≡ f_{j} ∀ b ∈ {0, 1} and so this equality doesn’t depend on b. Since we have 1 ≤ d ≤ 2, by the Lemma 3 the probability that f_{i}(r, x) = f_{j}(r, x) for random r, x is at most \frac{2}{q} (The factor 2 disappears if m_{b}h^{r} is removed of the input and so the degree is at most 1) □ Proof of the Lemma 3 The random b, r, x enter into the generic compu-

tation only via the group elements g^{r}, g^{x}, m_{b}g^{r}x. Therefore, b, r, x enter into non-group data only via non-trivial collisions of group elements.

□

Proof of the Proposition 1 We use the property that ∀ A, B A = (A ∩ B) ∪ (A ∩ ¬B), so:

P r_{x}(y = log_{g} h) = P r_{x}(y = log_{g} h ∩ CO_{t} ≠ ∅) + P r_{x}(y = log_{g} h ∩ CO_{t} = ∅)

We use Lemma 2 for a generic A with input g, h (without inputs g^{r}, m_{b}h^{r}) so the factor 2 disappears as the polynomials log_{g} f_{j} have total degree ≤ 1.

P r_{x}(y = log_{g} h ∩ CO_{t} ≠ ∅) ≤ P r_{x}(CO_{t} ≠ ∅) ≤ \frac{1}{q}\binom{t}{2}

For a collision-free A, x is statistically independent of the non-group output y and thus P r_{x}(y = log_{g} h) = \frac{1}{q}

P r_{x}(y = log_{g} h ∩ CO_{t} = ∅) ≤ \frac{1}{q}

□

5.2 Formalization

You can see the proofs at http : //www − sop.inria.fr/lemme/Sabrina.Tarento/

and the graph of files dependence in the figure 1.

5.2.1 Formalization of generic algorithms

This is a formalization of the notion non-interactive generic algorithms. Compared to Schnorr’s definition, the formalization is slightly simplified. Since each member of a finite cyclic group can be expressed using the generator g and an exponent, we let the group input consist of only the exponents. The input (1, x, r, log_{g}m + rx) should thus be thought of as (g, g^{x}, g^{r}, mg^{rx}). The group output is simplified in a corresponding way. Consider a group element, computed by the algorithm, on normal form:

f_{i} = (g^{1})^{a_{i,1}} · (g^{x})^{a_{i,2}} · (g^{r})^{a_{i,3}} · (mg^{rx})^{a_{i,4}}

In this case we just output the exponents a_{i,1}, … a_{i,4} computed by the algorithm.

Let Sec be the set of the secrets parameters. To have random secrets parameters, we consider an arbitrary interpretation f : Sec → ℤ_{q}. Instead of defining the notion of statistical independence and of proving that elements are statistically independent from secret, we define ExprS a set of expressions over secrets to specify the type of the output and input elements in the algorithm.

\frac{x ∈ Sec}{secret(x) ∈ ExprS}

\frac{x ∈ ℤ_{q}}{const(x) ∈ ExprS}

\frac{e_{1} ∈ ExprS e_{2} ∈ ExprS}{e_{1} + e_{2} ∈ ExprS}

\frac{e_{1} ∈ ExprS e_{2} ∈ ExprS}{e_{1} ∗ e_{2} ∈ ExprS}

With this definition, an element is statistically independent to the secret if it equals const(a) for a ∈ ℤ_{q}.

Now we can define inductively a notion of generic algorithms: Run:

\overline{empty run ∈ Run}

\frac{R ∈ Run e ∈ (list ExprS)}{step(R, e) ∈ Run}

The output of a Run is defined recursively:

Output : Run → (list (list ExprS))
empty run ↦ nil
step(r, e) ↦ cons(e, Output(r))

The list membership relation for G is defined as usual:

∈_{G}: G × (list G) → 𝔹
(a, nil) ↦ F alse
(a, cons(b, l)) ↦ a =_{G} b ∨ a ∈_{G} l

collisions is now defined using ∈_{G}:

collisions : (list G) → 𝔹
nil ↦ F alse
cons(b, l) ↦ b ∈_{G} l ∨ collisions(l)

The definition of collisions in the output of a Run with respect to a certain interpretation f is:

collisions_{run} : Run → 𝔹
r ↦ collisions(map(ExprS2G, Output(r))

where ExprS2G : (list ExprS) → G takes a list of elements in ExprS, transforms it in list of elements in ℤ_{q} by using the function f and apply the function mex with the input elements and this list. A generic algorithm is a “good” Run and we mean what is “good” by the following predicate. goodrun, below, defines the restrictions for a generic algorithm. A Run is “good” provided that, if there are no collisions in the previous step, the output is constant. goodrun is an inductively defined predicate with respect to a certain interpretation f:

\overline{goodrun(empty run)}

\frac{r ∈ Run goodrun(r) ¬collisions_{run}(r) Const(e) length(e) = nb of Run’s input e ∉ Output(r)}{goodrun(step(r, e))}

\frac{r ∈ Run goodrun(r) collisions_{run}(r)}{goodrun(step(r, e))}

where r is a Run and Const is the function returns if an element of ExprS is constant (i.e, statistically independent of the secrets). Note that, if there are no collisions then e must be constant but if there are collisions e can contain a “secret” value. A consequence of goodrun(r) is also that each output is unique. In thus way trivial collisions are eliminated.

For all Run R, if we have goodrun(R) and there are no non-trivial collisions in the previous Run then all the outputs of the Run R are constants, i.e, for all l ∈ Output(R) and for all e ∈ l, we have e = const(a) where a ∈ ℤ_{q}.

If a Run r holds goodrun(r) then we can consider r as a generic algorithm.

5.2.2 Construction of polynomials starting to a list of elements in ExprS

We inductively define a function that construct a polynomial starting to a element in ExprS:

transl : ExprS → P oly
secret(e) ↦ cons((1, mon1e(e)), nil)
const(e) ↦ cons((e, mon0), nil)
mult(e_{1}, e_{2}) ↦ mult_{pol pol}(transl(e_{1}), transl(e_{2}))
add(e_{1}, e_{2}) ↦ add_{pol}(transl(e_{1}), transl(e_{2}))

where mon0 is the monomial where all the exponent of the variables are 0 and:

mon1e : F inset(k) ⟶ F inset(k) → ℕ
v_{1} ⟼ v_{2} ↦ if v_{1} = v_{2} then 1

else 0

Now, we can define a function that takes a list of ExprS and returns a polynomial:

make pol : (listExprS) → P oly
e ↦ flat mapT (transl, e)

In fact the outputs of Run are some list of ExprS, i.e, the Run doesn’t return exactly the f_{j} but it just returns the exponents: a_{j}. So to have the polynomial log_{g} f_{j}, i.e, a_{j,1} + a_{j,2}r + a_{j,3}x + a_{j,4}(log_{g} m_{b} + rx) we need to construct a function giving the product of two lists:

scal expr : (listExprS) × (listExprS) → (listExprS)
(nil, ) ↦ nil
( , nil) ↦ nil
(cons(a, l), cons(b, g)) ↦ cons(a ∗ b, scal expr(l, g))

In our particular case, we have the first list is an output of the Run and the second is the list (1, r, x, log_{g} m_{b} + rx)

5.2.3 Formalization of Lemma 1

First, we prove that for all Run R such that goodrun(R) and the previous step of R is not an empty run (indeed, we need to have at least two steps to find a collision), if there are no non-trivial collisions in the previous step of R then the probability of having collisions in R is smaller than \frac{2}{q} times the number of steps of R minus 1, i.e:

∀ R, P revRun(R) ≠ empty run, goodrun(R), ¬collisions_{run}(P revRun(R))

⟹ P r_{r,x}(collisions_{run}(R)) ≤ \frac{2}{q} × steps(P revRun(R))  (1)

where steps : Run → ℕ is the function giving the number of steps of a Run and P revRun is the function taking a Run and returning the previous Run. To prove this, we make an induction over R, in the empty case, we prove:

P r_{r,x}(collisions_{run}(empty run)) = P r_{r,x}(F alse) = 0
≤ \frac{2}{q} × steps(P revRun(empty run)) = 0

and in the case where R = step(r0, e), we rewrite the probability:

P r_{r,x}(collisions_{run}(R)) = P r_{r,x}(collisions_{run}(step(r0, e)) ∧ collisions_{run}(r0)) +P r_{r,x}(collisions_{run}(step(r0, e)) ∧ ¬collisions_{run}(r0))

As in the hypotheses we have ¬collisions_{run}(r0) where r0 = P revRun(R), we obtain: P r_{r,x}(collisions_{run}(R)) = P r_{r,x}(collisions_{run}(step(r0, e)) ∧ ¬collisions_{run}(r0)) As we are in the non-empty case: collisions_{run}(step(r0, e)) = ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r0))

∨ collisions(mapT (ExprS2G, Output(r0)))

So we must prove:

P r_{r,x}(ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r0)))

∧¬collisions(mapT (ExprS2G, Output(r0)))) ≤ \frac{2}{q} × steps(r0)

To prove this, we make an induction over r0, in the empty case, we prove:

P r_{r,x}(ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(empty run)) ∧¬collisions(mapT (ExprS2G, Output(empty run)))) = P r_{r,x}(F alse ∧ T rue)

= 0 ≤ \frac{2}{q} × steps(P revRun(empty run)) = 0

And in the case where r0 = step(r1, e_{1}), we have:

ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(step(r1, e_{1}))) = e =_{G} e_{1} ∨

ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1))

And as ∀ A, B, P r(A ∩ B) ≤ P r(A), we just prove:

P r_{r,x}(e =_{G} e_{1} ∨ ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1))) ≤ \frac{2}{q} × (steps(r1) + 1)

so we have: P r_{r,x}(e =_{G} e_{1} ∨ ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1))) = P r_{r,x}(e =_{G} e_{1})

+P r_{r,x}(ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1)))

−P r_{r,x}(e =_{G} e_{1} ∧ ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1)))

And as there are not non-trivial collisions in r1, we have:

P r_{r,x}(e =_{G} e_{1} ∧ ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1))) = 0 And we rewrite the probability of equality between 2 outputs of the Run like the probability of equality between 2 polynomials and so: P r_{r,x}(e =_{G} e_{1}) = P r_{r,x}(make pol(scal expr(e, Elgamal)) − make pol(scal expr(e_{1}, Elgamal)) = 0)

By Lemma 1,

P r_{r,x}(make pol(scal expr(e, Elgamal)) − make pol(scal expr(e_{1}, Elgamal)) = 0) ≤ \frac{2}{q}

To finish, we must show:

P r_{r,x}(ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1))) ≤ \frac{2}{q} × steps(r1)

As there are not non-trivial collisions in r1,

P r_{r,x}(ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1))) =

P r_{r,x}(ExprS2G(e) ∈_{G} mapT (ExprS2G, Output(r1))) ∧ ¬collisions_{run}(r1)) By the hypothese of induction this last probability is ≤ \frac{2}{q} × steps(r1). We finally proved (1). And by (1), we show:

∀ R, P revRun(R) ≠ empty run, goodrun(R)

⟹ P r_{r,x}(collisions_{run}(R) ∧ ¬collisions_{run}(P revRun(R))) ≤ \frac{2}{q}(t − 1)

where t is the number of steps of R, and so t − 1 the number of steps of P revRun(R). and now, by the previous inequality we can show the Lemma 2:

∀ R, P revRun(R) ≠ empty run, goodrun(R)

⟹ P r_{r,x}(collisions_{run}(R)) ≤ \frac{2}{q}\binom{t}{2}

To prove it, we make an induction of R, as P revRun(R) ≠ empty run, the empty case is impossible and R = step(r0, e), we rewrite the probability: P r_{r,x}(collisions_{run}(R)) = P r_{r,x}(collisions_{run}(step(r0, e)) ∧ collisions_{run}(r0))

+P r_{r,x}(collisions_{run}(step(r0, e)) ∧ ¬collisions_{run}(r0))

By the hypothese of induction we can prove:

P r_{r,x}(collisions_{run}(step(r0, e)) ∧ collisions_{run}(r0))

≤ P r_{r,x}(collisions_{run}(step(r0, e))) ≤ \frac{2}{q}\binom{t}{2}

By the in-equation (1),

P r_{r,x}(collisions_{run}(step(r0, e)) ∧ ¬collisions_{run}(r0)) ≤ \frac{2}{q}\binom{t}{1}

As \binom{t+1}{2} = \binom{t}{2} + \binom{t}{1}, we proved the Lemma 1.

5.2.4 Formalization of the Proposition 1

∀ g ∈ ℤ_{q}^{Sec} secret found is an inductively defined predicate with respect to a certain interpretation f:

\frac{collisions_{run}(r)}{secret found(r, g)}

\frac{¬collisions_{run}(r) f ≡_{Sec} g}{secret found(r, g)}

where r is a Run.

The Proposition 1 can be seen like:

∀ R, ∀g ∈ ℤ_{q}^{Sec}, P revRun(R) ≠ empty run, goodrun(R)

⟹ P r_{f}(secret found(R, g)) ≤ \frac{1}{q}\binom{t}{2} + \frac{1}{q}

We rewrite this probability:

∀ R, ∀g ∈ ℤ_{q}^{Sec}
P r_{f}(secret found(R, g)) = P r_{f}(secret found(R, g) ∧ collisions_{run}(R))

+ P r_{f}(secret found(R, g) ∧ ¬collisions_{run}(R))

By Lemma 2 for a Run with input g, h (without g^{r}, m_{b}h^{r}),

P r_{f}(secret found(R, g) ∧ collisions_{run}(R)) ≤ P r(collisions_{run}(R))
≤ \frac{1}{q}\binom{t}{2}

And we show:

P r_{f}(secret found(R, g) ∧ ¬collisions_{run}(R)) ≤ \frac{1}{q}

In fact, if there are no non-trivial collisions, the output of the Run are some elements in ℤ_{q}, and so we can see the equality x = y where y is the output of the generic algorithm as the equality f ≡_{Sec} g.

6 Conclusion

We developped within the Coq proof assistant a framework in which to reason about generic algorithms, and exploited this framework to prove the safety of the ElGamal cryptosystem against generic attacks. As this work required some concepts of Algebra and Probability, we must have formalized it. We showed Proposition 1 in Coq, it is the first step to show that A doesn’t succeed better than with probability \frac{1}{2} + \frac{2}{q} \binom{t}{2}. So the greater q is, the more secure is the cryptosystem.

As future work, we intend to complete our formalization of the Generic Model by proving the following results in Coq. First, we can prove the Lemma 3

Proposition 2 (Indistinguishability) Let a non-interactif generic algorithm A be given g, h, two messages m_{0}, m_{1} ∈ G and a cipher-text (g^{r}, m_{b}h^{r}) for random r ∈ ℤ_{q} and b ∈ {0, 1}. Let A output a guess b′ for b. Then P r_{b, r, x}(b′ = b) ≤ \frac{2}{q} \binom{t}{2} + \frac{1}{2}.

Proof Suppose that there is no non-trivial collision of group elements in A’s computation. Then, b, r, x are, by Lemma 3, statistically independent of the non-group output b′, thus P r_{b, r, x}(b′ = b) = \frac{1}{2}. Non-trivial collisions occur with probability ≤ \frac{2}{q} \binom{t}{2}.

□

The decisional Diffie-Hellman problem (DDH-problem). This problem is to distinguish g^{xy} and g^{z} when given g, g^{x}, g^{y} for random x, y, z ∈ ℤ_{q}. Proposition 2 implies the hardness of the DDH-problem in a generic model with was first shown by Shoup [?].

Proposition 3 [?] Let a generic algorithm A be given g, g^{x}, g^{y} and {g^{xy}, g^{z}} in random order for random x, y, z ∈ ℤ_{q} and output a guess for the order of g^{xy}, g^{z}. Then A succeeds with no better probability than \frac{2}{q} \binom{t}{2} + \frac{1}{2}.

We proved some results on the security of DL-cryptosystem ElGamal against generic attacks assuming the generic group model. It assumes an ideal group G of prime order q. The generic group model is a stronger assumption than assuming that the discrete logarithm is intractable (it has been shown that the discrete logarithm has exponential complexity in the generic group model [?, ?]), Schnorr claims that it is appropriate for elliptic and hyper-elliptic curves as the known attacks are all generic but it is less appropriate for group of units as it doesn’t cover attacks using sieving or index calculus. So an other step is to formalize the random oracle model (ROM) which goes back to Fiat and Shamir [?] and has been further enhanced by Bellare and Rogaway [?], let us define it The ROM: Let H be an ideal hash function, modeled as an oracle, that given an input (query) outputs a random number in the range of H. Hash functions are of the type H : G × M → ℤ_{q}, where G is a group of prime order q, M is a range of messages and ℤ_{q} is the field of integers modulo q. Formally, H is a random function H : G × M → ℤ_{q} chosen at random over all functions of that type with uniform probability distribution. The ROM assumes an ideal random hash function and is a stronger assumption that assuming the hash function to be collision resistant (collisions of random functions have negligibly small probability).