Botan [ Botan

Diaz

Alves

Sidorov

Lee

Ridhuan

Elgamal Hpp

[ Wang

[ Pellegrini

Elgamal Py

[ Musat

Rsa-Elgamal

Ioannou

Safe prime QR Generator Encoding Decoding DDH

Keywords: ElGamal, Encryption schemes, Distributed systems, Secure information flow, Type system. iii PyCrypto [Pycrypto, 2012

This thesis proposes the use of provable encryption schemes to obtain end-to-end security of distributed systems. We first analyze sufficient conditions of a provable encryption scheme used in voting systems and discover several inconsistencies in the satisfaction of these hypotheses in the implementations of the ElGamal encryption scheme. We propose and compare different methods to obtain chosen plaintext attacks indistinguishable implementations. We also study broadcast encryption schemes and propose a new scheme based on ElGamal. We implement and compare different broadcast encryption schemes in means of execution time and memory space. Furthermore, we consider scenarios based on broadcast encryption schemes to securely deliver messages in hierarchical distributed systems. We extend these scenarios to a more complex architecture where software updates are required, combining broadcast encryption schemes and remote attestation protocols. To express different levels of confidentiality and integrity, we use security classes featuring an order among them. Our key insight is that by mapping broadcast subgroups of nodes to security levels, we can control that information securely flows from the server to the nodes belonging to different security classes. We demonstrate this via two type systems and soundness proofs with respect to a new secure information flow property for server code fitting our architectures.

RESUMÉ

Notre idée clé est qu'en faisant correspondre des sous-groupes de noeuds de diffusion à des niveaux de sécurité, nous pouvons contrôler que les informations circulent en toute sécurité du serveur vers les noeuds appartenant à des classes de sécurité différentes.

Nous le démontrons par le biais de deux systèmes de types et de preuves de solidité concernant une nouvelle propriété de flux d'informations sécurisé pour le code serveur adapté aux notres architectures.

Mots clés:

ElGamal, Schémas de chiffrement, Systèmes distribués, Flux d'informations sécurisé, Systèmes de types.

i

ACKNOLEDGEMENTS

There are no appropriate words to express my gratitude and respect for my thesis advisors, Tamara Rezk and Benjamin Grégoire. Tamara has inspired me and helped me realize my journey as a PhD student. She has been a mentor, a friend, a second mother and much more. Without her nothing of this would have been feasible.

My sincere thanks also go to the members of my thesis jury and exam committee: Professors Alejandro Hevia, Bruno Martin, David Naumann, and Karthikeyan Bhargavan. They generously gave their time to offer me helpful comments toward improving my work. In particular, Prof. Alejandro Hevia showed me the potential of applying specific cryptographic primitives to solve information flow problems which helped me develop a broader perspective to my thesis.

There is no way to express how much it meant to me to have been a member of Indes and Marelle Teams. These exceptional colleagues and friends inspired me over the many years: Adam Khayam, Martin, Carlo, Ignacio, Héloise, Maxime, Yoon Seok, Manuel Serrano, Cécile, Sophie, Maxime Dénès, Cyril Cohen, Laurent Théry, Laurence Rideau, Yves Bertot and many others.

I cannot forget friends who went through hard times together, cheered me on, and celebrated each accomplishment: Zak, Ziad, Adam, Tota, Andrea, Pedro. I deeply thank my parents, especially my mother for her endless love, patience and her overseas support. I also thank my girlfriend Deborah for her love, support, and encouragement that helped me get through this agonizing period in the most positive way. v

INTRODUCTION

Whenever we talk about communication, we may think about secret communications or the communication of a secret. Cryptography can ensure the communication of secrets over insecure channels. With the beginning of public-key cryptography due to Diffie and Hellman [START_REF] Diffie | New directions in cryptography[END_REF], many cryptographic schemes have been proposed.

Their security depends on hard computational problems such as integer factorization and discrete logarithm. Even though they rely on such complex problems, cryptographic schemes may leak information about their encrypted message [START_REF] Lipton | How to Cheat at Mental Poker[END_REF]. The security of cryptographic schemes was inferred from the absence of known attacks until the work of Golwasser and Micali [START_REF] Goldwasser | Probabilistic encryption and how to play mental poker keeping secret all partial information[END_REF] in which they introduced the idea of provable security. In particular, they proposed the notion of semantic security also known as polynomial indistinguishability (IND) . Their scheme was the first probabilistic encryption scheme to be provably secure under standard cryptographic mathematical assumptions. A provable security defines the meaning of security in a given condition and proves that a cryptographic scheme achieves it (under certain assumptions). Afterwards, many cryptographic schemes have been proved to be IND secure, particularly IND-CPA and IND-CCA. In this thesis, we investigate the security of encryption schemes. Specifically, we analyze the ElGamal encryption scheme [START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF] and focus on a group property in which the Decisional Diffie-Hellman (DDH) assumption holds. The ElGamal encryption scheme is know to be IND-CPA under the DDH assumption over safe prime order groups. We analyze 26 libraries that implement ElGamal scheme and verify which libraries does respect the DDH assumption. Throughout the analysis, we point out four different encoding and decoding techniques and compare them. Actually, many cryptographic schemes are based on the DDH assumption to achieve IND-CPA security.

The DDH assumption is also useful for other cryptographic constructions as broadcast encryption schemes. Broadcast encryption schemes [START_REF] Fiat | Broadcast encryption[END_REF], allow a sender to securely communicate messages or key information with a privileged group of nodes.

The first security notion of broadcast encryption schemes required that any coalition of nodes can not learn any secret about the content of the broadcast. In our work, we investigate broadcast encryption schemes and discuss their security aspects. On one hand, we propose a new scheme based on ElGamal and implement it along with other existing schemes. We compare and evaluate the execution time of the key generation, the encryption and the decryption process of these schemes. We also measure the maximum key storage and the ciphertext size for 1 node in different subgroups.

On the other hand, we consider scenarios in which a server maps broadcast subgroups of nodes to levels in information flow security lattices to ensure secure information flow policies. In a confidentiality lattice, data is labeled as high (for secret) and low (for public), where an attacker is assumed to observe the data labeled as low and information can only flow from low to high. In an integrity lattice, data is labeled as trusted and untrusted, where an attacker is assumed to control the data labeled as untrusted and information from untrusted data does not affect trusted data (information can flow from trusted to untrusted). In a confidentiality and integrity lattice, namely a product lattice, data is labeled with a confidentiality and integrity levels. Information can only flow from public and trusted data to secret and untrusted data. Information flow policies [Sabelfeld andMyers, 2003, Denning and[START_REF] Denning | Certification of programs for secure information flow[END_REF] focus on preventing information flow from secret to public sources. To prevent insecure information flow , static information flow enforcement [START_REF] Volpano | A sound type system for secure flow analysis[END_REF] or dynamic enforcement [Askarov andSabelfeld, 2009, Bielova and[START_REF] Bielova | A taxonomy of information flow monitors[END_REF]] can be employed. In [START_REF] Volpano | A sound type system for secure flow analysis[END_REF], Volpano, Irvine and Smith proved through a type system that information flow policies ensure secure information flow policies.

By mapping broadcast encryption subgroups of nodes to levels in information flow security lattices we study secure information flow in the server code. We first consider a scenario in which a server broadcasts to nodes with static security levels (where we verify the use of the correct encryption keys) then we extend it to a scenario for nodes with dynamic security levels where software updates are needed to verify the correct behavior of nodes (and are encrypted to prevent attacks as the injection of malicious code to compromise the software update image [IETF, 2017] ) by relying on broadcast encryption schemes and remote attestation. In the latter, our goal is to allow for automate decisionmaking and easy key management at the server side while preserving confidentiality and integrity of information. Since broadcast subgroups of nodes are mapped to security classes, this allows the server to control the secure information flow and to record which nodes necessitate software updates. Hence, only node that verify the correct loading of software update ( through remote attestation) could move to higher integrity level.

We demonstrate our ideas through two type systems of the server code that ensure the compliance of our scenarios with a formally defined information flow policy. The first type system checks that messages broadcasted to a specific subgroup of nodes are not leaked to nodes in security levels with less privileges. It also checks that cryptographic keys variables and variables that record nodes according to their security class are not maliciously modified or wrongly manipulated. Regarding the second type system, besides checking the aforementioned variables, it also controls that variables containing information of nodes belonging to the same security level are updated only if the remote attestation succeeds. We finally prove the soundness of our type systems with respect to a new secure information flow policy by induction on the height of the typing derivation tree of Γ ⊢ p.

The manuscript is organized as follows:

• In Chapter 2, we give a mathematical overview in which we briefly discuss the group theory, and hard computational problems. We then introduce encryption schemes, particularly ElGamal encryption scheme discussing its IND-CPA security and its respective security parameters. In the last part, we briefly discuss the RSA scheme, RSA-OAEP and the IND-CCA security of the RSA scheme.

• In Chapter 3, we investigate the security of ElGamal implementations. We manually analyze the source code of 26 libraries that implement the ElGamal encryption scheme and give an overview of our results. Finally, we identify four different message encoding and decoding techniques and we discuss the different designs.

• In Chapter 4, we investigate broadcast encryption schemes. We propose a new scheme base on ElGamal and discuss its security parameters. We then implement and compare three existing broadcast encryption schemes in terms of execution time, key storage, and ciphertext size.

• In Chapter 5, we consider scenarios for broadcasting messages and software updates to a set of nodes in hierarchical distributed systems. The purpose is to allow the server to securely communicate with nodes whilst maintaining the integrity and confidentiality of communications. We build on ordered security classes to map broadcast subgroups of nodes to security levels to control secure information flow between server and nodes in different security classes. We also present two typing systems to control that information between server and nodes flows in a secure way.

Finally, we instantiate a theorem to show how the proposed architecture works backed with a soundness proof regarding a new secure information flow property for the server side that suits our architecture.

• In Chapter 6, the conclusion and directions for future work resume the results obtained in this thesis, and point out some future developments.

• Appendix A and Appendix B include the proofs of the theorems discussed in Chapter 5. Appendix C provides the ocaml implementations of the three schemes compared in Chapter 4.

C HAPTER

2

BACKGROUND

This chapter is devoted to recall some basic notions and definitions that will be used in the subsequent chapters of this thesis. We begin by group theory preliminaries in Section 2.1 and its related notations as an introduction for Chapter 3. In Section 2.2, we present the discrete logarithm problems (DLP) on which ElGamal encryption scheme in Chapter 3 is based on, and, the factorization problem on which the RSA scheme relies on.

In Section 2.3 we introduce the encryption schemes and discuss their related security problems. In Section 2.4, we focus on ElGamal encryption scheme and its security parameters that will be discussed in details in Chapter 3. Finally, in Section 2.5, we evoke the RSA cryptosystem that will be used in Chapter 4, and discuss some of its security notions.

Group Theory Preliminaries

In this section we recall some basic definitions and notations concerning group theory that are used throughout Chapter 3.

A group is a set of objects with an operation defined between any two objects in the set and satisfying the following axioms: Definition 1 (Group). A group consists of a non-empty set G together with a binary operation •, < G, •>, such that the following properties hold:

1. Closure Axiom: ∀a, b ∈ G: a • b ∈ G. 2. Associativity Axiom : ∀a, b, c ∈ G: a • (b • c) = (a • b) • c.
3. Identity Axiom: ∃e ∈ G such that, for any a ∈ G, a • e = e • a = a. The element e is called the identity element. 4. Inverse Axiom: ∀a ∈ G, there exists an element a -1 ∈ G such that a • a -1 = a -1 • a = e.

In the rest of the thesis, we omit the operation • and use G to designate a group

< G, •>.
Definition 2 (Finite and Infinite Groups). A group G is said to be finite if the number of elements in the set G is finite, otherwise, the group is infinite. |G| denotes the number of elements in G and is called the order of G.

Definition 3 (Abelian Group). A group G is abelian if for all a, b

∈ G, (a • b) = (b • a).
In other words, an abelian group is a commutative group. In this thesis we only deal with finite abelian groups. This said, all the groups that appear in Chapter 3 are abelian, and we always omit the prefix "abelian".

Example 1 (Additive vs. Multiplicative Groups). We briefly introduce two examples to highlight the difference between an additive group and a multiplicative group:

1. The set of integers Z a group under addition +, namely (Z, +), where e = 0 and a -1 = -a. This is an additive and infinite group. The same applies to the set of rational numbers Q, the set of real numbers R and the set of complex numbers C.

2. Non-zero elements of Q, R and C under multiplication "•", are groups with e = 1 and a -1 being the multiplicative inverse. Such groups are denoted as Q * , R * and C * , namely (Q * , •), (C * , •) and (R * , •), respectively. Such groups are called multiplicative groups and are infinite.

GROUP THEORY PRELIMINARIES

In the rest of the dissertation, we only rely on multiplicative groups and the multiplicative notation "•" for the operations of the groups.

In what follows, we introduce the notion of a subgroup, order of a group and Langrange's theorem. We rely on these definitions to achieve security (this will be discussed in detail in Section 2.4 of this chapter, and in Chapter 3).

Definition 4 (Subgroup). A subgroup of a finite group G is a non-empty subset H of G

which is itself a group under the same operation as that of G. We write H ⊆ G to denote that H is a subgroup of G, and H ⊂ G to denote that H is a proper subgroup of G (i.e., H = G).

Definition 5 (Order of a Group). The number of elements in a finite group G is called the order of G and is denoted by #G.

Example 2 (Subgroups and Order of a Group). We introduce some examples on subgroups and orders of groups:

1. The additive group (Z 10 , + (mod 10)), where Z 10 = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}, has the following subgroups: ({0}, +), ({0, 5}, +), ({0, 2, 4, 6, 8}, +) and (Z 10 , +). satisfying a i = e, and is denoted by ord(a). If such an integer i does not exist, then a is called an element of infinite order.

The multiplicative group (Z

The following theorem is important for cryptography as it establishes that the order of a subgroup divides the order of its group. Such property is important as we show in Subsection 2.4.1 for ElGamal encryption scheme.

Theorem 1 (Lagrange's Theorem). If H is a subgroup of the finite group G, then #H|#G.

Corollary 1 (Lagrange). Let G be a finite group and a ∈ G be any element. Then ord(a)|#G.

Proof. For any a ∈ G, if a = e then ord(a) = 1 and so ord(a)|#G is a trivial case. Let a = e.

Since G is finite, we have 1 < ord(a) < ∞. Elements

(2.1) a, a 2 , ..., a ord(a) = e are necessarily distinct. Suppose that they were not distinct, then a r = a s for some non-negative integers r and s satisfying 1 ≤ r < s ≤ ord(a). By applying the inverse axiom of (a r ) -1 to both sides, we will have: a r-s = e where 0 < sr < ord(a). This contradicts Definition 6 of ord(a) being the least positive integer satisfying a ord(a) = e. It is easy to check that the ord(a) of elements in 2.1 form a subgroup of G. By Langrange's theorem,

ord(a)|#G. ■
Corollary 1 is a direct application of Lagrange's Theorem and provides a relationship between the order of a group and the orders of elements in the group. Such relationship is important for public-key cryptosystems such as the security ElGamal encryption scheme as we show in Chapter 3.

Another important notion we use in Chapter 3 is the notion of cyclic groups and group generators.

Definition 7 (Cyclic Group, Group Generator). A group G is said to be cyclic if there exists an element g ∈ G such that for any b ∈ G, there exists an integer i ≥ 0 such that b = g i . The element g is then called a generator of G. And G is called the group generated by g, written as G =< g >.

In Figure 2.1, we show an example of a generator of the multiplicative cyclic group , 3, 4, 5, 6, 7, 8, 9, 10} is a group under multiplication modulo 11 and the element 2 is a generator and provides a cyclic view for Z * 11 . Corollary 2. A prime-order group is cyclic, and any non-identity element in the group is a generator.

Z * 11 . Z * 11 = {1, 2
2 = 2 1 4 = 2 2 8 = 2 3 5 = 2 4 10 = 2 5 9 = 2 6 7 = 2 7 3 = 2 8 6 = 2 9 1 = 2 10
Proof. Let G be a group of prime order p. Let g ∈ G be any non-identity element.

From Corollary 1, ord(g)|p. Since g = e and ord(g) = 1, then it has to be the case that ord(g) = p. Therefore, < g >= G, i.e. g is a generator of G. ■

Hard Computational Problems

In this section, we present two well-known hard computational problems [START_REF] Martin | Codage, Cryptologie et Applications[END_REF].

In Subsection 2.2.1, we introduce the discrete logarithm problem and its related problems on which the ElGamal cryptosystem (See Algorithm 5) in Chapter 3 is based on. In Subsection 2.2.2, we introduce the factorization problem used in Chapter 4.

Discrete Logarithm Problems

This subsection is devoted to the discrete logarithm problem (DLP), an assumption used by cryptographic protocols such as ElGamal encryption scheme [START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF].

Consider a finite cyclic group G and a generator g. The assumption states that, given h ∈ G, it is computationally unfeasible for an adversary to find an integer x such that

h = g x .
In what follows, we concisely list the definition of the discrete logarithm and some related problems. In what follows, we use q to denote a prime number, and Z q to denote < Z q , • (mod q) >.

Definition 8. (Discrete Logarithm Problem (DLP)) Given g x ∈ G, where G is a cyclic group of prime order q, g the generator of G, and x ∈ Z q , compute x.

Definition 9. (Computational Diffie-Hellman (CDH)) Given g x ∈ G and g y ∈ G , where G is a cyclic group of prime order q, g the generator of G, and x, y ∈ Z q , compute g xy ∈ G. where D 1 = (g x , g y , g xy ), D 2 = (g x , g y , g z ) and x, y, z are randomly distributed in Z q .

Distinguish D 1 from D 2 .

If the discrete logarithm problem is easy to solve, then the DHP is also easy to solve, and thus, the cryptographic protocol that relies on such assumption is considered insecure. Therefore, we are interested in finding difficult instances of the DLP. For instance, the hardness of the discrete logarithm problem depends on the representation of the group G. Note that DDH ≤ p CDH ≤ p DL [START_REF] Boneh | The decision diffie-hellman problem[END_REF] where ≤ p indicates polynomial time reductions (See Definition 11, Algorithm 1 and 2).

The discrete logarithm problem (DLP) is thought to be mathematically difficult, at least when implemented in cryptographically strong groups of large order (e.g., when q is of size 2048 bits or more). In 2015, a group of researchers published a paper [START_REF] Adrian | Imperfect forward secrecy: How diffiehellman fails in practice[END_REF] in which they publicly reported a security vulnerability in TLS, called Logjam, that allows users to downgrade connections to "export-grade" Diffie-Hellman key exchange (based on the difficulty of solving the discrete logarithm problem) that ranges from 512 to 1024-bit keys. The researchers used the number field sieve discrete log algorithm to compute arbitrary discrete logs in a 512-bit group. While solving the discrete logarithm problem for 2048-bit prime is believed to be beyond anyone's reach, the authors of the paper estimated the feasibility of an attack against 1024-bit prime to be at least within the range of nation-state attackers such as NSA.

Definition 11. (Polynomial Time Reduction) Let X and Y be two computational problems.

Then X is said to polytime reduce to Y , written X ≤ p Y if

• There is an algorithm which solves X using an algorithm which solves Y .

• This algorithm runs in polynomial time if the algorithm for Y does.

Algorithm Reducing CDH to DLP 1: Given g x and g y , find g x•y . 2: Use an oracle to solve DLP by computing y = DLP(g, g y ).

3: Compute (g x ) y = g x•y . 4: Then CDH is no harder than DLP: CDH ≤ p DLP.

Algorithm Reducing DDH to CDH

1: Given g x , g y and g z , determine if g z = g x•y . 2: Use an oracle to solve CDH by computing g x•y = CDH(g, g x , g y ).

3: Check whether g x•y = g z . 4: Then DDH is no harder than CDH: DDH ≤ p CDH.

Factorization Problem

In this subsection, we define the integer factorization problem on which the RSA cryptosystem [START_REF] Rivest | A method for obtaining digital signatures and public-key cryptosystems[END_REF] relies. This subsection gives an overview on the complexity problem that stands behind RSA and discuss a related problem, namely the Deciding Composite Residuosity introduced by [START_REF] Paillier | Public-key cryptosystems based on composite degree residuosity classes[END_REF].

The integer factorization problem states that it is easy to find the product of the multiplication of two factors, but the inverse operation is difficult.

The integer factorization problem was used by [START_REF] Rivest | A method for obtaining digital signatures and public-key cryptosystems[END_REF]

Encryption Schemes

In this section, we give an overview on encryption schemes and discuss their security aspects. An encryption scheme consists of four algorithms: a setup, a key generator, that generates a pair of keys (encryption and decryption key), a probabilistic encryption algorithm that converts plaintexts into ciphertexts, and a decryption algorithm that transforms ciphertexts into plaintexts, using the adequate keys. When encryption schemes have only one private key for encryption and decryption, they are called symmetric key encryption schemes. In 1970 Diffie and Hellman [START_REF] Diffie | New directions in cryptography[END_REF] introduced public key encryption schemes, also know as asymmetric key encryption schemes, where the encryption key and the decryption key are different.

For what concerns Chapter 3, we rely on asymmetric key encryption schemes.

An encryption scheme is a set of algorithms defined as follows:

Definition 16. (Encryption Scheme)

• Setup: Receiving η as input, the algorithm initializes the parameters needed by the scheme.

• Key generation: Given a security parameter η, the key generation algorithm KG(η)

returns an encryption and decryption key pair (pk, sk);

• Encryption: Given an encryption key pk and a plaintext m, the encryption algorithm E(pk, m) computes a ciphertext corresponding to the encryption of m under pk;

• Decryption: Given a decryption key sk and a ciphertext c, the decryption algorithm D(sk, c) returns the plaintext corresponding to the decryption of c, if it is a valid ciphertext.

The key generation and encryption algorithms may be probabilistic, while the decryption algorithm is always deterministic. For an encryption scheme to be correct, it is required that decryption be the inverse of the encryption: for every pair of keys (pk, sk)

that can be output by the key generation algorithm, and every plaintext m, it must be the case that D(sk, E(pk, m)) = m.

Security Definitions of Encryption Schemes

An essential condition for an encryption scheme is the difficulty of retrieving an encrypted plaintext without the knowledge of the decryption key. Such condition may be weak in some applications since partial information about the plaintext could endanger the security of an entire scheme. Therefore, it must be unfeasible to learn anything about the plaintext from the ciphertext, following the principle "whatever an eavesdropper can compute about the clear text given the ciphertext, he can also compute without the ciphertext" [START_REF] Goldwasser | Probabilistic encryption and how to play mental poker keeping secret all partial information[END_REF]. Schemes achieving this requirement, such as the Goldwasser-Micali scheme [START_REF] Goldwasser | Probabilistic encryption and how to play mental poker keeping secret all partial information[END_REF], are called semantically secure.

An encryption scheme is said to be secure if the success probability of an adversary trying to break the scheme is insignificant. This notion is achieved by negligible functions.

Definition 17 (Negligible Function). A function v : N → R is said to be negligible if it decreases asymptotically faster than the inverse of any polynomial:

∀c ∈ N, ∃n c ∈ N s.t. ∀n ∈ N, n ≥ n c ⇒ |v(n)|<n -c
A scheme is considered to be secure if it cannot be broken in polynomial time (with respect to the predefined security parameter). The idea of negligible probability encompasses this exact notion.

To satisfy the aforementioned definition, an encryption scheme must necessarily be probabilistic, otherwise an adversary could trivially detect to which message corresponds the challenge ciphertext by simply encrypting one of the messages it has chosen and comparing the resulting ciphertext with the challenge ciphertext. The reason for this choice is because negligible probability of success stays negligible after even a polynomially many attempts to break the system.

Adversarial Goals and Capacities

In terms of security for cryptosystems, there are different adversarial goals and capacities.

Such goals and capacities must be well defined. In what follows, we review the adversarial goals and capacities against cryptographic schemes.

Adversarial goals. For semantic security, the adversary has three main goals: Onewayness, indistinguishability and malleability.

ONE-WAYNESS.

A most important security notion for an encryption scheme is to achieve the property of one-wayness: an attacker should not be able to recover the plaintext matching a given ciphertext. However, this is a weak notion of security as unveiling almost all the plaintext is unsuccessful according to this definition. More formally, for any adversary, succeeding in inverting the effects of the encryption on a ciphertext c should occur with negligible probability.

• In CCA, an adversary possesses a conditional decryption box. The box expires before the target ciphertext is given to the adversary.

• In CCA2, an adversary possesses a decryption box as long as he does not feed the target ciphertext to the box.

Indistinguishability Against Attacks

Indistinguishibality against attacks is a fundamental security property of several cryptosystems. Indistinguishability means that an adversary is unable to distinguish between two ciphertexts. Such property under chosen-plaintext attacks is a essential necessity for asymmetric key encryption schemes and corresponds to the property of semantic security.

In addition, some schemes are also distinguishable against chosen-ciphertext attacks.

A cryptosystem enjoys the indistinguishability property if there exists no adversary, given a message encryption randomly chosen between two elements, able to identify which message has been encrypted with a probability better than blind guessing. Such definition suggests that a scheme is secure as long as the adversary cannot learn any information about the original message.

In what follows, we present indistinguishability against CPA and CCA.

Indistinguishability against

IND-CPA [b = b ′ ] - 1 2
| is negligible in the security parameter.

Even though the adversary have knowledge about m 0 , m 1 and pk, the encryption algorithm being probabilistic, means that the encryption of m b is one of several valid ciphertexts. This prevents the adversary from learning some information by encrypting m 0 and m 1 to compare the result and therefore binds the advantage of the adversary. Definition 19 (IND-CCA). An encryption scheme is said to be IND-CCA secure if the advantage of any efficient adversary is a negligible function of the security parameter, i.e., the adversary cannot do much better than a blind guess.

Indistinguishability against

|Pr IND-CCA [b = b ′ ] - 1 2
| is negligible in the security parameter.

ElGamal Encryption Scheme

ElGamal [START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF] is an asymmetric key encryption scheme, it enjoys homomorphic properties that are fundamental for the electronic voting systems. ElGamal scheme (see Algorithm 5) consists of three algorithms: key generation(η), η being a security parameter, encryption E(m, pk) with m being a plaintext and pk a public key, and decryption D(c, sk) where c is a ciphertext and sk is a private key.

Algorithm ElGamal Scheme

1: Setup: Let G be a cyclic group of prime order q and g a generator.

2: Key Generation: Pick randomly a secret key x ∈ Z q , then compute y = g x to obtain the public key. 3: Encryption: Let m ∈ G and r ∈ Z q randomly selected. The resulting ciphertext is c = (u, v) = (g r , m.y r ). 4: Decryption: To recover the plaintext, one computes m = v • u -x .

Security of ElGamal Parameters

The ElGamal encryption scheme is known to be IND-CPA secure under the Decisional Diffie-Hellman assumption with the key length as its security parameter. A key point for the security of the ElGamal encryption scheme resides in the group G and its order [START_REF] Boneh | Why textbook elgamal and RSA encryption are insecure[END_REF]. One should start by generating a pair of keys (public and private), then map the message into a group where the Decisional Diffie-Hellman assumption holds. Hence, the difficulty consists in finding an efficient invertible group encoding procedure so that one can recover the original message when decrypting. The ElGamal cryptosystem operates in a finite cyclic group, which by convention is written multiplicatively. For the sake of simplicity, we will restrict our discussion to the group of integers from {1} to {p -1} under multiplication mod p for some prime p, commonly denoted Z * p and subgroups of Z * p of prime order. Moreover, we will also use |g| to denote the order of an element g in Z * p and < g > to denote the cyclic subgroup of Z * p generated by g. Unless otherwise noted, assume multiplications and exponentiations involving elements of Z * p are done mod p. As if all subgroups of a cyclic group are cyclic and if G = 〈g〉 is cyclic, then for every divisor d of |G| there exists exactly one subgroup of order d which may be generated [START_REF] Rotman | An Introduction to the Theory of Groups[END_REF]. One may rely on this property to form a unique subgroup of quadratic residues elements. To achieve this goal, the idea is to use a Sophie Germain prime [START_REF] Pollard | Monte carlo methods for index computation[END_REF]: it is a safe prime p of the form 2q + 1 where q is also prime. Safe primes of that form are important for modulo groups as they guarantee the existence of a subgroup of prime order. For ElGamal, using a safe prime p, where the order is p -1 = 2q permits to form a subgroup of prime order q that forms the message space we need in order to encrypt messages. One may take advantage of the Lagrange Theorem (Theorem 1) [START_REF] Pollard | Monte carlo methods for index computation[END_REF] that States that in a finite group G, the order of any subgroup H divides the order of the group, to conclude that the prime order subgroup has no subgroups being prime. Finally, the message space must be restrained to this prime order subgroup.

Quadratic Residues. To make the ElGamal cryptosystem IND-CPA secure, the Decisional Diffie-Hellman assumption must be respected. As a matter of fact, one needs to find which type of groups satisfies the underlying assumption. A good technique is to restrict the messages to form the subgroup of prime order q of quadratic residues. In what follows we will introduce further explanations and examples to better understand the role of quadratic residues for the security of the ElGamal encryption scheme.

Definition 20 (Quadratic Residue). An element a ∈ Z * n is said to be a Quadratic Residue modulo n if there exists x ∈ Z * n , such that x 2 ≡ a(mod n). Every such x is called a square root of a modulo n. If no such x exists, then a is called a Quadratic Non-Residue modulo n. We denote the set of all quadratic residues modulo n by QR n and the set of all quadratic non-residues by QNR n Quadratic residues are exactly those elements which can be written of the form g i where i is even: {g 2 , ..., g p-1 } are distinct quadratic residues, while {g, gg 2 , ..., gg p-1 } are quadratic non-residues. There exists an efficient algorithm based on Euler's criterion for deciding quadratic residuosity in Z * p , with p prime:

Definition 21 (Euler's Criterion). Let p be an odd prime. Then a ∈ Z * p is a quadratic residue modulo p iff a p-1 2 ≡ 1 (mod p).

Therefore, by restricting all the messages to be Quadratic residues in a safe prime group, a polynomial time adversary cannot distinguish between elements as all the elements are then quadratic residues. Hereinafter, we will be using the Legendre symbol based on Euler's criterion for its convenient notation that reports the quadratic residuosity of a mod p.

Definition 22 ( Legendre symbol). Let p be an odd prime , a an integer, such that gcd(a, p) = 1. The Legendre symbol (LS) is defined to be

a p =        1 if a ∈ QR p -1 if a ∈ QNR p
Example 3. Let us compute the set of quadratic residues modulo 11 (QR 11 ), using

Legendre symbol :

Elements LS QR 1 1 2 -1 ✗ 3 1 4 1 5 1 6 -1 ✗ 7 -1 ✗ 8 -1 ✗ 9 1 10 -1 ✗

RSA Scheme

The RSA cryptosystem [START_REF] Rivest | A method for obtaining digital signatures and public-key cryptosystems[END_REF]

The RSA Encryption

The RSA encryption consists of three algorithms: an RSA public key/private key generation, an encryption algorithm and a decryption algorithm.

Key

Generation. An RSA key generation algorithm consists of the following steps described in Algorithm 6.

Algorithm Key Generation KG RSA 1: Choose a pair of large random primes, namely p and q. Both p and q are kept secret. 2: Compute the public RSA modulus N = p • q.

3: Select a large integer e, a public odd exponent where 3 < e < N -1, prime to φ(N). 4: Compute the private exponent d ≡ e -1 mod φ(N). 5: Output the public key (N, e) and the private key (N, d).

Encryption. An RSA encryption operation is the exponentiation to the e th power modulo N of a message m ∈ N:

c = ENC RSA (m, e) = m e mod N.
Where m is the message, c is the resulting ciphertext and ENC RSA (m, e) is the encryption algorithm. The message m is encrypted using the public exponent e.

Decryption. An RSA decryption operation is the exponentiation to the d th power modulo N of a ciphertext c:

m = DEC RSA (c, d) = c d mod N.
Where DEC RSA (c, d) is the decryption algorithm. Note that the correctness of the RSA cryptosystem relies on the fact that the exponentiation to the d th power modulo N, is the inverse of the exponentiation to the e th power. In fact, to recover a message m, one should calculate: m ≡ c d mod N ≡ (m e ) d mod N, where e • d ≡ 1 mod N.

The Security of RSA

The RSA encryption is deterministic, meaning that the same ciphertext is produced for the same key pair and plaintext. Being deterministic makes the scheme vulnerable to chosen-ciphertext attacks, where an adversary with access to a random oracle, can obtain the decryption of ciphertexts of its choice. To make RSA semantically secure against chosen-ciphertext attacks, padding is added to the ciphertext.

Typically, the padding function used is OAEP [START_REF] Bellare | Optimal asymmetric encryption[END_REF], resulting

in RSA-OAEP, for which there exists, in the random oracle model, a loose reduction of the RSA problem towards IND-CCA attacks [START_REF] Bellare | Optimal asymmetric encryption[END_REF][START_REF] Shoup | OAEP reconsidered[END_REF],Barthe et al., 2011a]. OAEP, namely Optimal Asymmetric Encryption Padding, is a technique for converting the RSA trapdoor permutation into a chosen-ciphertext secure system in the random oracle model. Moreover, OAEP relies on a pseudo-random number generator for ensuring the indistinguishability of ciphertexts by making the encryption algorithm probabilistic, instead of deterministic as in the original RSA scheme.

The RSA-OAEP cryptosystem consists of triple (KG RSA , ENC RSA , DEC RSA ) obtained by a trapdoor permutation RSA on {0.1} k and two hash functions G and H:

G : {0, 1} k 0 → {0, 1} k-k 0 H : {0, 1} k-k 0 → {0, 1} k 0
Where KG RSA is the key generation function of RSA, ENC RSA , the encryption function of RSA, and, DEC RSA , the decryption function of RSA.

The Optimal Asymmetric Encryption Padding (OAEP) scheme applied to RSA consists of three algorithms:

Algorithm RSA-OAEP 1: Key Generation: The key generation algorithm specifies an instance of the function KG RSA that generates the public key e and the private key d. 2: Encryption: Given a message m ∈ {0, 1} n , and a random value r ← R {0, 1} k 0 , the encryption algorithm computes s = (m||0 k 1 ) ⊕ G(r) and t = r ⊕ H(s), and outputs the ciphertext c = ENC RSA (e, s||t). 3: Decryption: Using the private key, the decryption algorithm extracts (s||t) = DEC RSA (d, c), then r = t ⊕ H(s) and finally

M = s ⊕ G(r). If [M] k 1 = 0 k 1 , the algo- rithm returns [M] n , otherwise it returns "Reject".
In their paper [START_REF] Bellare | Optimal asymmetric encryption[END_REF], Bellare et. al. proved that the OAEP encryption scheme is semantically secure and weakly plaintext-aware, provided that f is a one-way trapdoor function. While Shoup [START_REF] Shoup | OAEP reconsidered[END_REF] showed that it was absurd to extend the results obtained in [START_REF] Bellare | Optimal asymmetric encryption[END_REF] to obtain adaptive chosenciphertext security exclusively under the one-wayness of the permutation.

RSA-OAEP was proved to be IND-CCA by Fujisaki et. al. [START_REF] Fujisaki | RSA-OAEP is secure under the RSA assumption[END_REF], and machine-checked proved by [START_REF] Barthe | Beyond provable security verifiable IND-CCA security of OAEP[END_REF].

C HAPTER 3

SECURITY ANALYSIS OF ELGAMAL IMPLEMENTATIONS

Throughout the last century, especially with the beginning of public key cryptography due to Diffie-Hellman [START_REF] Diffie | New directions in cryptography[END_REF], many cryptographic schemes have been proposed. Their security depends on hard computational problems such as integer factorization and discrete logarithm. In fact, it is thought that a cryptographic scheme is secure if it resists cryptographic attacks over a long period of time. On one hand, since certain schemes may take several years before being widely studied in depth, they become vulnerable as time passes. On the other hand, a cryptographic scheme is a provable one, if it resists cryptographic attacks relying on mathematical hypothesis.

Being easily adaptable to many kinds of cryptographic groups, the ElGamal encryption scheme enjoys homomorphic properties while remaining semantically secure [START_REF] Goldwasser | Probabilistic encryption and how to play mental poker keeping secret all partial information[END_REF], provided that the Decisional Diffie-Hellman (DDH) assumption holds on the chosen group. While the homomorphic property forbids resistance against chosen ciphertext attacks, it is very convenient for voting systems [START_REF] Cortier | Beleniosrf: A strongly receipt-free electronic voting scheme[END_REF].

The ElGamal encryption scheme [START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF] (See Section 2.4 of Chapter 2) is the most extensively used homomorphic encryption scheme for voting systems (see also

Paillier [START_REF] Paillier | Public-key cryptosystems based on composite degree residuosity classes[END_REF]). Moreover, ElGamal is the only homomorphic encryption scheme implemented by default in many hardware security modules [Volkamer, 2009, Orr and[START_REF] Orr | SAC '15[END_REF].

In order to be provably secure, the ElGamal encryption needs to be implemented on top of a group verifying the Decisional Diffie-Hellman (DDH) assumption. Since this assumption does not hold for all groups, one may have to wrap an encoding and a decoding phase to ElGamal to be able to have a generic encryption scheme. In this chapter, our main goal is to study ElGamal encryption scheme libraries to identify which implementations respect the DDH assumption.

We manually analyze the source code of 26 libraries that implement the ElGamal encryption scheme in the wild. We focus our analysis on understanding whether the DDH assumption is respected in these implementations, ensuring a secure scheme in which no information about the original message could be leaked. The DDH assumption is crucial for the security of ElGamal because it ensures indistinguishability under chosen-plaintext attacks (IND-CPA). Without a group satisfying the DDH assumption, encryption mechanisms may leak one bit of information about the plaintext and endanger the security of the electoral system, thus threatening the privacy in an election. For instance, when considering an approval ballot with a yes or no vote, leaking one bit of information signifies a full leakage of the vote. One way to comply with the DDH assumption is by using groups of prime order. In particular, when adopting safe primes, one can ensure the existence of a large prime order subgroup [START_REF] Milne | Fields and galois theory (v4.22)[END_REF] and restrict messages to belong to this subgroup. Mapping plaintexts into subgroups is called message encoding. Such encoding necessitates to be efficient and precisely invertible to allow decoding after the decryption.

In Table 3.1, we give an overview of our results : out of 26 analyzed libraries, 20 are wrongly implemented because they do not respect the conditions to achieve IND-CPA security under the DDH assumption. This means that encryptions using ElGamal from any of these 20 libraries may leak one bit of information (see Section 3.1).

From the 6 libraries which respect the DDH assumption, we also study and compare various encoding and decoding techniques. We identify four different message encoding and decoding techniques summarized in Table 3.2. Finally, in Section 3.3, we discuss the different designs and conclude which implementation is more efficient for voting systems.

In summary, our contributions in Chapter 3 are:

• We analyze 26 libraries implementing ElGamal encryption, and point out which ones are not satisfying the DDH assumption and hence are not semantically secure.

• We identify and compare 4 different message encoding and decoding techniques that comply with the DDH assumption.

We refer the reader to Chapter 2 in which we present various definitions and notions used in this chapter.

Breaking ElGamal

We consider a prime p and a generator g ∈ Z * p . Given a public key g x , the ElGamal encryption scheme encrypts a message m ∈ Z p by computing (g r , m.g xr ), with r chosen randomly in Z * p . Using the private key x, decryption can be done by first computing (g xr ) and then dividing to retrieve m. The cryptosystem is not semantically secure when g is a generator of Z * p , as information about the plaintext is leaked (See Section 2.4.1 of Chapter 2). Specifically, the Legendre symbol of (m.g xr ) uncovers the Legendre symbol of the message m. In order to prove that ElGamal is IND-CPA under the DDH assumption, one may choose g to be the generator of the group in which the DDH assumption holds and restrict the message space to this group. This way, the system is semantically secure as given (g x ) and (g r ), the secret value (g xr ) cannot be distinguished from a random element in the group. Therefore, (m.g xr ) cannot be distinguished from a random element and an attacker cannot learn any information about the original message. In what follows, we will show an example on how to break the DDH assumption and ElGamal encryption scheme for Z * p groups.

Example 4 (Breaking the DDH Assumption). In order to break the DDH assumption, one should be able to distinguish between two distributions having elements randomly distributed in a group. Let p = 2q + 1 = 11 be the group on which we want to perform the attack (to ease the comprehension of the example, we consider small parameters size and not secure). Being prime, p has {p -1} elements, half being quadratic residues (QR) and the other half being quadratic non-residues (QNR). Given a tuple (g x , g y , g c ) it is hard to decide whether c = xy or c = z, where z is randomly generated. By Legendre Symbol, we can check the quadratic residuosity of the elements g x , g y and g c : x p = 1 if x is a square (i.e., quadratic residue), then g x p = 1 if x is even. Therefore, g x is quadratic residue if x is a quadratic residue too. In addition, if x or y are even, then xy is even and g xy is quadratic residue. Taking advantage of all the before-mentioned notions, we will give a detailed example on how to break the DDH assumption. A tuple is a valid DDH tuple if xy≡ c mod p and can be written as (g x , g y , g xy ).

Let p = 11, the challenge is to distinguish whether (4, 5, 9

) is DDH 0 or DDH 1 in G 11 . For Euler's criterion, a ∈ Z * p is a QR iff a p-1 2 ≡ 1 (mod p). 4 5 ≡ 1 mod11 5 5 ≡ 1 mod11 9 5 ≡ 1 mod11
By testing the quadratic residuosity of the three elements, one can notice that all of them are quadratic residues. In this case, we cannot distinguish between xy and z. Since the multiplication between two elements that are quadratic residues, results in an quadratic residue element, it might be that the third element of the tuple belongs to DDH 0 or DDH 1 .

Consequently, we are not able to break the DDH assumption.

In this second example, the challenge is to distinguish whether (4, 5, 8) is (g x , g y , g xy ) or

(g x , g y , g z ) in G 11 . 4 5 ≡ 1 mod11 5 5 ≡ 1 mod11 8 5 ≡ 1 mod11
One can notice that the third element of the tuple is not a quadratic residue. Being both quadratic residues, the multiplication between g x = 4 and g y = 5 must result in an quadratic residue element. However, g c = 8 results being a non quadratic residue element.

In this case, we are able to distinguish between xy and z by ensuring that (4, 5, 8) is DDH 1

and break the DDH assumption as a consequence. We emphasize on the importance of choosing a safe prime group p, to be able to work in the subgroup of prime order q by restricting the elements to form the subgroup of quadratic residues. This guarantees the difficulty of such attacks on the DDH assumption.

Example 5. (Breaking the ElGamal Scheme using a QR generator) Being in a group in which the DDH does not hold may leak information about the original plaintext.

An attacker able to calculate the quadratic residuosity of an encrypted message, can learn one bit of information about the original message. An attacker can check whether the encryption of a message is a QR or not and therefore deduce whether the original message is a QR too. In fact, by taking g xr ∈ QR and encrypting the message as

E (m, k) = (g r , m.g xr ), one can notice that if m.g xr ∈ QR then m ∈ QR.
Consider the group G 11 , let x = 4 ∈ sk, r = 2 ∈ rnd, g = 3 ∈ QR and y = g x = 4 ∈ pk.

In the above example, the group G 11 has {1, 3, 4, 5, 9} as a subgroup of quadratic residues.

Actually, encrypting a message m ∈ QR with a public key pk ∈ QR, results always in an encryption E (m, k) ∈ QR. Thus, by using G 11 and taking messages belonging to its entire message space, one endangers the security of the scheme as he allows QR and QNR messages to be encrypted. An attacker able to calculate the quadratic residuosity of an element could learn one bit of information about the original message by performing the following attack:

(a) g ∈ QR, then (g xr ) is QR. (b) Check if E (m,k) p is QR or not. (c) If E (m,k) p
∈ QR, the attacker can learn that the message m ∈ QR, as the multiplication between QR elements result always in a QR element.

(d) If E (m,k) p
∈ QNR, then the attacker can learn that the message m ∈ QNR.

Let us check E (1, 5) = (9, 5):

(a) 3 11 = 1 ⇒ g ∈ QR, 3 8 11 = 1 ⇒ (g xr ) ∈ QR. (b) 5 11 = 1 ⇒ E (1, 5) ∈ QR.
(c) Being m.g xr ∈ QR leaks the quadratic residuosity of m. In fact 1 11 = 1 ⇒ m ∈ QR.

The previous example could also be adopted for QNR messages. In summary, the feasibility of calculating the quadratic residuosity of an element in a modulo prime groups, may leak information about the original message on top of groups that do not respect DDH.

Study of Libraries

We focus our study on manually checking whether the underlying groups in ElGamal implementations satisfy the Decisional Diffie-Hellman assumption. A summary of our results regarding 26 analyzed libraries can be found in Table 3.1.

We split our work into three tasks to analyze the implementations. We first verify that the implementations use safe primes, next we check if they adopt quadratic residue gener- (B) Libraries that do respect the DDH assumption. There are 6 libraries in this category.

However, they do not all use the same encoding technique. Thus, we describe in detail the 4 different encoding techniques, discussing their advantages and drawbacks.

Libraries' Relevance. We provide a brief description on the relevance of some of the chosen libraries for analysis. Belenios [START_REF] Belenios | Public source code of library n.1[END_REF] has been deployed on an online platform and it is used in more than 200 elections, both in academia and in education.

Similarly, Helios [START_REF] Helios | Public source code of library n[END_REF] is used for the election of the International Association for Cryptographic Research members board, the ACM general elections, the election of UCLouvain president and for other student elections. On the other hand, the Estonian voting system [Estonia, 2017] has been used for the European Parliament elections, local government council elections and the election of the president of the Republic. Swisspost [START_REF] Swisspost | Public source code of library n[END_REF] then offers voting system services for cantons and municipalities in Switzerland, while Verificatum [START_REF] Verificatum | Public source code of library n[END_REF] is used in binding elections, student body elections and intra-party elections.

Libraries That Do Not Respect DDH

In this section, we will present the implementations that do not respect the conditions to achieve an IND-CPA secure ElGamal scheme. Working on groups modulo p, a secure ElGamal scheme has to adopt safe primes, a quadratic residue generator, and a message encoding technique to map the messages into a subgroup that respects the Decisional Diffie-Hellman assumption. Twenty out of twenty six libraries violate one or more of the before-mentioned conditions: all the libraries in this section do not employ message encoding techniques.

Lack of Safe Prime. In this category, 10 libraries [START_REF] Diaz | Public source code of library n.4[END_REF][START_REF] Alves | Public source code of library n[END_REF][START_REF] Sidorov | Public source code of library n[END_REF][START_REF] Lee | Public source code of library n.7[END_REF][START_REF] Wang | Public source code of library n.9[END_REF][START_REF] Pankratiew | Public source code of library n.10[END_REF][START_REF] Pellegrini | Public source code of library n[END_REF][START_REF] Musat | Public source code of library n[END_REF], Libgcrypt, 2013, Moscow, 2019a] do not use safe primes. Instead, these implementations focus on generating large numbers and checking their primality. This method does not guarantee the generation of a safe prime. In fact, a safe prime of the form p = 2q+1 where q is also a large prime, is essential as it forms a large prime subgroup of order q. Conversely, using an arbitrary large prime results in a p -1 group order, that can be decomposed into small ✗✗ No Verificatum [START_REF] Verificatum | Public source code of library n[END_REF] T1 T1 Yes

Table 3.1: An overview on the 26 analyzed libraries (where T1, T2, T3 and T4 are listed in Table 3.2).

prime order subgroups. Hence, small prime order subgroups are exposed to subgroup attacks in which the discrete logarithm is easy to compute by using the Pohlig-Hellman algorithm [START_REF] Pohlig | An improved algorithm for computing logarithms over gf(p) and its cryptographic significance (corresp.)[END_REF] or the Pollard's rho algorithm [START_REF] Pollard | Monte carlo methods for index computation[END_REF].

Lack of QR Generators. In this category, we discuss the libraries that do not use quadratic residue generators. Among the 20 libraries that do not respect DDH, 5 libraries [START_REF] Nasr | Public source code of library n[END_REF][START_REF] Ridhuan | Public source code of library n.8[END_REF][START_REF] Elgamir | Public source code of library n[END_REF][START_REF] Pycrypto | Public source code of library n[END_REF][START_REF] Ioannou | Public source code of library n[END_REF]] use a safe prime p = 2q + 1 but do not choose a quadratic residue generator. Using a safe prime without a quadratic residue generator does not guarantee a subgroup of prime order q in which the DDH assumption stands. In what follows we show an example on the feasibility of learning information about the plaintext when we do not employ a quadratic residue generator.

Example 6. (Breaking ElGamal without a QR generator) To break ElGamal without a QR generator, it is sufficient to break the underlying assumption. The DDH assumption does not hold in Z * p if g is a generator of Z * p . This is because the Legendre symbol of g a reveals whether a is even or odd. Given (g a , g b , g ab ), one can compute the LS and compare the least significant bit of a, b and ab, which allows to distinguish between g ab and a random element group. Having a distinguisher against DDH means having a distinguisher against ElGamal and therefore break ElGamal.

Lack of Encoding.

We point out the relevance of message encoding mechanisms as a crucial requirement in ElGamal scheme. Despite generating a safe prime and choosing a quadratic residue generator, 5 libraries [START_REF] Botan | Public source code of library n[END_REF][START_REF] Riddle | Public source code of library n[END_REF][START_REF] Norvegia | Public source code of library n[END_REF], Pycryptodome, 2018[START_REF] Swisspost | Public source code of library n[END_REF] do not use a message encoding to map the messages into a valid subgroup. However, by adopting the standard encryption scheme of ElGamal, the message space is not restricted to the expected subgroup. This imply that even in the presence of a safe prime and consequently the presence of a subgroup of prime order generated by a quadratic residue generator, the message to encrypt is not mapped into the designed subgroup. Hence, an attacker can gain knowledge about the original message and expose the entire scheme to total insecurity. To better understand the importance of using a message encoding method, we display an attack on how to break a scheme that does not map messages into the intended subgroup (see example in Section 3.1).

Libraries That Do Respect DDH

In this section, we will present the implementations that respect the DDH assumption and therefore implement an IND-CPA secure ElGamal scheme. As mentioned in the previous section, a well implemented library should adopt a safe prime, a quadratic residue generator, and a message encoding technique. Only 6 out of the 26 analyzed libraries [START_REF] Belenios | Public source code of library n.1[END_REF], Estonia, 2017[START_REF] Helios | Public source code of library n[END_REF], Microsoft, 2019, Moscow, 2019b[START_REF] Verificatum | Public source code of library n[END_REF]] respect all of the previously mentioned conditions. In the following paragraphs, we will discuss in detail the message encoding techniques implemented in these libraries. In particular, we can categorize four different techniques.

Limited Message Space and q-exponentiations

The Estonian and Verificatum In this paragraph, we will present two libraries that implement ElGamal using the same technique: the Estonian voting system and Verificatum. The Estonian government relies on Internet voting in a significant way for national elections. While the Estonian voting system [Estonia, 2017] is implemented in Java, Verificatum [START_REF] Verificatum | Public source code of library n[END_REF], which implements provably secure cryptography libraries for electronic voting systems, is implemented in JavaScript. To comply with the IND-CPA security of ElGamal, these two implementations adopt a safe prime, and generate the subgroup of prime order in which the DDH assumption holds. Both implementations allow messages m to be any integer from [1, p -1]. Hence, before encrypting, one checks if m is a QR by checking m q ≡ 1 mod p: Listing 3.1: Limited space and q-exponentiations ElGamal encoding [START_REF] Verificatum | Public source code of library n[END_REF].

Proof. Euler's criterion states that a ∈ Z * p is a quadratic residue modulo p iff a p-1 2 ≡ 1 (mod p). Being q = p-1 2 , then a p-1 2 = a q ≡ 1 (mod p). ■ switch (legendre(m)) {
If the equivalence is confirmed then m is encrypted as a QR, else the message is rejected and an error is raised (see Listing 3.5). In fact, these two implementations take as an input messages in Z * p and rejects half of the messages that are not QR instead of encoding them (also see Helios in Subsection 3.2.2.2). Besides that, using q-exponentiations to encrypt messages can be optimized as we will explain in the next section.

Encoding with q-exponentiations

Helios Helios [START_REF] Helios | Public source code of library n[END_REF], is a known library implemented in Python. It is used for voting systems and can be manipulated to meet the needs of the users. Helios, is vulnerable to ballot stuffing as a dishonest bulletin board could add ballots without anyone noticing [START_REF] Belenios | Public source code of library n.1[END_REF]. Being IND-CPA secure, ElGamal in Helios is implemented by generating a safe prime p = 2q + 1 where p and q are both large primes. It then selects a generator g of the subgroup of prime order q. Before encrypting a message m, a mapping to the prime order subgroup is done. As the implementation allows the message m to be any integer from [0, p -1], one computes m 0 = m + 1 (to avoid picking m = 0) and checks whether m 0 is a QR. If m 0 q ≡ 1 mod p then it outputs m 0 which belongs to the QR elements (as in Subsection 3.2.2.1), else, it outputs -m 0 . Please note that -m 0 mod p belongs also to the QR elements. Being a safe prime p and p ≡ 3 mod 4, ensures the fact that 1 is a square element and -1 is a non-square element. This is essential in turning a non-square element m into a square element -m. After decryption, one obtains m and

checks if m ≤ q. If m ≤ q then m 0 = m otherwise m 0 = -m.
To recover the message, one computes m = m 0 -1 (see Listing 3.6).

Proof. This is because x 2 ≡ (-x) 2 mod p. So the squares of the first half of the nonzero numbers mod p give a complete list of the nonzero quadratic residues mod p. If p is an odd prime, the residue classes of {1 2 , 2 2 , ..., ( p-1

2 ) 2 } are distinct and give a complete list of the quadratic residues modulo p. So there are p-1 2 residues and p-1 2 non-residues. This gives a complete list as x 2 and (px) 2 are equivalent mod p:

x 2 ≡ y 2 mod p ⇔ p|x 2 -y 2 ⇔ p|(x -y)(x + y) ⇔ p|(x -y) or p|(x + y)
which is impossible if x and y are two different members of the set.

■

As we will see in the next section, it is possible to reduce to 2 the q-exponentiations, and therefore obtain a more efficient encoding process. [START_REF] Helios | Public source code of library n[END_REF].

Hard Decoding

Belenios and Microsoft Belenios [START_REF] Belenios | Public source code of library n.1[END_REF] is a verifiable voting system built upon Helios. It can be used to organize elections and perform verification. Contrary to Helios, Belenios provides eligibility verifiability as anyone can check that ballots are coming from legitimate voters: each voter receives a private credential, while the election server receives only the corresponding public credential. Therefore, even if the election server is compromised, no ballot can be added. Microsoft Election guard [Microsoft, 2019] is a library that verifies voting ballots. Concerning ElGamal encryption scheme a message m is encoded as g m where g is the QR generator of the prime order subgroup: every element written in the form of g m belongs to the subgroup generated by g. The choice of using the exponential version of ElGamal is to benefit from turning the multiplicative homomorphism of ElGamal into an additive one. After decryption, one should compute the discrete logarithm of g m in order to recover the initial message m. This is possible by using Pollard-lambda algorithm or brute force only if m is taken from a small subset and not from the entire interval {0, ..., q -1}. Being in a subgroup of prime order q, where q is a large prime, it is not possible to decompose the subgroup in smaller subgroups (Lagrange Theorem [START_REF] Pollard | Monte carlo methods for index computation[END_REF]) since the computation of the discrete logarithm is unfeasible in general (see Listing 3.7). Listing 3.3: Hard decoding implementation [START_REF] Belenios | Public source code of library n.1[END_REF].

Encoding with 2-exponentiations

Moscow Voting System For the elections of September 2019, the Russian government decided to employ an electronic voting system [Moscow, 2019a] to elect governors for local parliaments in Moscow. In July 2019, the source code, developed by the Moscow Department of Information Technology, was made public to test its vulnerabilities. At that time, the Moscow voting system was discovered to be subjected to two attacks by researchers [START_REF] Gaudry | Breaking the encryption scheme of the moscow internet voting system[END_REF]. In the first test, the researchers exploited the fact that the keys used are small: three keys of 256 bits were used. Discrete logarithms defined by small primes are easy to calculate in feasible time. Therefore, one can compute the discrete logarithm and recover the secret keys used for decryption. Moreover, one can decrypt messages employing the same time as a legitimate possessor of secret keys. After reporting this issue, the developers of Moscow voting system increased the key size to 1024 bits. However, a second test was made to verify the security of the modified version. In this version, the message space was not restricted to the subgroup of quadratic residues as any message was allowed to be encrypted. By relying on subgroup attacks, one can get enough information about the voter's choice and indeed can reveal one bit of information about the original message (see Section 3.1). Therefore the Decisional Diffie-Hellman assumption did not hold and the system leaked strong information. Two days before the elections, the developers modify the source code [Moscow, 2019b] and adopt an efficient method to secure their voting system. To map a message m into the QR subgroup, it is sufficient to square the message: m → m 2 (see Listing 3.8).

Proof. The quadratic residue theorem states that always the case when using a safe prime. As a matter of fact, the underlying group in this last version respects the DDH assumption. We will discuss the adopted method in the next section.

a ∈ QR if ∃ x s.t. x 2 ≡ a(p). Let m = x, then m 2 ∈ QR if m 2 ≡ m 2 (p),

Comparison of encodings

T1: Limited msg space & q-expon. T2: q-expon. T3: m-expon. T4: 2-expon.

Encoding m q ≡ 1(p)? m : error m q ≡ 1(p)? m : -mg m m 2 Decoding mm < q ?: m : -ml og g (g m ) m q+1 2

Table 3.2: Message Encoding Comparison.

In the previous section, we have seen 4 different encoding techniques of ElGamal that comply with the DDH assumption. In Table 3.2, we summarize the four techniques by giving a general overview on the encoding and the decoding processes.

T1

The first message encoding technique (T1) checks whether a message m is a QR or not by checking the following equivalence: m q ≡ 1(p). If the equivalence holds, then the message is encrypted, otherwise an error is raised and the message is rejected. The decoding operation is simple as one outputs directly the message m.

T2

The second message encoding technique (T2) uses the same method as the previous one, but instead of raising an error and rejecting the messages, it maps the message as -m. For what concerns the decoding process, one first checks if m < q and output m, otherwise it outputs -m.

T3

The third message encoding technique (T3) maps a message m as g m . The decoding mechanism is hard in general and can be only applied on a small subset of messages in which the computation of discrete logarithm can be solved by brute force.

T4 Concerning the fourth message encoding technique (T4), one maps a message m as m 2 into the subgroup of order q. This squaring technique is sufficient to map any message as a QR element. In addition, it is efficient as it needs only 2 exponentiations for encoding any message. To decode, one computes the square root by modular exponentiation of m: m q+1 2 to recover the original message.

Whereas in T4, the encoding technique is faster than T1 and T2 (2-exponentiations is more performant than q-exponentiations as q is large), the decoding process is T1 and T2 is faster. However, for what concerns electronic voting systems, usually several encryptions are made and only one decryption is needed to reveal the result of an election.

We conclude that T4 is more efficient to apply to electronic voting systems. Additionally, as reported in the note on Moscow voting systems [START_REF] Gaudry | Breaking the encryption scheme of the moscow internet voting system[END_REF], this technique is efficient since the decryption (q-exponentiations) is usually done on high-end servers, while the encryption (2-exponentiations) is done on the voter's device.

In addition, T1, T2, T3, and T4 implement a QR generator using q-exponenentiations since they check its quadratic residuosity by calculating g q (p). However, one can simply implement a quadratic residue generator by using only 2-exponentiations instead of using q-exponentiations (q-exponentiations are used in [START_REF] Belenios | Public source code of library n.1[END_REF][START_REF] Helios | Public source code of library n[END_REF], Microsoft, 2019, Moscow, 2019b[START_REF] Verificatum | Public source code of library n[END_REF] for the quadratic residue generator). But clearly, a more direct and efficient way to calculate the generator is by fixing it in advance. For example g = 4 if we are working in Z * p . Note that the performance of the encoding is more important than the performance of the generator calculation, which occurs only once at the initial phase of the voting process.

Moreover, the performance of the decoding is also less important than the encoding in a voting process as discussed previously.

We provide a reference implementation in Ocaml [START_REF] Rémy | Using, understanding, and unraveling the ocaml language. from practice to theory and vice versa[END_REF] (see Listings 3.5,3.6,3.7,3.8,3.9,3.10,3.11 ) in which we apply the encoding and decoding process as in T4. In addition, in our implementation, the generation of the quadratic residue generator differs from all the other implementations as we use 2-exponentiations instead of q-exponentiations.

• We generate a safe prime of the form p = 2 • q + 1 and check the primality of both p and q. let rec random_safe_prime nbits = let q = sample (nbits -1) in let q = Z.nextprime q in let p = Z.succ (Z. shift_left q 1) in if Z.probab_prime q 10 <> 0 && Z.probab_prime p 10 <> 0 then p else random_safe_prime nbits Listing 3.5: Our Ocaml implementation for a safe prime generator.

• We implement a QR generator for safe prime order groups. let generator pbits p = let q = Z.shift_right p 1 in let g = Z.succ (sample_le pbits (Z.sub p (Z.of_int 2)) ) in Z.powm g (Z.of_int 2) p Listing 3.6: Our Ocaml implementation for a QR Generator.

• We define the property of the group we use in our implementation, with p a random safe prime group, and g its generator.

let sample_group pbits = let p = random_safe_prime pbits in let g = generator pbits p in { pbits = pbits } Listing 3.7: Our Ocaml implementation for defining the group property.

• We encode the message to encrypt as a QR element: (m + 1) 2 mod p. let encode gr m = Z.powm (Z.succ m) (Z.of_int 2) gr.p Listing 3.8: Our Ocaml implementation encoding a message as a QR element.

• For encryption, we first check that 0 < m < q -1. Then we encrypt the message as a pair (g r mod p, pk r • encode(m) mod p). Notice that rmodpis a random element in q and pk is the public key g x mod p. let encrypt gr pk m = if (( Z.leq Z.zero m) && (Z.lt m (Z.pred (q gr)))) then let r = sample_le (gr.pbits -1) (q gr) in (Z.powm gr.g r gr.p, mulm gr (Z.powm pk r gr.p) (encode gr m)) else raise (Invalid_argument "ElG encryption") Listing 3.9: Our Ocaml implementation for a message encryption.

• Concerning the decryption, we decrypt the message m by using the private key sk.

We first calculate the inverse of g r mod p with functions mult and modulo, then multiply the encoded encrypted message with the resulting inverse to obtain the decryption of m. let decode gr m = let p = gr.p in let q = q gr in let r = Z.powm m (Z.shift_right (Z.succ q) 1) p in let m = if Z.leq r q then r else (Z.sub p r) in (Z.pred m) Listing 3.11: Our Ocaml implementation for decoding a decrypted message.

Related work

The ElGamal Scheme. The ElGamal encryption scheme was introduced in 1985 by Taher ElGamal [START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF]. It relies on Diffie-Hellman key exchange and is known to be semantically secure under the Decisional Diffie-Hellman (DDH) assumption where the discrete logarithm problem is hard to solve. In 2009, [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF] proved that the ElGamal encryption scheme is secure against chosen-plaintext attacks (CPA) in the standard model assuming that the DDH problem is hard in the underlying group family by using the proof assistant Coq. The Cramer-Shoup cryptosystem (CS) [START_REF] Cramer | A practical public key cryptosystem provably secure against adaptive chosen ciphertext attack[END_REF] Semantic Security. The mental poker [START_REF] Rivest | Mental poker[END_REF] is the first protocol known to be vulnerable to attacks because its encryption scheme does not respect the DDH assumption. The game of mental poker is an ordinary poker game and communications between players are done via messages since it is a game without physical cards. Being exposed to attacks, the mental poker game can leak one bit of information about the cards by observing whether the encryption scheme preserves the quadratic residuosity of a number [START_REF] Lipton | How to Cheat at Mental Poker[END_REF]. Consequently, in 1982, Goldwasser and Micali introduced the first probabilistic public-key encryption scheme [START_REF] Goldwasser | Probabilistic encryption and how to play mental poker keeping secret all partial information[END_REF] which is provably secure under standard cryptographic assumptions. It is based on the intractability of Quadratic Residuosity Assumption modulo a composite n. Considering that the distribution of quadratic residues and quadratic non-residues is not the same, one restricts oneself to a subset where the number of quadratic residues is equal to the number of quadratic non-residues, and takes only the messages that are quadratic residues to prevent an attacker from gaining any information about the original message.

Encoding Mechanisms. What we call message encoding refers to the mechanism that maps a message into a specific group. An approach to encode a message is the hash-ElGamal encoding. This scheme consists of including a hash function during the encryption process. Let h : G → {0, 1} l , w → h(w) be a hash function mapping elements to l-bit strings. The encryption of a message m ∈ M where the message space is defined as M = {0, 1} l is then given by (g r , m ⊕ h(y r )). This encoding mechanism solves the problem of leaking information about the original message but unfortunately, it cannot be used for voting systems as it loses its homomorphic property. Another option to encode messages is exponent-ElGamal encoding [START_REF] Cramer | A secure and optimally efficient multi-authority election scheme[END_REF]. This technique takes advantage of a property where any element w ∈ G =< g > is uniquely represented as w = g z for some z ∈ Z/qZ. For any message m ∈ Z/qZ, the resulting encoding is g m . The corresponding ciphertext is given by (c 1 , c 2 ) = (g r , g m y r ). In this case, the problem is in the decryption process: to retrieve the original message, the computation of the discrete logarithm in G is needed. Considering that the discrete logarithms are hard to solve in G, this leads to limit the message space to a small set where the discrete logarithm problem is easy to solve by using brute force or Pollard's rho algorithm [START_REF] Pollard | Monte carlo methods for index computation[END_REF].

Elliptic curve ElGamal is a different variant where a message m is represented as a point on an elliptic curve, more accurately, as a point on a prime order subgroup. Elliptic curve cryptography [START_REF] Koblitz | The state of elliptic curve cryptography[END_REF][START_REF] Miller | Use of elliptic curves in cryptography[END_REF] offers smaller key sizes resulting in gains in speed and memory, and benefits of the absence of sub-exponential algorithms that solve the elliptic curve discrete logarithm problem. However, encodings [START_REF] Farashahi | Hashing into hessian curves[END_REF][START_REF] Fadavi | Injective encodings to binary ordinary elliptic curves[END_REF][START_REF] Bernstein | Elligator: ellipticcurve points indistinguishable from uniform random strings[END_REF] mostly do not handle prime-order elliptic curves as there is no known polynomial time algorithm for finding a large number of points on an arbitrary curve. Furthermore, several encodings are hash-to-curve that are not invertible and therefore not compatible with group operation which destroys the homomorphic property [START_REF] Faz-Hernandez | Hashing to Elliptic Curves[END_REF].

Application to E-voting. We briefly discuss electronic voting systems that use ElGamal encryption. To get familiar with voting systems, we refer the interested reader to [START_REF] Ne Oo | A survey of different electronic voting systems[END_REF][START_REF] Cortier | Sok: Verifiability notions for e-voting protocols[END_REF][START_REF] Volkamer | Evaluation of Electronic Voting[END_REF]]. E-voting systems are important as they expand the participation of voters and offer an efficient way to count votes. However, without employing secure systems, the use of voting systems would be meaningless. E-voting uses public-key cryptography: ElGamal is the most common used encryption algorithm as it enjoys multiplicative homomorphic properties that allows the addition on the ciphertexts in order to count ballots without revealing the identity of the voters.

Additionally, ElGamal enables re-encryption which results in a different ciphertext containing the same information. (Paillier encryption scheme [START_REF] Paillier | Public-key cryptosystems based on composite degree residuosity classes[END_REF] is a possible option as well, relying on the DCR assumption). Various studies demonstrated the importance of ElGamal as an encryption scheme for electronic voting systems [START_REF] Haines | Verified verifiers for verifying elections[END_REF][START_REF] Adida | Helios: Web-based open-audit voting[END_REF]. Additionally, several countries (e.g. Estonia [START_REF] Kubjas | Estonian voting verification mechanism revisited again[END_REF], Norway [START_REF] Puigalli | Cast-as-intended verification in norway[END_REF] and Russia [START_REF] Babenko | A model of a secure electronic voting system based on blind intermediaries using russian cryptographic algorithms[END_REF]) are using e-voting systems as a main mechanism for elections and are employing ElGamal to count and verify votes. Moreover, in a note of 15 November 2019, Pierrick Gaudry [START_REF] Gaudry | Breaking the encryption scheme of the moscow internet voting system[END_REF] reveals an attack about the Moscow voting system because it does not comply with the DDH assumption.

Conclusion

During our analysis, we have discovered a number of ElGamal scheme implementations that are not IND-CPA secure since they do not respect the DDH assumption. On one hand, some implementations do not employ safe primes, an essential condition to form subgroups of large prime order in which the DDH assumption holds. On the other hand, other implementations do not apply message encoding mechanisms or use Quadratic Residue Generators. As a consequence, 20 out of the 26 analyzed libraries may leak one bit of information about the original message and therefore, may endanger the validity of an election. Finally, after comparing four different message encoding techniques that satisfy the DDH assumption, we conclude which implementation is most convenient for voting systems. We focused the current study on manually analyzing the IND-CPA security of open source code libraries of ElGamal encryption scheme. However, it is also possible to check the IND-CPA (in-) security when source code is not available. In fact, by applying the technique discussed in the Example 5 of Section 3.1, one can black-box test applications. In particular, such tests can be applied to ElGamal encryptions obtained by Hardware Security Modules (HSM) [ Volkamer, 2009, Orr and[START_REF] Orr | SAC '15[END_REF], which are used e.g. in the Estonian I-voting system [START_REF] Springall | Security analysis of the estonian internet voting system[END_REF].

In this chapter, we study correct implementations, regarding message encoding, of ElGamal over cyclic subgroups of Z * p . In the case of ElGamal over elliptic curves the underlying hard problem, the elliptic curve discrete logarithm problem, compels the encoding of the plaintext message m as a point on on a prime-order subgroup G of an elliptic curve. We leave the study of the implementations of such encodings as future work.

BROADCAST ENCRYPTION SCHEMES

Broadcast encryption schemes (BES) [START_REF] Fiat | Broadcast encryption[END_REF][START_REF] Boneh | Collusion resistant broadcast encryption with short ciphertexts and private keys[END_REF][START_REF] Lee | BESTIE: broadcast encryption scheme for tiny iot equipments[END_REF] offer an efficient solution in means of transmission length and key storage to securely broadcast messages to a privileged subset of nodes. They also aim to allow two nodes (unknown to each other), to agree on a common key. Broadcast encryption schemes provide cryptographic primitives to generate a common cryptographic key for a subgroup of nodes to ensure that only nodes of a privileged subgroup can decrypt a message. Generally, broadcast encryption schemes offer high security properties while adopting small key sizes [START_REF] Boneh | Collusion resistant broadcast encryption with short ciphertexts and private keys[END_REF][START_REF] Lee | BESTIE: broadcast encryption scheme for tiny iot equipments[END_REF]. Some schemes are known to be collusion resistant, which ensures that non authorized nodes cannot learn anything about the broadcast message. Other schemes enjoy traitor-tracing characteristics, in the sense that a sender can trace back which dishonest nodes have leaked the decryption key to non authorized nodes. Broadcast encryption schemes are classified as stateless or stateful. While stateless schemes provide nodes with permanent keys, stateful schemes provide nodes with updatable keys under certain conditions i.e. join or revocation event.

In this chapter, we investigate broadcast encryption schemes while providing some examples and discussing their security aspects. We also propose a new broadcast encryption scheme based on ElGamal [START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF]. We finally implement and compare three broadcast encryption schemes in terms of execution time, key storage and ciphertext space.

In Section 4.1, we give the general definition of a broadcast encryption scheme then present several schemes as the Fiat-Naor scheme,the ElGamal Baseline scheme, and the Boneh-Franklin scheme. In Section 4.1.4, we propose a new broadcast encryption scheme with constant size ciphertext and key storage based on ElGamal. Section 4.2 is devoted for the comparison and evaluation in terms of time and space of three broadcast encryption scheme. We implement and compare the execution time (Table 4.1) , ciphertext size (Table 4.3) and the maximum key storage (Table 4.2) in ElGamal Baseline, Fiat-Naor and the new scheme.

In summary, our contributions in Chapter 4 are:

• We propose a new broadcast encryption scheme based on ElGamal with constant size key storage and ciphertext.

• We implement and compare the execution time, the ciphertext size and the maximum key storage for nodes of three different broadcast encryption schemes.

General Definition of BES

Broadcast encryption schemes allow the sender to dynamically choose a privileged subset of nodes and send a ciphertext in such a way that only nodes in the privileged subset can read the message. We begin by formally defining what is a broadcast encryption scheme. Definition 23. A broadcast encryption scheme for a set of nodes S and a server consists of four primitives defining an encryption scheme and a broadcast primitive. The encryption scheme includes:

• Setup(S, λ) An initial setup algorithm that given a set S of n nodes and a security parameter λ, generates a master key K for the server (only the server has K) and n public/private pairs of keys (PK i , SK i ), one pair for each node. SK i is private to node n i . Private key SK i will be used for node n i in S to compute the decryption key whenever n i belongs to the privileged subset.

• KG(L, K) A key generation algorithm used at the server that takes as input a set L ⊆ S of nodes and a master key K and generates an encryption key K L to encrypt a message for nodes in L.

• Encrypt(L, K L , m) An encryption algorithm that takes as input a subset L of nodes, an encryption key K L for subset L, and a message m. The algorithm outputs a ciphertext and a header (H 1 ,...,H n ).

• Decrypt(L, SK i , H 1 ,...,H n , C m ) A decryption algorithm that is used in a node n i that takes as input a subset L, a private key SK i for node n i , headers H 1 ,...,H n for all nodes in L, and a ciphertext C m . First the algorithm calculates the decryption key for L by using SK i and public keys of nodes in L and then it outputs the decrypted message.

In what follows, we present three broadcast encryption schemes and propose a new scheme based on ElGamal encryption scheme [START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF].

Fiat-Naor

The first broadcast encryption scheme was proposed by A. Fiat and M. Naor [START_REF] Fiat | Broadcast encryption[END_REF]. In their scheme, they consider a key distribution center and a set of nodes. Their idea is to assign predefined keys to nodes, and compute a common key whenever the center wants to broadcast a message to a privileged subset of nodes. To retrieve the message, each node has to compute the common key itself. This scheme is cryptographically equivalent to RSA [START_REF] Rivest | A method for obtaining digital signatures and public-key cryptosystems[END_REF]. The scheme consists of four algorithms as follows:

• Setup. The server chooses a composite number that is hard to factorize N = P • Q, where P and Q are large primes, an element g of high value kept secret, and

φ(N) = (P -1) • (Q -1).
• Key Generation. For each node i ∈ T, the server assigns a private key g i = g p i and public key p i : {g i , p i }, where p i and p j are relatively prime for all i, j ∈ T and T is the subset of targeted nodes to whom the server is willing to broadcast messages.

The server also computes a common key g T = g i∈T p i mod N.

• Encryption. To broadcast a message m, the server computes the encryption key as

K enc = g T -1 mod φ(N)
, then encrypts m as m K enc mod N. The server broadcasts the following ciphertext: (p 1 , ..., p k , m K enc mod N).

• Decryption. To decrypt, every node i ∈ T evaluates g T = g i j∈T-{i} p j mod N, and computes m = (m K enc mod N) g T mod N.

Example 7. In this example, we consider a server willing to broadcast a message m to a privileged subset of nodes (n 0 , n 1 ). We also show how a node n 2 (that does not belong to the privileged subset) cannot decrypt the message.

Setup and Key generation. The server chooses a composite number that is hard to factorize 55 = 5 • 11 and an element g of high value kept secret. The server also computes a common key g T = g p 0 •p 1 mod N.

Phase 1: Setup and Key Generation 1: The server selects a generator g = 48.

2: For each node, the server assigns a private key g i = g p i and public key p i : {g i , p i } a: For node n 0 , the server assigns {27, 7}. b: For node n 1 , the server assigns {53, 13}. 3: The server computes g T = 48 7•13 mod 55 = 37.

Broadcast. To broadcast a message m = 6 to nodes in n 0 and n 1 , the server computes the encryption key as K enc = 37 -1 mod 55, then encrypts m as m K enc mod 55. The server broadcasts the following ciphertext: (n 0 , n 1 , m K enc mod 55).

Phase 2: Broadcast 1: The server selects a message m = 6. 2: To encrypt the m, the server computes the encryption key as K enc = 37 -1 mod 55 = 3.

3: The server encrypts m as 6 3 mod 55 = 51. 4: The server broadcasts (7, 13, 51).

Decryption. Upon receiving the broadcasted message, nodes n 0 and n 1 , evaluate the decryption key g T = g i j∈T-{i} p j mod 55, and computes m = (m K enc mod N) g T mod 55.

Note that node n 2 cannot compute the decryption as he cannot evaluates the decryption key.

Phase 3: Decryption for nodes n 0 and n 1 1: To decrypt, n 0 and n 1 compute the decryption key respectively as 27 13 mod 55 = 37 and 53 7 mod 55 = 37. a: Node n 0 computes m = 51 37 mod 55 = 6. b: Node n 1 computes m = 51 37 mod 55 = 6.

Security Aspects. The security of Fiat-Naor broadcast encryption scheme is equivalent to the security of RSA. It is based on the difficulty of factorizing a large composite integer. This is the reason why the server chooses N, a composite of two large primes. Moreover, it is k-resilient, in the sense that is secure against a coalition of at most k non privileged nodes. This scheme can be adapted to use RSA-OAEP algorithms to obtain an IND-CCA2

security [Barthe et al., 2011a]. Notice that elliptic curves cryptography offers the same security with smaller key size [START_REF] Gura | Comparing elliptic curve cryptography and RSA on 8-bit cpus[END_REF], one may consider replacing RSA algorithms relying on elliptic curves cryptography.

ElGamal Baseline

We present ElGamal Baseline scheme [START_REF] Chhatrapati | A performance evaluation of pairing-based broadcast encryption systems[END_REF] is a simple baseline broadcast encryption scheme based on ElGamal encryption scheme. This scheme is the broadcast version of the basic scheme of ElGamal (See Chapter 3). The idea of the ElGamal Baseline is broadcast a message to a subset of nodes by encrypting k times the same message using k public keys of k nodes. While in the basic scheme, the server selects one private key and compute the corresponding public key, in the ElGamal Baseline scheme, the server selects k private keys and computes k public keys.

• Setup. The server chooses a safe prime order group Z * p where p = 2 • q + 1, with p and q large primes. Let G q be the subgroup of Z * p of order q.

• Key Generation. The server selects g ∈ G q to be the generator of G q . For each node n i with i = 1, ..., k, the server chooses a random x i ∈ Z q and computes y i = g x i mod p.

The server outputs g, y 1 , ..., y k .

• Encryption. To encrypt a message m ∈ G q to a set of nodes S, the server picks a random r ∈ Z q . For each node i ∈ S, the server computes v i = m • y i r mod p. The server broadcasts the following ciphertext: (g r mod p, v 1 , ..., v k ) = (u, v 1 , ..., v k ).

• Decryption. To decrypt, a node i computes m = v i u x i mod p.

Example 8. Setup and Key Generation. The server chooses a safe prime order group Z * 11 and a generator g ∈ G 5 where G 5 is the subgroup of quadratic residues of Z * 11 [START_REF] El Laz | Security analysis of elgamal implementations[END_REF]. For nodes n 0 and n 1 , the server chooses (x 0 , x 1 ) ∈ Z 5 and computes y i = g x i mod 11.

Phase 1: Setup and Key Generation 1: The server selects a generator g = 4 ∈ G 5 . 2: For each node n i with (i = 0, 1), the server chooses x i ∈ Z 5 and computes y i = g x i .

a: For node n 0 , the server picks x 0 = 2 and computes y 0 = 4 2 mod 11 = 5. b: For node n 1 , the server picks x 0 = 3 and computes y 1 = 4 3 mod 11 = 9. 3: The server outputs (43, 9). Encryption. To encrypt a message m ∈ G 5 , the server picks a random r ∈ Z 5 . For each node, the server computes v i = y i r mod 11. The server broadcasts the following ciphertext:

(u, v 0 , ..., v 1 ).

Phase 2: Broadcast 1: The server selects a message m = 3 ∈ G 5 and a random element r = 2 ∈ Z 5 .

2: To encrypt the m, the server computes v i = y i r mod 11.

a: For node n 0 , the server computes v 0 = 3 • 5 2 mod 11 = 9. b: For node n 1 , the server computes v 1 = 3 • 9 2 mod 11 = 9. 3: The server broadcasts (5, 9, 1).

Decryption. To decrypt, a node i computes m =

Boneh-Franklin

Te broadcast encryption scheme proposed by A. Boneh and M. K. Franklin [START_REF] Boneh | An efficient public key traitor tracing scheme[END_REF]] is a traitor tracing scheme. Besides allowing to broadcast to a privileged subset of nodes, it also allows the server to identify a traitor in the system. The traitor in this scheme is a dishonest user who leaks the decryption key to an unauthorized node.

Since the scheme is based on error-correcting codes, the tracing problem can be viewed as watermarking the distributed secret keys.

• Setup. The server chooses a safe prime order group Z * p where p = 2 • q + 1, with p and q large primes. Let G q be the subgroup of Z * p of order q.

• Key Generation. The server selects g ∈ G q to be the generator of G q . For each node n i with i = 1, ..., k, the server chooses a random r i ∈ Z q and computes h i = g r i mod p. The public key is the set (y, h 1 , ..., h k ), where y can be written in the

form of y = k i=1 h i α i = g k i=1 r i •α i for random α i ∈ Z q .
A private key is an element θ i ∈ Z q such that θ i • γ (i) is the representation of y with respect to the base < h 1 , ..., h k >.

Let Γ = {γ (1) , ..., γ (k) } where each γ (i) = (γ 1 , ..., γ k ) a vector over Z q . The set Γ is fixed in advance and not secret. There exist several methods to compute Γ, we only show one method: for each node n 1 , the server computes

γ (1) = ( α 1 α 1 , α 2 α 1 , ..., α k α 1 )
. Each node n i then receives α i which will also be its decryption key θ i .

• Encryption. To broadcast a message m ∈ G, the server first picks a random element r ∈ Z q and encrypts the message m as m • y r mod p. The server then broadcasts the following ciphertext: (h 1 r , ..., h k r , m • y r mod p) = (H 1 , ..., H k , C).

• Decryption. To decrypt, a node n i computes m as:

m = C U θ i where U = k i=1 H i γ i .
Example 9. We consider a server willing to broadcast a message m to a targeted subset of nodes (n 0 , n 1 ).

Setup. The server chooses a safe prime order group Z * 11 and a generator g ∈ G 5 where G 5 is the subgroup of quadratic residues of Z * 11 [START_REF] El Laz | Security analysis of elgamal implementations[END_REF].

Phase 1: Key Generation 1: The server selects a generator g = 4 ∈ G 5 . 2: For each node n i with (i = 0, 1), the server chooses r i ∈ Z 5 and computes h i = g r i . a: For node n 0 , the server picks r 0 = 2 and computes h 0 = 4 2 mod 11 = 5. b: For node n 1 , the server picks r 1 = 4 and computes h 1 = 4 4 mod 11 = 3. 3: The server outputs a set of public keys as (y, h 0 , h 1 ).

a: For node n 0 , the server picks α 0 = 1. b: For node n 1 , the server picks

α 1 = 3. c: y = 1 i=0 h i α i = 3. 4:
The server outputs a public set of vectors Γ = (γ (0) , γ (1) = ((1, 3), (2, 1)) calculated as follows: a: For γ (0) , the server computes ( α 0 α 0 , α 1 α 0 ) = (1, 3). b: For node γ (1) , the server computes ( α 0 α 1 , α 1 α 1 ) = (2, 1).

Key Generation. The server selects r i ∈ Z 5 for each n i and computes h i = g r i and outputs a set of public keys (y, h 0 , h 1 , h 2 ), with y = 2 i=0 h i α i and α i ∈ Z 5 .

Since the server is willing to broadcast only to nodes n 0 and n 1 , he publishes Γ = {γ (0) γ (1) } and securely assign the private keys α 0 = θ 0 to n 0 and α 1 = θ 1 to n 1 .

Broadcast. To broadcast a message 5 ∈ G 5 to nodes in n 0 and n 1 , the server first chooses are random element 4 ∈ Z 5 , then encrypts the message. The server then broadcasts the following ciphertext :

(h 0 r , h 1 r , m • y r ) = (H 0 , H 1 , C).
Phase 2: Broadcast 1: The server selects a message m = 5 ∈ G 5 and a random element r = 4 ∈ Z 5 .

2: To encrypt the m, the server computes C = Encrypt({n 0 , n 1 }, 3, 5) = 5 • 3 4 mod 11 = 9. 3: The server then computes H 0 = 5 4 = 9 and H 1 = 3 4 = 4. 4: The server broadcasts (H 0 , H 1 , C) = (9, 4, 9).

Decryption. Upon receiving the broadcasted message, node n 0 and n 1 use θ 0 and θ 1 for n 1 to decrypt the ciphertext. The decryption process is described in the table below for n 0 . The node n 1 computes the same operation by using its private key. Note that node n 2 cannot compute the decryption as it does not possess its private key.

Phase 3: Decryption for node n 0 1: To decrypt, n 0 uses its private key θ 0 .

a: Node n 0 computes m = C U θ 0 = 9 4 1 = 5 where U = H

γ (0) 0 0 • H γ (0) 1 1 = 4.
Security Aspects. Besides being IND-CPA under the DDH assumption as proven in [START_REF] Boneh | An efficient public key traitor tracing scheme[END_REF], the Boneh-Franklin scheme authors presented a modified version secure against adaptive attacks.

A New BES Based On ElGamal

We propose a new broadcast encryption scheme with constant size ciphertext and key storage based on ElGamal. Its security relies on the e th root problem (We refer the reader to Section in Chapter 2) and is IND-CPA under the assumption of DDH in the random oracle model (The proof has been made in Easycrypt [START_REF] Barthe | Easycrypt: A tutorial[END_REF] but it is not part of the contribution of this thesis). In contrast with the broadcast encryption schemes discussed in Subsections 4.1.1, 4.1.2 and 4.1.3, in the new scheme, a node stores only one private key and one private key for all the subgroups it belongs to.

• Setup. The server chooses a public safe prime s = 2• s ′ +1, with s and s ′ large primes and 2 k ≤ s ′ ≤ 2 k+1 . The server also chooses a composite number N = p • q hard to factorize, with p = 2• p ′ +1, q = 2• q ′ +1 large safe primes kept secret, p, q ≡ 3 mod 4,

φ(N) = (p -1)(q -1) and N < s ′ .
Let G s ′ be the subgroup of Z * s of order s ′ . The server selects g ∈ G s ′ to be the generator of G s ′ , with g being public. Finally, the server computes a list L of public keys pk i for each node where pk i , pk j are relatively prime for all i, j ∈ Z * N such that gcd(pk i , pk j ) = 1 and gcd( pk i ∈S pk i , φ(N)) = 1, for ∀ S ⊆ L.

• Key Generation. Let G q ′ be the subgroup of Z * N of order q ′ . The server selects h ∈ G q ′ , where h is kept secret. For each node i the server assigns a secret key SK i = h pk i mod N. The server outputs (g, pk 1 , ..., pk k ).

• Encryption. The server evaluates x ′ = h ( pk i ∈S pk i ) mod N, where S ⊆ L. Let H be a hash function that takes a bitstring and returns a bitstring in {0, 1} k+1 . The server calculates x = H(x ′ ) and computes y = g x mod s. To encrypt a message m ∈ G s ′ , the server picks a random r ∈ Z s ′ and encrypts m as m• y r mod s. The server broadcasts the following ciphertext: ( pk i ∈S pk i ) mod N, g r mod s, m • y r mod s) = (z, u, v).

• Decryption. To decrypt, node i first computes pk = z pk i . To calculate its decryption

key k dec , node i computes k ′ dec = SK pk i mod N, then k dec = H(k ′ dec ) .
To retrieve the message m, node i computes:

m = v u k dec mod s.
Example 10. Setup and Key Generation. The server chooses a safe prime order group Z * 47 and a generator g ∈ G 23 where G 23 is the subgroup of quadratic residues of Z * 47 [START_REF] El Laz | Security analysis of elgamal implementations[END_REF]. It also chooses a composite number hard to factorize 21 = 3 • 7 with φ(21) = (3 -1)(7 -1) and 21 < 23. The server selects g = 4 ∈ G 23 and h = 1 ∈ G 3 . For each node i the server assigns a secret key SK i = h sk i mod 21, where sk i , sk j are relatively prime for all i, j ∈ Z * 21 . The server outputs (g, sk 1 , ..., sk k ).

Phase 1: Setup and Key Generation 1: The server selects a generator g = 4 ∈ G 23 , and h = 1 ∈ G 3 . 2: For each node n i with (i = 0, 1), the server assigns SK i = h pk i mod 21. a: For node n 0 , the server picks pk 0 = 13 and computes SK 0 = 1 13 mod 21 = 1. b: For node n 1 , the server picks pk 1 = 5 and computes SK 1 = 1 5 mod 21 = 1. 3: The server outputs (4, 13, 5). Encryption. In this example, we do not consider the hash function for encryption. The server evaluates x ′ = h ( pk i ∈S pk i ) mod 21, and computes y = g x mod 47. To encrypt a message m ∈ G 23 , the server picks a random r ∈ Z 23 and encrypts m as m • y r mod 47. The server broadcasts the following ciphertext: (z, u, v). Phase 3: Decryption for node n 0 and n 1 1: To decrypt, n 0 and n 1 calculate their respective private keys as: a: Node n 0 computes pk = 2 13 mod 21 = 5 and computes k dec = 1 5 mod 21 = 1. b: Node n 1 computes pk = 2 15 mod 21 = 13 and computes k dec = 1 1 3 mod 21 = 1. 2: Node n 0 and n 1 calculate m = 37 17 1 mod 47 = 16.

Security Aspects. We conjecture that the new scheme is IND-CPA under the assumption of DDH since it is based on ElGamal encryption scheme. Moreover, its security relies on the e th root problem (See Section 2.2 of Chapter 2). This problem is hard as long as factoring the composite number N is hard.

An attacker willing to compute the decryption key needs to possess either a private key assigned by the server or h ∈ Z * N . Since we choose h not only to be an element of a composite number hard to factorize, but also an element of the prime order subgroup G q ′ of Z * N , it is hard to compute the eth root of h since this problem is believed to be computationally hard in such composite numbers. Therefore, an attacker cannot compute the decryption key and will not be able to learn any information about the original message. Moreover, there are no algorithms able to calculate the eth root of composite modulus.

Evaluation and Comparison

In this section, we implement and compare three broadcast encryption schemes: the ElGamal Baseline scheme, the Boneh-Franklin scheme and the new scheme. We carry out a runtime evaluation based on experimental values for the key generation, encryption and decryption in Table 4.1. Moreover, we compare the size of keys for 1 node in n subgroups (Table 4.2), and the size of ciphertext for u nodes in 1 subgroup (Table 4.3) for each broadcast encryption schemes. While the ElGamal Baseline and the Boneh-Franklin schemes are tested over a prime order group of 1024 bits, our scheme is tested over a 2048 bits prime order group since we aim to generate a sufficient large composite number to achieve security guarantees. We implement the schemes using the Ocaml programming language [START_REF] Rémy | Using, understanding, and unraveling the ocaml language. from practice to theory and vice versa[END_REF], and the runtimes are tested on a 2017 Macbook Pro with a 3.1 GHz Quad-Core Intel Core i7 and 16 GB RAM. The source code of our implementation can be found here.

Key Generation Time

We start by analyzing the key generation time for u nodes. The results can be observed in the first row of Table 4.1. This phase requires the generation of a safe prime order group, a quadratic residue generator and the computation of public and private keys.

Notice that the key generation time of ElGamal Baseline is 100 % faster than the key generation time of the Boneh-Franklin scheme, and approximately 30 % slower than the key generation time in the new scheme.

• For ElGamal Baseline scheme, we generate a safe prime order group of 1024 bits (Z * p ), and choose a quadratic residue generator g. For u nodes, we randomly sample a list of private keys x i and compute a list y of public keys as a set of k times y i = g x i . Such operations are usually fast to compute over Z * p .

• For Boneh-Franklin scheme, we also generate a 1024 bits prime order group and choose a quadratic generator. For k nodes, we randomly sample a list of r i and compute a list h of public keys as a set of u times h i = g r i . Moreover, we randomly sample a list of α i and compute a public key y are the multiplication of u group exponentiation of h

α i i .
Finally, we generate a list γ of u vectors where each vector is a set of u group multiplication. Since the number of computations is bigger than the one in ElGamal Baseline, it explains why it takes approximately more time to compute.

• For the new scheme, we generate a 2048 bits prime order group and choose a quadratic generator g. We also generate a composite number H of two large primes such that H < q. The choice of a 2048 bits prime order group is to obtain a group Z * H of 1024 bits. We provide the keygen function with a list of pre-computed coprime numbers as input. In our scheme, this can be done because this list is public.

Because of this, the computation time of this list is not considered in the evaluation time of key generation. We only consider the time to calculate the list y of private keys as a set of k times h n i . The new scheme is faster than ElGamal Baseline and Boneh-Franklin scheme. While in Boneh-Franklin, it takes 120 seconds the generate keys for 100 k nodes, in the new scheme it takes only 45 seconds.

We evaluate and compare the execution time for 2, 5, 100, 1k, 10k and 100k nodes.

In summary, for the key generation time, we conclude that:

• The ElGamal Baseline scheme is faster than Boneh-Franklin scheme, and time increases linearly with the increase of the number of nodes.

• The Boneh-Franklin scheme is slower than ElGamal Baseline and the new scheme, and the time increases linearly with the increase of the number of nodes.

• The new scheme is faster than the other two schemes, and time increases linearly with the increase of the number of nodes.

Encryption Time

In the encryption phase, we measure the computation time needed by the server to encrypt a message to a set of nodes. The results can be observed in the second row of Table 4.1. By analyzing the encryption time, we observe that the encryption time for ElGamal Baseline and Boneh-Franklin are analogous. In fact, during the encryption, in ElGamal Baseline the server computes v i = (h i ) r • mktimes in addition to g r ; while in Boneh-Franklin, the server computes H r i u times in addition to m • y r , which results in the same number of group operations.

• In ElGamal Baseline scheme, the server samples are a random r ∈ Z q and computes k times v i = m • y i r mod p. By observing Table 4.1, we note that the encryption time increases linearly with the increase of the number of nodes. It is clear since the server encrypts u times the same message using the public key of u nodes.

• In Boneh-Franklin scheme, the server samples are a random r ∈ Z q and computes k times v i = H i r mod p. Again, by observing Table 4.1, we note that the encryption time increases linearly with the increase of the number of nodes. It is clear since the server encrypts the message only once, but it computes u times H i r mod p using the public key of u nodes.

• In the new scheme, the server samples a random r ∈ Z q . It evaluates

x = h k i=1 n i mod H
and computes y = g x mod p. The server then encrypts the message once by employing a group multiplication. In Table 4.1, in contrast with the other two schemes, we observe that the encryption time in the new scheme is constant till 1000 k nodes.

Note that, for a number of node greater than 10 k, the encryption time increases by little due to the fact that the server evaluates x for a larger number of nodes.

However, the time increase results to be small and the new scheme is faster than in the other two schemes.

In summary, for the encryption time, we conclude that:

• The ElGamal Baseline and the Boneh-Franklin schemes have the same encryption time. Yet, the encryption time increases linearly with the increase of the number of nodes.

• The encryption time in the new scheme is the fastest among the three schemes.

Furthermore, it is constant (the increase for larger set of nodes is limited) independently of the number of nodes in the system.

Decryption Time

For decryption time, we focus our analysis on the decryption time for 1 node since all nodes compute the same operation to retrieve the original message. The results can be observed in the third row of Table 4.1. The decryption time of the ElGamal Baseline and the new new scheme remain constant with the increase of the number of nodes. In both schemes, to decrypt, nodes either use their own private key or compute the decryption key by only using their private key. Yet, the ElGamal Baseline scheme is faster than the new scheme since nodes use directly their own private key to decrypt while in the new scheme nodes should first compute the decryption key in order to decrypt.

• In ElGamal Baseline scheme, a node computes one group multiplication using its private key x i to calculate the message. That is why the decryption time for one node is constant since the node only uses its private key to decrypt without the need of computing a decryption key. Hence, its decryption key is independent from the number of nodes in the subgroup.

• In Boneh-Franklin scheme, a node first computes U as u multiplication of exponentiation H i γ i . Then it computes a group multiplication using its private key α i to calculate the message. That is why the decryption time increases linearly with the increase of the number of nodes in the system.

• In the new scheme, a node first calculates n = z n i mod H which is a multiplication group operation independent of the number of nodes since it is computed modulo H. Then, it computes its decryption key using its private key SK i . To retrieve the message, the node performs a multiplication group operation. As shown in Table 4.1, the decryption time is constant and faster than the one in Boneh-Franklin scheme.

Comparing to ElGamal Baseline, the decryption time in the new scheme is greater by only 0.003 seconds.

In summary, for the decryption time, we conclude that:

• The Boneh-Franklin scheme is the slowest scheme in terms of decryption since the nodes computes k + 2 group operations.

• In ElGamal Baseline, the decryption time is constant independently of the number of nodes.

• Analogously to ElGamal Baseline, the decryption time is constant and marginally slower since nodes compute an extra operation to decrypt the ciphertext.

Item Scheme Time of execution per u nodes

u = 2 u = 5 u = 100 u = 1k u = 10k u = 100k

Maximum Storage of Keys

In this section, we measure the maximum storage size of keys concerning only 1 node belonging to n subgroups. The results can be observed in Table 4.2.

• In the ElGamal Baseline, each node needs to store a private key x i for each subgroup it belongs to. For n subgroups, a node have to store n keys of 1023 bits each. From Table 4.2, we can observe that the size of key storage increases linearly with the increase of the number of subgroups. The ElGamal Baseline is much better than Boneh-Franklin scheme in all subgroups. Yet, in comparison with the new scheme, it is only better when the number of subgroups is 2.

• In the Boneh-Franklin scheme, each node has to store a private key α i and a public key Γ i for each subgroup. We assume for this calculation that each subgroup has a maximum of 2 nodes. This is an arbitrary choice to calculate a minimal lower bound for key storage in Boneh-Franklin scheme. Notice that the more nodes are in each subgroup , the larger space is needed for key storage in this scheme. For n subgroups, a node stores n private keys and 2 • n keys of 1023 bits with the total of 3n • 1023 bits. Analogously to ElGamal Baseline, the size of key storage increases linearly with the increase of the number of subgroups. In the Boneh-Franklin scheme, a node maximum storage of keys is greater than the maximum storage of keys in ElGamal Baseline by a factor of 3.

• In the new scheme, each node needs to store a public key n i and a private key h n i for all the subgroups it belongs to. For n subgroups, a node stores only 2 keys of 2047 bits each for the total of 4094 bits. From Table 4.2, we can observe that the maximum storage of keys for 1 node is constant for any number of subgroup.

Only for n = 2, the ElGamal Baseline and Boneh-Franklin contain less key storage.

The new scheme is better than the other schemes for n = 5 and above. For n = 1k, the maximum key storage size in the new scheme is 250 times smaller than the storage of ElGamal Baseline scheme. For n = 100k the new scheme, the maximum key storage size is smaller by factor of 75000 than the one in the Boneh-Franklin scheme.

In summary, for the key storage, we conclude that:

• The maximum key storage is ElGamal Baseline is three times smaller than the size of the one in the Boneh-Franklin scheme. In both cases, the key size depends on the number of nodes in the subgroup. In fact, the key size increases linearly with the increase of the number of nodes.

• In the new scheme, the maximum key storage size is smaller than the the size in the other two schemes. Beside being smaller, the size of key storage in the new scheme is constant.

Scheme Keys

Max storage of keys for 1 node in n subgroups (in bits)

n n = 2 n = 5 n = 100 n = 1k n = 10k n = 100k Baseline {x G1 , ...,

Ciphertext Size

We analyze the ciphertext size of the three broadcast encryption schemes for u nodes in 1 subgroup. The results can be observed in Table 4.3.

• In the ElGamal Baseline scheme, the server broadcasts {g r , v 1 , ..., v u }. Since we are working in a 1024 bits groups, it translates to broadcasting 1024 bits+ ku • 1024 bits for a total of (u+1)•1024 bits. In Table 4.3, we can observe that ciphertext size increases linearly with the increase of the number of subgroups.

• In the Boneh-Franklin scheme, the server broadcasts {H r i , ..., H r u , v}. In a 1024 bits groups, this is equivalent to broadcasting u • 1024 bits+ 1024 bits for a total of (u + 1) • 1024 bits. Hence, as shown in Table 4.3, the ciphertext size increases linearly with the increase of the number of subgroups.

• In the new scheme, the server broadcasts { u i=1 n i , g r , v}. Since we are working in a 2048 bits groups, it means that the server is broadcasting 3 • 2048 bits for a total of 6144 bits. The ciphertext size is constant independently of the number of subgroups. In contrast to the ElGamal Baseline and the Boneh-Franklin schemes, the new scheme offers constant size ciphertext. Moreover the ciphertext size in the new scheme is smaller than the one in the other two schemes for a number of subgroups greater than 5.

In summary, for ciphertext size, we conclude that:

• In the ElGamal Baseline and the Boneh-Franklin schemes, the ciphertext size increases linearly with the increase of the number of nodes.

• Besides offering smaller ciphertext size than the other two schemes, the new scheme enjoys a constant size ciphertext.

Scheme Ciphertext

Ciphertext size for u nodes in 1 subgroup (in bits)

k u = 2 u = 5 u = 100 u = 1k u = 10k u = 100k Baseline {g r , v 1 , ..., v u } (u + 1)

Related Work

The concept of broadcast encryption was proposed by Fiat and Naor [START_REF] Fiat | Broadcast encryption[END_REF] who presented a scheme that allows the sender to broadcast a message to all the users except the revoked ones (users with compromised keys). The security notion required that any coalition of users (up to a threshold) can not obtain any secret about the other users or the content of the broadcast. After that seminal work, several schemes were proposed to get good trade-offs between key storage cost and transmission cost [START_REF] Boneh | Collusion resistant broadcast encryption with short ciphertexts and private keys[END_REF][START_REF] Delerablée | Fully collusion secure dynamic broadcast encryption with constant-size ciphertexts or decryption keys[END_REF][START_REF] Boneh | Low overhead broadcast encryption from multilinear maps[END_REF][START_REF] Agrawal | Optimal broadcast encryption from pairings and LWE[END_REF]. Further improvements were done in the context of multi-cast protocols [START_REF] Canetti | Multicast security: A taxonomy and some efficient constructions[END_REF]. In these types of protocols, participants must agree on one or more keys to achieve confidentiality as well as authentication, with potentially many senders. For such settings, clients are no longer stateless (they must keep state beyond group information) but that allows protocols to cope with more diverse scenarios, like authentication in dynamic groups with or without group managers. For the case of confidentiality under single source broadcast, the scheme by Fiat and Naor [START_REF] Fiat | Broadcast encryption[END_REF] provides a simple and efficient solution for the case of dynamic groups (ie.

user revocation in [START_REF] Canetti | Multicast security: A taxonomy and some efficient constructions[END_REF]). In terms of security notions, several schemes have been shown to achieve IND-CPA and IND-CCA [START_REF] Boneh | Collusion resistant broadcast encryption with short ciphertexts and private keys[END_REF][START_REF] Zhang | Adaptively secure identity-based broadcast encryption with constant size private keys and ciphertexts from the subgroups[END_REF][START_REF] Yang | Broadcast encryption based non-interactive key distribution in manets[END_REF][START_REF] Chen | Adaptively secure efficient broadcast encryption with constant-size secret key and ciphertext[END_REF]. BE can also be built on top of other primitives such as identity-based Encryption (IBE), which allows the sender to specify an arbitrary string as public key. This flexibility comes at the expense of requiring a central authority which, using a master key, can compute private keys for any identity. In hierarchical identity-based encryption (HIBE) [START_REF] Horwitz | Toward hierarchical identity-based encryption[END_REF]Lynn, 2002, Gentry and[START_REF] Gentry | Hierarchical id-based cryptography[END_REF],

a collection of authorities is arranged in a organizational hierarchy (a tree). Any authority at level k in the hierarchy can issue private keys for any descendant in the hierarchy but cannot decrypt messages intended for identities. It turns out that HIBE schemes can be converted into public-key broadcast encryption schemes with a dynamic set of receivers (albeit with rather large ciphertext length [START_REF] Naor | Revocation and tracing schemes for stateless receivers[END_REF][START_REF] Boneh | Collusion resistant broadcast encryption with short ciphertexts and private keys[END_REF]). None of these constructions, however, seem to exploit the underlying hierarchy to BE schemes with interesting properties among groups of receivers.

Conclusion

In this chapter, we investigated broadcast encryption schemes. We presented three existing schemes and discussed their security aspects. We also proposed a new broadcast encryption scheme based on ElGamal with constant size ciphertext and key storage. We implemented and compared, in terms of execution time, ciphertext and key storage space, three broadcast encryption schemes: the ElGamal Baseline scheme, the Boneh-Franklin scheme and the new scheme. Comparing to ElGamal Baseline, the new scheme is faster in key generation (given the fact that the public keys list is already pre-calculated) and encryption time but slightly slower in terms of decryption. Comparing to the Boneh-Franklin scheme, the new scheme results faster in the key generation, the encryption and the decryption time. Moreover, while in ElGamal Baseline and Boneh-Franklin the encryption time increases linearly with the increase of the number of nodes, the encryption time in the new scheme remains constant.

Concerning the key storage space, we showed that the new scheme contains a smaller size of keys with respect to the other two schemes, and enjoys a constant size key storage equivalent to 4094 even for 100k subgroups of nodes. For the ciphertext size, the new scheme is also better than the other two schemes. While in ElGamal Baseline and Boneh-Franklin schemes, the ciphertext size increases linearly with the increase of the number of subgroups, in the new scheme the ciphertext size remains constant and much smaller than in the other two schemes. For instance, the ciphertext in the new scheme for 10k subgroups is only 6144 bits, while in ElGamal Baseline and Boneh-Franklin scheme, the size is 10342400 bits. Since elliptic curve cryptography requires smaller key sizes, resulting in significant gains in speed and memory, it would be interesting to implement the broadcast schemes compared in this chapter over a prime-order subgroup G of an elliptic curve for comparison. We leave this as future work along with proving the IND-CPA security of the new scheme.

C HAPTER

TYPES FOR SECURE ARCHITECTURES IN DISTRIBUTED

SYSTEMS

In this chapter, we propose two architectures for broadcasting messages to subgroups of nodes. Our idea is to map subgroups of nodes to levels in information flow security lattices to verify secure information flow in the server code. The purpose of the proposed architectures is to allow the server to securely communicate with a set of nodes in hierarchical distributed systems. We focus on implementing the idea via a type system for each architecture. Our main focus is to preserve, or more precisely, protect the confidentiality and integrity of the communications between server and nodes. We divide this chapter in two parts. In the first part, we present an architecture and a type system for broadcasting to nodes with static security levels. In the second part, we present a more complex architecture and type system in which we consider broadcasting software updates to nodes with dynamic security levels.

In Section 5.1, we introduce an architecture for broadcasting messages and define its model and the security properties we would like to achieve. We then present a server language with special syntax for broadcast encryption and for key generation. In Subsection 5.1.3, we present the semantics of our the language and in Subsection 5.1.4, we develop a type system that enforces information flow security relying on the connection between BES privileged subgroups and security classes in distributed systems combined.

Our typing rules enforce an appropriate usage of cryptographic primitives as broadcast encryption and keys. It verifies that cryptographic keys variables are not being altered. It also checks that messages designated to a privileged subgroup of nodes are not exposed to nodes with less authorization.

In Section 5.2, we introduce an architecture for broadcasting software updates and discuss its system model and the security properties we would like to enforce. In Subsection 5.2.2, we present a server language with syntax for broadcast encryption and syntax for remote attestation to verify the integrity of nodes. In Subsection 5.2.3 and Subsection 5.2.4, we give the semantics and the type system of our the language. Our type system enforces the integrity of nodes through remote attestation. Regarding the information flow policy, our type system captures insecure information flow between server and nodes belonging to different security classes. In particular, our typing rules ensure the update of variables holding information of nodes of the same security level, once the integrity of nodes is verified. Our main results comply with information flow security. Moreover, they guarantee that an attacker cannot distinguish between different executions, and therefore, its knowledge is not increased.

In Subsection 5.1.5, in our theorem, we express non-interference as preservation of confidentiality property and we parametrize it by an attacker observation level, and support our theorem with a soundness proof that we present in Appendix A. In addition to preserving confidentiality, in Subsection 5.2.5, we present a security property that preserves also integrity supported by a soundness proof in Appendix B. Both proofs are done by induction on the height of the typing derivation tree of Γ ⊢ p. We conclude the chapter with related work and discuss conclusions and future work.

In summary, our contributions in Chapter 5 are:

• We consider two architectures: while the first architecture considers broadcasting messages to nodes with static security levels, the second architecture considers broadcasting software updates to nodes with dynamic security levels.

• We propose two type systems. The first type system applies to a server language that features a cryptographic operation of broadcast encryption and one for generation of cryptographic keys to broadcast to a group of nodes with different security clearances. In addition to this, the second type system also considers integrity and endorsement. In particular, it monitors that variables containing information of nodes belonging to the same security level are updated only if the remote attestation succeeds.

• We support our work by soundness proofs for the two type systems, that ensure the compliance of type-checked server code with a formally defined information flow policy preserving confidentiality (for both type systems) and integrity of data (for the second type system).

Types for Broadcasting to Nodes with Static

Security Levels

Security of distributed systems depends on protection mechanisms to ensure confidentiality of information traveling over an open network. Cryptography provides essential mechanisms for confidentiality. Cyptographic encryption schemes can provide strong security guarantees, such as IND-CPA or semantic security [START_REF] Goldwasser | Probabilistic encryption and how to play mental poker keeping secret all partial information[END_REF]. However, even with plain encryption, the confidentiality of keys, plaintexts, and ciphertexts are interdependent [START_REF] Rezk | Secure Programming[END_REF]: encryption with untrusted keys is clearly dangerous, and plaintexts should never be more secret than their decryption keys. Our proposal is that, to verify that information in the server flows to nodes with the appropriate clearances (e.g. verify the use of the correct encryption keys), we can map broadcast subgroups of nodes to levels in information flow security lattices. We implement this idea via a type system and provide a soundness proof with respect to a formally defined secure information flow property for server code.

An Architecture for Broadcasting Messages

We consider scenarios in which a server broadcasts messages with different confidentiality levels to nodes subgroups holding the appropriate clearance. We build on IND-CPA broadcast encryption schemes to preserve the message's confidentiality over a network and map subgroups of nodes to security lattices.

Security Lattices. In order to keep track of the confidentiality clearance of nodes, we use a mapping from nodes to security classes that we formalize as elements or levels in a lattice [START_REF] Denning | A lattice model of secure information flow[END_REF]. These security levels are used for messages so that the server can identify to which subgroups messages can be securely delivered. We use a lattice structure for modeling confidentiality, i.e. a partially ordered set together with least upper bound (join operator) and greatest upper bound (meet operator) on the set.

In our architecture, the set of security classes is partially ordered by ≤ in a lattice (L , ≤).

A confidentiality security level ranges over τ and indicates a read level. In the lattice, τ ≤ τ ′ means that τ ′ has more confidentiality than τ. We write ⊥ for the lowest security level and ⊤ for the highest security level in lattice L .

Example 11. In this example, we show a confidentiality security lattice namely diamond lattice with three nodes placed as follows:

L = {n 0 , n 1 , n 2 }, M 1 = {n 0 }, M 2 = {n 1 } and H = {n 1 }. The partial order of the lattice is L ≤ M 1 ≤ H and L ≤ M 2 ≤ H.
IN the rest of the paper, we will be referring to the lattice in Figure 5.1.

H = {n 1 } L = {n 0 , n 1 , n 2 } M 1 = {n 0 , n 1 }M 2 = {n 1 } Figure 5
.1: Security lattice

Models and Goals

This section covers the system model and the attacker model. We then informally introduce the security property that we want to provide.

System Model. We consider a framework where a single infrastructure provider, a server S, controls and manages a large set of networked nodes in a distributed system that we simply indicate as set of nodes N. Such framework is suitable for many IT systems in which the nodes can vary between smart cards, cloud systems and IoT systems. The server seeks to securely communicate with nodes belonging to privileged subgroups. Indeed, the server maps subgroups of nodes into security classes that we indicate as security levels.

Attacker Model. We assume passive attackers that listen to the network that the server uses to communicate with nodes. We also assume that an attacker can read all the public information but cannot prevent communications between a server and the nodes.

Security Properties

We want to provide the following security properties:

• Secure communication. A server communicates with a specific node with confidentiality guarantees. In our architecture, confidentiality is ensured via the use of a IND-CPA [START_REF] Rackoff | Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack[END_REF]] BES, the correct usage of cryptographic keys on the server for nodes at a given security level.

• Secure information flow. Information intended to more privileged security levels cannot flow into less privileged security levels. More specifically, messages with higher confidentiality clearances cannot be read by nodes with lower confidentiality clearances. This is ensured via a type system on the server code.

Syntax

In what follows, we consider the server language described below. It consists of programs, which can be expressions e or commands c. We let x, n, k range over variables and v ranges over strings, integers and boolean literals. We distinguish special variables n, n 1 , n 2 ,... to designate nodes. We use • for basic arithmetic and boolean operations.

Commands include standard statements (assign, sequence, if, while) and special statements (sbroadcast, KG). In the broadcast statement sbroadcast({n 1 , ..., n j }, k,e), the server uses a broadcast encryption scheme to communicate a message e to a set of nodes (designated by {n 1 , ..., n j }) using an encryption key k. In the key generation statement k := KG({n 1 , ..., n i }, k ′ ), the server uses a master key k ′ to generate the encryption key k for a set of nodes {n 1 , ..., n i }.

Semantics

A program is related to a memory µ which is a finite function that maps variables into values. We write µ[x := v] for the memory that assigns value v to a variable x.

The semantics allows us to derive judgments of the form µ ⊢ e ⇒ v for expressions and µ ⊢ c ⇒ t µ ′ for commands. These judgments affirm that evaluating expressions e in memory µ results in literal v. Evaluating command c in memory µ results in a new memory µ ′ with t being a side effect that represents the command sends a message to the network. The semantics rules are given in Figure 5.2.

• In the Base rule, v evaluates itself.

• In the Var rule, the value v is applied to x.

• In the Op rule, e is evaluated to v and e ′ to v ′ ; then the operation e • e ′ between e and e ′ is evaluated into the operation v • v ′ .

• In the Loop-True rule, e is true, c is evaluated in µ ′ , while statement in µ ′ is evaluated in µ ′′ ; then the while statement in µ is evaluated in µ ′′ .

• In the Loop-False rule, e is false; then the while statement is evaluated in µ.

• In the Secure Broadcast rule, the server takes as input a set of nodes {n 1 , ..., n i }, the evaluation vk of key k in µ and the evaluation "m" of message e. To broadcast a message, the server employs a broadcast encryption scheme. We model the ciphertext that goes to the network by the annotation BEnc({n 1 , ..., n i }, vk,"m").

• In the Key Generation rule, the server applies a key generation algorithm KG({n 1 , ...,

n i }, v),
that takes in input a set of nodes {n 1 , ..., n i }, the evaluation v of key k ′ in µ and outputs the encryption key vk.

Typing Rules

The types of the language are stratified as follows, where τ ranges over security levels from a confidentiality security lattice.

(Programs types) ρ ::

= τ | τ var | τ cmd | τ Nvar(n) | τ Kvar (n 1 ,...,n i ) | ⊤ MKvar
Type τ var is the type of a variable, τ cmd is the type of a command, and type ⊤ MKvar the type of master keys. Type τ Nvar(n) is the type of node variables. We write Γ(n) = τ Nvar(n1, ..., n i ) to specify that τ is the maximum confidentiality clearance for node n. Type τ Kvar (n 1 ,...,n i ) is the type of encryption keys, meaning that the encryption key is used for nodes n 1 ,...,n i , where each of these nodes have a minimal confidentiality clearance of τ.

The typing rules of our language are given in Figure 5.3. Typing judgments have the form: Γ ⊢ p : ρ where Γ is a typing environment mapping variables to variable security types from ρ. We write Γ(x) = ρ to assign to the variable x type ρ. Our typing system includes standard rules (Var, Assign, Sequence, If, While) for secure information flow control [START_REF] Volpano | A sound type system for secure flow analysis[END_REF] and special rules (Nvar, MKvar, Kvar-Assign, SBroadcast).

Γ ⊢ n : τ VAR Γ(x) = τ var Γ ⊢ x : τ var NVAR Γ(n) = τ Nvar(n) Γ ⊢ n : τ Nvar(n) Γ ⊢ e : τ Γ ⊢ n i : τ Nvar(n i ) i ∈ {1... j} Γ ⊢ k : τ Kvar (n 1 ...n j ) Γ ⊢ sbroadcast({n 1 , ..., n j }, k,e):τ cmd Subtyping rules BASE τ ≤ τ ′ ⊢ τ ⊆ τ ′ S-VAR Γ ⊢ x : τ var Γ ⊢ x : τ S-NVAR ⊢ τ ⊆ τ ′ Γ ⊢ τ ′ NVar(n) ⊆ τ NVar(n) CMD ⊢ τ ⊆ τ ′ Γ ⊢ τ ′ cmd ⊆ τ cmd SUBTYPE Γ ⊢ p : ρ ⊢ ρ ⊆ ρ ′ Γ ⊢ p : ρ ′
The Var rule binds the type τ var to a variable x. The MKvar rule binds the type ⊤ MKvar to master key variable k. The SBroadcast rule binds each node n i to be of type τ Nvar(n i ) and e (the message to broadcast) of type τ. Moreover, it binds the key variable k to be of type τ Kvar(n 1 ...n j ). The Kvar-Assign rule binds each node n j to be of type τ Nvar(n j ), k to be of type τ Kvar (n 1 ,...,n i ) and the master key k ′ of type ⊤ MKvar.

Notice that since the Assign rule requires x to be of type τ var, it cannot be applied to a key variable. Hence our type system not only ensures secure information flow, but it also protects the use of keys, which ensure its integrity with respect to key generation.

The remaining rules of the type system constitute the subtyping logic and are given in the lower part of Figure 5 In what follows, we display some examples and show how our type system can type secure programs or catch insecure ones. We consider the confidentiality lattice in Figure 5.1,

where

L ≤ M 1 ≤ H and L ≤ M 2 ≤ H.
Example 12. We consider a server willing to send a message m: Γ(m) = M 1 var to a set of nodes in {n 0 , n 1 } such that Γ(n 0 ) = M 1 NVar(n 0 ) and Γ(n 1 ) = HN Va r (n 1 ) . We also consider a master key k ′ : Γ(k ′ ) = ⊤ MKVar and a key k: Γ(k) = M 1 KVar(n 0 , n 1 ).

We show that the following program p is typable in Γ:

k := KG({n 0 , n 1 }, m,k ′ ); sbroadcast({n 0 , n 1 }, k,m)
This program consists of a sequence of two programs p 1 and p 2 . To type p 1 , we apply the KVar-Assign rule. This rule checks (a) the type of nodes n 0 and n 1 , (b) the type of the master key k ′ , and (c) the type of the encryption key k for nodes n 0 and n 1 such that Γ(k) = M 1 KVar(n 0 , n 1 ). In (a), we apply (a 1 ) the NVar rule that binds n 0 to Γ(n 0 ) = M 1 NVar(n 0 ) and (a 2 ) the subtype rule that binds n 1 to Γ(n 1 ) = M 1 NVar(n 1 ).

(a 2 )

Γ(n 1 ) = HN Va r (n 1 )

Γ ⊢ n 1 : HN Va r (n 1 ) ⊢ M 1 ⊆ H Γ ⊢ HN Va r (n 1 ) ⊆ M 1 NVar(n 1 ) Γ ⊢ n 1 : M 1 NVar(n 1 )
Since all the constraints are valid, then p 1 is typable.

To type p 2 , we apply the SBroadcast. The SBroadcast rule checks (a) the type of the message to broadcast m, (b) the type of the nodes variables n 0 , n 1 , and (c) that the type of the encryption k corresponds to the type of nodes variable. In (a), we apply the S-Var then the Var rule that bind m to Γ(m) = M 1 Var. Concerning (b), we apply the Nvar rule on nodes n 0 and n 1 that check their types ((b) for n 0 and (b ′ ) for n 1 ). In (c), the rule binds the encryption key to be of type M 1 KVar(n 0 , n 1 ).

(SBROADCAST) (a)

Γ(m) = M 1 Var Γ ⊢ m : M 1 Var Γ ⊢ m : M 1 (b) Γ(n 0 ) = M 1 NVar(n 0 ) Γ ⊢ n 0 : M 1 NVar(n 0 ) (b ′ ) Γ(n 1 ) = M 1 NVar(n 1 ) Γ ⊢ n 1 : M 1 NVar(n 1 )( c) Γ ⊢ sbroadcast({n 0 , n 1 }, k,m):M 1 cmd
Since all the constraints are valid, then p 2 is typable and the sequence p 1 ; p 2 is typable.

Example 13. In contrast with Example 12, we consider a server willing to send a message m to a set of nodes in {n 0 , n 1 } but generates a key also for a node n 2 . We show that the following program is not typable:

k := KG({n 0 , n 1 , n 2 }, k ′ ); sbroadcast({n 0 , n 1 }, k,m)
In fact, the server program contains an error in the key generation (generating key also for n 2 ), which leads to a confidentiality problem since n 2 will also be able to read a message intended to n 0 and n 1 only. Hence, such error is detected by our type system.

Example 14. In this example, we consider a server willing to send a message m: Γ(m) = Lvarto a set of nodes {n 0 , n 1 , n 2 } but does not generate a key for node n 2 . We show that the following program is not typable:

k := KG({n 0 , n 1 }, k ′ ); sbroadcast({n 0 , n 1 , n 2 }, k,m ′ )
The server program contains an error in the key generation (does not generate a key for n 2 ), which leads to a problem since n 2 will not be able to decrypt. Therefore, our type systems detects such error.

Example 15. In this example, we consider a server willing to send a message m ′ : Γ(m ′ ) = Lvarto a set of nodes {n 0 , n 1 , n 2 }. We show that the following program is not typable:

k := KG({n 0 , n 1 , n 2 }, k ′ ); m ′ := m; sbroadcast({n 0 , n 1 , n 2 }, k,m ′ )
This program consist of a sequence of three programs p 1 , p 2 and p 3 . Despite the fact that the p 1 and p 3 are typable and the broadcast in p 3 seems to be secure; p 2 is not typable since it assigns a high value M 1 var to a lower value Lv a rand therefore, the entire program is not typable. Indeed, our type system detects this error, otherwise, the broadcast may leak confidential information M 1 var to nodes with lower confidentiality clearance LNv ar (n i ), i ∈ {0, 1, 2}.

Limitations of the Type System

In this section, we show some examples to highlight on the limitations of our type system.

We consider a server willing to send a message to a set of nodes {n 0 , n 1 }. We also consider a master key k ′ : Γ(k ′ ) = ⊤ MKVar and a key k : Γ(k) = M 1 KVar(n 0 , n 1 ). For the initial configuration, we let µ(k ′ ) = 3 and µ(k) = 0. To encrypt in a correct way, the server should generate the correct keys corresponding to the intended nodes. Ideally, a type system handling cryptographic primitives should detect any violation of the hypothesis of the type system. Our type system is capable of detecting violations in some cases as in Example 16 and Example 17, but not in other cases as in Example 18.

We rely on this initial configuration to show how our system can be limited in certain cases.

Example 16.

p 1 ∆ = k := KG({n 0 , n 1 }, k ′ ); sbroadcast({n 0 , n 1 }, k,m)
The program p 1 is correct since the server first generates an encryption key for nodes n 0 and n 1 , then broadcasts a message to those nodes with the correct key. The program is typable by our type system.

Example 17.

p 2 ∆ = k := KG({n 0 , n 1 }, k ′ ); k = 0; sbroadcast({n 0 , n 1 }, k,m)
The program p 2 is wrong since the server first generates an encryption key for nodes n 0 and n 1 but then uses the key k = 0 to broadcast a message to those nodes. The server is using the wrong key to broadcast the message and therefore it cannot broadcast the message to the nodes. The program is not typable by the type system.

Example 18.

p 3 ∆ = sbroadcast({n 0 , n 1 }, k,m)
The program p 3 is wrong since the server is broadcasting a message to nodes n 0 and n 1 without generating the right keys. However, since k have type M 1 KVar(n 0 , n 1 ) in the initial configuration, our type system types this program despite the fact that the value in the initial memory is equal to zero. Unfortunately, our type system is limited in such cases since it is not able to detect such errors.

Security Properties

We define confidentiality (secure information flow between nodes of different security levels) as a new noninterference property [START_REF] Sabelfeld | Language-based information-flow security[END_REF].

We parametrize the definition by an attacker observation level, τ. For our security definition, it is useful to define an equivalence between memories. Intuitively, the definition τ -Equal memories states that two memories are equal from the view point of an attacker that can observe only parts of the memory with security level less or equal than τ.

Definition 24 (τ -Equal Memories). Two memories µ 0 , µ 1 are τ -Equal for Γ, written

µ 0 = Γ τ µ 1 , iff dom(µ 0 ) = dom(µ 1 ) ∧∀x ∈ µ 0 such that if Γ(x) = τ ′ var ∧ τ ′ ≤ τ, then µ 0 (x) = µ 1 (x).
We say that two memories µ 0 and µ 1 are τ -Equal, µ 0 = Γ τ µ 1 if they contain the same variables that have value less or equal than τ. Two memories are τ -Equal if the mapping of the same variables of the same type τ or lower have the same value in both memories. This definition considers only variables of type τ var.

For our security property, we also need to consider messages that are sent to different groups of nodes. In the semantics of server programs, messages that are broadcasted are given as traces that parametrize the semantics relation. We define a filtering function to project parts of the broadcasted messages that are sent to nodes mapped to security levels less or equal than the attacker observation level.

Definition 25 (Filtering). Let filter τ (t) = filter ′ τ (t, [])and filter

′ τ ([], t) = t. filter ′ τ (BEnc({n 1 , ..., n k }, vk,v ′ ) • t ′ , t) =        filter ′ τ (t ′ , t • ({n 1 , ..., n k }, v ′ )) if Γ(n 1 ) ⊓ Γ(n 2 )... ⊓ Γ(n k ) ≤ τ filter ′ τ (t ′ , t)

Otherwise

We are now ready to formalize secure information flow in our architecture. Intuitively this definition states that for an attacker that observes memories and messages on the network at τ, the system starting with τ -Equal memories will lead to memories which are τ -Equal. Thus, the attacker cannot distinguish the executions and will broadcast the same messages to nodes less or equal than τ in both executions.

"n 0 ", n 1 = "n1", m := 5, m ′ := 5}. Notice that the final memories µ ′ 0 and µ ′ 1 are not L-Equal since the value of m ′ is different, and filter

L (t 0 ) = [{n 0 , n 1 , n 2 }, 4] = filter L (t 1 ) = [{n 0 , n 1 , n 2 }, 5].
Therefore p is not NI Γ L .

Types for Broadcasting to Nodes with Dynamic

Security Levels

Cryptographic protocols ensure confidentiality and integrity of information in distributed systems. The security of distributed systems, in some cases, depends also on constantly updating software with patches to deal with known vulnerabilities. Software updates play a crucial role in the life-cycle management of a node in a system. Regular software update processes are needed to guarantee the appropriate functioning of a node. A secure software update process has to prevent attempts of an attacker to inject malicious code in the software update image and therefore alter the behavior of an update, and has to be confidentiality protected [IETF, 2017]. Since the same software update may be distributed to several nodes, key management and decision-making is challenging on the server side. Having different necessities and vulnerabilities, nodes on the same network require different software updates at different times. Performing distribution of software updates in a secure way is a non-trivial task. In fact, the server needs to classify nodes into subgroups in order to ensure that only the intended devices receive the appropriate software updates. Furthermore, the server needs to encrypt software updates to prevent an attacker from injecting malicious code and compromising the software image [IETF, 2017], and needs to verify which nodes successfully installed the software updates [?] to keep a record of such nodes. These requirements push the server to take decisions that not only can be error prone, but can also compromise the security of the system. Hence, verification process is required in order to ensure the correctness of the entire process of software updates.

We build on broadcast encryption schemes and remote attestation protocols to propose an architecture to securely deliver software updates in hierarchical distributed systems.

Our goal is to allow for automate decision making at the server side while preserving confidentiality and integrity of all communication. We propose a type system to control that information securely flows from the server to the nodes belonging to different security classes, and demonstrate its security via a proof with respect to a well-defined secure information flow policy for server code fitting our architecture.

An Architecture for Software Updates

We consider a scenario in which a server broadcasts messages to nodes with different levels of confidentiality. Moreover, nodes may require software updates and are also classified with integrity levels according to their installed software. Thus, the server needs to keep track of subgroups of nodes classified according to their confidentiality and integrity levels.

Remote Attestation Protocols. Remote attestation protocols [START_REF] Sailer | Attestation-based policy enforcement for remote access[END_REF][START_REF] Shaneck | Remote software-based attestation for wireless sensors. In Security and Privacy in Ad-hoc and Sensor Networks[END_REF][START_REF] Banks | Remote attestation: A literature review[END_REF] allow a sender (trusted party) to verify the integrity of a software running on a remote device. Remote attestation is performed over the network, where the sender (server) and the receiver (node) communicate directly with each other. Loading a software update to a node may not be completely trustworthy since an attacker can alter the software amid the loading process [START_REF] Francillon | Attacking and Protecting Constrained Embedded Systems from Control Flow Attacks[END_REF]. In our design, we apply a remote attestation protocol to verify the integrity of software running on a node. A common approach to implement remote attestation is a challenge-response protocol.

Security Lattices. We use a lattice L , a product of two lattices, a lattice of confidentiality levels (L C , ≤ C ) and a lattice of integrity levels (L I , ≤ I ). A confidentiality security level is written as s C and indicates a read level while an integrity security level is written as s I and indicates a write level. In the confidentiality lattice, s C ≤ C s ′ C means that s ′ C has more confidentiality than s C . In the integrity lattice, s I ≤ I s ′ I means that s I has more

HL LH HM 1 M 1 L HM 2 M 2 L M 1 M 1 M 2 M 1 LL HH M 1 M 2 M 2 M 2 M 1 H LM 1 M 2 H LM 2
Figure 5.4: A diamond lattice of security levels.

integrity than s ′ I . We write ⊥ for the lowest security level and ⊤ for the highest security level in lattice L . In Figure 5.4, we show a confidentiality and integrity security lattice.

Models and Goals

In this section, we present the system model and the security properties of the proposed architecture.

System Model. We consider a server that controls and manages a large set of networked nodes in a distributed system. The server aims to communicate securely with nodes belonging to privileged subgroups and maps subgroups of nodes into security classes. Subsequently, the server remote attest nodes and moves them to higher integrity security levels whenever the verification of the installed software update succeeds.

Attacker Model. We assume that an attacker manipulates the communication network that the server uses to communicate with nodes. An attacker can modify and inject messages over the network, or can mount man-in-the-middle attacks [START_REF] Conti | A survey of man in the middle attacks[END_REF] or replay attacks [START_REF] Syverson | A taxonomy of replay attacks[END_REF]. We also assume that an attacker can exploit software vulnerabilities and load malicious content to nodes. Finally, an attacker can access public information without being able to inhibit communications between a server and the nodes during an update nor make the nodes unavailable (e.g. resource exhaustion) [START_REF] Zandberg | Secure firmware updates for constrained iot devices using open standards: A reality check[END_REF].

Security Properties. The security properties needed for our architecture are the following:

• Security level integrity. The system guarantees that each node increases its integrity level after that a successful software update is attested. Moreover, a node at an integrity level cannot be tricked by the attacker to install an old software update.

In our architecture, this is ensured via the protection of variables mapping security classes to nodes in the server and via a counter that is incremented with each communicated message to avoid replay attacks.

• Secure communication. A server communicates with a specific node with confidentiality, integrity, and freshness guarantees. Confidentiality and non-malleability of the ciphertexts are ensured via the use of a IND-CCA [START_REF] Rackoff | Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack[END_REF] BES, the correct usage of cryptographic keys on the server for nodes at a given security level; and integrity is ensured via the use of remote attestation protocols, the fact that only the servers can broadcast messages, and a protocol for security level integrity.

• Secure information flow. Information intended to more privileged security levels cannot flow into less privileged security levels. For confidentiality, messages with higher confidentiality clearances cannot be read by nodes with lower confidentiality clearances. As for integrity, software versions are mapped to integrity levels and nodes only receive software updates from the server corresponding to their integrity level. Secure information flow is guaranteed through a type system on the server code.

Syntax

In what follows, we consider the server language described below. It consists of programs, which can be expressions e or commands c. We let x, K, L, pc range over variables and v ranges over strings, integers and Boolean literals. We distinguish special variables {L 1 , L 2 , L 3 , ...} to designate groups of nodes in a broadcast command. In our server language, we use special variable L to keeps set of nodes identifiers belonging to a common security level, K for cryptographic keys, and pc for counters. We use • to compute basic arithmetic and Boolean operations.

Commands include standard statements (assign, sequence, if, while) and special statements (Sbroadcast, Endorse Ra). We only highlight on the special statements and we refer the reader to see Subsection 5.1.2 for the standard statements.

• The Endorse Ra statement for n ∈ LendorseRa(L,L ′ , n) iterates over every node n ∈ L to run a remote attestation protocol to decide whether to move n to another set of nodes L ′ (representing a more privileged security level) and remove it from L if the verification succeeds, or leave it in the same security level L if the verification fails.

• In the Sbroadcast statement sbroadcast(L,e,K), the server uses a broadcast encryption scheme to communicate a message e ′ to a set of nodes (designated by variable L) using a key K.

Semantics

A program is related to a memory µ which is a finite function that maps variables into values. We write µ[x := v] for the memory that assigns value v to a variable x.

The semantics allows us to derive judgments of the form µ ⊢ e ⇒ v for expressions and µ ⊢ c ⇒ t µ ′ for commands. These judgments affirm that evaluating expressions e in memory µ results in literal v. Evaluating command c in memory µ results in a new memory µ ′ with t being a side effect that represents the command sends a message to the network. The semantics rules are given in Figure 5.5.

We only highlight on the Secure Broadcast rule and the Endorse-Ra rule. We refer the reader to see Subsection 5.1.3 for the other rules.

• In the Secure Broadcast rule, the server applies a key generation algorithm that takes in input a set of nodes {"n 1 ", "n 2 ", ..., "n n "} ∈ L, the evaluation v ′ of K in µ and outputs a keys vk, sk: Key generation({"n 1 ", "n 2 ", ..., "n n "}, v ′ ). To broadcast a message, the server employs a broadcast encryption scheme. We model the ciphertext that goes to the network by the annotation BEnc(L,vk,"m"||"v").

• In the Endorse-Ra rule, for each node stored in the memory of variable L, the server applies a remote attestation protocol. If the remote attestation succeeds, it outputs a set of nodes S. This set of nodes is then moved into L ′ which represents a more privileged security level than L.

Typing Rules

The types of the language are stratified as follows. • Type τ var is the type of a variable.

• Type τ cmd is the type of a command.

• Type τ Lvar is the type for the security levels variables L.

• Type ⊤ Kvar is the type of keys variables K. Keys are placed in the top of the lattice with the highest confidentiality as only the server possesses the keys.

• The type ⊥ Cvar designates the type of counters. Counters are used to enforce the integrity of our protocol. For that, they are placed in the bottom of the lattice with the highest integrity and the lowest confidentiality as only the server can increment the value of pc and everyone can read it.

The typing rules of our language are given in Figure 5.6. Typing judgments have the form: Γ ⊢ p : ρ where Γ is a typing environment mapping variables to variable security types from ρ. We write Γ(x) = ρ to assign to the variable x type ρ.

Our typing system includes standard rules (Var, Assign, Sequence, If, While) for secure information flow control [START_REF] Volpano | A sound type system for secure flow analysis[END_REF] and special rules (Lvar, Kvar, Assign-Counter, SBroadcast, Remote Attestation). • The LVar rule binds the type τ Lvar to security levels variable L.

REMOTE ATTESTATION

Γ ⊢ L : τ Lvar Γ ⊢ L ′ : τ ′ Lvar I(τ ′ ) ≤ I I(τ) C(τ) ≤ C C(τ ′ ) Γ ⊢ for n ∈ LendorseRa(L,L ′ , n):τ cmd Subtyping rules BASE τ ≤ τ ′ ⊢ τ ⊆ τ ′ S-VAR Γ ⊢ x : τ var Γ ⊢ x : τ S-CVAR Γ ⊢ pc : ⊥ Cvar Γ ⊢ pc : ⊥ CMD ⊢ τ ⊆ τ ′ ⊢ τ ′ cmd ⊆ τ cmd SUBTYPE Γ ⊢ p : ρ ⊢ ρ ⊆ ρ ′ Γ ⊢ p : ρ ′
• The KVar rule binds the type ⊤ Kvar keys variable K.

• The Op rule binds e and e ′ to be of type τ.

• The Assign rule says that, in order to ensure a secure flow from e ′ to x, e ′ and

x must agree on their security levels, which is conveyed by τ appearing in both hypotheses of the rule.

• The Assign-Counter rule binds pc to be of type ⊥ CV ar since only the server can write this variable and everyone can read it. Notice that since the Assign rule requires x to be of type τ var, it cannot be applied to a variable of type ⊥ Cvar.

Thus, for a program with an assignment to pc to be typable, such assignment can be only of the shape pc := pc + 1. This restricts the use of ⊥ Cvar variable in a program. Hence our type system not only ensures secure information flow (see Section 5.4), but it also protects the use of counters, which ensure secure level integrity.

• The Sequence rule says that, in order to execute c then c ′ , both c and c ′ must agree on the same type of command τ cmd.

• The If rule says that, in order to execute the if command, e, c and c ′ must agree on their security levels τ.

• The While rule says that, in order to execute the while command, e and c and c ′ must agree on their security levels τ.

• The SBroadcast rule binds L to be of type τ Lvar and e ′ (the message to broadcast) of type τ. Moreover, it binds the keys variable K to be of type ⊤ Kvar and the counter variable of type ⊥ Cvar. A broadcast program is well-typed if the type of the message e ′ is ≤ than the type of L to secure the flow of information and avoid that lower security levels receive higher security level messages.

• The Remote Attestation rule requires L to be of type τ Lvar and L ′ of type τ ′ Lvar where τ ≤ τ ′ . Furthermore, it checks if I(τ ′ ) ≤ I I(τ) and C(τ) ≤ C C(τ ′ ). This means that in order to move a node from L to L ′ , L ′ should have higher integrity level and at least the same confidentiality level.

The remaining rules of the type system constitute the subtyping logic and are given in the lower part of Figure 5.6.

• The Base rule states that τ is a subset of τ ′ if τ ≤ τ ′ .

• The Cmd rule states that τ ′ cmd is a subset of τ cmd if τ is a subset of τ ′ .

• The Subtype rule states that a program p of type ρ can be bound to type ρ ′ if ρ is a subset of ρ ′ .

• The S-Var rule states that a variable x of type τ var can be bound to type τ.

• The S-Cvar rule states that a counter variable of type ⊥ Cvar is bound to type ⊥.

In what follows, we display some examples and show how our type system can type secure programs or catch insecure ones. We consider the confidentiality lattice in Example 21. We consider the diamond lattice in Figure 5. We show that the following program p is typable:

pc := pc+ 1; sbroadcast(L HM 2 , SU M 1 M 2 ||pc, K); for n ∈ L HM 2 endorse Ra(L HM 2 , L HH , n)
This program consists of a sequence of three programs p 1 , p 2 and p 3 .

• In p 1 we apply the rule Assign-Counter that binds the type of pc to be ⊥ Cvar.

Finally, we apply the Subtype rule on p 2 to bind it to type HH cmd:

(SBROADCAST) (CMD) HH ≤ HM 2 ⊢ HH ⊆ HM 2 (BASE) ⊢ HM 2 cmd ⊆ HH cmd Γ ⊢ sbroadcast(L HM 2 , SU M 1 M 2 ||pc, K):HH cmd (SUBTYPE)
Therefore, p 2 is typable. Example 22. We consider the diamond lattice in Figure 5.4, in which LH ≤ HH where L ≤ C H which means that L has less confidentiality than H. In this example, we consider a server willing to send a message x of type LH var to a set of nodes in L LH . We also consider a variable y of type HH var, a counter, pc of type ⊥ Cvar, and a key, K of type ⊤ Kvar. We show that the following program p is not typable:

pc := pc+ 1;x LH := y HH ; sbroadcast(L LH , x LH ||pc, K)
The program p consists of a sequence of three programs p 1 , p 2 and p 3 .

• In p 1 we apply the rule Assign-Counter that binds the type of pc to be ⊥ Cvar. We apply the Assign rule on p and we immediately observe that it is not typable because the Assign rule binds the first element of the assignment to be of type LH var.

Γ ⊢ pc : ⊥ Cvar Γ ⊢ pc := pc+ 1 : ⊥ cmd (ASSIGN-COUNTER)
Γ ⊢ L LH : τ var Γ ⊢ x HH : τ Γ ⊢ L LH := x HH : τ cmd (ASSIGN)
Since L LH is of type LH Lvar and since there are no rules in our type system that allow a variable of type τ Lvar to be typed as τ var, our type system catches this wrong flow of information and accordingly p is not typable.

Security Properties

We define confidentiality and integrity of secure information flow between nodes of different security levels as a new noninterference property [START_REF] Sabelfeld | Language-based information-flow security[END_REF].

We parametrize the definition by an attacker observation level, τ. For our security definition, it is useful to recall the definition of equivalence between memories from Definition 24 in Subsection 5.1.5.

We also define a filtering function in the purpose of projecting parts of the broadcasted messages sent to nodes mapped to security levels less or equal than the attacker observation level.

Definition 27 (Filtering). Let filter τ (t) = filter ′ τ (t, [])and filter

′ τ ([], t) = t. filter ′ τ (BEnc(L, vk,v ′ ||v) • t ′ , t) =        filter ′ τ (t ′ , t • (L, v ′ ) if Γ(L) ≤ τ filter ′ τ (t ′ , t)

Otherwise

Our main result follows: a well-typed program is noninterferent at τ for Γ.

Theorem 3. Let Γ be a typing environment and τ ∈ L a security label. If Γ ⊢ p then p is

NI Γ τ .
We prove this theorem by induction on the height of the typing derivation tree of

Γ ⊢ p in Appendix B.
Example 24. Concerning the security property, we show that the program p of Example 21 is noninterferent at HM 2 . Let two memories µ 0 and µ 1 :

µ 0 pc := 1 K := vk ′ 1 L HH := {"n 0 "} L HM 2 := {"n 1 ", "n 2 "} SU M 1 M 2 := v 2 µ 1 pc := 2 K := vk ′ 3 L HH := {"n 0 "} L HM 2 := {"n 1 ", "n 2 "} SU M 1 M 2 := v 2 Notice that µ 0 = Γ HM 2 µ 1 : By Definition 24, µ 0 = Γ HM 2
µ 1 since only variables of type τ var (in our example SU M 1 M 2 ) should be equal.

The resulting two memories µ ′ 0 and µ ′ 1 are:

µ ′ 0 pc := 2 K := vk ′ 1 L HH := {"n 0 ", "n 2 "} L HM 2 := {"n 1 "} SU M 1 M 2 := v 2 µ ′ 1 pc := 3 K := vk ′ 3 L HH := {"n 0 ", "n 2 "} L HM 2 := {"n 1 "} SU M 1 M 2 := v 2
After executing p, the value of SU M 1 M 2 does not change in the resulting memories.

Since only variables of type τ var are considered, then µ ′ 0 = Γ HM 2 µ ′ 1 . In order to satisfy the full hypothesis in Definition 27, we need to prove that filter HM 2 (t 0 ) = filter HM 2 (t 1 ). Actually, t 0 and t 1 are the traces of the messages broadcasted over the network through the Secure Broadcast rule in Figure 5.5: BEnc(L,K,SU||pc).

• For an execution that starts with µ 0 , t

0 = BEnc(L HM 2 , v ′ 1 , v 2 ||1), thus filter HM 2 (t 0 ) = [L HM 2 , v 2 ]. filter HM 2 (t 0 ) = filter ′ HM 2 (t 0 , [ ]) = filter ′ HM 2 (BEnc(L HM 2 , v ′ 1 , v 2 ||1) • [], [ ]) = filter ′ HM 2 ([ ], []• (L HM 2 , v 2 )) = [L HM 2 , v 2 ]
• For an execution that starts with µ 1 , t

1 = BEnc(L HM 2 , v ′ 3 , v 2 ||2), thus filter HM 2 (t 1 ) = [L HM 2 , v 2 ]. filter HM 2 (t 1 ) = filter ′ HM 2 (t 1 , [ ]) = filter ′ HM 2 (BEnc(L HM 2 , v ′ 3 , v 2 ||2) = filter ′ HM 2 ([ ], []• (L HM 2 , v 2 )) = [L HM 2 , v 2 ]
Hence, filter HM 2 (t 0 ) = filter HM 2 (t 1 ) and p is NI Γ x HH := 4 The resulting memories are also LH-Equal. Since p is an assignment command, there are no messages broadcasted over the network, and therefore the traces are empty. Thus, filter(t 0 ) = filter(t 1 ) and p is NI Γ LH despite the fact that p is not typable.

Related Work

Confidentiality vs. integrity. The fundamental purpose of controlling information flow is to provide confidentiality and integrity properties of code running on computers.

Concerning confidentiality, sensitive or secret data should be prevented from flowing to public targets, and jointly, concerning integrity, untrusted data should be prevented from flowing or affecting trusted outputs [START_REF] Sabelfeld | Language-based information-flow security[END_REF][START_REF] Li | Information integrity policies[END_REF][START_REF] Biba | Integrity considerations for secure computer systems[END_REF]]. An information flow policy can be defined through a security lattice [START_REF] Denning | Certification of programs for secure information flow[END_REF], that classifies and labels the data. A security lattice can represent confidentiality, integrity, and the combination of both. In a confidentiality lattice, data is labeled as high (for secret) and low (for public), where an attacker is assumed to observe the data labeled as low and information can only flow from low to high. In an integrity lattice, data is labeled as trusted and untrusted, where an attacker is assumed to control the data labeled as untrusted and information from untrusted data does not affect trusted data (information can flow from trusted to untrusted). In a confidentiality and integrity lattice, namely product lattice, data is labeled with a confidentiality and integrity levels.

Information can only flow from public and trusted data to secret and untrusted data. [START_REF] Denning | Certification of programs for secure information flow[END_REF][START_REF] Sabelfeld | Language-based information-flow security[END_REF], Banerjee and Naumann, 2002a] mainly focus on controlling the leak of information from secret data to public data through a program. Particularly, secure information flow can protect the confidentiality and integrity of data flows. Goguen et. al [START_REF] Goguen | Security policies and security models[END_REF] first introduced noninterference in the form of simulation relations in the intent of formalizing information flow policies. By employing static enforcement through a type system, Volpano and Smith proved that the latter ensures noninterference [START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. Afterwards, several researchers have proposed type systems for secure information flow [START_REF] Smith | A new type system for secure information flow[END_REF][START_REF] Fournet | Cryptographically sound implementations for typed information-flow security[END_REF][START_REF] Fournet | A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms[END_REF][START_REF] Fournet | Information-flow types for homomorphic encryptions[END_REF][START_REF] Magazinius | A lattice-based approach to mashup security[END_REF][START_REF] Bastys | Prudent design principles for information flow control[END_REF][START_REF] Sabelfeld | Probabilistic noninterference for multi-threaded programs[END_REF][START_REF] Banerjee | Secure information flow and pointer confinement in a java-like language[END_REF][START_REF] Barthe | Deriving an information flow checker and certifying compiler for java[END_REF]. In fact, to prevent insecure flows, one may use static information flow enforcement [START_REF] Volpano | A sound type system for secure flow analysis[END_REF] or dynamic enforcement [Askarov andSabelfeld, 2009, Bielova and[START_REF] Bielova | A taxonomy of information flow monitors[END_REF]. In our work, we choose to apply an static mechanism to enforce secure information flow through a type system. In the literature of secure information flow, several works consider combining cryptography to information flow [START_REF] Laud | Semantics and program analysis of computationally secure information flow[END_REF][START_REF] Askarov | Cryptographic enforcement of language-based information erasure[END_REF][START_REF] Gregersen | A dependently typed library for static information-flow control in idris[END_REF][START_REF] Fournet | Cryptographically sound implementations for typed information-flow security[END_REF][START_REF] Fournet | A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms[END_REF][START_REF] Fournet | Information-flow types for homomorphic encryptions[END_REF] including our work. None of these works consider the association of security classes to subgroups of nodes in distributed systems and combine them with BES.

Secure information flow. Information flow policies

Moreover, none of these works except [START_REF] Fournet | Cryptographically sound implementations for typed information-flow security[END_REF] consider endorsement of integrity: while they obtain endorsement via cryptographic signatures, we obtain the endorsement through remote attestation. In our configuration, we enforce the integrity of communications by employing remote attestation protocols. The goal is to verify that nodes has successfully installed software updates, and therefore are moved to higher integrity security levels. By doing that, the server can identify which nodes necessitate software updates and the system can avoid leaking information to nodes placed in lower security levels.

Conclusion

We propose two architectures to securely deliver messages (and software updates) in hierarchical distributed systems relying on broadcast encryption schemes (and remote attestation). By associating broadcast encryption keys to security classes, we pave the way to enforcement of secure information flow between server and nodes. We demonstrate this by building two type systems for server code. In the first type system, nodes are associated to static security levels and in the second type system, nodes are associated to dynamic security levels, which is an appropriate scenario for delivering software updates. We also prove the soundness of the two type systems with respect to a new secure information flow property. While the first property preserves only confidentiality, the second property preserves both confidentiality and integrity of secure information flow. To the best of our knowledge, we are the first to propose the association of security classes to cryptographic keys in BES and the employment of remote attestation in order to verify secure information flow. Our current results are mainly theoretical, but being based on known bricks such as broadcast encryption schemes and remote attestation an implementation is feasible. We leave the experimental evaluation of our results as future work.

C HAPTER 6

CONCLUSION

In this thesis, we investigate the security of encryption schemes. First, we focus our study on the security properties that the ElGamal encryption scheme relies on. ElGamal encryption scheme is semantically secure on top of groups that comply with the Decisional Diffie-Hellman (DDH) assumption. Specifically, it is IND-CPA over safe prime order groups (in a safe prime order group, the DDH assumption is respected). We inspect ElGamal encryption scheme libraries in order to identify which implementations respect the DDH assumption. From the analysis of the implementations, we identify and compare four message encoding and decoding techniques that satisfy the aforementioned assumption.

Since the DDH assumption applies also to other cryptographic constructions, we investigate broadcast encryption schemes and discuss their security aspect. We propose a new broadcast encryption scheme based on ElGamal that enjoys constant size ciphertext and key storage. We implement three different broadcast encryption schemes in Ocaml, and compare them in means of execution time and ciphertext and key space. It turns out that the our scheme is faster than the other compared schemes offering constant time encryption and decryption even for a large set of nodes. Comparing to Boneh-Franklin scheme and ElGamal Baseline, the new scheme shows significant advantage in terms of execution time, ciphertext space and key storage.

Because broadcast encryption schemes involve communication with a large set of nodes, we consider scenarios that employ broadcast encryption schemes to securely communicate with nodes. We propose an architecture to deliver messages to nodes with static security levels, and we extend it to a more complex architecture to deliver software updates to nodes with dynamic security levels. We associate broadcast encryption keys to security classes to enforce secure information flow between server and nodes, in particular, to preserve the confidentiality and integrity of communication. To demonstrate our idea, we build two type systems (one for each architecture) and prove their soundness with respect to a new secure information flow property that preserves confidentiality and integrity of information.

In what follows, we detail some perspective for future work, building on the work presented so far.

Security of Implementations and elliptic curves. An interesting study related to our work is to analyze and study implementations of ElGamal over elliptic curves. Since we focus our analysis on message encoding over cyclic subgroups of Z * p , it is possible to extend it and examine in detail how encodings are implemented using the elliptic curves cryptography [START_REF] Koblitz | The state of elliptic curve cryptography[END_REF]. Another extension regarding this topic is to black-box test applications that employ ElGamal encryption scheme through Hardware Security Modules [START_REF] Volkamer | Evaluation of Electronic Voting[END_REF].

Security of broadcast encryption schemes.

In this thesis, we propose a broadcast encryption scheme based on ElGamal and implement it over prime order groups. In the short term, we plan to prove that this scheme is IND-CPA using the Easycrypt tool [START_REF] Barthe | Easycrypt: A tutorial[END_REF]. We conjecture that this proof is closely related to the proof of ElGamal [START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF] combined with the higher order residuosity hypothesis used in the proof of the Paillier Encryption scheme [START_REF] Paillier | Public-key cryptosystems based on composite degree residuosity classes[END_REF]. As a second line of future work, we would like to adapt the scheme to elliptic curve cryptography to seek optimization in terms of speed, memory space, and small key sizes. Since elliptic curve cryptography offers the same security level while adopting smaller keys, it is interesting to implement the schemes evaluated in Chapter 4 to compare results and draw conclusions on the benefit of employing elliptic curves cryptography for secure broadcasting. Considering the comparison done with the Boneh-Franklin scheme, we plan to further investigate traitor-tracing schemes as they offer an efficient and secure way to detect malicious nodes in the system and find an optimized way (in term of speed and memory) to integrate traitor-tracing approaches to our scheme.

Real life applications of the proposed architecture and type systems. Considering that the proposed architectures are based on well-known notions as broadcast encryption schemes and remote attestation, and since they are supported by to type systems for enforcing secure information flows, our aim is to provide an implementation of our type systems (i.e. in Hop.js [START_REF] Serrano | A glimpse of hopjs[END_REF]) for real life applications. By the semantics rule Update, we have that:

(H 12 ) t = [].
For (H 2 ), we have that τ ′ ≤ τ. Since the only variable in which µ and µ ′ are different is k by (H 11 ) and the type of k is τ ′ Kvar(n 1 ..., n i ) by (H 5 ), we can conclude that µ = Γ τ µ ′ which is (G 1 ).

To prove (G 2 ), by (H 12 ), t = []. Therefore filter τ (t) = [], which is (G 2 ) Subcase 1.3 (SBroadcast: sbroadcast({n 1 , ..., n j }, k,e)). By the hypothesis of the lemma, we have that:

(H 4 ) Γ ⊢ sbroadcast({n 1 , ..., n j }, k,e):τ ′ cmd.

By (H 4 ) and the typing rule SBroadcast, we have that:

(H 5 ) Γ ⊢ e : τ ′ .

(H 6 ) Γ ⊢ n i : τ Nvar(n i ).

(H 7 ) Γ ⊢ k : τ Kvar (n 1 ...n j ).

By (H 3 ) and the semantics rule Secure Broadcast, we have that:

(H 8 ) µ ⊢ sbroadcast({n 1 , ..., n j }, k,e) ⇒ t µ.

By the semantics rule Secure Broadcast, we have that:

(H 9 ) t = BEnc({n 1 , ..., n k }, vk,v ′ ).

(H 3 ) t i = [].
Hence, by the semantics rule Update and (H 2 ), we have that:

(H 4 ) µ i ⊢ e ′ ⇒ v i . (H 5 ) µ ′ i = µ i [x := v i ].
By the hypothesis of Theorem 2, we have:

(H 6 ) Γ ⊢ x := e ′ : τ ′ cmd.

By (H 6 ) and the typing rule Assign, we have that:

(H 7 ) Γ ⊢ x : τ ′ var.

(H 8 ) Γ ⊢ e ′ : τ ′ .

By (H 7 ) and the typing rule Var, we have:

(H 9 ) Γ(x) = τ ′ var.

Depending on τ ′ , we have two cases:

(H 10 ) τ ′ ≤ τ.
By Lemma 1 that can be applied due to (H 1 ), (H 8 ), (H 10 ) and (H 4 ) then (H 11 ): v 0 = v 1 .

To prove (G 1 ), we rely on the Definition 24 that states that µ 0 = Γ τ µ 1 , if ∀x ∈ µ 0 such that Γ(x) = τ ′ var and τ ′ ≤ τ then µ 0 (x) = µ 1 (x).

Since (H 1 ) holds and the only variable in which µ i and µ ′ i are different is x by (H 5 ), then we need to prove that µ 0 (x) = µ 1 (x) which holds by (H 11 ).

To prove (G 2 ) we rely on the Definition 25 and (H 3 ). Since t 0 = t 1 = []then filter τ (t 0 ) = filter τ (t 1 ).

Since we proved (G 1 ) and (G 2 ), then p is NI Γ τ .

To prove (G 1 ), we rely on the Definition 24 that states that µ 0 = Γ τ µ 1 , if ∀y ∈ µ 0 such that Γ(y) = τ ′ var and τ ′ ≤ τ then µ 0 (y) = µ 1 (y). For (H 7 ), Γ(k) = τ ′ Kvar(n 1 , ..., n i ). Since we are only interested in variables of type τ ′ var, we conclude by (H 5 ) and (H 1 ) that

µ ′ 0 = Γ τ µ ′ 1 .
To prove (G 2 ) we rely on the Definition 25 and (H 3 ). Since t 0 = t 1 = []then filter τ (t 0 ) = filter τ (t 1 ).

Since we proved (G 1 ) and (G 2 ), then p is NI Γ τ .

Subcase 1.3. p ∆ = sbroadcast({n 1 , ..., n j }, k,e).

Concerning (G 1 ) and (G 2 ), by Definition 26, we have that:

(H 1 ) µ 0 = Γ τ µ 1 .

(H 2 ) µ i ⊢ sbroadcast({n 1 , ..., n j }, k,e) ⇒ t i µ i .

By the semantics rule Secure Broadcast, we have: (H 3 ) t i = BEnc({n 1 , ..., n k }, vk,v ′ ).

(H 4 ) µ i ⊢ k ⇒ vk i .

(H 5 ) µ i ⊢ e ⇒ "m i ".

By the hypothesis of Theorem 2, we have:

(H 6 ) Γ ⊢ sbroadcast({n 1 , ..., n j }, k,e):τ ′ cmd.

By (H 6 ) and the typing rule SBroadcast, we have:

(H 7 ) Γ ⊢ e : τ ′ .
(H 8 ) Γ ⊢ n i : τ Nvar(n i ).

(H 9 ) Γ ⊢ K : τ Kvar(n 1 , ..., n j ).

To prove (G 1 ), we rely on the Definition 24 that states that µ 0 = Γ τ µ 1 , if ∀y ∈ µ 0 such that Γ(y) = τ ′ var and τ ′ ≤ τ then µ 0 (y) = µ 1 (y). For (H 7 -H 9 ), all the variables types are

• By (H ′ 1 ) we have that (1) µ 0 = Γ τ µ 1 .

• By Lemma 2 we have that (2) µ 0 = Γ τ µ ′ 0 and (3) µ 1 = Γ τ µ ′ 1 .

• By ( 1) and ( 2) we have that ( 4) µ 1 = Γ τ µ ′ 0 .

• By ( 1) and ( 3) we have that ( 5) µ 0 = Γ τ µ ′ 1 .

• By ( 4) and ( 5) we conclude that ( 6)

µ ′ 0 = Γ τ µ ′ 1 .
By applying structural induction, we have that filter τ (t ′ 0 ) = filter τ (t For the typing rule If, we have that:

(H 1 ) Γ ⊢ e : τ ′ .

(H 2 ) Γ ⊢ c ′ : τ ′ cmd.

(H 3 ) Γ ⊢ c ′′ : τ ′ cmd.

For the semantics rule Branch, we have that:

(H 4 ) µ i ⊢ e ⇒ v i . (H 5 ) µ i ⊢ c ′ ⇒ t i µ ′ i . (H 6 ) µ i ⊢ c ′′ ⇒ t i µ ′ i .
Concerning c ′ , by induction, we conclude that:

(H 7 ) µ ′ c ′ 0 = Γ τ µ ′ c ′ 1 .
(H 8 ) filter τ (t 0 ) = filter τ (t 1 ).

(H 8 ) Γ ⊢ if e then c ′ else c ′′ : τ ′ cmd.

(H 9 ) µ ⊢ if e then c ′ else c ′′ ⇒ t µ ′ .

(H 10 ) µ ⊢ if e then c ′ else c ′′ ⇒ t µ ′ .

(H 11 ) τ ′ ≤ τ.

Then we want to prove that:

(G 1 ) µ = Γ τ µ ′ . (G 2 ) filter τ (t) = [].
By the semantics rule of Branch-True, we have that:

(H 12 ) µ ⊢ e ⇒ v.
(H 13 ) µ ⊢ c ′ ⇒ t µ ′ .

(H 14 ) t = [].

By (H 3 ) and (H 4 ) we can conclude that µ = Γ τ µ ′ . By (H 5 ) and (H 14 ) we conclude that

filter τ (t) = [].
By the semantics rule of Branch-False, we have that:

(H 15 ) µ ⊢ e ⇒ v. (H 16 ) µ ⊢ c ′′ ⇒ t µ ′ . (H 17 ) t = [].
By (H 3 ) and (H 5 ) we can conclude that µ = Γ τ µ ′ . By (H 6 ) and (H 17 ) we conclude that

filter τ (t) = [].
■

  Cette thèse propose l'utilisation de schémas de chiffrement prouvables pour obtenir la sécurité de bout en bout de systèmes distribués. Nous analysons d'abord les conditions suffisantes d'un schéma de cryptage prouvable utilisé dans les systèmes de vote et découvrons plusieurs incohérences dans la satisfaction de ces hypothèses dans les implémentations du schéma de cryptage ElGamal. Nous proposons et comparons différentes méthodes pour obtenir des implémentations indiscernables d'attaques en texte clair choisies. Nous étudions également les schémas de cryptage de diffusion et proposons un nouveau schéma basé sur ElGamal. Nous mettons en oeuvre et comparons différents schémas de cryptage par diffusion en fonction de temps d'exécution et d'espace mémoire. De plus, nous considérons des scénarios basés sur des schémas de cryptage de diffusion pour délivrer de manière sécurisée des messages dans des systèmes distribués hiérarchiques. Nous étendons ces scénarios à une architecture plus complexe où des mises à jour logicielles sont nécessaires, en combinant des schémas de cryptage par diffusion et des protocoles d'attestation à distance. Pour exprimer différents niveaux de confidentialité et d'intégrité, nous utilisons des classes de sécurité présentant un ordre entre elles.

Figure 2 . 1 :

 21 Figure 2.1: Generator of multiplicative group Z * 11

Definition 10 .

 10 (Decisional Diffie-Hellman (DDH)) Given two distributions D 1 and D 2 ,

  to build RSA. In what follows we define the integer factorization problem, then the RSA modulus and the safe RSA modulus used in the factorization problem. Definition 12. (RSA Modulus) An RSA modulus is an integer N = p • q, where p and q are two distinct prime numbers. Definition 13. (Euler Phi Function φ(N)) φ(N) is the number of non-negative integers less than N that are relatively prime to N. Definition 14. (e th Root Problem) Let N be an RSA modulus, y ∈ Z * N , and e ≥ 3 a prime integer with gcd(e, φ(N)) = 1. The e th root problem is then to find x ∈ Z * N , such that y = x e mod N. The difficulty of the RSA problem depends on the difficulty of the integer factorization problem. Definition 15. (Integer factorization problem) Given a positive RSA modulus N, compute its decomposition into prime numbers N = p i e i (unique up to reordering).

  chosen-plaintext attacks (IND-CPA). Indistinguishability against chosen-plaintext attacks (IND-CPA) for asymmetric key encryption schemes is defined by a game between a polynomial time adversary and a challenger. The adversary selects two plaintexts of his choice and sends them to the challenger, who randomly selects one of the two plaintexts, encrypts it and sends the challenge ciphertext back to the adversary. The goal of the adversary is to find out which of the two plaintexts has been encrypted by the challenger. Definition 18 (IND-CPA). An encryption scheme is said to be IND-CPA secure if the advantage of any efficient adversary is a negligible function of the security parameter, i.e., the adversary cannot do much better than a blind guess. Algorithm IND-CPA Game 1: The challenger generates an encryption key pk and a decryption key sk. Only the encryption key is public. 2: The adversary outputs a pair of messages (m 0 , m 1 ) of equal length. 3: The challenger randomly selects a bit b ∈ {0, 1}, and send the challenge ciphertext c = Enc(pk, m b ). 4: The adversary outputs his guess b ′ of the value of b. 5: If b = b ′ , the adversary wins the game.

  |Pr

  chosen-ciphertext attacks (IND-CCA). Indistinguishability against chosen-ciphertext attacks (IND-CCA) is similar to IND-CPA, with the only difference that an adversary possesses access to a decryption oracle (instead of an encryption oracle in IND-CPA) to decrypt ciphertexts chosen by the adversary. The adversary selects two plaintexts of his choice and sends them to the challenger, who randomly selects one of the two plaintexts, encrypts it and sends the challenge ciphertext back to the adversary. The goal of the adversary is to find out which of the two plaintexts has been encrypted by the challenger. Note that the adversary cannot query the decryption oracle to decrypt ciphertexts after receiving the target ciphertext (in the case of IND-CCA) nor to decrypt the received ciphertext by the challenger (in the case of IND-CCA2). Algorithm IND-CCA Game 1: The challenger generates an encryption key pk and a decryption key sk. Only the encryption key is public. 2: The adversary outputs a pair of messages (m 0 , m 1 ) of equal length. 3: The challenger randomly selects a bit b ∈ {0, 1}, and send the challenge ciphertext c = Enc(pk, m b ). 4: The adversary outputs his guess b ′ of the value of b. 5: If b = b ′ , the adversary wins the game.

  ators to generate subgroups in which the DDH assumption holds. Finally, we analyze the message encoding techniques deployed to map the messages into the before-mentioned subgroups. This study led us to notice that a large number of the considered libraries are not IND-CPA secure as the encryption may leak at least one bit of information on the plaintext: 20 libraries do not respect the DDH assumption. Moreover, among these 20 libraries, 10 do not use a safe prime. In what follows, we describe in details the problems found in the investigated libraries using the following classification:(A) Libraries that do not respect the DDH assumption. There are 20 libraries in this category. In this class we further classify the libraries that do not respect the DDH assumption due to 3 different concerns: libraries that do not deploy a safe prime, libraries that do not adopt a quadratic residue generator, and libraries that do not use a correct message encoding technique to map the messages into the intended subgroup.

  type factor = elt partial_decryption let eg_factor x {alpha; _} = let zkp = "decrypt|" ^G.to_string (g ** ~x) ^"|" in alpha ** ~x, fs_prove [| g; alpha |] x (hash zkp) let check_ciphertext c = Shape.forall (fun {alpha; beta} -> G.check alpha && G.check beta) c

  which can be trivially satisfied. ■ After decryption, one obtains m by calculating its modular square root: m = c q+1 2 [Nishihara et al., 2009]. The algorithm computes the square root of c iff p ≡ 3 mod 4, which is

  let decrypt gr sk (u,v) = let mult = Z.mul (Z.pred (q gr)) sk in let modulo = Z.powm u mult gr.p in let dec = mulm gr v modulo in decode gr dec Listing 3.10: Our Ocaml implementation for a message decryption. • Let r = m q+1 2 mod p. To decode a decrypted message, we check if m ≤ r. If it is the case then m = r else m = pr.

  was developed by Ronald Cramer and Victor Shoup in 1998. It is a generalization of ElGamal's protocol and is provably secure against adaptive chosen ciphertext attacks (CCA), under the DDH assumption. Even though it is a modified version of ElGamal, the Cramer-Shoup cryptosystem cannot be used however as a substitute of ElGamal in voting systems. In fact, being resistant to CCA results in losing the homomorphic property of the scheme, which is fundamental for voting systems. In 2006, Benoît Chevallier-Mames et al. [Chevallier-Mames et al., 2006] proposed an ElGamal encryption alternative, using a new encoding-free technique. Their approach holds better performance than plain ElGamal without the necessity to map the message into a subgroup. The authors introduce the notion of the class function based on the difficulty of the Decisional Class Diffie-Hellman (DCDH) assumption. An essential improvement of the Encoding-Free version scheme is to avoid message conversion, providing a wider message space. ElGamal encoding-free is IND-CPA. However, to date, it is not known how to identify whether a group satisfies the DCDH assumption or not. An encoding-free version of ElGamal cryptosystem over elliptic curves has also been proposed in 2017 by Marc Joye et al. in [Joye and Libert, 2017].

  mod 11 using its private key x i .Security Aspects. The security of the ElGamal Baseline scheme is equivalent to the security of ElGamal[START_REF] Elgamal | A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF] encryption scheme. Hence, it is IND-CPA under the assumption of DDH (We refer the reader to Section 2.4 of Chapter 2).

Phase 3 :

 3 Decryption for node n 0 and n 1 1: To decrypt, n 0 and n 1 use their respective private keys 3 and 9. a: Node n 0 computes m = 9 5 2 mod 11 = 3. b: Node n 1 computes m = 1 5 3 mod 11 = 3.

Phase 2 :

 2 Broadcast 1: The server selects a message m = 16 ∈ G 23 and a random element r = 3 ∈ Z 23 . 2: The server evaluates x = 1(13•5) mod 21 = 1 and computes y = 4 1 mod 47 = 4. 3: To encrypt m = 16, the server computes 16 • 4 3 mod 47 = 37. 4: The server broadcasts (2, 17, 37). Decryption. In this example, we do not consider the hash function for decryption. To decrypt, n 0 and n 1 compute pk = z pk i mod 21 and respectively calculate their decryption key as k dec = SK pk 0 and k dec = SK pk 1 .

(

  Programs) p ::= e | c (Expressions) e ::= x | n | v | k | e • e ′ (Commands) c ::= e := e ′ | c; c ′ | k := KG({n 1 , ..., n i }, k ′ ) | while e do c | if e then c else c ′ | sbroadcast({n 1 , ..., n j }, k,e)

Figure

  Figure 5.3: Typing rules

(

  Programs) p ::= e | c (Expressions) e ::= x | L | K | pc | v | e • e ′ (Commands) c ::= e := e ′ | c; c ′ | while e do c | if e then c else c ′ | for n ∈ LendorseRa(L,L ′ , n) | sbroadcast(L,e,K)

(

  Data types) τ ::= (s C , s I ) (Programs types) ρ ::= τ | τ var | τ cmd | τ Lvar | ⊤ Kvar| ⊥ Cvar Metavariables (s C , s I ) range over the set of security classes partially ordered by ≤ in the product lattice (L , ≤) as described in Subsection 4.4.2. Hence, s I represents the integrity level in (L I , ≤ I ) and s C represents the confidentiality level in (L C , ≤ C ).

Figure

  Figure 5.6: Typing rules

Figure

  Figure 5.4.

HM 2 .

 2 Example 25. We show that the program p of Example 22 does not comply with NI Γ LH according to Definition 26.Let memories µ 0 and µ 1 be:

(H 9

 9 ) µ ⊢ k ′ ⇒ v. (H 10 ) µ(n j ) = v j . (H 11 ) µ ⊢ k := KG({v 1 , ..., v i }, k ′ ) ⇒ t µ[k := vk], then µ ′ = µ[k := vk].

Table 4

 4

		x Gn }	n • 1023 2046 5115 102300 1023000 10230000 102300000
	(p = 1024 bits)		bits	bits	bits	bits	bits	bits	bits
	Boneh-Franklin			6138 15345 306900 3069000 30690000 306900000
	(p = 1024 bits)		bits	bits	bits	bits	bits	bits	bits
	New Scheme	n i , h ni	4094	4094 4094	4094	4094	4094	4094
	(p = 2048 bits)		bits	bits	bits	bits	bits	bits	bits

1 {α G1 , ..., α Gn }, Γ i =< γ G1 , ..., γ Gn >* 3n • 1023 .2: Maximum keys storage for 1 node in n subgroups.

Table 4

 4

	• 1024 3072 6144 103424 1034240 10342400 103424000

.3: Ciphertext size in 1 subgroup for k nodes.

  .3. The Base rule states that τ is a subset of τ ′ if τ ≤ τ ′ . The Cmd rule states that τ ′ cmd is a subset of τ cmd if τ is a subset of τ ′ . The Subtype rulestates that a program p of type ρ can be bound to type ρ ′ if ρ is a subset of ρ ′ . The S-Var rule states that a variable x of type τ var can be bound to type τ, and the S-NVar rule states that τ ′ NVar(n) is a subset of τ Nvar(n) if τ is a subset of τ ′ .

  4, in which HH ≤ HM 2 and M 1 M 2 ≤ HM 2 where H ≤ I M 2 which means that H has more integrity than M 2 . We also consider a server willing to send a software update SU M 1 M 2 of type M 1 M 2 var to a set of nodes in L HM 2 and upgrade the security level of node n ∈ L HM 2 to L HH if it succeeds to install correctly its software update. We finally consider a counter, pc of type ⊥ Cvar and a key, K of type ⊤ Kvar.

•

  In order to type p 3 , we apply the Remote Attestation rule to check the integrity of SU M 1 M 2 running on nodes that belongs to the security level L HM 2 and subsequently to ensure that nodes n can be moved to the security level L HH if the verification HM 2 ) = L HM 2 Lvar Γ ⊢ L HM 2 : HM 2 Lvar As a last step, we apply the Sequence rule on p 1 , p 2 and p 3 to show that p is typable.

	Γ ⊢ p 1 : HH cmd	Γ ⊢ p 2 : HH cmd Γ ⊢ p 1 ; p 2 ; p 3 : HH cmd	Γ ⊢ p 3 : HH cmd	(SEQUENCE)
				(LVAR)
		B:
		Γ(L HH ) = L HH Lvar Γ ⊢ L HH : HH Lvar	(LVAR)

succeeds. In addition to checking (A, B) the types of the security levels variables, this rule constrains a confidentiality and integrity order between the two security levels :I(HH) ≤ I I(HM 2 ) and C(HM 2 ) ≤ C C(HH).

(REMOTE ATTESTATION) (A)( B)( C) Γ ⊢ for n ∈ L HM 2 endorse Ra(L HM 2 , L HH , n) A:

Γ(L Finally, we apply the Subtype rule on p 3 to bind it to type HH cmd and therefore show that the program p 3 is typable.

  We apply the Var rule on x LH that checks if Γ(x LH ) = LH var which is the case. We consider the diamond lattice in Figure5.4, in which LH ≤ HH and L has less confidentiality than H. We consider a program p: L LH := x HH that is not typable but our security property does not detect it and considers the program as secure.

	secure despite the fact that the broadcast seems to be secure. Actually, the server is
	broadcasting a message that contains high confidentiality information (H) to nodes
	with confidentiality clearance (L) since x LH contains information from y HH . This flow
	of information is not allowed by our architecture as it leaks confidential information to
	nodes placed in L LH . This may compromise the confidentiality and security of a system
	broadcasting important messages. It would allow the server to transmit confidential
	information to nodes situated in lower security classes.
	Example 23.
	(VAR)

• In p 2 the Assign rule constrains the types x LH and y HH .

Γ ⊢ x LH : τ var Γ ⊢ y HH : τ Γ ⊢ x LH := y HH : τ (ASSIGN) -Γ(x LH ) = LH var Γ ⊢ x LH : LH var

  ′ 1 ). By previous induction on c we have that filter τ (t 0 ) = filter τ (t 1 ). Since t i • t ′ i is the concatenation of two traces t i and t ′ i , and since filter τ (t 0 ) = filter τ (t 1 ) and filter τ (t ′ 0 ) = filter τ (t ′ 1 ), we conclude thatfilter τ (t 0 • t ′ 0 ) = filter τ (t 1 • t ′ 1 ) from which (G 2 ) follows.Since (G 1 ) and (G 2 ) are satisfied, then while e do c ′ is NI Γ

τ . Subcase 2.3. p ∆ = if e thenc ′ else c ′′ .

We only consider the minimal lower bound for key storage with

nodes per subgroup.

MKVAR Γ(k) = ⊤ MKvar Γ ⊢ k : ⊤ MKvar KVAR-ASSIGN Γ(k) = τ Kvar(n 1 ...n i ) Γ ⊢ n j : τ Nvar(n j ) j ∈ {1...i} Γ ⊢ k ′ : ⊤ MKvar Γ ⊢ k := KG({n 1 ...n i }, k ′ ):τ cmd OP Γ ⊢ e : τ Γ ⊢ e ′ : τ Γ ⊢ e • e ′ : τ ASSIGN Γ ⊢ x : τ var Γ ⊢ e : τ Γ ⊢ x := e : τ cmd SEQUENCE Γ ⊢ c : τ cmd Γ ⊢ c ′ : τ cmd Γ ⊢ c; c ′ : τ cmd IF Γ ⊢ e : τ Γ ⊢ c : τ cmd Γ ⊢ c ′ : τ cmd Γ ⊢ if e then c else c ′ : τ cmd WHILE Γ ⊢ e : τ Γ ⊢ c : τ cmdΓ ⊢ while e do c : τ cmd SBROADCAST

Γ ⊢ L : τ Lvar KVAR Γ(K) = ⊤ Kvar Γ ⊢ K : ⊤ Kvar OP Γ ⊢ e : τ Γ ⊢ e ′ : τ Γ ⊢ e • e ′ : τ ASSIGN Γ ⊢ x : τ var Γ ⊢ e ′ : τ Γ ⊢ x := e ′ : τ cmd ASSIGN-COUNTER Γ ⊢ pc : ⊥ Cvar Γ ⊢ pc := pc+ 1 : ⊥ cmd SEQUENCE Γ ⊢ c : τ cmd Γ ⊢ c ′ : τ cmd Γ ⊢ c; c ′ : τ cmd IF Γ ⊢ e : τ Γ ⊢ c : τ cmd Γ ⊢ c ′ : τ cmd Γ ⊢ if e then c else c ′ : τ cmd WHILE Γ ⊢ e : τ Γ ⊢ c : τ cmd Γ ⊢ while e do c : τ cmd SBROADCAST Γ ⊢ e ′ : τ Γ ⊢ L : τ Lvar Γ ⊢ K : ⊤ Kvar Γ ⊢ pc : ⊥ Cvar Γ ⊢ sbroadcast(L,e ′ ||pc, K):τ cmd

µ • In the Sequence rule, c is evaluated in µ ′ and c ′ is evaluated in µ ′′ ; then the sequence c; c ′ is evaluated in µ ′′ .

• In the Branch-True rule, e is true and c is evaluated in µ ′ ; then the if statement is evaluated in µ ′ .

• In the Branch-False rule, e is false and c is evaluated in µ ′ ; then the if statement is evaluated in µ ′ .

Definition 26 (NonInterference). A server program p is NI at τ for Γ, written NI Γ τ (p),

1 ∧ filter τ (t 0 ) = filter τ (t 1 ).

Our main result follows: a well-typed program is noninterferent at τ for Γ.

Theorem 2. Let Γ be a typing environment and τ ∈ L a security label. If Γ ⊢ p then p is

We prove this theorem by induction on the height of the typing derivation tree of

Example 19. Concerning the security property, we show that the program p of Example 12 is noninterferent at M 1 . We let two memories µ 0 = {k := vk 0 , k ′ := vk ′ 0 , n 0 = "n 0 ", n 1 = "n1", m := v} and µ 1 = {k := vk 1 , k ′ = vk ′ 1 , n 0 = "n 0 ", n 1 = "n1", m := v}. Notice that µ 0 = Γ M 1 µ 1 . By Definition 24, µ 0 = Γ M 1 µ 1 since only variables of type τ var (in our example m) should be equal. After executing p, the value of m does not change in the resulting memories µ ′ 0 and µ ′ 1 . Since only variables of type τ var are considered, then

In order to satisfy the full hypothesis in Definition 26, we need to prove that filter M 1 (t 0 ) = filter M 1 (t 1 ). Actually, t 0 and t 1 are the traces of the messages broadcasted over the network through the Secure Broadcast rule in Figure 5.2: BEnc({n 1 , ..., n k }, k,v). For an execution that starts with µ 0 , t 0 = BEnc({n 0 , n 1 }, vk 3 , v), thus filter M 1 (t 0 ) = [{n 0 , n 1 }, v].

For an execution that starts with µ 1 , t 1 = BEnc({n 0 , n 1 }, vk 4 , v) and filter M 1 (t 1 ) = [{n 0 , n 1 }, v].

Hence, filter M 1 (t 0 ) = filter M 1 (t 1 ) and p is NI

Example 20. We show that the program p of Example 15 does not comply with NI Γ L according to Definition 26. Let two memories µ 0 = {k := vk 3 , k ′ := vk ′ 3 , n 0 = "n 0 ", n 1 = "n1", m := 4, m ′ := 2} and µ 1 = {k := vk 4 , k ′ = vk ′ 4 , n 0 = "n 0 ", n 1 = "n1", m := 5, m ′ := 2}. The memories µ 0 and µ 1 are L-Equal since the value of m ′ is the same in both memories, and m ′ is the only variable of type Lvar. The resulting memories of the execution of p are µ ′ 0 = {k := vk 3 , k ′ := vk ′ 3 , n 0 = "n 0 ", n 1 = "n1", m := 4, m ′ := 4} and µ ′ 1 = {k := vk 4 ,

µ(L) = {"n 1 ", "n 2 ", ..., "n n "} µ ⊢ pc ⇒ v µ ⊢ sbroadcast(L,e||pc,K) ⇒ BEnc(L,vk,"m"||"v") µ ENDORSE-RA µ(L) = {"n 0 ", "n 1 ", ..., "n n "} µ(L ′ ) = {"n ′ 0 ", "n ′ 1 ", ..., "n ′ n "} µ ⊢ Ra(L) ⇒ SS⊆ {"n 0 ", ..., "n n "} µ ⊢ for n ∈ LendorseRa(L,L ′ , n) ⇒ µ ′ [L := L \ S;L ′ := L ′ ∪ S]

• In p 2 , the SBroadcast rule checks (A) the type of the message to broadcast SU, (B) the type of the security level variable L HM 2 , (C) the type of the key variable K and finally (D) the type of pc.

-To bind y HH to type LH, we apply the Subtype rule. To apply correctly the rule, HH ⊆ LH requires to be satisfied. Since HH ⊆ LH, the Subtype rule fails.

Hence, p 2 is not typable.

• To type p 3 , we apply the SBroadcast rule and check that all the constraints are satisfied.

Therefore p 3 is well-typed. Since the second program p 2 is not typable, the Sequence rule is not applicable and therefore the entire program is not typable. Indeed, p is not µ 0

x LH := 2 y HH := 4

The memories µ 0 and µ 1 are LH-Equal since the value of x LH is the same in both memories. The two memoriesµ ′ 0 and µ ′ 1 are the resulting memories of the execution of p.

µ ′ 0

x LH := 4 y HH := 4

The two memories µ ′ 0 and µ ′ 1 are not LH-Equal since the value of x LH is different and therefore the program p is not NI Γ LH .

Example 26. We show that the program p of Example 23 , is indeed NI Γ LH because our security property is not strong enough as to capture information flows to level variables (in contrast to our type system that do capture them).

Let memories µ 0 and µ 1 be:

The two memories µ 0 and µ 1 are LH-Equal as our security property considers only variables of type LH var.

The resulting memories µ ′ 0 and µ ′ 1 of the execution of p are:

BIBLIOGRAPHY

A PPENDIX A PROOF OF THEOREM 2 OF SECTION 5.1

To prove Theorem 2, we need to introduce two Lemmas:

A.1 Proof of Lemma 1

Proof. We prove Lemma1 by structural induction on e with P Struct (e) = n. According to our type system, specifically the subtyping rule S-Var, only variables of type τ var can be typed as τ. That is the reason we omit the cases of NVar and MKVar.

It follows that:

From the hypothesis of Lemma 1, we have that:

And we need to prove that:

Case 1 (Base Case).

Subcase 1.1 (Lit: v). By (H 2 ) and the typing rule Lit, we have that:

By (H 4 ) and the semantics rule Base, we have that:

By (H 5 ) and the semantics rule Base, we have that:

From (H 7 ) and (H 8 ), (G 1 ) is trivially true.

Subcase 1.2 (Var: x). By (H 2 ) and the subtyping rule S-Var (which is the only rule that allows variables of type τ ′ var to be typed as variables of type τ ′ ), we have that:

By (H 6 ) and the typing rule Var, we have that:

By (H 4 ) and the semantics rule Var, we have that:

By (H 5 ) and the semantics rule Var, we have that:

By Definition 24 and (H 1 ) of Lemma 1, we have that:

From this, and by (H 6 ) and (H 3 ), we have that :

By (H 10 ), (H 8 ) and (H 9 ), we conclude that v 0 = v 1 , which is (G 1 ).

Case 2 (Op: e ′ • e ′′ ). Inductive hypothesis for e For P Struct (e) = n, we have that:

Then we conclude that:

Inductive case: height = P Struct (e) = n + 1.

Op: e ′ • e ′′ . For the typing rule Op, we have that:

By (IH 4 ) and the semantics rule Op, we have that:

By (IH 5 ) and the semantics rule Op, we have that:

Concerning e', from the inductive hypothesis on e, it follows that:

Concerning e", from the inductive hypothesis on e, it follows that:

By the transitive property of = and since v

Proof of Lemma 2

Proof. We prove lemma2 by structural induction on c with P Struct (c) = n. It follows that:

• P Struct (sbroadcast({n 1 , ..., n j }, k,e)) = 1.

• P Struct (while e do c) = P Struct (c) + 1.

From the hypothesis of Lemma 2, we have that:

And we need to prove that:

Case 1 (Base case).

Subcase 1.1 (Assign: x := e ′ .). By the hypothesis of the lemma, we have that:

By (H 4 ) and the typing rule Assign, we have that:

By (H 5 ) and the typing rule Var, we have that:

By (H 3 ) and the semantics rule Update, we have that:

By the semantics rule Update, we have that:

For (H 2 ), we have that τ ′ ≤ τ.

By (H 4 ) and the typing rule KVar-Assign, we have that:

(H 6 ) Γ ⊢ n j : τ ′ Nvar(n j ).

By (H 3 ) and the semantics rule Update, we have that:

For (H 2 ), we have that τ ′ ≤ τ. Since the initial memory µ and the final memory µ are equal by (H 8 ), we conclude that µ = Γ τ µ ′ which is (G 1 ).

To prove (G 2 ), by (H 9 ), t = BEnc({n 1 , ..., n k }, vk,v ′ ). By Definition 25, and by (H 2 ) and

Inductive hypothesis for c For P Struct (c) = n, we have that:

Then we conclude that:

Inductive case: height = P Struct (c) = n + 1.

Sequence: c ′ ; c ′′ . For the typing rule Sequence, we have that:

By (IH 2 ) and the semantics rule Sequence, we have that:

Concerning c', from the inductive hypothesis on c, it follows that:

Concerning c", from the inductive hypothesis on c, it follows that:

By the transitive property of = Γ τ and since µ = Γ τ µ ′ and µ ′ = Γ τ µ ′′ , we can conclude

In the semantics rule Sequence, t While: while e do c. For the typing rule While, we have that:

By (H 1 ) and because the height of Γ ⊢ while e do c is n + 1, we know that the height of the typing derivation tree of (H 1 ) is ≤ n. By applying the inductive hypothesis on c, we get that:

We want to prove that the inductive hypothesis works for while e do c also. By the hypothesis of Lemma 2, we have that if:

Then we want to prove that:

By the semantics rule of Loop, we have that:

Base case. The only possibility for the semantics tree to be of height = 2 is when

By (H 3 ) we conclude that µ = Γ τ µ. We also conclude that

Assuming that our inductive hypothesis holds for the case of while when evaluating the height of the semantics tree ≤ m, we want to prove the case of While with height

By applying the structural induction to (1), we have that µ = Γ τ µ ′′ and filter τ (t) = []. By applying the inductive hypothesis on while e do c by (H ′ 6 ), we can conclude that

If: if e then c ′ else c ′′ . For the typing rule If, we have that:

By (H 1 ) and the inductive hypothesis on c ′ , we get that:

By (H 1 ) and the inductive hypothesis on c ′′ , we get that:

Concerning if e then c ′ else c ′′ , by the hypothesis of Lemma 2, we have that if:

Then we want to prove that:

By the semantics rule of Branch-True, we have that:

By (H 3 ) and (H 4 ) we can conclude that µ = Γ τ µ ′ . By (H 5 ) and (H 14 ) we conclude that

By the semantics rule of Branch-False, we have that:

By (H 3 ) and (H 5 ) we can conclude that µ = Γ τ µ ′ . By (H 6 ) and (H 17 ) we conclude that

■

A.3 Proof of Theorem 2

Proof. By Definition 26, for p to be NI Γ τ , we need to prove that:

(G 2 ) filter τ (t 0 ) = filter τ (t 1 ).

We prove this theorem by induction on the height of typing derivation tree Γ ⊢ p.

Concerning (G 1 ) and (G 2 ), by Definition 26, we have that:

Moreover, for the semantics rule Update we have that:

To prove (G 1 ), we rely on the Definition 24 that states that µ 0 = Γ τ µ 1 , if ∀y ∈ µ 0 such that Γ(y) = τ ′ var and τ ′ ≤ τ then µ 0 (s) = µ 1 (y). For (H 12 ), we have that τ ′ ≤ τ. Since we are only interested by variables with security level less or equal than τ, we can conclude by (H 5 ) and (H 1 )

To prove (G 2 ) we rely on the Definition 25 and (H 3 ). Since t

Since we proved (G 1 ) and

Concerning (G 1 ) and (G 2 ), by Definition 26, we have that:

By the semantics rule Update we have that:

Moreover, by the semantics rule Update and (H 2 ), we have that:

By the hypothesis of Theorem 2, we have:

By the typing rule Kvar-Assign, we have that:

(H 8 ) Γ ⊢ n j : τ ′ Nvar(n j ).

(H 9 ) Γk ′ : ⊤ MKvar.

different than τ ′ var. Since we are only interested in variables of type τ ′ var,(G 1 ) follows by (H 1 ) and (H 2 ).

To prove (G 2 ), we have two cases:

and by (H 2 ) and(H 3 ) we have that t 0 = t 1 . For an execution that starts with µ 0 , t 0 = BEnc({n 1 , ..., n k }, vk 0 , v ′ ) and for an execution that starts with

It results that filter(t 0 ) = filter(t 1 ) and therefore we prove (G 2 ).

Since we proved (G 1 ) and

and by (H 2 ) and(H 3 ) we have that t 0 = t 1 . For an execution that starts with µ 0 , t 0 = BEnc({n 1 , ..., n k }, vk 0 , v ′ ) and for an execution that starts with µ 1 ,

It results that filter τ (t 0 ) = filter τ (t 1 ) and therefore we prove (G 2 ).

Since we proved (G 1 ) and (G 2 ), then p is NI Γ τ .

Case 2. Inductive case: height= n + 1 Subcase 2.1.

We want to prove that

We assume that c ′ and c ′′ are of height ≤ n, and c ′ ; c ′′ of height n + 1.

For the typing rule Sequence, we have that:

For the semantics rule Sequence, we have that:

Concerning c ′ , from the inductive hypotheses, it follows that:

Concerning c ′′ , from the inductive hypotheses, it follows that:

In the semantics rule Sequence, we use t

Subcase 2.2. p ∆ = while e do c.

For the typing rule While, we have that:

In the following, we show by induction that c is NI Γ τ .

By (H 1 ) and because the height of Γ ⊢ while e do c is n + 1, we know that the height of the typing derivation tree of (H 1 ) is ≤ n. Hence, we can apply the inductive hypothesis and get:

Then,

We want to prove that while e do c is NI Γ τ . By the hypothesis of the theorem, we have that if:

Then, we want to prove that:

(G 1 ) filter τ (t 0 ) = filter τ (t 1 ).

By (H ′

2 ) and the semantics rule of Loop, we have that:

By (H ′ 3 ) and the semantics rule of Loop, we have that:

Depending on τ ′ , we have two cases:

In the case of (H ′ 6 ), we check if we can apply the Subtype rule on While command. We would like to check if the command While of type τ ′ cmd can be typable as τ ′′ cmd, where τ ′′ ≤ τ ′ . If the Subtype rule can be applied, the the proof of this case is analogous to Subcase 3.2.2.

Otherwise, if the Subtype rule cannot be applied, then by Lemma 1 that can be applied on (H ′ 1 ), (H 2 ), (H ′ 6 ), (H ′ 4 ) and (H ′ 5 ), we conclude that v 0 = v 1 . We prove this case by induction on the height of the semantics tree of (H ′ 2 ). (We do not show this formally, but we rely on the fact that the height of (H ′

2 ) is equal to the height of (H ′ 3 ) by Lemma 1).

Base case: height = 2. The only possibility for the semantics tree to be of height = 2 is:

Assuming that our inductive hypothesis holds for the case of While when evaluating the height of semantics tree ≤ m with Γ ⊢ e : τ ′ , τ ′ ≤ τ, let us prove the case of While with height = m + 1.

Inductive case: height = m+1.

By the previous induction on c, we have that

1 and filter τ (t 0 ) = filter τ (t 1 ),

Moreover, by induction on while e do c by (H ′ 7 ) and (H ′ 8 ), we can conclude that

which is already our goal (G 1 ) and filter τ (t ′ 0 ) = filter τ (t ′ 1 ). This is because we have that

i is the concatenation of two traces t i and t ′ i , and since filter τ (t 0 ) = filter τ (t 1 ) and filter τ (t ′ 0 ) = filter τ (t ′ 1 ), we conclude that filter τ (t

Since (G 1 ) and (G 2 ) are satisfied, then while e do c is NI

By Lemma 2 that can be applied on (H 1 ), (H 4 ), (H 5 ) and (H ′ 9 ), we conclude that

We prove that µ ′ 0 = Γ τ µ ′ 1 by applying the transitive property on = Γ τ :

Concerning c ′′ , by induction, we conclude that:

Depending on τ ′ , we have two cases:

In the case of (H 10 ), we check if we can apply the Subtype rule on If command. We would like to check if the command If of type τ ′ cmd can be typable as τ ′′ cmd, where

If the Subtype rule can be applied, the the proof of this case is analogous to Subcase 3.2.5.

Otherwise, if the Subtype rule cannot be applied, then by Lemma 1, we can conclude that:

then filter τ (t 0 ) = filter τ (t 1 ).

By Lemma 2, we conclude that

1 by applying the transitive property on = Γ τ .

• We have that (1)

• By ( 1) and ( 3) we have that ( 4)

• By ( 2) and ( 3) we have that ( 5)

• By ( 4) and ( 5) we conclude that (6

To prove Theorem 3, we rely on Lemma 1 and 2. Since Lemma 1 is analogous to the one in Appendix A, we only prove Lemma 2 and Theorem 3.

B.1 Proof of Lemma 2

Proof. We prove this lemma by structural induction on c with P Struct (c) = n. It follows that:

• P Struct (x := e ′ ) = 1.

• P Struct (pc := pc+ 1) = 1.

• P Struct (sbroadcast(L, e||pc,K)) = 1.

• P Struct (for n ∈ LRa(L,L ′ , n)) = 1.

• P Struct (c ′ ; c ′′ ) = P Struct (c ′ ) + P Struct (c ′′ ).

• P Struct (while e do c) = P Struct (c) + 1.

• P Struct (if e then c ′ else c ′′ = MAX(P Struct (c ′ ), P Struct (c ′′ ) + 1.

From the hypothesis of Lemma 2, we have that:

And we need to prove that:

Case 1 (Base case).

Subcase 1.1 (Assign: x := e ′ .). By the hypothesis of the lemma, we have that:

By (H 4 ) and the typing rule Assign, we have that:

By (H 5 ) and the typing rule Var, we have that:

By (H 3 ) and the semantics rule Update, we have that:

By the semantics rule Update, we have that:

For (H 2 ), we have that τ ′ ≤ τ. Since the only variable in which µ and µ ′ are different is x by (H 9 ) and the security level of the variable x is τ ′ var, we can conclude that µ = Γ τ µ ′ which is (G 1 ).

To prove (G 2 ), by (H 10 ), t

Subcase 1.2 (Assign-Counter: pc := pc + 1). By the hypothesis of the lemma, we have that:

(H 4 ) Γ ⊢ pc := pc+ 1 : ⊥ cmd.

By (H 4 ) and the typing rule Assign-Counter, we have that:

By (H 3 ) and the semantics rule Update, we have that:

By the semantics rule Update, we have that:

For (H 2 ), we have that τ ′ ≤ τ. Since the only variable in which µ and µ ′ are different is pc by (H 7 ) and the security level of the variable pc is ⊥ ′ Cvar, we can conclude that

Subcase 1.3 (SBroadcast: sbroadcast(L,e||pc,K)). By the hypothesis of the lemma, we have that:

(H 4 ) Γ ⊢ sbroadcast(L,e||pc,K):τ ′ cmd.

By (H 4 ) and the typing rule SBroadcast, we have that:

By (H 3 ) and the semantics rule Secure Broadcast, we have that:

By the semantics rule Secure Broadcast, we have that:

(H 10 ) t = BEnc(L,vk,"m"||"v").

For (H 2 ), we have that τ ′ ≤ τ. Since the initial memory µ and the final memory µ are equal by (H 9 ), we conclude that µ = Γ τ µ ′ which is (G 1 ).

To prove (G 2 ), by (H 10 ), t = BEnc(L,vk,"m"||"v"). By Definition 27, and by (H 2 ) and

Subcase 1.4 (Remote Attestation: for n ∈ LRa(L,L ′ , n)). By the hypothesis of the lemma, we have that:

By (H 4 ) and the typing rule Remote Attestation, we have that:

(H 8 ) Γ ⊢ pc : ⊥ Cvar.

(H 9 ) I(τ ′′ ≤ I I(τ ′ ).

By (H 3 ) and the semantics rule Endorse-Ra, we have that:

By the semantics rule Endorse-Ra, we have that:

For (H 2 ), we have that τ ′ ≤ τ. By (H 9 ) and (H 10 ) we have that τ ′ ≤ τ ′′ , therefore τ ′′ ≤ τ .

Since τ ′ ≤ τ and τ ′′ ≤ τ and because µ and µ ′ are different only for variables L of type τ ′ and L ′ of type τ ′′ by (H 9 ), we conclude that µ = Γ τ µ ′ which is (G 1 ).

To prove (G 2 ), by (H 10 ), t

Inductive hypothesis for c For P Struct (c) = n, we have that:

Then we conclude that:

Inductive case: height = P Struct (c) = n + 1.

Sequence: c ′ ; c ′′ . For the typing rule Sequence, we have that:

By (IH 2 ) and the semantics rule Sequence, we have that:

Concerning c', from the inductive hypothesis on c, it follows that:

Concerning c", from the inductive hypothesis on c, it follows that:

By the transitive property of = Γ τ and since µ = Γ τ µ ′ and µ ′ = Γ τ µ ′′ , we can conclude

In the semantics rule Sequence, t While: while e do c. For the typing rule While, we have that:

By (H 1 ) and because the height of Γ ⊢ while e do c is n + 1, we know that the height of the typing derivation tree of (H 1 ) is ≤ n. By applying the inductive hypothesis on c, we get that:

We want to prove that the inductive hypothesis works for while e do c also. By the hypothesis of Lemma 2, we have that if:

Then we want to prove that:

By the semantics rule of Loop, we have that:

Base case. The only possibility for the semantics tree to be of height = 2 is when

By (H 3 ) we conclude that µ = Γ τ µ. We also conclude that filter

Assuming that our inductive hypothesis holds for the case of while when evaluating the height of the semantics tree ≤ m, we want to prove the case of While with height

By applying the structural induction to (1), we have that

If: if e then c ′ else c ′′ . For the typing rule If, we have that:

By (H 1 ) and the inductive hypothesis on c ′ , we get that:

By (H 1 ) and the inductive hypothesis on c ′′ , we get that:

Concerning if e then c ′ else c ′′ , by the hypothesis of Lemma 2, we have that if:

B.2 Proof of Theorem 3

Proof. By Definition 26, for p to be NI Γ τ , we need to prove that:

(G 2 ) filter τ (t 0 ) = filter τ (t 1 ).

We prove this theorem by induction on the height of typing derivation tree Γ ⊢ p.

Case 1. Base case: height = 2 Subcase 1.1.

Concerning (G 1 ) and (G 2 ), by Definition 26, we have that:

Moreover, for the semantics rule Update we have that:

Hence, by the semantics rule Update and (H 2 ), we have that:

By the hypothesis of Theorem 3, we have:

By (H 6 ) and the typing rule Assign, we have that:

By (H 7 ) and the typing rule Var, we have:

Depending on τ ′ , we have two cases:

By Lemma 1 that can be applied due to (H 1 ), (H 8 ), (H 10 ) and (H 4 ) then

To prove (G 1 ), we rely on the Definition 24 that states that

Since (H 1 ) holds and the only variable in which µ i and µ ′ i are different is x by (H 5 ), then we need to prove that µ 0 (x) = µ 1 (x) which holds by (H 11 ).

To prove (G 2 ) we rely on the Definition 27 and (H 3 ). Since t 0 = t 1 = []then filter τ (t 0 ) = filter τ (t 1 ).

Since we proved (G 1 ) and (G

To prove (G 1 ), we rely on the Definition 24 that states that µ 0 = Γ τ µ 1 , if ∀y ∈ µ 0 such that Γ(y) = τ ′ var and τ ′ ≤ τ then µ 0 (s) = µ 1 (y). For (H 12 ), we have that τ ′ ≤ τ. Since we are only interested by variables with security level less or equal than τ, we can conclude by (H 5 ) and (H 1 )

To prove (G 2 ) we rely on the Definition 27 and (H 3 ). Since t 0 = t 1 = []then filter τ (t 0 ) = filter τ (t 1 ).

Since we proved (G 1 ) and (G

Concerning (G 1 ) and (G 2 ), by Definition 26, we have that:

By the semantics rule Update we have that:

Moreover, by the semantics rule Update and (H 2 ), we have that:

By the hypothesis of Theorem 3, we have:

By the typing rule Assign-Counter, we have that:

To prove (G 1 ), we rely on the Definition 24 that states that

For (H 7 ), Γ(pc) = ⊥ Cvar. Since we are only interested in variables of type τ ′ var, we conclude by (H 5 ) and (H 1 ) that

To prove (G 2 ) we rely on the Definition 27 and (H 3 ). Since t 0 = t 1 = []then filter τ (t 0 ) = filter τ (t 1 ).

Since we proved (G 1 ) and (G 2 ), then p is NI Γ τ .

Subcase 1.3. p ∆ = sbroadcast(L,e||pc,K).

Concerning (G 1 ) and (G 2 ), by Definition 26, we have that:

By the semantics rule Secure Broadcast, we have:

(H 7 ) µ i (L) = {"n 0 ", "n 1 ", ..., "n n "}.

By the hypothesis of Theorem 3, we have:

By (H 8 ) and the typing rule SBroadcast, we have:

To prove (G 1 ), we rely on the Definition 24 that states that µ 0 = Γ τ µ 1 , if ∀y ∈ µ 0 such that Γ(y) = τ ′ var and τ ′ ≤ τ then µ 0 (y) = µ 1 (y). For (H 9 -H 12 ), all the variables types are different than τ ′ var. Since we are only interested in variables of type τ ′ var,(G 1 ) follows by (H 1 ) and (H 2 ).

To prove (G 2 ), we have two cases:

and by (H 2 ) and(H 3 ) we have that t 0 = t 1 . For an execution that starts with µ 0 , t 0 = BEnc(L,vk 0 , "m"||"v") and for an execution that starts with µ 1 ,

It results that filter(t 0 ) = filter(t 1 ) and therefore we prove (G 2 ).

Since we proved (G 1 ) and

and by (H 2 ) and(H 3 ) we have that t 0 = t 1 . For an execution that starts with µ 0 , t 0 = BEnc(L,vk 0 , "m"||"v") and for an execution that starts with µ 1 ,

It results that filter τ (t 0 ) = filter τ (t 1 ) and therefore we prove (G 2 ).

Since we proved (G 1 ) and (G 2 ), then p is NI Γ τ .

Subcase 1.4.

Concerning (G 1 ) and (G 2 ), by Definition 26, we have that:

By the semantics rule Endorse-Ra we have that:

(H 5 ) µ i (L) = {"n 0 ", "n 1 ", ..., "n n "}.

By (H 2 ) and the semantics rule Endorse-Ra we have that:

By the hypothesis of Theorem 3, we have:

By (H 8 ) and the typing rule Remote Attestation, we have that:

To prove (G 1 ), we rely on the Definition 24 that states that µ 0 = Γ τ µ 1 , if ∀y ∈ µ 0 such that Γ(y) = τ ′ var and τ ′ ≤ τ then µ 0 (y) = µ 1 (y). For (H 9 -H 12 ), all the variables types are different than τ ′ var. Since we are only interested in variables of type τ ′ var,(G 1 ) follows by (H 1 ) and (H 2 ).

To prove (G 2 ) we rely on the Definition 27 and (H 3 ). Since t 0 = t 1 = []then filter τ (t 0 ) = filter τ (t 1 ).

Since we proved (G 1 ) and (G 2 ), then p is NI Γ τ .

Case 2 (Case: height ≤ n). We will state our inductive hypothesis for a program c:

For the hypothesis of the theorem, we have that:

For the derivation tree of height ≤ n, we have that:

Then we conclude that:

(IH 6 ) filter τ (t 0 ) = filter τ (t 1 ).

We suppose that (IH 1 -IH 6 ) are valid for programs of height ≤ n of typing derivation tree Γ ⊢ p.

Case 3. Inductive case: height= n + 1 Subcase 3.1.

We want to prove that Γ ⊢ c ′ ; c ′′ is NI Γ τ . We assume that c ′ and c ′′ are of height ≤ n, and c ′ ; c ′′ of height n + 1.

For the typing rule Sequence, we have that:

For the semantics rule Sequence, we have that:

Concerning c ′ , from the inductive hypotheses, it follows that:

Concerning c ′′ , from the inductive hypotheses, it follows that:

In the semantics rule Sequence, we use t

We conclude that filter τ (t ′ 0

Subcase 3.2. p ∆ = while e do c.

For the typing rule While, we have that:

In the following, we show by induction that c is NI Γ τ .

By (H 1 ) and because the height of Γ ⊢ while e do c is n + 1, we know that the height of the typing derivation tree of (H 1 ) is ≤ n. Hence, we can apply the inductive hypothesis and get:

Then,

(H 7 ) filter τ (t 0 ) = filter τ (t 1 ).

We want to prove that while e do c is NI Γ τ . By the hypothesis of the theorem, we have that if:

Then, we want to prove that:

(G 1 ) filter τ (t 0 ) = filter τ (t 1 ).

By (H ′

2 ) and the semantics rule of Loop, we have that:

By (H ′ 3 ) and the semantics rule of Loop, we have that:

Depending on τ ′ , we have two cases:

In the case of (H ′ 6 ), we check if we can apply the Subtype rule on While command. We would like to check if the command While of type τ ′ cmd can be typable as τ ′′ cmd, where τ ′′ ≤ τ ′ . If the Subtype rule can be applied, the the proof of this case is analogous to Subcase 3.2.2.

Otherwise, if the Subtype rule cannot be applied, then by Lemma 1 that can be applied on (H ′ 1 ), (H 2 ), (H ′ 6 ), (H ′ 4 ) and (H ′ 5 ), we conclude that v 0 = v 1 . We prove this case by induction on the height of the semantics tree of (H ′ 2 ). (We do not show this formally, but we rely on the fact that the height of (H ′ 2 ) is equal to the height of (H ′ 3 ) by Lemma 1).

Base case: height = 2. The only possibility for the semantics tree to be of height = 2 is:

Assuming that our inductive hypothesis holds for the case of While when evaluating the height of semantics tree ≤ m with Γ ⊢ e : τ ′ , τ ′ ≤ τ, let us prove the case of While with height = m + 1.

Inductive case: height = m+1.

The height of (H ′ 3 ) is m + 1. By the previous induction on c, we have that µ ′′ 0 = Γ τ µ ′′ 1 and filter τ (t 0 ) = filter τ (t 1 ),

Moreover, by induction on while e do c by (H ′ 7 ) and (H ′ 8 ), we can conclude that µ ′ 0 = Γ τ µ ′ 1 which is already our goal (G 1 ) and filter τ (t ′ 0 ) = filter τ (t ′ 1 ). This is because we have that

i is the concatenation of two traces t i and t ′ i , and since filter τ (t 0 ) = filter τ (t 1 ) and filter τ (t

Since (G 1 ) and (G 2 ) are satisfied, then while e do c is NI

By Lemma 2 that can be applied on (H 1 ), (H 4 ), (H 5 ) and (H ′ 9 ), we conclude that

We prove that µ ′ 0 = Γ τ µ ′ 1 by applying the transitive property on = Γ τ :

• By (H ′ 1 ) we have that (1) µ 0 = Γ τ µ 1 .

• By Lemma 2 we have that ( 2)

• By ( 1) and ( 2) we have that ( 4)

• By ( 1) and ( 3) we have that ( 5)

• By ( 4) and ( 5) we conclude that ( 6)

By applying structural induction, we have that filter τ (t ′ 0 ) = filter τ (t ′ 1 ). By previous induction on c we have that filter τ (t 0 ) = filter τ (t 1 ). Since t i • t ′ i is the concatenation of two traces t i and t ′ i , and since filter τ (t 0 ) = filter τ (t 1 ) and filter τ (t ′ 0 ) = filter τ (t ′ 1 ), we conclude that

Since (G 1 ) and (G 2 ) are satisfied, then while e do c ′ is NI Γ τ .

Subcase 3.2.3. p ∆ = if e thenc ′ else c ′′ .

For the typing rule If, we have that:

For the semantics rule Branch, we have that:

Concerning c ′ , by induction, we conclude that:

Concerning c ′′ , by induction, we conclude that:

Depending on τ ′ , we have two cases:

In the case of (H 10 ), we check if we can apply the Subtype rule on If command. We would like to check if the command If of type τ ′ cmd can be typable as τ ′′ cmd, where τ ′′ ≤ τ ′ . If the Subtype rule can be applied, the the proof of this case is analogous to Subcase 3.2.5.

Otherwise, if the Subtype rule cannot be applied, then by Lemma 1, we can conclude that:

By Lemma 2, we conclude that µ i = Γ τ µ ′ i . We prove that µ ′ 0 = Γ τ µ ′ 1 by applying the transitive property on = Γ τ .

• We have that (1)

• By ( 1) and ( 3) we have that ( 4)

• By ( 2) and ( 3) we have that (5) µ 0 = Γ τ µ ′ 1 .

• By ( 4) and ( 5) we conclude that (6

IMPLEMENTATIONS OF THE SCHEMES IN CHAPTER 4

In this appendix, we provide the Ocaml implementations of the three schemes compared in Chapter 4. We only provide the source code of the key generation, the encryption and the decryption. The full source code can found here. Listing C.12: Safe decrypting algorithm

C.1 Implementation of