Gaby Bou Tayeh
email: gaby.boutayeh@edu.univ-fcomte.fr

Abdallah Makhoul
email: abdallah.makhoul@univ-fcomte.fr

David Laiymani
email: david.laiymani@univ-fcomte.fr

Jacques Demerjian
email: jacques.demerjian@ul.edu.lb

A Distributed Real-Time Data Prediction and Adaptive Sensing Approach for Wireless Sensor Networks

Keywords: Wireless Sensor Networks, Data estimation, Data reduction, Data prediction, Adaptive Sampling, Energy saving

Many approaches have been proposed in the literature to reduce energy consumption in Wireless Sensor Networks (WSNs). Influenced by the fact that radio communication and sensing are considered to be the most energy consuming activities in such networks. Most of these approaches focused on either reducing the number of collected data using adaptive sampling techniques or on reducing the number of data transmitted over the network using prediction models. In this article, we propose a novel prediction-based data reduction method. furthermore, we combine it with an adaptive sampling rate technique, allowing us to significantly decrease energy consumption and extend the whole network lifetime. To validate our work, we tested our approach on real sensor data collected at our offices. The final results were promising and confirmed our theoretical claims.

Introduction

A Wireless Sensor Network (WSN) consists of a base station (Sink) and a number of small, wireless electronic devices called sensor nodes. These nodes react to inputs from both the physical or environmental conditions of a monitored area, such as pressure, temperature, humidity, motion, light, etc [START_REF] Yick | Wireless sensor network survey[END_REF], and they cooperatively pass data through the network to the Sink for further processing. In recent years, efficient design of Wireless Sensor Networks has become a leading area of research for scientists. Several challenges needed to be addressed for a realistic implementation of WSNs, such as localization, deployment, coverage, data integrity, reliability, etc. All of these challenges are subject to many constraints that sometimes might be incompatible. However, the most important constraint is the limitation in energy resources.

Generally, wireless sensors are not connected to an electrical circuit that feeds them power. Instead, due to design constraints they rely on small, low powered batteries. Therefore, the optimal use of energy is the key solution for other challenges and to an extended operational lifetime of these networks.

In WSN, sensing and radio communication are considered to be the most expensive activities in term of energy consumption. Therefore, many approaches have been proposed in the literature to reduce the number of sampled data and the transmitted ones.

Due to the nature of WSNs, sensor data tend to change smoothly over time and it contains a significant chunk of redundant information. Therefore, to reduce the number of sampled data some researchers proposed several adaptive sampling techniques [START_REF] Silva | Litesense: An adaptive sensing scheme for wsns[END_REF][START_REF] Jon | Adaptive sampling in wireless sensor networks for air monitoring system[END_REF][START_REF] Yang | An interactive context-aware power management technique for optimizing sensor network lifetime[END_REF][START_REF] Makhoul | Data reduction in sensor networks: Performance evaluation in a real environment[END_REF][START_REF] Makhoul | Residual energy-based adaptive data collection approach for periodic sensor networks[END_REF][START_REF] Laiymani | Adaptive data collection approach for periodic sensor networks[END_REF] that dynamically increase or decrease the sampling rate of a sensor according to the level of variance between collected data over a certain period of time. This approach prevents the sensor from collecting redundant information. Thus, the sensing activity is reduced which in turn leads to a reduction in the transmission activity. Hence, less energy is consumed.

Instead of relying on adapted sampling rate to produce less transmissions, other approaches preferred to tackle the problem differently through a direct reduction of radio communication, since it consumes more energy than sensing. One of the most commonly used technique to limit data transmission is the dual prediction mechanism [START_REF] Jain | Adaptive stream resource management using kalman filters[END_REF][START_REF] Santini | An adaptive strategy for quality-based data reduction in wireless sensor networks[END_REF][START_REF] Ali | Approximate replication of data using adaptive filters in wireless sensor networks[END_REF][START_REF] Tan | Data reduction in wireless sensor networks: A hierarchical lms prediction approach[END_REF][START_REF] Raza | Practical data prediction for realworld wireless sensor networks[END_REF]. An identical prediction model is shared between each node and the Sink. This model is used to forecast future values. Thus, instead of transmitting all the collected data, a sensor transmits only the measurements that deviate from the predicted value by a threshold predefined by the user. Therefore, if the Sink does not receive any measurement at a given time, it acknowledges that the model's prediction is within the error budget.

Merging both adaptive sampling and dual prediction based transmission reduction into a single mechanism, can reduce energy consumption significantly compared with the approaches relying on either one of them.

In this paper we present an approach combining an adaptive sampling and a novel transmission reduction technique into a single energy efficient algorithm. Thus, our main contributions in this work can be summarized as follows:

• Proposing a new data transmission reduction algorithm that reduces the amount of data reported to the sink using a dual prediction model. In contrast to other similar techniques our model is light in term of computational cost and requires a very small memory footprint, yet it is robust and efficient.

• Coupling our novel transmission reduction algorithm with an adaptive sampling technique. Enabling the sensor to collect fewer measurements which in turn increase the efficiency of the transmission reduction algorithm and reduces the amount of energy consumed by the sensing activity.

• Conducting experiments on real sensor data and comparing our proposed method with a recent data reduction approach [START_REF] Monteiro | Dpcas: Data prediction with cubic adaptive sampling for wireless sensor networks[END_REF] based on a combination of a prediction model and an adaptive sampling technique. The final results demonstrates that our proposal outperforms the latter in reducing the overall energy consumption.

The rest of this paper is organized as follows. In section 2 the work related to data transmission reduction, adaptive sampling and approximate replication of sensor data is briefly presented. In section 3 the Kruskal-Wallis based algorithm that allows the sensor to adapt its sampling rate is explained. In section 4 our novel dual prediction based transmission reduction method is introduced. Section 5 explains how the adaptive sampling and transmission reduction techniques can be merged together. The obtained experimental results are shown in section 6. Finally, the paper is concluded in section 7.

Related Work

The elements of energy dissipation in a wireless sensor node that monitors a specific environment and report the collected information to a central workstation are very different [START_REF] Hill | System architecture directions for networked sensors[END_REF][START_REF] Raghunathan | Energy-aware wireless microsensor networks[END_REF]. However, in the monitoring stage, the micro-controller, sensor and radio components dominate the energy consumption and they are the main optimization targets.

In previous studies, authors studied several energy-saving schemes for wireless monitoring operations such as: data aggregation [START_REF] Bahi | A two tiers data aggregation scheme for periodic sensor networks[END_REF][START_REF] Du | A high efficient and real time data aggregation scheme for wsns[END_REF], data compression [START_REF] Wu | A holistic approach to reconstruct data in ocean sensor network using compression sensing[END_REF][START_REF] Basheer | Cluster-based quality-aware adaptive data compression for streaming data[END_REF], adaptive sampling [START_REF] Silva | Litesense: An adaptive sensing scheme for wsns[END_REF][START_REF] Jon | Adaptive sampling in wireless sensor networks for air monitoring system[END_REF][START_REF] Yang | An interactive context-aware power management technique for optimizing sensor network lifetime[END_REF][START_REF] Makhoul | Data reduction in sensor networks: Performance evaluation in a real environment[END_REF][START_REF] Makhoul | Residual energy-based adaptive data collection approach for periodic sensor networks[END_REF][START_REF] Laiymani | Adaptive data collection approach for periodic sensor networks[END_REF][START_REF] Harb | Energy-efficient sensor data collection approach for industrial process monitoring[END_REF] and data prediction [START_REF] Jain | Adaptive stream resource management using kalman filters[END_REF][START_REF] Santini | An adaptive strategy for quality-based data reduction in wireless sensor networks[END_REF][START_REF] Ali | Approximate replication of data using adaptive filters in wireless sensor networks[END_REF][START_REF] Tan | Data reduction in wireless sensor networks: A hierarchical lms prediction approach[END_REF][START_REF] Raza | Practical data prediction for realworld wireless sensor networks[END_REF][START_REF] Monteiro | Dpcas: Data prediction with cubic adaptive sampling for wireless sensor networks[END_REF].

Compression and Aggregation

The authors in [START_REF] Bahi | A two tiers data aggregation scheme for periodic sensor networks[END_REF], present a data reduction method called the Prefix-Frequency Filtering (PFF). In this approach, the first layer of data reduction is done locally on each sensor node, and a second layer of data reduction is done on a central node collecting data from neighboring nodes which is also referred to as "Aggregator". On the latter PFF uses Jaccard similarity to measure the correlation among reported measures from different nodes in order to merge and send them to the Sink. In [START_REF] Du | A high efficient and real time data aggregation scheme for wsns[END_REF] the Dynamical Message List Based Data Aggregation (DMLDA) technique is presented. This method is based on the data clustering technique and it provides a real time data aggregation. The backbone of this method is a special data structure named dynamical list. This list is deployed in every filtering node to store history messages before transmission. Thus, instead of using period delays, older messages are used to filter duplicated ones.

In [START_REF] Wu | A holistic approach to reconstruct data in ocean sensor network using compression sensing[END_REF] the authors uses raw signal processing and signal reconstruction to develop a reordering algorithm that resorts the sensor nodes at the Sink. This method enhances the sparsity of the signal by reducing the number of measurements needed for its reconstruction, consequently resulting in a low compression sampling rate that in turn scale down irrelevant communication traffic. The authors in [START_REF] Basheer | Cluster-based quality-aware adaptive data compression for streaming data[END_REF] proposed a cluster-based quality-aware adaptive data compression scheme, which takes into consideration the applications data quality and it also limits information loss by using adaptive clustering and novel coding algorithm.

Adaptive Sampling

In [START_REF] Jon | Adaptive sampling in wireless sensor networks for air monitoring system[END_REF] the amount of data is reduced by adapting the sampling rate for air pollution monitoring. The suggested work used the Kalman filter to remove noise from the sensed data. The algorithm adapts the period sampling based on the similarity between the current and the previous sensed data.

In [START_REF] Yang | An interactive context-aware power management technique for optimizing sensor network lifetime[END_REF] the sampling rate of the sensor node is adapted by taking into consideration both the system and the application context levels. For instance, the availability of the energy for harvesting represents the system context. This availability is the criteria used to set the maximum sampling rate for the node. The application context is represented by the user request, where feedback from the system executing specific rules of user or field scientist is used to set the rates of sensor node sampling in optimal way.

In [START_REF] Harb | Energy-efficient sensor data collection approach for industrial process monitoring[END_REF] the authors propose three different data collection and adaptive sampling techniques for Industrial Process Monitoring. The first one uses the ANOVA model, while the second one is based on sets similarity functions, and the third one on the distance functions.

Adaptive sampling techniques are remarkably efficient when the temporal correlation among collected data is high and the irregularity and sudden changes are low. In opposite conditions, where correlation is low and irregularity is high, these techniques perform poorly since the sampling rate will be kept at maximum most of the time. Thus, the computing cost will overcome the achieved reduction in sampling and transmission cost.

Prediction-based Data Reduction

In [START_REF] Raza | Practical data prediction for realworld wireless sensor networks[END_REF] the authors proposed a Derivative Based Prediction model (DBP) that is computed based on a learning window, containing m data points. The model is linear, computed as the slope d of the segment connecting the average values over the first and last l edge points at the beginning and end of the learning window.

In [START_REF] Monteiro | Dpcas: Data prediction with cubic adaptive sampling for wireless sensor networks[END_REF] the authors proposed a technique named Dual Prediction with Cubic adaptive sampling (DPCAS) that combines an exponential time series predictive model with a TCP CUBIC congestion adaptive sampling technique. Enabling the sensor node to reduce its sampling rate based on the produced prediction error. Moreover, measurements are transmitted to the sink only when a significant change in readings occur. The whole data set is then reproduced on the sink by interpolating the received measurements.

The authors in [START_REF] Jain | Adaptive stream resource management using kalman filters[END_REF] proposed a prediction model that is based on the Kalman filter. The same instance of this model is built by the Sink using historical data reported by the sensor and then is shared with the latter. The same model on both ends simultaneously performs linear predictions for future readings, enabling the sensor to transmit a measurement to the Sink only when the prediction is not accurate.

The dual Kalman filter method requires a priory knowledge and statistical data on the environment being monitored, in order to build the model. Therefore, the authors in [START_REF] Santini | An adaptive strategy for quality-based data reduction in wireless sensor networks[END_REF] proposed a dual prediction mechanism that is based on Least Mean Square (LMS) adaptive filter. LMS lends itself to be compact, light and requires no priory statistical knowledge of the data. Thus, it makes the prediction model more stable and adaptable with changes.

The authors in [START_REF] Ali | Approximate replication of data using adaptive filters in wireless sensor networks[END_REF] proposed to combine the LMS and Recursive Least Squares (RLS) adaptive filters in a single prediction model. Since the latter is able to achieve faster convergence and produces a prediction model that is more stable, RLS is used to build the prediction model. Once this model is built, the parameters are then passed to an LMS adaptive filter to perform predictions. The reason for this switch is that LMS has lower complexity, thus it suits the energy constraints of the sensor better than RLS.

In [START_REF] Tan | Data reduction in wireless sensor networks: A hierarchical lms prediction approach[END_REF] the authors proposed a dual prediction model that is based on the Hierarchical Least Mean Squares (HLMS) adaptive filter. The HLMS is a multi-level LMS filter, that makes a trade-off between increasing the complexity of LMS filter and having a better prediction filter.

The speed and the success of convergence of the adaptive filters is conditioned by some predefined parameters such as the "step size". A small alteration in these parameters can heavily affect the performance of these filters, and choosing an optimal value is not feasible most of the time, since it requires a training phase.

We propose in this paper to combine our adaptive sampling technique [START_REF] Makhoul | Data reduction in sensor networks: Performance evaluation in a real environment[END_REF] with our novel dual prediction based forecasting model that is free from any parameters limiting its performance and which only requires two measurements to be built and one measurement to be updated. Targeting at the same time the two most energy consuming activities in WSNs, in order to preserve as much energy as possible.

In the following sections, adaptive sampling and data transmission reduction techniques are explained. Then an algorithm merging these two approaches together is presented.

Adaptive Sampling

First of all let us begin by explaining the Kruskal-Wallis statistic model. It forms the skeleton of the adaptive sampling algorithm aiming to reduce the number of data sampled by each sensor.

The Kruskal-Wallis Statistic Model

The Kruskal-Wallis test [START_REF] Mckight | Kruskal-wallis test[END_REF] takes as input a group of data sets to identify whether there is a difference between at least two of these sets. To understand how this test works and how it could help us to reduce the sampling rate of a sensor, we give the following illustrative example that explains its functionality and applicability in WSNs.

Illustrative example

Let us consider that a sensor operates in rounds, where each round consists of p periods. To simplify the example, let us assume that p is equal to two. Table 1 shows a set of measurements collected by a sensor during two consecutive periods.

The first step is to order the measurements in both periods by increasing order of their values and assign a rank denoted r to each one of them, representing its position in the ordered list. However, two or more measurements could have the same value. In this case the mean value of their ranks is calculated and assigned to each one of them. For instance, in Table 1 the value 7.0 is repeated twice, both in period 1 and 2 with ranks 5 and 6 respectively. The mean value of both ranks is 5.5. Thus, the ranks of both measurements holding the value 7.0 are replaced by 5.5.

The second step is to pass the ranked measurements as input to the Kruskal-Wallis test in order to find which one of the following assumptions is correct: • Assumption 1: the two groups of data (measurements in period 1 and 2) are significantly different.

• Assumption 2: the difference between the two groups of data is not significant.

The test is conducted by calculating the following formula :

H = 12 N × (N + 1) p i=1 r 2 i n i -3 × (N + 1) (1)
where:

• N is the total number of measurements in all periods.

• n i is the number of measurements inside the i th period.

• r i is the sum of all ranks in the i th period.

Using the data in Table 1 and based on equation ( 1), H is calculated as follows:

H = 12 13 × (13 + 1) ( 39 2 6 + 52 2 7 ) -3 × (13 + 1) = 0.183
Finally, to check which assumption is the correct one, the result of this formula is compared with a "difference value" denoted H t . H t varies according to the false rejection probability predefined by the user, denoted α. The relation between α and H t can be found in the chi -square Table . The risk α is defined in a statistical test as the risk of rejecting the Null hypothesis when in fact it is true, it is also known as Type I error. This risk is stated in terms of probability (such as 0.05 or 5%). It corresponds to the confidence level of a statistical test, so a level of significance α = 0.05 corresponds to a 95% confidence level. In our approach it is the probability that a sensor node find a high variance between its collected data while in reality there is no variances and it should adapt the sampling rate. Therefore, when α decreases the value of H t increases and then the condition H < H t becomes more difficult to be satisfied. Consequently, the sampling rate increases when α decreases.

Let us assume α = 0.05, for this value of α, H t is equal to 5.991. Comparing the results of the previous equation we notice that H < H t (0.183 < 5.991). Therefore, the first assumption is accepted. Hence, the sampling rate must be adapted.

The Behavior curve function

Based on the Kruskal-Wallis test, when a node notices high variance differences, it increases its sampling rate in order to prevent missing important measurements and decreases its sampling rate when the variance is less than the threshold H t . Following the example above low variance was detected, since H < H t .

To compute the sampling rate of the sensor a behavior function (BV) is used, taking as input the risk of the application denoted R, or in other words, how important the quality of data is to the end user. This BV function is expressed by a Bezier curve that passes through three points as shown in Figure 1: (0,0), (H t , Maximum Sampling Rate), and R.

Transmission reduction

To transmit the collected data to the base station, the network involves a large number of radio operations, including listening to the channels, receiving and transmitting data. Since the main part of energy dissipation in wireless sensors is indeed the radio components, the lifetime of the network can be extended significantly if we optimize the radio communication operations.

The data in WSN are defined as time series, since they are sequential data points collected over successive time. Such data is generally affected by three main factors: Trend, Cyclical and Irregular factors. As brief description of these factors, time series in general tend to increase, decrease or stand still over a long period of time, this tendency is usually called "a Trend". For example, the temperature of a room tend to have an increasing trend, from when the sun rises until it starts to set. Cyclic variations can be seen during a longer period of monitoring. For instance, the same cycle of increase and decrease in the temperature takes place every day. Finally, irregular factors are variations caused by unpredictable influences, such as clouds covering the skies during the day and suddenly reducing the temperature or dimming the light.

Therefore, since time series data follows a specific trend and tend to change smoothly over time, one can forecast future measurements by observing past patterns. In the light of this, we propose a dual prediction based reporting mechanism to conserve energy and maximize the lifetime of the network. Let us first begin by explaining the concept of the dual-prediction mechanism.

Dual-Prediction Mechanism (DPM)

The Dual-Prediction Mechanism is a model that analyzes the history of previously collected information, extract the moving trend of data in order to approximately estimate future readings. In the DPM, the same prediction model is deployed at both the sensor nodes and the base station. Using the same historical data, sensor nodes and the base station regularly make the same prediction of any future observation. This technique allows the sensor nodes to avoid transmitting its sensed data to the base station, as long as the predictions match the readings.

Meanwhile, the base station always presume that its prediction reflects the real observation, unless it receives the corrections from the sensor node (since the sensor can compare the prediction with the real sensed measurement). Figure 2. illustrates in a simplified way how this mechanism work.

Transmission reduction method based on DPM

As mentioned previously, the prediction model is built using historical measurements collected by the concerned sensor. The number of these measurements depends on the type of the chosen prediction model. Different types of prediction models has been proposed in the literature [START_REF] Jain | Adaptive stream resource management using kalman filters[END_REF][START_REF] Santini | An adaptive strategy for quality-based data reduction in wireless sensor networks[END_REF][START_REF] Ali | Approximate replication of data using adaptive filters in wireless sensor networks[END_REF][START_REF] Tan | Data reduction in wireless sensor networks: A hierarchical lms prediction approach[END_REF][START_REF] Raza | Practical data prediction for realworld wireless sensor networks[END_REF], where the number of data needed to train the model can vary from tens to hundred even thousands of reading depending on its learning capacity. In our method, only two measurements are sufficient to build the prediction model, and a single measurement to correct it.

At the beginning, the sensor collects and sends to the Sink the two first measurements x[0] and x [START_REF] Yick | Wireless sensor network survey[END_REF] at time t 0 and t 1 . Each time the sink receives a new measurements it stores in its memory the value of this measurement and the time when it was received. Let us denote the newly received value as N R and the time when it is received as t nr . Subsequently, both the sensor and the sink calculate simultaneously the difference between these two measurements denoted d, as shown in the equation [START_REF] Silva | Litesense: An adaptive sensing scheme for wsns[END_REF].

d[0] = x[1] -x[0] (2)
Once the difference is calculated, the sensor and the Sink switches to the prediction phase, where they both assume that the difference between any two successive measurements will always be equal to d[0]. Based on the fact that time series data tend to change smoothly over time and the values of measurements at neighboring time ticks, are usually very close to each other. Therefore, as shown in equation (3), to predict x[k], the value of the measurement x[k] at time t k , both the sensor and the sink adds d[0] to x[k-1] which is the predicted measurement at time t (k-1) .

x

[k] = x[k -1] + d[0] (3)
Afterward, the sensor compares the predicted value x[k] to the real sensed measurement x[k]. If the difference between them does not exceed an error threshold emax predefined by the user, the real reading is discarded and not transmitted to the Sink. Meanwhile, when the Sink does not receive anything, it assumes that its prediction is within the error threshold.

Oppositely, if the prediction does not respect the error budget, the sensor discards it and transmits to the Sink the real reading, which we will refer to as "correction packet". Once the Sink receives the packet, they both update the value of d, by subtracting N R from the correction value x[k] and dividing the result by the time difference between the reception of these tow measurements, as shown in the equation [START_REF] Yang | An interactive context-aware power management technique for optimizing sensor network lifetime[END_REF]. And once again to keep track of the last received value for potential future update, the old value of N R is replaced in the memory by the newly received measurement

x[k]. d[k] = x[k] -N R t k -t nr (4)
In other words, d represents an estimated linear change rate of future readings, for a certain period of time. Moreover, as mentioned earlier, time series data usually have an increase, stand still and decrease cycle, especially when measuring environmental features, such as temperature, humidity, light etc. Thus, to harmonize the prediction line with the real data curve, d is multiplied by a rectification value denoted β ∈ [0, 1].

Accordingly, the predicted value is calculated using equation ( 5) instead of equation ( 3).

x

[k] = x[k -1] + d[k] × β (5)
The algorithm 1 illustrates the functioning of our method.

Algorithm 1 Transmission reduction.

1: Read x 0 and x 1 2: Transmit x 0 and x 1 to Sink

3: d[0] ← x 1 -x 0 4: N R ← x 1 5: t nr = t 1 6: while Energy = 0 do 7:
Read x t at time t x 8: N R ← x t 13:

x t ← x t-1 + d × β 9: if |x t -x t | ≥ emax
t nr ← t x 14:

x t ← x t 15:

end if 16: end while

Merging Adaptive Sampling and DPM based Transmission reduction

The Adaptive Sampling algorithm (AS) reduces the sampling rate of a sensor when the difference between collected measurements is not significant. Thus, enabling the sensor node to avoid collecting redundant and superfluous information. The Transmission Reduction algorithm (TR) reduces the number of data transmitted to the Sink, using a prediction model that can forecast future measurements within a narrow error range. The efficiency of the prediction model is at peak when data is smoothly changing with low variance between measurements.

Thus, one can notice that these two techniques are compatible. First their work does not overlap and they do not affect each other's results. Secondly, the prediction model is capable of filling the gap of "non collected data", since as mentioned before these measurements are mostly redundant or roughly similar to closely collected ones, and the prediction model efficiency is at maximum when the change in values is smooth and slow. Therefore, on one hand the sampling rate is reduced and on the other hand, the end user will still have access to the complete set of data. Finally the complexity of the transmission reduction algorithm is extremely low. Thus, when combined with the adaptive sampling algorithm the overall complexity will remain unchanged. Therefore, we propose to combine these two techniques into a single algorithm, enabling us to achieve lower energy consumption compared to each one of them when implemented solely.

Let us begin by explaining how to combine these two techniques together, and how the algorithm works as a whole. As mentioned earlier, the operations conducted by AS and TR does not overlap, and they do not affect the results of each others. Therefore, since they are totally compatible they can be implemented as they are originally without any changes in the way of working.

The only difference is, instead of having a single sampling rate, the sensor has two: a real one and a hypothetical one. The real sampling rate is the rate defined by the AS algorithm after each round. The hypothetical one is a fixed rate that is always equal to the maximum sampling rate. The sensor collects measurements at the real rate speed returned by AS. However, it uses the hypothetical rate while applying the TR algorithm. In other words, let us suppose for a round ro, the real rate is RR measures/period and the hypothetical rate is HR measures/period. In this case, during this period, on one hand the sensor collects RR measurements, on the other hand it predicts HR measurements. Note that RR is always less than HR, as HR is equal to the maximum sampling rate allowed for the sensor. Thus, the sensor is able to predict the "non collected" measurements caused by a slowed down sampling rate forced by AS.

Figure 3 gives an illustrative example on how this algorithm behave.

X1, X2, X3, X4, X5 X6, X7, X8, X9, X10, X11, X12 X13, X14, X15 X16, X17, X18, …..

Raw Data

X1, X2, X3, X4, X5

Sampled Data

X6, X9, X12 X13 X16, X17, X18, ….. 𝑥1 , 𝑥2, 𝑥3, 𝑥4 𝑥5 𝑥6, 𝑥7 𝑥8 , 𝑥9, 𝑥10, 𝑥11, 𝑥12, 𝑥13, 𝑥14 𝑥15 𝑥16, 𝑥17, 𝑥18, ….. We have explained in section 4.2 that every time a sensor predicts a new measurement it must compare it with the real sensed value in order to decide whether it should send it to the Sink or not. However, when adding AS to the equation, if RR is ≤ HR some predictions might not have a matching sensed measurements to validate its accuracy. Therefore, these predictions are considered to be within the error budget automatically. Since the "non collected" measurements are assumed to be redundant or already similar to collected neighboring measures. This assumption should not affect the accuracy of replicated data. However, we discuss this issue in the Experimental Results section below.

Experimental Results

In this section, we present the experimentation we have conducted on real wireless sensor readings, collected by twenty Crossbow TesloB nodes deployed in our laboratory as shown in Figure 4. The walls separating the rooms of the lab are of a thickness of 8 cm. Each one of the twenty nodes collects five environmental features: temperature, humidity, light, infrared and voltage. The collected measurements are directly transmitted to a central node (Sink) called SG1000 [START_REF]advanticsys[END_REF], connected to a laptop machine, through a star topology. We have chosen to test our approach on temperature, humidity, and infrared data since the variation in measured values for each one of them is different. For instance, the variation in temperature data is low, medium for humidity, and high for infrared. Thus, we can assess the efficiency of our approach on different scenarios. The simulation was conducted on twenty sets of 300,000 readings each (100,000 temperature, 100,000 humidity, and 100,000 infrared readings), which is equivalent to approximately 35 days of non-stop data collection. Since the effectiveness of these algorithms depends on the variation of the data being collected and can greatly differ from one node to another. The setup parameters for this experimentation are shown in table 2.

Transmission reduction

To test the effectiveness of our transmission reduction method compared to DPCAS. We have simulated both methods on the same sets of data using Matlab. The error threshold "emax" was set to ±0.1 for temperature and humidity, and ±1 for infrared. shows a comparison between the amount of temperature, humidity, and infrared data that have been transmitted to the sink when both DPCAS and AS+TR were implemented. For instance, On average, only 193 temperature readings or 0.193% were transmitted when our algorithm was implemented. When DPCAS is used, the number of data transmitted increased slightly to 714 (0.714%).

For humidity and infrared, the results were identical, our method outperformed DPCAS in reducing the number transmissions. The average amount of transmitted humidity and infrared data for AS+TR is 6148 and 5528 respectively. As for DPCAS the numbers increase to 13964 and 15848 respectively. Hence, these results show that our transmission reduction method is better at reducing radio communication, which enables the node to preserve more of its energy resources.

Adaptive Sampling

By looking at figure 8, 9 and 10, it is clear that DPCAS has the upper hand when it comes to reducing the sensing activity. Since the latter decreases gradually the sampling rate after each sample. However, AS decreases it only at the end of each period (after 50 samples in this experiment). The average amount of temperature, humidity and infrared data sampled by DPCAS are 16688, 26643 and 15847 respectively. As for AS+TR the numbers increase to 77731, 83873 and 46247 respectively. Hence, DPCAS outperforms our adaptive sampling algorithm in reducing the amount of sampled data and the energy consumed by the sensor board.

Energy consumption

It was shown that about 3000 instructions could be executed for the same energy cost as sending a bit for 100 meters by radio [START_REF] Pottie | Wireless integrated network sensors[END_REF]. Therefore, to compare the amount of energy consumed by each method, we neglected the cost of computing operations by considering that both algorithms have the same computation complexity. We focused only on the cost of radio transmission and data sensing. In order to calculate the energy consumed by a sensor node we used the energy consumption model in [START_REF] Liang | Minimizing energy consumptions in wireless sensor networks via two-modal transmission[END_REF]. The previous results demonstrated that on one hand, our method transmits less data to the sink. Therefore, the energy consumed by the radio component is less when compared to DPCAS. On the other hand, the latter samples fewer data. Therefore, the energy consumed by the sensor board is lower when compared to ours.

The amount of energy consumed by the sensor board is significantly smaller than the one consumed by the radio component. Therefore, the greater is the difference between the amount of data transmitted by each algorithm, the harder is for DPCAS to compensate the energy consumed by transmission with less sampling energy.

Figure 11, 12 and, 13 are a great proof for this assumption. The difference between the amount of temperature data transmitted by DPCAS and AS+TR is negligible, and large between the amount of sensed data. Consequently, the energy consumed by the sensor board will impact greatly the overall energy consumption calculation, which gave DPCAS the lead. However, when the gap between the number of transmissions grows bigger, as it is the case for humidity and infrared data. The energy consumed by the sensing activity will have a minor impact on the overall energy consumption calculation. Therefore, the total energy consumed by AS+TR for humidity and infrared data is smaller for the majority of the nodes.

Quality of replicated data

Data quality is a very important factor in WSNs, since the end user depends on it to make appropriate decisions. Accuracy, precision, completeness, and consistency are the attributes that measure the quality of data.

When we reduce the sampling rate within a certain period, we risk missing sudden variations in measurements. Thus, the estimation of these irregular non sampled data may exceed the desired error threshold. To study the impact of the adaptive sampling algorithms on the integrity of the replicated data we compare the estimated measurements with its corresponding raw data collected by the sensor node, and we calculate the values of 4 quality metrics: Mean Absolute Error (MAE), Mean Absolute Percentage Error (MAPE), Mean Square Error (MSE), Root Mean Square Error (RMSE). The lower the values of these metrics the better are the results. 14, 15, and 16 shows a comparison between the quality metrics for each set of data of the three environmental features. For temperature data, both algorithms are neck to neck. However, AS+TR has a clear superiority for humidity and Infrared. Since Infrared contains 0 elements the value of MPAE cannot be computed. As for MSE in order to keep figure 16 simple an comprehensible, instead of plotting the curve we provide the average values which are 2.49 and 2.72 for AS+TR and DPCAS respectively.

Adaptive sampling makes a trade-off between data quality and the amount of sampled measurements, to deliver a minimum amount of readings while satisfying quality requirements of the application. Thus, the integrity of data depends on how tolerant is the end user to the error in replications. The obtained results demonstrated that our method was able to reproduce the whole data set with less error and better quality compared with DPCAS.

Conclusion

In this research work, we proposed an energy-efficient data reduction method for Wireless Sensor Networks based on a combination of the adaptive sampling and dual prediction mechanism techniques. The former, allows the sensor to adapt its sampling rate according to the variance in data. Thus, the sensor samples relevant data only and avoids the sampling of redundant and insignificant information. The latter enables the Sink to estimate the collected data through a prediction mechanism that is shared with the sensor node. Thus, Instead of transmitting all the readings, the sensor report to the Sink a measurement only when the estimation exceeds a predefined error threshold. By merging these two techniques together, we were able to reduce radio communication and data sensing at the same time. Since these two activities are considered to consume most of the energy resources, we were able to preserve a great amount of energy and extend the lifetime of the network significantly compared with another similar technique.

For future work, we plan on improving our adaptive sampling technique in order to reduce the risk of losing important information and increase the quality of the replicated data.

Acknowledgement

This work is partially funded by the Labex ACTION program (contract ANR-11-LABX-01-01), the France-Suisse Interreg RESponSE project and Lebanese University research program (Number: 4/6132).

Figure 1 :

 1 Figure 1: Sampling rate adaptation using the Behavior function.

Figure 2 :

 2 Figure 2: The concept of DPM

  then

Figure 3 :

 3 Figure 3: Illustrative example of our method (AS+TR)

Figure 4 :

 4 Figure 4: Deployment of the sensor network

Figure 5 :Figure 6 :

 56 Figure 5: Amount of temperature data transmitted to the Sink

Figure 7 :Figure 8 :Figure 9 :Figure 10 :

 78910 Figure 7: Amount of infrared data transmitted to the Sink

Figure 13 :

 13 Figure 11: Energy consumption comparison for temperature data

Figure 15 :Figure 16 :

 1516 Figure 15: Quality metrics comparison for replicated humidity data

Figure

  Figure 14,[START_REF] Raghunathan | Energy-aware wireless microsensor networks[END_REF][START_REF] Bahi | A two tiers data aggregation scheme for periodic sensor networks[END_REF] shows a comparison between the quality metrics for each set of data of the three environmental features. For temperature data, both algorithms are neck to neck. However, AS+TR has a clear superiority for humidity and Infrared. Since Infrared contains 0 elements the value of MPAE cannot be computed. As for MSE in order to keep figure16simple an comprehensible, instead of plotting the curve we provide the average values which are 2.49 and 2.72 for AS+TR and DPCAS respectively.Adaptive sampling makes a trade-off between data quality and the amount of sampled measurements, to deliver a minimum amount of readings while satisfying quality requirements of the application. Thus, the integrity of data depends on how tolerant is the end user to the error in replications. The obtained results demonstrated that our method was able to reproduce the whole data set with less error and better quality compared with DPCAS.

Table 1 :

 1 Example of collected measures

	Raw Measures	Measures Rankings
	Period 1 Period 2	Period 1 Period 2
	3.4	4.6	1	2
	6.2	5.8	4	3
	7.0	7.0	¡ 5 5.5	¡ 6 5.5
	7.3	7.5	7	8
	7.6	8.0	9	10
	10.3	10.2	& & 12 12.5	11
		10.3		& & 13 12.5
	Number of Measures	Sum of Rankings
	6	7	39	52

Table 2 :

 2 setup parameters

	DPCAS		AS+TR
	Smin	310 sec	Smin	310 sec
	Smax	31 sec	Smax	31 sec
	smoothing coefficient α & multiplicative reduction factor β	0.2	Risk R	0.6
	cubic parameter C	0.4	Rejection Probability α	0.05
	Figures 5, 6 and 7


Karthikeyan Bhargavan
email: karthikeyan.bhargavan@inria.fr

Antoine Delignat-Lavaud

Nadim Kobeissi
email: nadim.kobeissi@inria.fr

Formal Modeling and Verification for Domain Validation and ACME

Web traffic encryption has shifted from applying only to sensitive websites (such as banks) to a majority of all Web requests. Until recently, one of the main limiting factors for enabling HTTPS was the requirement to obtain a valid certificate from a trusted certification authority. This process traditionally involves steps such as paying a certificate issuance fee, ad-hoc private key and certificate request generation, and domain validation procedures. To remove this barrier of entry, the Internet Security Research Group (ISRG) introduced "Let's Encrypt", a new non-profit certificate authority that uses a new protocol called Automatic Certificate Management Environment (ACME) to automate certificate management at all levels (request, validation, issuance, renewal, and revocation) between clients (website operators) and servers (certificate authority nodes). Let's Encrypt's success is measured by its issuance of over 27 million free certificates since its launch in April 2016. In this paper, we survey the existing process for issuing domain-validated certificates in major certification authorities. Based on our findings, we build a security model of domain-validated certificate issuance. We then model the ACME protocol in the applied pi-calculus and verify its stated security goals against our security model. We compare the effective security of different domain validation methods and show that ACME can be secure under a stronger threat model than that of traditional CAs. We also uncover weaknesses in some flows of ACME 1.0 and propose verified improvements that have been adopted in the latest protocol draft submitted to the IETF.

Introduction

Since the dawn of HTTPS, being able to secure a public website with SSL or TLS requires obtaining a signature for the website's public certificate from a certificate authority [START_REF] Chokhani | Internet X.509 Public Key Infrastructure: Certificate Policy and Certification Practices Framework[END_REF] (CA). All major operating system and browser vendors maintain lists of trusted CAs (represented by their root certificates) that can legitimately attest for a reasonable link between a certificate and the identity of the server or domain it claims to represent.

For example, all major operating systems and browsers include and trust Symantec's root certificates, which allows Alice to ask Symantec to attest that the certificate she uses on her website AliceShop.com has indeed been issued to her, rather than to an attacker trying to impersonate her website. After Alice pays Symantec some verification fee, Symantec performs some check to verify that Alice and her web server indeed have the authority over AliceShop.com. If successful, Symantec then signs a certificate intended for that domain. Since the aforementioned operating systems already trust Symantec, this trust now extends towards Alice's certificate being representative of AliceShop.com.

The security of this trust model has always relied on the responsibility and trustworthiness of the CAs themselves, since a single malicious CA can issue arbitrary valid certificates for any website on the Internet. Each certificate authority is free to engineer different user sign-up, domain validation, certificate issuance and certificate renewal protocols of its own design. Since these ad-hoc protocols often operate over weak channels such as HTTP and DNS without strong cryptographic authentication of entities, most of them can be considered secure only under relatively weak threat models, reducing user credentials to a web login and domain validation to an email exchange.

The main guidelines controlling what type of domain validation CAs are allowed to apply are the recommendations in the CA/Browser Forum Baseline Requirements [START_REF]Baseline requirements for the issuance and management of policy-trusted certificates[END_REF]. These requirements, which are adopted by ballot vote between the participating organizations, cover the definition of common notions such as domain common names (CNs), registration authorities (RAs) and differences between regular domain validation (DV) and extended validation (EV).

These guidelines have not proven sufficient for a well-regulated and well specified approach for domain validation: Mozilla was recently forced to remove WoSign [START_REF] Markham | Wosign and startcom[END_REF] (and its subsidiary StartSSL, both major certificate authorities) from the certificate store of Firefox and all other Mozilla products due to a series of documented instances that range from the CA intentionally ignoring security best-practices for certificate issuance, to vulnerabilities allowing attackers to obtain signed certificates for arbitrary unauthorized websites.

The lack of a standardized protocol operating under a well-defined threat model and with clear security goals for certificate issuance has so far prevented a systematic treatment of certificate issuance using well-established formal methods. Instead, academic efforts to improve PKI security focus on measurement studies [START_REF] Olivier Levillain | One year of SSL Internet measurement[END_REF][START_REF] Delignat-Lavaud | Web pki: Closing the gap between guidelines and practices[END_REF] and transparency and public auditability mechanisms [6,[START_REF] Basin | Arpki: Attack resilient public-key infrastructure[END_REF] for already-issued certificates.

In 2015, a consortium of high-profile organizations including Mozilla and the Electronic Frontier Foundation launched "Let's Encrypt" [START_REF]Let's encrypt overview[END_REF], a non-profit effort to specify, standardize and automate certificate issuance between web servers and certificate authorities and to provide certificate issuance itself as a free-ofcharge service. Since its launch in April 2016, Let's Encrypt has issued more than 27 million certificates [START_REF]Let's encrypt statistics[END_REF] and has been linked to a general increase in HTTPS adoption across the Internet.

Let's Encrypt also introduces ACME [START_REF] Barnes | Automatic certificate management environment (acme)[END_REF], an automated domain validation and certificate issuance protocol that gives us for the first time a protocol that can act as a credible target for formal verification in the context of domain vali-dation. ACME also removes almost entirely the human element from the process of domain validation: the subsequently automated validation and issuance of millions of certificates further increases the necessity of a formal approach to the protocol involved.

In this paper, we formally specify, model and verify ACME using ProVerif. Against a classic symbolic protocol adversary, ACME achieves most of its stated security goals. Notably, we show that ACME's design allows it to resist a substantially stronger threat model than the ad-hoc protocols of traditional CAs that rely on bearer tokens (passwords, cookies, authorization strings) for authentication and domain validation, thanks to its stronger cryptographic credentials and to the binding between the clients identity and the validated domain.

Nevertheless

Current State of Domain Validation

A goal of this work is to establish a relationship between current domain validation practices in the real world and a more formal threat model on which we base our security results. We begin by taking a closer look into the network infrastructure, user authentication and domain validation protocols currently in use by traditional CAs.

Our panel of surveyed CA is selected from the data set of Delignat-Lavaud et al. [START_REF] Delignat-Lavaud | Web pki: Closing the gap between guidelines and practices[END_REF], which uses machine learning to classify certificates issued by domain validation. Our CA panel covers about 85% of the collected domain validated certificates from 2014, which is consistent with the January 2015 market share data from the Netcraft SSL survey3 . For each CA, we obtain a regular one year, single-domain certificate signature for a domain name that we own. §3.2.2.4 of the CA/Browser Forum's Baseline Requirements allow for domain validation to occur in ten different ways, including over postal mail. Of these methods, only three are in popular use: validation via email, the setting of an arbitrary DNS record, or serving some HTTP value on the target domain.

Domain Validation Mechanisms

With ad-hoc CAs, user C authenticates its identity C pk to CA A as a simple username/password web login, with an option for account recovery via email. C can then request that A validate some domain C w ⊂ C ⋆ , where C ⋆ w is the set of all domain names that C controls. A's flow with the various domain validation channels proceeds thus:

-HTTP Identifier A sends to C a nonce A N C via an HTTPS channel that C must then advertise at some agreed-upon location under C w . A then accesses C w using an unauthenticated, unencrypted HTTP connection to ensure that it can retrieve A N C . This identifier depends both on honest DNS resolution of the validated domain's A/A6 records and an untampered HTTP connection to the domain.

In practice, we find that CAs that allow HTTP identifiers require the nonce to be written on a text file with a long random name in the root of the validated domain. In practice, we observe that CAs use dangerous heuristics to generate a list of possible E C that C can pick from: first, they presume that any email addresses that appear in the WHOIS records of C w is controlled by C. A large majority of registrars provide WHOIS privacy services to defend against spam. Such services can easily obtain certificates for any of their customers' domains as validation email transit through their mail servers. Second, CAs' heuristics include generic names such as postmaster, webmaster, or admin.

If the validated domain provides an email service for which users may chose their username, an attacker may register under one of those generic names and obtain a unauthorized certificate. Such attacks have been carried successfully in the past against public email services such as Hotmail.

Once one of the above identifiers succeeds in validating C's ownership of C w to A, A issues the certificate and the protocol ends.

User Authentication and Domain Validation

CA Identifiers Email Recovery

Public Key Auth.

Per-CSR Check AlphaSSL

Email N/A

Comodo PositiveSSL Email

DigiCert Email

GeoTrust QuickSSL Email

GlobalSign

HTTP, DNS, Email

GoDaddy SSL HTTP, DNS

Let's Encrypt (ACME draft-1)

HTTP

Network Solutions Email

RapidSSL Email

SSL.com BasicSSL HTTP, DNS, Email N/A

StartCom StartSSL Email

Fig. 1: Popular CAs, their validation methods, whether they permit account recovery via email, whether they allow login via a public-key based approach (such as client certificates) and whether domain validation is carried out once for every certificate request, even for already-validated domain names.

While CAs are required to document their certificate issuance policies in Certificate Practice Statements [11][12][13][START_REF] Globalsign | GlobalSign CA Certification Practice Statement[END_REF][15][16][START_REF]StartCom Certificate Policy and Practice Statements[END_REF][18], we find that these statements are not always accurate or complete (for instance, they typically provision for validation methods that are not offered in practice; the address heuristics for email-based validation is rarely listed exhaustively). Most ad-hoc CAs in our study favor email-based validation. Unlike HTTP and DNS identifiers, email identifiers effectively rely on a read capability challenge instead write access proof for C. In §3, we discuss how email identifiers are the weakest available form of identification given our threat model. In §4, we elaborate on a weakness in ACME affecting both account recovery and domain validation. While this weakness is also generalizable to traditional certificate authorities, ACME offers an opportunity for a stronger fix.

None of CAs we surveyed offers a login mechanism that is completely independent of email. An exception almost occurs with StartSSL, which supports browser-generated X.509 client certificates for web login, but this exception is negated by the email-based account recovery in case of a lost certificate private key. Reliance on the security of the email channel can in many cases be even more serious: in many surveyed CAs, simply being able to complete a web login enables user to re-issue certificates for domains they had already validated before, without further validation.

A scan of the DNS MX and NS records of the web's top 10,000 websites (according to Alexa.com) [START_REF][END_REF] showed that roughly 45% of surveyed domain names used only six DNS providers, of which CloudFlare alone had a 18% share. 4 A similar centralization of authority exists with email, where the top six providers serve more than 55% of domain names surveyed, with Google alone holding roughly 27% market share (Figure 2.)

These results suggest that the number of actors of which the compromise could affect traditional domain validation is significantly small. This is relevant given how top CAs allow for account recovery, certificate re-issuance and more with simple email-based validation.

A Security Model for Domain Validation

The protocols considered in this work operate between a party C claiming to serve and represent one or more domain names C w (for which it wants certificates) and it is incumbent upon a certificate issuer A to verify that all domains in C w are indeed controlled and managed by C. User C authenticates itself to the certificate authority A using a public key C pk corresponding to the private signing key C k . C can then link identifiers under C k that prove that it manages and controls domains in C w . This and following sections are largely based on our full symbolic model5 of ACME and ad-hoc CA protocol and network flow, which is written in the applied pi calculus and verified using ProVerif. Excerpts of this model are inlined throughout.

Security Goals and Threat Model

Our security goals are straightforward: for any domain C w ∈ C, A must not sign a certificate asserting C's ownership of C w for that domain unless C can validate C pk as representing the identity that owns and manages this domain. ACME allows C to validate C w with respect to C pk by using the secret value C k in order to demonstrate either read or write capabilities on certain predefined network channels, each with its own security model. A domain name C w is considered validated under C w if C k can be used to complete a verification challenge on one of the network channels offered by the ACME protocol between C and A that in consequence asserts a relationship between C pk and C w .

The network topology, channels and actors are essentially the same for both ACME and ad-hoc CAs. However, the manner in which these actors communicate over the channels is different and leads to different attempts to establish the same security guarantees. A shared consideration between ACME and ad-hoc CAs involves the critical importance of DNS resolution: if the attacker can simply produce false DNS responses for A resolving a domain request for any domain in C w , it becomes impossible to safely carry out domain validation under any circumstances. As a sidenote, this allows us to argue that since the DNS channel must be trusted, it could also be considered as the safest channel on which to carry out domain validation using DNS Identifiers since that would allow C to avoid needlessly involving other channels.

Channels

In formally describing our network model in ProVerif, we simulate simultaneous requests from Alice, Bob and Mallory as independent clients C. Alice and Bob both act as honest clients, while Mallory acts as a compromised participant client. All three follow the same protocol top-level process. We also simulate two independent ACME CAs, which interchangeably assume the role of A. For each C, we specify a triple of distinct channels:

(C HT T P , C EM AIL , C DN ST XT )
Each channel represents access to a different domain validation mechanism. While C is given complete access over these channels, C EM AIL is only handed to A after being applied through a "write transformation" which returns a variant of the channel that is effectively write-only:

w(channel) → channel
Similarly, a "read transformation" r(channel) → channel is applied to C HT T P and C DN ST XT .

A routing proxy is then specified in order to model the transportation across these channels by executing the following unbounded processes in parallel 6 : in(w(C EM AIL ), x); out(r(C EM AIL ), x) in(pub, x); out(r(C EM AIL ), x) in(w(C HT T P ), x); out(pub, x); out(r(C HT T P ), x) in(w(C DN ST XT ), x); out(pub, x); out(r(C DN ST XT ), x) Threat Model We assume that the adversary controls parts of the network and so can intercept, tamper with and inject network messages. As such, an attacker could make requests for domains they do not own, intercept and delay legitimate certificate requests and so on. Our adversary has full access to pub, w(C EM AIL ), r(C HT T P ) and r(C DN ST XT ). We also publish Mallory's channels and C k over pub. As such, the attacker controls a set of valid participants (e.g. M ) with their own valid identities (e.g. M k , M pk ). The attacker may advertise any identity for its controlled principals, including false identities and may attempt to obtain a certificate for domains not legitimately under M w .

The adversary also has at his disposal certain special functions:

-PoisonDnsARecord, which takes in a domain C w and allows the attacker to poison its DNS records to redirect to a server owned by M . Calling this function triggers the ActiveDnsAttack(C w ) event.

-ManInTheMiddleHttp, which allows the attacker to write arbitrary HTTP requests as if they were emitting from C HT T P by disclosing C HT T P to the attacker. Calling this function triggers the ActiveHttpAttack(C w ) event.

ProVerif Events and Queries

Under ProVerif, queries under our symbolic model are constructed from sequences of the following events, each callable by a particular type of actor:

-Client The client is allowed to assert that they own some domain by triggering the event Owner(C, C w ). Once C receives a certificate C wcert for C w from A, they also trigger CertReceived(C w , C wcert , C pk , A pk ) -Server The server (ACME instance or CA) triggers the event HttpAuth(C pk , C w ), DnsAuth(C pk , C w ) and EmailAuth(C pk , C w ) depending on the type of domain validation used. Once A issues a certificate C wcert for C w to C, they also trigger CertIssued(C w , C wcert , C pk , A pk ) -Adversary As noted above, the adversary may trigger the events ActiveDnsAttack(C w )

and ActiveHttpAttack(C w ). In addition, the adversary is allowed to masquerade as M in order assert that they own some domain by triggering the event Owner(M pk , C w ).

Queries Queries encode the security properties that we expect our model to satisfy. For example, informally, we expect a CertIssued event may only occur following an HttpAuth or DnsAuth event for the same domain, expressing the fact that ACME should not issue a certificate for an non-validated domain under any circumstance. Running ProVerif on the query can result in three outcomes: either it diverges (in which case the model or query needs to be simplified), or it proves that the model satisfies the query, or it finds a counter-example and outputs its trace (which can be turned into an attack).

Validation with DNS Identifiers

We assert that if DNS validation succeeded, then A must have been able to successfully carry out DNS validation according to spec, or an adversary was able to instantiate an active DNS poisoning attack (with no third possible scenario). In ProVerif, this can be expressed using injective event queries:

DnsAuth(C pk , C w ) =⇒ (Owner(C k , C w ) ∨ DnsAttack(C w ))
Validation with HTTP Identifiers We explicitly show that HTTP authentication is weaker than DNS authentication, since an attack is possible under both cases of DNS poisoning and an HTTP man-in-the-middle attack:

HttpAuth(C pk , C w ) =⇒ Owner(C k , C w ) ∨ (HttpAttack(C w ) ∨ DnsAttack(C w ))
Predictable Certificate Issuance We attempt to verify that all received certificates were issued by the expected CA. This query fails to verify and leads us to the attack we discuss in §6:

CertReceived(C w , C wcert , C pk , A pk ) =⇒ CertIssued(C w , C wcert , C pk , A pk )

Specifying and Formally Verifying ACME

In this section we provide a formal description of the ACME protocol functionality and identify three issues that affect ACME's security. We also discuss details of how we describe the ACME protocol flow in the applied pi calculus, so that we can verify for certain queries using ProVerif.

ACME Network Flow

C recovery A = KDF (C Z A , C H A , recovery) A prk AC C recovery A = KDF (C Z A , C H A , recovery) Sign(Ck, newauthz) authz(A N C ) (Cpk, A N C ) (Cpk, A N C ) Sign(Ck, newcert(Cw csr ))
Generates Cw cert based on Cw csr Sign(Ak, Cw cert ) Fig. 4: ACME draft-1 protocol functionality for C account registration, recovery key generation, and validation with certificate issuance for C w . This chart demonstrates validation via an HTTP identifier. In draft-3 and above, the HTTP challenge

(C pk , A N C ) is replaced with Sign(C k , (C pk , A N C )).
HTTP Identifier A sends to C a nonce A N C via the HTTPS channel. C must then advertise, at an agreed-upon location under C w , the value (C pk , A N C ). A then accesses C w using an unauthenticated, unencrypted HTTP connection to ensure that it can retrieve the intended value. ACME also supports a very similar validation mode that operates at the level of the TLS handshake rather than at the HTTP level (using the SNI extension and a specially crafted certificate in place of the HTTP request and response). We believe this mode is intended for TLS termination software and hardware, and despite its apparent complexity, it is semantically equivalent to the HTTP identifier method. Since the details of the formatting of payloads is abstracted in our symbolic model we model both TLS-SNI and HTTP validation under the same framework in our model.

DNS Identifier

A sends to C a nonce A nonce C via the HTTPS channel. C advertises this nonce in the form of a DNS record served by C w 's name servers, thereby proving ownership of C w . A can then query its DNS server to verify that the nonce has been set. While this behavior is specified in ACME, it is not used in any implementation of Let's Encrypt: since ACME is designed to take advantage of domain validation methods that can be automated and since DNS record management depends on a series of ad-hoc protocols of its own between C and DNS service providers, it is not used by ACME.

Out-of-Band Validation

The ACME standard draft supports an out-of-band validation mechanism, which can be used to implement legacy validation methods, including email-based validation. However, since this method is underspecified, we do not cover it in our models and advise against using any out-of-bound validation unless it is analyzed under a specific model.

ACME Protocol Functionality

In this work we focus on draft-1 of the IETF specification for the ACME protocol, which is as of October 2016 also the draft specification deployed in official Let's Encrypt client and server implementations. In part due to the issues we discuss in the work and have communicated with the ACME team, draft-3 (and subsequently draft-4) does away with some features, most notably Account Recovery and generally is resistant to the issues discussed here.

Preliminaries In some parts of ACME's protocol flow, C and A will need to establish a number of shared secrets, each bound to a strict protocol context, over their public keys. In ACME, this is accomplished using ANSI-X9.63-KDF:

1. C and A agree on a ECDH shared secret C Z A using their respective key pairs (C k , C pk ) and (A k , A pk ).

A hashing function C H

A is chosen according to the elliptic curve used to calculate C Z A : SHA256 for P 256, SHA384 for P 384 and SHA512 for P 521.

C label

A = KDF (C Z A , C H A ,
label), with label indicating the chosen context for this particular key's usage.

As a protocol, ACME provides the following six certificate management functionalities (illustrated in Figure 4) between web server C and certificate management authority A: it may request that a certificate be issued for C w simply by requesting one from A. Generally, A will send the signed certificate with no further steps required. The renewal procedure is similarly straightforward. -Certificate Revocation C may ask A to revoke the certificate for C w by sending a POST message containing the certificate in question, signed under either C pk or the key pair for the certificate itself. C may choose which key to use for this signature. A verifies that the public key of the key pair signing the request matches the public key in the certificate and that the key pair signing the request is an account key and the corresponding account is authorized to act for all of the identifier(s) in the certificate.

-
Given this description of the ACME protocol and the threat model defined in §3, we modeled ACME using the automated verification tool ProVerif [START_REF] Truderung | Using ProVerif to analyze protocols with Diffie-Hellman exponentiation[END_REF]. In our model, we involve three different candidates for C: Alice, Bob and Mallory and two CA candidates as A.

In our automated verification process, we consider an active attacker over the three channels specified in §3. As a result, we were able to find the issues discussed in §6. The first two are relatively minor; however, the third could lead to account compromise in the case of contact-based account recovery and potentially to the issuance of false certificate signatures if email-based domain validation were to be implemented in ACME. Furthermore, this third issue is also generalizable to affect traditional certificate authorities, as described in §2.

Model Processes

Using the modeling conventions we established in §3 which include channels, adversaries, actors and events, we instantiate in our ProVerif model of ACME a top-level process that executes the following processes in parallel:

-ClientAuth Run simultaneously by Alice, Bob and Mallory assuming the role of C (with a compromised Mallory), this process registers a new account with A and sends the queries illustrated in Figure 4. The events Owner and CertReceived are triggered as part of this process. -ServerAuth Run simultaneously by two independent CAs assuming the role of A, this process accepts registrations from C and follows the protocol illustrated in Figure 4. The events HttpAuthenticated and CertIssued are triggered as part of this process.

The processes RoutingP roxy, P oisonDnsARecord and M anInT heM iddleHttp, all described in §3, are also run in parallel with the above.

Weaknesses in Traditional CAs

Traditional CA dependence on weak channels gives us a threat model where real-world attacks can have a small cost and come with severe consequences.

Email Validation

In ad-hoc CAs, C is generally simply sent an email containing a URI to their email inbox, which they're supposed to click in order to validate for their chosen domain. Figure 5 Usage of Nonces Traditional CAs use random nonces with no special cryptographic properties as the values that they then verify over HTTP, email or DNS. In addition to this helping caused the attack described above, another more general attack on nonces is shown in Figure 6 in the case of an active attacker. For example, this attack can be used by a compromised CA website to get certificates issued for domain C w by another (more reputable) CA, hence amplifying the compromise across CAs. None of these attacks would be effective if nonces were tied to some cryptographic properties, such as MACs or even just by deriving them from a hash of the certificate request's public key.

In order to avoid a similar attack, ACME draft-3 and draft-4 require that HTTP identifiers be validated by broadcasting

Sign(C k , A N C ) via the web server instead of ACME draft-1's (C pk , A N C ). Secure DNS Server D CA Website W Attacker V Mail Server E CertRequest(Cw, Cpk) QueryM X(Cw) M ailServer(Cw, M ) EmailChallenge(Cw, n) V alidate(Cw, n) Cert(W, Cw, Cpk

Weaknesses in ACME

Cross-CA Attacks on Certificate Issuance Suppose an ACME client C requests a certificate from A but A is malicious or the secure channel between A and C is compromised. Now, an attacker can intercept authorization and certificate requests from C to A, and instead forward them to another ACME server A ′ . If A ′ requests domain validation with a token T , the attacker forwards the token to the client, who will dutifully place its account key K and token T on its validation channel. A ′ will check this token and accept the authorization and issue a certificate that the attacker can forward to C. This means that C asked for a certificate from A, but instead received a certificate from A ′ . Moreover, it may have paid A for the service, but A ′ might have done it for free. This issue, while not critical, can be prevented if C checks the certificate it gets to make sure it was issued by the expected CA. An alter-native and possibly stronger, mitigation would be for ACME to extend the Key Authorization string to include the CAs identifier.

More generally, this issue reveals that ACME does not provide channel binding, and this appears as soon as we model the ACME HTTPS Channel. We would have expected to model this as a mutually-authenticated channel since the client always signs its messages with the account key. However, although the clients signature is tunnelled inside HTTPS, the signature itself is not bound to the HTTPS channel. This means that a message from an ACME client C to A can be forwarded by A to a different A ′ (as long as C supports both A and A ′ ). This kind of credential forwarding attack can be easily mitigated by channel binding. For example, ACME could rely on the Token Binding specifications to securely bind the client signature to the underlying channel. Alternatively, ACME could extend the signed request format to always include the servers name or certificate-hash, to ensure that the message cannot be forwarded to other servers.

Contact-Based Recovery Hijacking

While the use of sender-authenticated channels in ACME seems to be relatively secure, more attention needs to be paid to the receiver-authenticated channels. For example, if the ACME server uses the website administrator's email address to send the domain validation token, a naïve implementation of this kind of challenge would be vulnerable to attack.

In the current specification, the contact channel (typically email) is used for account recovery when the ACME client has forgotten its account key. We show how the careless use of this channel can be vulnerable to attack and propose a countermeasure. Suppose an ACME client C issues an account recovery request for an account under C pk with a new key C k ′ to the ACME server A. A network attacker M blocks this request and instead sends his own account recovery request for the account under C pk (pretending to be C) with his own key M k ′ . A will then send C an email asking to click on a link. C will think this is a request in response to its own account recovery request and will click on it. Similarly to the (slightly different) flow described in Figure 5, A will think that C has confirmed account recovery and will transfer the account under C pk to the attackers key M k ′ . In the above attack, the attacker did not need to compromise the contact channel (or for that matter, the ACME channel).

The key observation here is that on receiver-authenticated channels (e.g. email) the receiver does not get to bind the token provided by A with its own account key. Consequently, we need to add a further check. The email sent from A to C should contain a fresh token in addition to Cs new account key. Instead of clicking on the link (out-of-band), C should cut and paste the token into the ACME client which can first check that the account key provided by A matches the one in the ACME client and only then does it send the token back to A, or alternatively that the email recipient at C visually confirms that the account key (thumbprint) provided by A matches the one displayed in the ACME client.

The attack described here is on account recovery, but a similar attack appears if we allow email-based domain validation. A malicious ACME server or manin-the-middle can then get certificate issued for C's domains with its own public key, without compromising the contact/validation channel. The mitigation for that attack would be very similar to the one proposed above.

Conclusion

In this work, we have provided the results of an empirical case study that allowed us to describe a real-world threat model governing both traditional certificate authorities and ACME in terms of user authentication and domain validation. We formally modeled these protocols and provided the results of security queries under our threat model, using automated verification. As a result of our disclosures to the ACME team, the latest ACME protocol version (draft-4) has been designed to avoid the pitfalls that make these attacks possible.

Given the weak threat model that traditional CAs are assuming for their domain validation process, we are not surprised by the regular occurrences of unauthorized certificate issuance (e.g. StartCom in 2008, Comodo and DigiNotar in 2011, WoSign in 2016). We advocate the CA/Browser forum to eventually mandate the use of ACME (or some other well-defined domain validation protocol that can be formally analyzed) to all certification authorities, as a long-term solution to reduce unauthorized certificate issuance. Until the issuance process for the whole PKI is unified, techniques to improve the validation of certificates such as certificate transparency [6] remain necessary to detect issuance failures and technologies such as DNSSEC [START_REF] Ateniese | A new approach to dns security (dnssec)[END_REF], DANE [START_REF] Hoffman | The dns-based authentication of named entities (dane) transport layer security (TLS) protocol: TLSA[END_REF], or SMTPS may help strengthen the channels involved in legacy domain validation.

Fig. 2 :

 2 Fig.2: Provider repartition among the Alexa Top 10,000 global sites, as of October 2016. Notably, CloudFlare and Akamai also provide CDN services to domains under their name servers, allowing them stronger control over HTTP traffic.

Fig. 3 :

 3 Fig. 3: Channels overview.

Fig. 6 :

 6 Fig. 6: Active attack on DNS/HTTP/Email Validation when using just nonces.

Fig. 7 :

 7 Fig. 7: Attack on Email Validation: Passive Adversary on Email Channel

survey of the domain validation practices of current CAs

  , we still discover issues and weaknesses in ACME's domain validation and account recovery features, potentially amounting to user account compromise. We attempt to address in this paper what seem to be open questions regarding ACME: how does ACME compare to the existing security model of the actual top real-world certificate authorities? How can we most fruitfully illustrate and formally verify its security properties and what can we prove about them?

	Contributions Our contributions in this paper consist of:
	-A

: in §2, we survey the issuance process and infrastructure of 10 of the most popular certificate authorities. We observe that traditional CAs support multiple methods for assessing domain control, that rely on different security assumptions.

-A threat model for domain validation: in §3, we specify a high-level threat model for certificate issuance based on domain validation, which applies to both traditional CAs and ACME. We relate this threat model to the various domain control validation methods surveyed in §2. In §4, we demonstrate that ACME resists a stronger threat model than other CAs. -Formally specifying and verifying ACME: in §4, we formally specify the ACME protocol within a symbolic model in the applied π-calculus that encodes the adversarial capabilities described in §3. We verify the main security goals of ACME using ProVerif. Although ACME is shown to be more resistant to attacks than ad-hoc CAs, we also discover weaknesses in ACME's domain validation and account recovery and propose countermeasures.

  Intuitively, the channels we want encapsulate the following properties:only A can read this request and respond, and only the sender can read this response.-Strong Identifier Channels These channels must be assumed to be writable only by C. They are therefore relevant for HTTP and DNS Identifiers. -Weak Identifier Channel Anyone can write to this channel, but only C can read from it. This makes it relevant for domain validation via email identifiers.

		C	Auth(C k , newcert(C 𝑤𝑥 , C 𝑤𝑥 csr)) HTTPS Channel	A
	DNS	DNS Channel
	HTTP	HTTP Channel
	SMTP	SMTP Channel

  Unlike ad-hoc CAs which are limited to a web login, ACME's authentication depends on C generating a private signing key C k with a corresponding public verification key C pk , which are used to generate automated client signatures throughout the protocol.

	Web Server	Domain Owner	ACME Server
	Cw	C	A
		Knows Ck, Crk, Cpk, Cprk, Cc	Knows Ak
		Cw ⊂ C
		Sign(Ck, (newreg, Cc, Cpk, Cprk))

Creates account for C under Cpk

Generates recovery key pair (A rk AC , A prk AC )

  Account Key Registration In this step, C specifies her contact information (email address, phone number, etc.) as C c and generates a random private signing key C k with (over a safe elliptic curve) a public keyC pk . A POST request is sent to A containing Sign(C k , (newreg, C c , C pk )).The newreg header indicates to A that this is an account registration request. If A has no prior record of C pk being used for an account and if the message's signature is valid under C pk , A creates a new account for C using C pk as the identifier and responds with a success message. -MAC-Based Account Recovery C may choose to identify an account recovery secret with A. In order to do this, C generates an account recovery key pair (C rk , C prk ) and simply includes C prk in an optional recoverykey field in its initial newreg message to A. A generates the complementary (A rk AC , A prk AC ) and both parties calculate C recovery A using their recovery key pairs. A communicates A prk AC in its response to C. Later, if C loses C k , she can ask A to re-assign her account to a new identity (C k ′ , C pk ′ ) by using C recovery A as a key to generate a MAC of some value chosen by A. -Contact-Based Account Recovery C can request that A send a verification token to one of the contact methods previously specified in C c . For example, this could be a URI sent to an email in C c . If C successfully opens this URI, she becomes free to replace C pk with a C pk ′ for some arbitrary C k ′ at A. -Identifier Authorization C can validate its ownership of a domain C w in C w by providing one of the identifiers discussed in §3 to A. C must first request authorization for C w by sending a newauthz message. A then responds with the types of identifiers it is willing to accept in a authz message. C is then free to use any one of the permitted identifiers to validate its ownership of C w and allow A to sign certificates for it issued to C and tied to the identity C pk . -Certificate Issuance and Renewal After C ties an identifier to C w under C pk ,

  shows an attack rendered possible by this mechanism. A could instead, upon a validation request, redirect C's browser to a secret, nonce-based URI A U RI C served to C over the HTTPS channel and independently mail C the value HM AC(A hk , A U RI C ) for some secret A hk held by A. C would need to retrieve this second value and enter it inside the page at A U RI C . This approach would largely negate the weakness discussed in §6, since an attacker-induced validation email would result in an email that does not include a value matching the URI given by A to C at the beginning of the validation process. Fig. 5: Attack on Email Validation: Concurrent Request by Active Adversary.

	Domain Owner	Attacker	CA Website	Mail Server
	C	V		W	E
	CertRequest(Cw, Cpk)
			CertRequest(Cw, Mpk)
				EmailChallenge(Cw, n)
				ReadEmail(Cw, n)
	V alidate(Cw, n)
	Cert(W, Cw, Mpk)
	Install Cert(W, Cw, Mpk)
	Read(Cert(W, Cw, Mpk))
	Domain Owner	Attacker	CA Website	DNS Server
	C	V		W	D
	CertRequest(Cw, Cpk)	CertRequest(Cw, Mpk)
	DN SChallenge(Cw, n)	DN SChallenge(Cw, n)
				W riteT XT (Cw, n)
				ReadT XT (Cw, n)
				Cert(W, Cw, Mpk)

https://www.netcraft.com/internet-data-mining/ssl-survey/

CloudFlare incidentally also operates Let's Encrypt's infrastructure, rendering it a centralized point of failure for ACME and ad-hoc CAs alike. While ACME is a centralization-agnostic protocol, Let's Encrypt operates with a fully centralized infrastructure.

Full model available at https://github.com/Inria-Prosecco/acme-model

We also specify a fully public channel named pub.

Acknowledgements

This research received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement nř 683032 -CIRCUS).