Dealing with the right of way in advanced traffic simulation. A characterization of drivers' behaviours in a multi-agent approach

Keywords: Drivers' behaviour, multi-agent systems, traffic, artificial intelligence, simulation

With the emergence of ADAS and autonomous vehicle, the need of simulation software to test advanced systems and models is unavoidable. The objective of this work is to characterize, in a multi-agent approach, the traffic vehicles behaviours, and to model them in a versatile traffic simulator, serving as a testing tool for integration in the traffic module of the SCANeR Studio T M simulation software. The algorithm will bring more natural interactions between vehicles in simulation and allow the emergence of new relevant situations for autonomous vehicles, observable in real, such as collision risk situations or even accidents, which have for now to be scripted in scenarios and do not occur naturally.

Introduction

With an increasing number of ADAS systems and incoming Autonomous Vehicles (AV), a huge amount of physical driving tests is needed (hundreds of millions of km) [Koo16] to validate systems. The use of numerical simulation is then crucial to reduce this amount of real tests, by covering a range of situations as large as required [Mas12]. Most of current simulation softwares : PTV Vissim 1 , ARCHISIM [Esp07], AIMSUN 2 , TrafficGen [Bon14] etc., do not yet include sufficiently fine microscopic traffic modules for AV testing in terms of driver behaviour modelling and cooperative driving [Baz14,Mic85]. It is then difficult to confront simulated AV to real like situations, especially critical situations in which behaviour of the automated systems is expected to achieve customer performance with the necessary safety requirements [Baz13]. Drivers' behaviours are various and changing, and they are at the origin of a great variability in road traffic situations. This disparity is generally related both to the human perception system (inter-individual differences), and to decision making mechanisms, as well as the actions and manoeuvres resulting from them [Wri02]. In our approach, we introduced this variability in perception and decision to our traffic agents' models, in order to have more natural and realistic behaviours.

Methodology

Model of driving mechanisms can be schematized as in Figure 4. and uses it to decide the action to do on the vehicle by acting on speed, acceleration/deceleration and steering wheel. This mechanism is implemented in a multi-agent simulation tool, Netlogo, where the agents represent vehicles and infrastructure elements.

The driver receives information from the environment

Tree main behaviours can be found in the literature.

[Wri02] :

The first one, is what usually can be considered as cautious behaviour. It can be described by a strict respect of the traffic code and a tendency to drive slowly as the other drivers and with an increased safety distance.

The second one, corresponding to a more aggressive behaviour, can be described by a no respect of the traffic code and a tendency to drive faster as the other drivers and with a decreased safety distance.

The third one, would be a standard behaviour, described by a complete respect of the traffic code, neither more, neither less.

In our work, we propose to add one more we call the normal driver. It may vary in function of his or her Variability across traffic agents is provided by a variability on perception parameters. Moreover, an error is pseudo-randomly (distribution on traffic population) introduced in perception and anticipation to provide more realistic non-perfect behaviours.

To validate our approach on a manoeuvre, we first chose to prototype the methodology in the case of overtake on a 2 lanes highway.

In this case, perception parameters are following : /20; 30; 40; 50; 70; 90; 110; 130/ the speed limit -T R the respect of traffic code t l the reaction time/latency These parameters are then correlated to the following overtaking decision rules :

For the implementation we choose the Netlogo language, and our algorithm takes into account the overtaking on a road with two lanes. A crossing in T is under development.

Expected results and discussions

The Multi-agent systems allows to model interactions between agents designed for large scale simulation. This methodology is more focused on the interactions than the agents and incremental design of simulations is thus supported intuitively and easily. Validation of the proposed algorithm will be done through the measurement of the rate of accidents or critical situations occurring during a simulation thanks to errors on perception and anticipation for some agents. The objective of the studied algorithm is to improve the overall traffic with realistic driving behaviour. We expect to show some accidents for agents with error and smoother manoeuvres for agents with good level of anticipation. This methodology will then be applied to cross intersection driving and to other cases and manoeuvres.

Conclusion

As our work show the better realism of behaviours thanks to the proposed models, it illustrates the new and more efficient way of testing which will be needed with a very large number of representative traffic scenarios for ADAS and automated vehicle functions. Indeed, to validate the corresponding embedded systems, automobile companies and road research institutes need today a realistic traffic which can reproduce the accidents that may arise in function of different and realistic driving behaviours. New implementation of the resulting enhanced traffic model will help automotive OEMs and suppliers to test the autonomous vehicle strategies in a simulated realistic traffic and allow both driver in the loop and highperformance computer (HPC) simulation validation in numerous critical situations for self-driving cars.

Figure 1 :

 1 Figure 1: Scheme of main driving mechanisms.

Figure 2 :

 2 Figure 2: The driver parameters.

Figure 3 :

 3 Figure 3: The overtaking's decision rules.

  With : -D S the safety distance -V E the speed of the ego car -( v fi , v bi , v li ) the speed of other vehicles (f for front, b for back, l for the lateral lane) -(t fi , t bi , t li ) the time to vehicle i (in front, back, on the lateral lane) -((α f ; d f ), (α b ; d b ), (α r ; d r ), (α l ; d l )) the field of view of the ego car r O the overtake risks r S the speed risk -S L =

Figure 4 :

 4 Figure 4: Diagram of the perception of our vehicles.

http ://vision-traffic.ptvgroup.com/fr/produits/ptv-vissim/

http ://www.aimsun.com/


Julien Bringer
email: julien.bringer@idemia.com

Hervé Chabanne
email: herve.chabanne@idemia.com

Daniel Le Métayer
email: daniel.le-metayer@inria.fr

Roch Lescuyer
email: roch.lescuyer@idemia.com

Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures

Keywords: Privacy by design, data protection, regulation, formal methods, verification, biometric systems

come   L'archive ouverte pluridisciplinaire

Introduction

Many applications of biometric recognition have been developed during the last decades in a variety of contexts, from criminal investigations and identity documents to a wealth of public and private usages, like physical access control or smartphone authentication. Biometric systems involve two main phases: enrolment and verification (either authentication or identification) [START_REF] Anil | An introduction to biometric recognition[END_REF]. enrolment is the registration phase, in which the biometric traits of a person are collected and recorded within the system. During this phase, the identity of the user is associated with his recorded biometric trait. In the authentication mode, a fresh biometric trait is collected and compared with the registered biometric reference to check that it corresponds to the claimed identity. In the identification mode, a fresh biometric data is collected and the corresponding identity is searched in a database of enrolled biometric references. During each phase, to enable efficient and accurate comparison, the collected biometric data are converted into discriminating features, leading to what is called a biometric template. The increased use of biometric systems has generated a lot of interest in privacy issues and the risks related to biometric trait processing. Since the leakage of biometric traits may lead to serious privacy risks, including tracking and identity theft, it is necessary to follow a privacy by design approach for this type of systems. The security of biometric systems has been an active research area since at least fifteen years and a wide-array of well-documented primitives have been studied, such as encryption, homomorphic encryption, secure multi-party computation, hardware security or biometric template protection. These building blocks have been used in a variety of privacy preserving biometric systems. Some solutions involve dedicated cryptographic primitives such as secure sketches [START_REF] Dodis | Fuzzy extractors: How to generate strong keys from biometrics and other noisy data[END_REF] and fuzzy vaults [START_REF] Juels | A fuzzy vault scheme[END_REF][START_REF] Uludag | Fuzzy vault for fingerprints[END_REF], others rely on adaptations of existing cryptographic tools [START_REF] Li | A novel biometric-based authentication scheme with privacy protection[END_REF] or the use of secure hardware solutions [37]. The choice of particular techniques and the role of the components (central server, secure module, terminal, smart card, etc.) in the architecture have a strong impact on the privacy guarantees provided by a solution. However, existing proposals were made on a case by case basis, which makes it difficult to compare them, to provide a rationale for the choice of specific options and to capitalize on past experience. The objective of the work presented in this paper is to show the applicability of the privacy by design approach to biometric systems and the benefit of using formal methods to this end. We build on a general framework introduced in [START_REF] Antignac | Privacy architectures: Reasoning about data minimisation and integrity[END_REF] for the formal definition and validation of privacy architectures. The goal is to specify the various design options in a consistent and comparable way, and then to reason about them in a formal way in order to justify their design in terms of trust assumptions and privacy properties. This work has been conducted within the French ANR research project BioPriv [START_REF] Biopriv | Biometric systems Private by design[END_REF], an interdisciplinary project involving lawyers and computer scientists. The BioPriv project itself built on the results of the Turbine European project 1 which studied the best practices for privacy by design applied to biometric systems [START_REF] Kindt | Best practices for privacy and data protection for the processing of biometric data[END_REF]. The privacy by design approach is often praised by lawyers as well as computer scientists as an essential step towards a better privacy protection. It is now enshrined in the General Data Protection Regulation [36] that will be applied in Europe in May 2018. Nevertheless, it is one thing to impose by law the adoption of privacy by design, quite another to define precisely what it is intended to mean technically-wise and to ensure that it is put into practice by developers. The overall philosophy is that privacy should not be treated as an afterthought but rather as a first-class requirement in the design phase of systems: in other words, designers should have privacy in mind from the start when they define the features and architecture of a system. However, the practical application raises a number of challenges: first of all the privacy requirements must be defined precisely; then it must be possible to reason about potential tensions between privacy and other requirements and to explore different combinations of privacy enhancing technologies to build systems meeting all these requirements. 1 7th European Framework Program.

TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 113

In Section 2, we provide an outline of the framework introduced in [START_REF] Antignac | Privacy architectures: Reasoning about data minimisation and integrity[END_REF] for defining privacy architectures and reasoning about their properties. Then we show how this framework can be used to apply a privacy by design approach to the implementation of biometric systems. In Section 3, we introduce the basic terminology used in this paper and the common features of the biometric architectures considered in the paper. In Section 4, we describe several architectures for biometric systems, considering both existing systems and more advanced solutions, and show that they can be defined in this framework. This makes it possible to highlight their commonalities and differences especially with regard to their underlying trust assumptions.

In the second part of this paper, we address a security issue which cannot be expressed in the framework presented in Section 2. The origin of the problem is that side-channel information may leak from the execution of the system. This issue is acute for biometric systems because the result of a matching between two biometric data inherently provides some information, even if the underlying cryptographic components are correctly implemented [START_REF] Bringer | Blackbox security of biometrics (invited paper)[END_REF][START_REF] Simoens | A framework for analyzing template security and privacy in biometric authentication systems[END_REF][START_REF] Pagnin | On the leakage of information in biometric authentication[END_REF]. To adress this issue we propose in Section 5 an extension of the formal framework, in which information leaks spanning over several sessions of the system can be expressed. In Section 6, we apply the extended model to analyse biometric information leakage in several variants of biometric system architectures.

Finally, Section 7 sketches related works and Section 8 concludes the paper with suggestions of avenues for further work.

General approach

The work presented in [START_REF] Antignac | Privacy architectures: Reasoning about data minimisation and integrity[END_REF] can be seen as a first step towards a formal and systematic approach to privacy by design. In practice, this framework makes it possible to express privacy and integrity requirements (typically the fact that an entity must obtain guarantees about the correctness of a value), to analyse their potential tensions and to make reasoned architectural choices based on explicit trust assumptions. The motivations for the approach come from the following observations:

• First, one of the key decisions that has to be made in the design of a privacy compliant system is the location of the data and the computations: for example, a system in which all data is collected and all results are computed on a central server brings strong integrity guarantees to the operator at the price of a loss of privacy for data subjects. Decentralized solutions may provide better privacy protections but weaker guarantees for the operator. The use of privacy enhancing technologies such as homomorphic encryption or secure multi-party computation can in some cases reconcile both objectives.

• The choice among the architectural options should be guided by the trust assumptions that can be placed by the actors on the other actors and on the components of the architecture. This trust itself can be justified in different ways (security protocol, secure or certified hardware, accredited third party, etc.).

As far as the formal model is concerned, the framework proposed in [START_REF] Antignac | Privacy architectures: Reasoning about data minimisation and integrity[END_REF] relies on a dedicated epistemic logic. Indeed, because privacy is closely connected with the notion of knowledge, epistemic logics [START_REF] Fagin | Reasoning About Knowledge[END_REF] form an ideal basis to reason about privacy properties. However, standard epistemic logics based on possible worlds semantics suffer from a weakness (called "logical omniscience" [START_REF] Halpern | Dealing with logical omniscience[END_REF]) which makes them unsuitable in the context of privacy by design.

We assume that the functionality of the system is expressed as the computation of a set of equations Ω := {X = T } over a language T erm of terms T defined as follows, where c represents constants (c ∈ Const), X variables (X ∈ V ar) and F functions (F ∈ F un):

T ::= X | c | F (T 1 , . . . , T n )
An architecture is defined by a set of components C i , for i ∈ [1, N ], and a set A of relations. The relations define the capacities of the components and the trust assumptions. We use the following language to define the relations:

A ::= {R} R ::= Has i (X) | Receive i,j ({St}, {X}) | Compute G (X = T ) | V erif y i (St) | T rust i,j
St ::= P ro | Att Att ::= Attest k ({Eq}) P ro ::= P roof i ({P }) Eq ::= P red(T 1 , . . . , T m )

P ::= Att | Eq
The notation {Z} denotes a set of terms of category Z. Has i (X) denotes the fact that component C i possesses (or is the origin of) the value of X, which may correspond to situations in which X is stored on C i or C i is a sensor collecting the value of X. In this paper, we use the set of predicates P red := {=, ∈}. Compute G (X = T ) means that the components in the set G can compute the term T and assign its value to X and T rust i,j represents the fact that component C i trusts component C j . Receive i,j ({St}, {X}) means that C i can receive the values of variables in {X} together with the statements in {St} from C j . We consider two types of statements here:

• Attestations: Attest k ({Eq}) is the declaration by the component C k that the properties in {Eq} hold.

• Proofs: P roof i ({P }) is a proof of properties P provided by C i .

V erif y i (St) is the verification by component C i of statement St. If St is a proof state- ment, V erif y i (St)
is the verification of the correctness of St. In contrast, if St is an attestation statement Attest k ({Eq}), then V erif y i (St) is the verification of the authenticity of the sender, that is to say C k . The actual implementation of the relations defining an architecture is not defined at this level. In practice, the verification of an attestation can be implemented as a digital signature verification. Graphical data flow representations can be derived from architectures expressed in this language. For the sake of readability, we use both notations in the next sections. The subset of the privacy logic used in this paper is the following dedicated epistemic logic:

ϕ ::= Has i (X) | Has none i (X) | K i (P rop) | ϕ 1 ∧ ϕ 2 P rop ::= P red(T 1 , . . . , T n ) | P rop 1 ∧ P rop 2
Has i (X) and Has none i (X) denote the facts that component C i respectively can or cannot get the value of X. K i denotes the epistemic knowledge following the "deductive algorithmic knowledge" philosophy [START_REF] Fagin | Reasoning About Knowledge[END_REF][START_REF] Pucella | Deductive algorithmic knowledge[END_REF] that makes it possible to avoid the logical omniscience TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 115

Has i (X) ∈ A H1 A Has i (X) Compute G (X = T ) ∈ A C i ∈ G H3 A Has i (X) Receive i,j (S, E) ∈ A X ∈ E H2 A Has i (X) Dep i (Y, X ) ∀X ∈ X , A Has i (X) H5 A Has i (Y ) A Has i (X) HN A Has none i (X) E i Eq 0 ∀Eq ∈ E : A K i (Eq) K A K i (Eq 0 ) Compute G (X = T ) ∈ A C i ∈ G K1 A K i (X = T ) V erif y i (P roof j (E)) ∈ A Eq ∈ E K3 A K i (Eq) V erif y i (P roof j (E)) ∈ A Attest k (E ) ∈ E Eq ∈ E T rust i,k ∈ A K4 A K i (Eq) V erif y i (Attest j (E)) ∈ A T rust i,j ∈ A Eq ∈ E K5 A K i (Eq)
Figure 1: A subset of rules from the axiomatics of [START_REF] Antignac | Privacy architectures: Reasoning about data minimisation and integrity[END_REF] problem. In this approach, the knowledge of a component C i is defined as the set of properties that this component can actually derive using its own information and The semantics S(A) of an architecture A is defined as the set of states of the components C i of A resulting from compatible execution traces [START_REF] Antignac | Privacy architectures: Reasoning about data minimisation and integrity[END_REF]. A compatible execution trace contains only events that are instantiations of relations (e.g. Receive i,j , Compute G , etc.) of A (as further discussed in Section 5.1). The semantics S(ϕ) of a property ϕ is defined as the set of architectures meeting ϕ. For example, A ∈ S(Has none i (X)) if for all states σ ∈ S(A), the sub-state σ i of component C i is such that σ i (X) = ⊥, which expresses the fact that the component C i cannot assign a value to the variable X. To make it possible to reason about privacy properties, an axiomatics of this logic is presented and is proven sound and complete. A ϕ denotes that ϕ can be derived from A thanks to the deductive rules (i.e. there exists a derivation tree such that all steps belong to the axiomatics, and such that the leaf is A ϕ). A subset of the axioms useful for this paper is presented in Figure 1.

Biometric systems architectures

Before starting the presentation of the different biometric architectures in the next sections, we introduce in this section the basic terminology used in this paper and the common features of the architectures. For the sake of readability, we use upper case sans serif letters TRANSACTIONS ON DATA PRIVACY 11 (2018) S, T, etc. as index variables i for components. Type letters dec, br, etc. denote variables. The set of components of an architecture is denoted by J . The variables used in biometric system architectures are the following:

• A biometric reference template br built during the enrolment phase, where a template corresponds to a set or vector of biometrics features that are extracted from raw biometric data in order to be able to compare biometric data accurately.

• A raw biometric data rd provided by the user during the verification phase.

• A fresh template bs derived from rd during the verification phase.

• A threshold thr which is used during the verification phase as a closeness criterion for the biometric templates.

• The output dec of the verification which is the result of the matching between the fresh template bs and the enrolled templates br, considering the threshold thr.

Two components appear in all biometric architectures: a component U representing the user, and the terminal T which is equipped with a sensor used to acquire biometric traits.

In addition, biometric architectures may involve an explicit issuer I, enrolling users and certifying their templates, a server S managing a database containing enrolled templates, a module (which can be a hardware security module, denoted HSM) to perform the matching and eventually to take the decision, and a smart card C to store the enrolled templates (and in some cases to perform the matching).

Application of the framework to several architectures for biometric systems with various protection levels

In this section, we describe several architectures for biometric systems, considering both existing systems and more advanced solutions, and we show that they can be defined in the framework presented in Section 3.

Protecting the reference templates with encryption

Let us consider first the most common architecture deployed for protecting biometric data. When a user is enrolled his reference template is stored encrypted, either in a terminal with an embedded database, or in a central database. During the identification process, the user supplies a fresh template, the reference templates are decrypted by a component (which can be typically the terminal or a dedicated hardware security module) and the comparison is done inside this component. The first part of Figure 3 While the solutions described in this section can be seen as superseded by the ones of the next section, we introduce them for two purposes: firstly, for a pedagogical reason in order to prepare the reader to better understand the more sophisticated techniques of section 4.2 and secondly, to start with the presentation of in-the-field solutions as they are commonly deployed today.

TRANSACTIONS ON DATA PRIVACY 11 (2018)

Use of an encrypted database

The first architecture A ed is composed of a user U, a terminal T, a server S managing an encrypted database ebr and an issuer I enrolling users and generating the encrypted database ebr. The set F un includes the encryption and decryption functions Enc and Dec. When applied to an array, Enc is assumed to encrypt each entry of the array. At this stage, for the sake of conciseness, we consider only biometric data in the context of an identification phase. The same types of architectures can be used to deal with authentication, which does not raise any specific issue. The functionality of the architecture is Ω := {ebr = Enc(br), br = Dec(ebr), bs = Extract(rd), dec = µ(br , bs, thr)}, and the architecture is defined as: From the point of view of biometric data protection, the property that this architecture is meant to ensure is the fact that the server should not have access to the reference template, that is to say: Has none S (br), which can be proven using Rule HN (the same property holds for br ):

Has S (br) ∈ A ed X : (br, X ) ∈ Dep S T : Compute S (br = T ) ∈ A ed j ∈ J , S, E, Receive S,j (S, E) ∈ A ed ∧ br ∈ E HN A ed Has none S (br)
It is also easy to prove, using H2 and H5, that the terminal has access to br : Has T (br ).

As far as integrity is concerned, the terminal should be convinced that the matching is correct. The proof relies on the trust placed by the terminal in the issuer (about the correctness of ebr) and the computations that the terminal can perform by itself (through Compute T and the application of ):

V erif y T ({Attest I (ebr = Enc(br))}) ∈ A ed T rust T,I ∈ A ed K5 A ed K T (ebr = Enc(br)) {ebr = Enc(br)} {br = Dec(ebr)} A ed K T (ebr = Enc(br)) K A ed K T (br = Dec(ebr)) Compute T (br = Dec(ebr)) ∈ A ed K1 A ed K T (br = Dec(ebr))
Assuming that all deductive relations include the properties (commutativity and transitivity) of the equality, K can be used to derive: A ed K T (br = br ). A further application of K1 with another transitivity rule for the equality allows us to obtain the desired integrity property:

TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 119

A ed K T (br = br ) Compute T (dec = µ(br , bs, thr)) ∈ A ed K1 A ed K T (dec = µ(br , bs, thr)) K A ed K T (dec = µ(br, bs, thr))

Encrypted database with a hardware security module

The architecture presented in the previous subsection relies on the terminal to decrypt the reference template and to perform the matching operation. As a result, the clear reference template is known by the terminal and the only component that has to be trusted by the terminal is the issuer. If it does not seem sensible to entrust the terminal with this central role, another option is to delegate the decryption of the reference template and computation of the matching to a hardware security module so that the terminal itself never stores any clear reference template. This strategy leads to architecture A hsm pictured in the second part of Figure 3.

In addition to the user U, the issuer I, the terminal T, and the server S, the set of components contains a hardware security module M. The terminal does not perform the matching, but has to trust M. This trust can be justified in practice by the level of security provided by the HSM M (which can also be endorsed by an official security certification scheme). The architecture is described as follows in our framework: where the set of attestations A received by the terminal from the module is A := {Attest M (dec = µ(br , bs, thr)), Attest M (br = Dec(ebr))}. The trust relation between the terminal and the module makes it possible to apply rule K5 twice:

V erif y T ({Attest M (dec = µ(br , bs, thr

))}) ∈ A hsm T rust T,M ∈ A hsm A hsm K T (dec = µ(br , bs, thr)) V erif y T ({Attest M (br = Dec(ebr))}) ∈ A hsm T rust T,M ∈ A hsm K5 A hsm K T (br = Dec(ebr))
The same proof as in the previous subsection can be applied to establish the integrity of the matching. The trust relation between the terminal and the issuer and the rules K5, K make it possible to derive: A hsm K T (br = Dec(ebr)). Then two successive applications of K regarding the transitivity of the equality lead to: A hsm K T (dec = µ(br, bs, thr)).

As in architecture A ed , the biometric references are never disclosed to the server. However, in contrast with A ed , they are not disclosed either to the terminal, as shown by rule HN:

Has T (br) ∈ A hsm X : (br, X ) ∈ Dep T T : Compute T (br = T ) ∈ A hsm j ∈ J , S, E, Receive T,j (S, E) ∈ A hsm ∧ br ∈ E HN A hsm Has none T (br)
TRANSACTIONS ON DATA PRIVACY 11 (2018)

Enhancing protection with homomorphic encryption

In both architectures of Section 4.1, biometric templates are protected, but the component performing the matching (either the terminal or the secure module) gets access to the reference templates. In this section, we show how homomorphic encryption can be used to ensure that no component gets access to the biometric reference templates during the verification. Homomorphic encryption schemes [START_REF] Gentry | Fully homomorphic encryption using ideal lattices[END_REF] makes it possible to compute certain functions over encrypted data. For example, if Enc is a homomorphic encryption scheme for multiplication then there is an operation ⊗ such that:

c 1 = Enc(m 1 ) ∧ c 2 = Enc(m 2 ) ⇒ c 1 ⊗ c 2 = Enc(m 1 × m 2 ).
Figure 4 presents an architecture A hom derived from A hsm in which the server performs the whole matching computation over encrypted data. The user supplies a template that is sent encrypted to the server (denoted ebs). The server also owns an encrypted reference template ebr. The comparison, i.e. the computation of the distance between the templates, is done by the server, leading to the encrypted distance edec, but the server does not get access to the biometric data or to the result. This is made possible through the use a homomorphic encryption scheme. On the other hand, the module gets the result, but does not get access to the templates. Let us note that A hom is just one of the possible ways to use homomorphic encryption in this context: the homomorphic computation of the distance could actually be made by another component (for example the terminal itself) since it does not lead to any leak of biometric data. The homomorphic property of the encryption scheme needed for this application depends on the matching algorithm. An option is to resort to a fully homomorphic encryption scheme (FHE) [START_REF] Gentry | Fully homomorphic encryption using ideal lattices[END_REF] as in the solution described in [START_REF] Ram Ón Troncoso-Pastoriza | Fully homomorphic faces[END_REF] which uses a variant of a FHE scheme for face-recognition. However, schemes with simpler homomorphic functionalities can also be sufficient (examples can be found in [START_REF] Bringer | An application of the Goldwasser-Micali cryptosystem to biometric authentication[END_REF][START_REF] Blanton | Secure and efficient protocols for iris and fingerprint identification[END_REF]). Since we describe our solutions at the architecture level, we do not need to enter into details regarding the chosen homomorphic scheme. We just need to assume the existence of a homomorphic matching function Hom-µ with the following properties captured by the algorithmic knowledge relations: where the set A of attestations received by the terminal from the server is: A := {Attest I ({ebr = Enc(br)}), Attest S ({edec = Hom-µ(ebr, ebs, thr)})}.

{ebr = Enc(
In order to prove that the terminal can establish the integrity of the result dec, we can proceed in two steps, proving first the correctness of edec and then deriving the correctness of edec using the properties of homomorphic encryption. The first step relies on the capacities of component T and the trust assumptions on components I and S using rules K1 and K5 respectively.

Compute T (ebs = Enc(bs)) ∈ A hom K1 A hom K T (ebs = Enc(bs)) V erif y T ({Attest I (ebr = Enc(br))}) ∈ A hom T rust T,I ∈ A hom K5
A hom K T (ebr = Enc(br)) V erif y T ({Attest S (edec = Hom-µ(br, bs, thr))}), T rust T,S ∈ A hom K5

A hom K T (edec = Hom-µ(br, bs, thr))

The second step can be done through the application of the deductive algorithmic knowledge regarding the homomorphic encryption property (with LHS 1 the left hand-side of equation ( 1)) :

LHS 1 {Dec(edec) = µ(br, bs, thr)} ∀Eq ∈ LHS 1 : A hom K T (Eq) K A hom K T (Dec(edec) = µ(br, bs, thr))
The desired property is obtained through the application of rules K5 and K exploiting the trust relation between T and M and the transitivity of equality.

V erif y T ({Attest

M (dec = Dec(edec))}) ∈ A hom T rust T,M ∈ A hom K5 A hom K T (dec = Dec(edec)) A hom K T (Dec(edec) = µ(br, bs, thr)) A hom K T (dec = Dec(edec)) K A hom K T (dec = µ(br, bs, thr))
As far as privacy is concerned, the main property that A hom is meant to ensure is that no component (except the issuer) has access to the biometric references. Rule HN makes it possible to prove that U, T, and S never get access to br, as in Section 4.

The Match-On-Card technology

Another solution can be considered when the purpose of the system is authentication rather than identification. In this case, it is not necessary to store a database of biometric reference templates and a (usually unique) reference template can be stored on a smart card. A smart card based privacy preserving architecture has been proposed recently which relies on the idea of using the card not only to store the reference template but also to perform the matching itself. Since the comparison is done inside the card the reference template never leaves the card. In this Match-On-Card (MOC) technology [37, [START_REF]MINEXII -an assessment of Match-On-Card technology[END_REF][START_REF] Govan | A computationally efficient fingerprint matching algorithm for implementation on smartcards[END_REF] (also called comparison-oncard), the smart card receives the fresh biometric template, carries out the comparison with its reference template, and sends the decision back (as illustrated in Figure 5). Using rule HN, it is easy to show that no component apart from C gets access to br. The proof of the integrity property relies on the capacities of component T and the trust assumption on component C using rules K1 and K5 respectively.

Extension of the framework to information leakage

In this section, we address a security issue which cannot be expressed in the framework presented in Section 2. The origin of the problem is that side-channel information may leak from the execution of the system. This issue is acute for biometric systems because the result of a matching between two biometric data inherently provides some information, even if the underlying cryptographic components are correctly implemented [START_REF] Bringer | Blackbox security of biometrics (invited paper)[END_REF][START_REF] Simoens | A framework for analyzing template security and privacy in biometric authentication systems[END_REF][START_REF] Pagnin | On the leakage of information in biometric authentication[END_REF].

TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 123

To address this issue we propose in Section 5.1 an extension of the architecture language and in Section 5.2 an extension of the privacy logic.

Extension of the architecture language

Motivated by the need to analyse the inherent leakage of the result of a matching between two biometric data in biometric systems (cf. [START_REF] Bringer | Blackbox security of biometrics (invited paper)[END_REF][START_REF] Simoens | A framework for analyzing template security and privacy in biometric authentication systems[END_REF][START_REF] Pagnin | On the leakage of information in biometric authentication[END_REF]), we now propose an extension of the formal framework sketched in Section 2, in which the information leaking through several executions can be expressed. In fact, in this line of work, it is shown that someone might mount an hill-climbing attack where he is trying, by repeated trials, to guess the templates that are privately stored in a secure component. Doing that, he will exploit the information leaked during one execution, e.g. the similarity result between his guess and the templates which leaks more than a direct match vs no match output. At the end, his strategy is to increase his knowledge of the templates, execution after execution. We thus have to extend our static model used in previous sections, to handle this more dynamic situation.

We highlight the difference with the framework introduced in Section 2 without repeating their common part. The term language we use is now the following.

T ::= X | c | F ( X1 , . . . , Xm , c 1 , . . . , c q ) X ::= X | X[k]
Functions may take as parameters both variables and constants. Variables X can be simple variables or arrays of variables. If X is an array, Range(X) denotes its size.

In this extended framework, in addition to defining a set of primitives, an architecture can also provide a bound on the number of times a primitive can be used.

A ::= {R} R ::= Has (n) i (X) | Has i (c) | Receive (n) i,j ({St}, {X} ∪ {c}) | T rust i,j | Reset | Compute (n) G (X = T ) | V erif y (n) i ({St})
St ::= P ro | Att Att ::= Attest i ({Eq}) P ro ::= P roof i ({P })

Eq ::= P red(T 1 , . . . , T m ) P ::= Att | Eq

The superscript notation (n) denotes that a primitive can be carried out at most n ∈ (N \ {0}) ∪ {∞} times by the component(s) -where (∀n ∈ N: n < ∞). We assume that n is never equal to 0. mul(α) denotes the multiplicity (n) of the primitive α, if any. The Reset primitive is used to reinitialize the whole system. As in the initial model, consistency assumptions are made about the architectures to avoid meaningless definitions. For instance, we require that components carry out computations only on the values that they have access to (either through Has, Compute, or Receive). We also require that all multiplicities n specified by the primitives are identical in a consistent architecture. As a result, a consistent architecture A is parametrized by an integer n ≥ 1 (we note A(n) when we want to make this integer explicit).

A key concept for the definition of the semantics is the notion of trace. A trace is a sequence of events and an event2 is an instantiation of an architectural primitive 3 . The notion of successive sessions is caught by the addition of a Session event 4 . A trace θ of events is said compatible with a consistent architecture A(n) if all events in θ (except the computations) can be obtained by instantiation of some architectural primitive from A, and if the number of events between two Reset events corresponding to a given primitive is less than the bound n specified by the architecture. We denote by T (A) the set of traces which are compatible with an architecture A.

θ ::= Seq( ) ::= Has i (X :

V ) | Has i (c) | Receive i,j ({St}, {X : V } ∪ {c}) | Session | Reset | Compute G (X = T ) | V erif y i ({St})
An event can instantiate variables X with specific values V . Constants always map to the same value. Let V al be the set of values the variables and constants can take. The set V al ⊥ is defined as V al ∪ {⊥} where ⊥ ∈ V al is a specific symbol used to denote that a variable or a constant has not been assigned yet.

The semantics of an architecture follows the approach introduced in [START_REF] Antignac | Privacy architectures: Reasoning about data minimisation and integrity[END_REF]. Each component is associated with a state. Each event in a trace of events affects the state of each component involved by the event. The semantics of an architecture is defined as the set of states reachable by compatible traces. The state of a component is either the Error state or a pair consisting of: (i) a variable state assigning values to variables, and (ii) a property state defining what is known by a component. The variable state assigns values to variables and to constants (each constant is either undefined or taking a single value).

State ⊥ = (State V × State P ) ∪ {Error} State V = V ar ∪ Const → List(V al ⊥ ) State P = {Eq} ∪ {T rust i,
σ v i (X)[m] (resp. σ v i (c)[m]
) denotes the m-th entry of the variable state of X ∈ V ar (resp. c ∈ Const). The initial state of an architecture A is denoted by Init A = Init A 1 , . . . , Init A N where: ∀C i : Init A i = (Empty, {T rust i,j | ∃C j : T rust i,j ∈ A}). Empty associates to each variable and constant a list made of a single undefined value (⊥). We assume that, in the initial state, the system is in its first session. Alternatively, we could set empty lists in the initial state and assume that every consistent trace begins with a Session event.

Let S T :

T race × (State ⊥ ) N → (State ⊥ ) N and S E : Event × (State ⊥ ) N → (State ⊥ ) N
be the following two functions. S T is defined recursively by iteration of S E : for all state σ ∈ (State ⊥ ) N , event ∈ Event and consistent trace θ ∈ T race, S T ( , σ) = σ and S T ( • θ, σ) = S T (θ, S E ( , σ)). The modification of a state is noted σ[σ i /(v, pk)] the variable and knowledge states of C i are replaced by v and pk respectively. σ[σ i /Error] denotes that the Error state is reached for component C i . We assume that a component reaching an Error state no longer gets involved in any later action (until a reset of the system). The function S E is defined event per event. 4 Computations can involve different values of the same variables from different sessions.

TRANSACTIONS ON DATA PRIVACY 11 (2018)

Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 125

The effect of Has i (X : V ) and Receive i,j (S, {(X : V )}) on the variable state of component C i is the replacement of the last value of the variable X by the value V : last(σ v i (X)) := V . This effect is denoted by σ v i [X/V ]. For instance, we have

S E (Has i (X : V ), σ) = σ[σ i /(σ v i [X/V ], σ pk i )]
where σ v i [X/V ] means that new values V replace the values of the variables X, and σ pk i stands for the property component of the state of C i . Similarly, one can write

S E (Receive i,j (S, {X : V }), σ) = σ[σ i /(σ v i [X/V ], σ pk i )]
In the case of constants, the value V is determined by the interpretation of c (as in the function symbols in the computation). The effect of Compute G (X = T ) is to assign to X, for each component C i ∈ G, the value V produces by the evaluation (denoted ε) of T . The new knowledge is the equation X = T . A computation may involve values of variables from different sessions. As a result, some consistency conditions must be met, otherwise an error state is reached:

S E (Compute G (X = T ), σ) =      σ[∀C i ∈ G : σ i /(σ v i [X/V ], σ pk i ∪ {X = T })] if the condition on the computation holds, σ[σ i /Error] otherwise, where V := ε (T, ∪ Ci∈G σ v i ).
For each X(n) ∈ T , the evaluation of T is done with respect to the n last values of X that are fully defined. An error state is reached if n such values are not available. The condition on the computation is then:

∀C i ∈ G, X(n) ∈ T : size m σ v i V X [m]
is fully defined ≥ n. Semantics of the verification events are defined according to the (implicit) semantics of the underlying verification procedures. In each case, the knowledge state of the component is updated if the verification passes, otherwise the component reaches an Error state. The variable state is not affected.

S E (V erif y i (P roof j (E)), σ) =      σ[σ i /(σ v i , σ pk i ∪ new pk P roof )] if the proof is valid, σ[σ i /Error] otherwise, S E (V erif y i (Attest j (E)), σ) =      σ[σ i /(σ v i , σ pk i ∪ new pk Attest )] if the attestation is valid, σ[σ i /Error] otherwise.
The new knowledge new pk P roof and new pk Attest are defined as:

new pk P roof := Eq Eq ∈ E ∨ ∃C k : Attest k (E ) ∈ E ∧ Eq ∈ E ∧ T rust i,k ∈ σ pk i and new pk Attest := {Eq | Eq ∈ E ∧ T rust i,j ∈ σ pk i }.
In the session case, the knowledge state is reinitialized and a new entry is added in the variable states:

S E (Session, σ) = σ[∀i : σ i /(upd v , {T rust i,j | ∃C j : T rust i,j ∈ A})],
TRANSACTIONS ON DATA PRIVACY 11 (2018) where the new variable state upd v is such that σ v i (X) := append(σ v i (X), ⊥) for all variables X ∈ V ar, and σ v i (c) := append(σ v i (c), last(σ v i (c))) for all constants c ∈ Const. The session event is not local to a component, all component states are updated. As a result, we associate to each global state σ a unique number, noted s(σ), which indicates the number of sessions. In the initial state, s(σ) := 1, and at each Session event, s(σ) is incremented.

In the reset case, all values are dropped and the initial state is restored:

S E (Reset, σ) = Init A .
This ends the definition of the semantics of trace of events. The semantics S(A) of an architecture A is defined as the set of states reachable by compatible traces.

Extension of the privacy logic

The privacy logic is enhanced to express access to n values of a given variable. The formula Has i represents n ≥ 1 accesses by C i to some variable X.

ϕ ::= Has i (X (n) ) | Has i (c) | Has none i (X) | Has none i (c) | K i (Eq) | ϕ 1 ∧ ϕ 2 Eq ::= P red(T 1 , . . . , T m )
Several values of the same variables from different sessions can provide information about other variables, which is expressed through the dependence relation. The semantics S(ϕ) of a property ϕ ∈ L P remains defined as the set of architectures where ϕ is satisfied. The fact that ϕ is satisfied by a (consistent) architecture A is defined as follows.

• A satisfies Has i (X (n) ) if there is a reachable state in which X is fully defined (at least) n ≥ 1 times.

• A satisfies Has i (c) if there is a reachable state in which c is fully defined.

• A satisfies Has none i (X) (resp. Has none i (c)) if no compatible trace leads to a state in which C i assigns a value to X (resp. c).

• A satisfies K i (Eq) if for all reachable states, there exists a state in the same session in which C i can derive Eq.

• A satisfies ϕ 1 ∧ ϕ 2 if A satisfies ϕ 1 and A satisfies ϕ 2 .
A set of deductive rules for this privacy logic is given in Figure 6. One can show that this axiomatics is sound and complete with respect to the semantics above. The soundness theorem states that for all A, if A ϕ, then A ∈ S(ϕ). Completeness means that for all A, if A ∈ S(ϕ) then A ϕ. Due to the length of the proofs and the lack of place, we only give sketch for these proofs. Soundness is proved by induction on the derivation tree. For each theorem A ϕ, one can find traces satisfying the claimed property, or show that all traces satisfy the claimed property (depending on the kind of property). Completeness is shown by induction on the property ϕ. For each property belonging to the semantics, one can exhibit a tree that derives it from the architecture. A trace is said to be a covering trace if it contains an event corresponding to each primitive specified in an architecture A (except trust relations) and if for each primitive it contains as much events as the multiplicity (n) of the primitive. As a first step to prove soundness, it is shown that for all consistent architecture A, there exists a consistent trace θ ∈ T (A) that covers A. Then the soundness is shown by induction on the depth of the tree A ϕ.

TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 127

Has (n) i (X) ∈ A H1 A Hasi(X (n) ) Receive (n) i,j (S, E) ∈ A X ∈ E H2 A Hasi(X (n) ) A Hasi(X (1) ) HN A Has none i (X) Hasi(c) ∈ A H1' A Hasi(c) Receive (n) i,j (S, E) ∈ A c ∈ E H2' A Hasi(c) A Hasi(c) HN' A Has none i (c) Compute (n) G (X = T ) ∈ A Ci ∈ G H3 A Hasi(X (n) ) A Hasi(X (n) ) 1 ≤ m ≤ n H4 A Hasi(X (m) ) Depi(Y, X ) ∀X (n) ∈ X : A Hasi(X (n) ) ∀c ∈ X : A Hasi(c) H5
A Hasi(Y (1) )

Depi(c, X ) ∀X (n) ∈ X : A Hasi(X (n) ) ∀c ∈ X : A Hasi(c ) H5' A Hasi(c) Compute (n) G (X = T ) ∈ A Ci ∈ G K1 A Ki(X = T ) A ϕ1 A ϕ2 I∧ A ϕ1 ∧ ϕ2 E i Eq0 ∀Eq ∈ E: A Ki(Eq) K A Ki(Eq0) A Ki(Eq1) A Ki(Eq2) K∧ A Ki(Eq1 ∧ Eq2) V erif y (n) i (P roofj(E)) ∈ A Eq ∈ E K3 A Ki(Eq) V erif y (n) i (P roofj(E)) ∈ A Attest k (E ) ∈ E Eq ∈ E T rust i,k ∈ A K4 A Ki(Eq) V erif y (n) i (Attestj(E)) ∈ A T rusti,j ∈ A Eq ∈ E K5
A Ki(Eq) Figure 6: Set of deductive rules for the extended privacy logic

• Let us assume that A Has i (X (n) ), and that the derivation tree is of depth 1. By definition of D, such a proof is obtained by application of (H1), (H2) or (H3). In each case, it is shown (thanks to the existence of covering traces) that an appropriate trace can be found in the semantics of A, hence A ∈ S(Has i (X (n) )). The case of A Has i (c) is very similar.

• Let us assume that A K i (Eq), and that the derivation tree is of depth 1. By definition of D, such a proof is obtained by application of (K1), (K2), (K3), (K4) or (K5). In each case, starting from a state σ ∈ S i (A) such that s(σ ) ≥ n, it is first shown that there exists a covering trace θ ≥ θ that extends θ and that contains n corresponding events Compute G (X = T ) ∈ θ in n distinct sessions (for the K1 case, and other events for the other rules). Then by the properties of the deductive algorithmic knowledge, it is shown that the semantics of the property A ∈ S(K i (X = T )) holds.

• Let us assume that A Has i (X (n) ), and that the derivation tree is of depth strictly greater than 1. By definition of D, such a proof is obtained by application of (H4) or (H5).

In the first case, by the induction hypothesis and the semantics of properties, there exists a reachable state σ ∈ S(A) and n indices i 1 , . . . , i n such that σ v i (X)[i l ] is fully defined for all l ∈ [1, n]. This gives, a fortiori, A ∈ S(Has i (X (m) )) for all m such that 1 ≤ m ≤ n.

TRANSACTIONS ON DATA PRIVACY 11 (2018) 128 Julien Bringer, Hervé Chabanne, Daniel Le Métayer, Roch Lescuyer In the second case, we have that (Y, {X

(n1) 1 , . . . , X (nm) m , c 1 , . . . , c q }) ∈ Dep i , that ∀l ∈ [1, m] : A Has i (X (n l ) l
) and ∀l ∈ [1, q] : A Has i (c l ). The proof shows the existence of a covering trace that contains an event Compute G (Y = T ) (where i ∈ G), allowing to conclude that A ∈ S(Has i (Y (1) )).

Again, the corresponding cases for constant are very similar.

• A derivation for Has none is obtained by application of (HN). The proof assume, towards a contradiction, that A ∈ S(Has none i (X)). It is shown, by the architecture semantics, that there exists a compatible trace that enable to derive A Has [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] i (X). However, since (HN) was applied, we have A Has [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] i (X), hence a contradiction.

• The last case (the conjunction ∧) is fairly straightforward.

The completeness is proved by induction over the definition of ϕ.

• Let us assume that A ∈ S(Has i (X (n) )). By the architecture semantics and the semantics of traces, it is shown that the corresponding traces either contain events where X is computed, received or measured, or that some dependence relation on X exists.

In the first case, we have A Has i (X (n) ) by applying (respectively) (H1), (H2), or (H3) (after an eventual application of (H4)). In the last case, the proof shows how to exhibit a derivation tree to obtain A Has i (X (n) ) (the (H5) rule is used).

• Let us assume that A ∈ S(Has none i (X)). By the semantics of properties, this means that in all reachable states, X does not receive any value. The proof shows that A S(Has i (X (1) )), otherwise A ∈ S(Has none i (X)) would be contradicted. So as a conclusion, A Has none i (X) by applying (HN).

• The constant cases A ∈ S(Has i (c) and A ∈ S(Has none i (c)) case are similar to the variable cases.

• Let us assume that A ∈ S(K i (Eq)). By the semantics of properties this means that for all reachable states, there exists a later state in the same session where the knowledge state enables to derive Eq. By the semantics of architecture, we can exhibit a compatible trace that reaches a state where Eq can be derived. By the semantics of compatible traces, the proof shows, by reasoning on the events on the traces, that A K i (Eq) by applying either (K1), (K2), (K3), (K4) or (K5).

• Finally the conjunctive case is straightforward.

Extension of the Match-On-Card to the identification paradigm

We now show of the extended framework can be used to reason about the privacy properties of a biometric system where some information leaks after several sessions of the same protocol.

The biometric system introduced in [START_REF] Bringer | Extending matchon-card to local biometric identification[END_REF] aims at extending the MOC technology (cf. Section 4.3) to the identification paradigm. A quantized version -corresponding to short binary representations of the templates -of the database is stored inside a secure module, playing the role of the card in the MOC case. From each biometric reference template, a quantization is computed, using typically a secure sketch scheme [START_REF] Juels | A fuzzy commitment scheme[END_REF][START_REF] Dodis | Fuzzy extractors: How to generate strong keys from biometrics and other noisy data[END_REF]. The reference TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 129 database is encrypted and stored outside the secure module, whereas the quantizations of the templates are stored inside. The verification step is processed as follows. Suppose one wants to identify himself in the system. A terminal captures the fresh biometrics, extracts a template, computes its quantization qs and sends them to the secure module. Then, the module proceeds to a comparison between the fresh quantization and all enrolled quantizations qr. The C nearest quantizations, for some parameter C of the system, are the C potential candidates for the identification. Then, the module queries the C corresponding (encrypted) templates to the database (by using the list of indices ind of those C nearest quantized versions qr of the enrolled templates). This gives the module the access to the set sebr of the C encrypted templates. The module decrypts them, and compares them with the fresh template bs. The module finally sends its response to the terminal: 1 if one of the enrolled templates is close enough to the fresh template, 0 otherwise. Figure 7 gives a graphical representation of the resulting architecture. N denotes the size of the database (i.e. the number of enrolled users), Q the size of the quantizations, and C the number of indices asked by the card. The ranges are Range(BR, ebr, qr) = N, Range(rd, THR, bs, qs, dec) = 1, and Range(ind, sebr, sbr) = C. The set F un of functions contains the extraction procedure Extract, the encryption and decryption procedures Enc and Dec, the (non-invertible) quantization Quant of the biometric templates, the comparison of the quantizations QComp, which takes as inputs two sets of quantizations and the parameter C, the selection of the encrypted templates EGet, and finally the matching µ, which takes as arguments two biometric templates and the threshold THR. The biometric reference templates are enrolled by the issuer (Has I (BR)). A verification process is initiated by the terminal T receiving as input a raw biometric data rd from the user U. T extracts the fresh biometric template bs from rd using the function Extract ∈ F un. The architecture then contains, as other biometric systems, Receive T,U ({}, {rd}) and Compute T (bs = Extract(rd)) and the Dep T relation is such that (bs, {rd}) ∈ Dep T . The user receives the final decision dec from the terminal: Receive U,T ({}, {dec}). To sum up, the architecture is described as follows in the framework of Section 2: The absence of such a relation in other dependencies prevents the corresponding components to get access to the plain references, even if they get access to the ciphertexts.

Learning from the selected quantizations

Let us now discuss the following point: the formalism of Section 2 is insufficient to consider the leakage of the sensitive biometric data stored inside the module. In A mi , we would like that the terminal gets no access to the quantizations: A mi ∈ Has none T (qr). It is indeed possible to derive A mi Has none T (qr), thanks to the (HN) rule. According to the notations of [START_REF] Antignac | Privacy architectures: Reasoning about data minimisation and integrity[END_REF], where Has i (X) stands for Has i (X (1) ) in this paper, we have: This corresponds to the intuition saying that quantizations are protected since they are stored in a secure hardware element. However, an attack (described in [START_REF] Bringer | Blackbox security of biometrics (invited paper)[END_REF]) shows that, in practice, quantizations can be learned if a sufficient number of queries to the module is allowed. The attack roughly proceeds as follows (we drop the masks for sake of clarity). The attacker maintains a N × Q table (say T ) of counters for each bit to be guessed. All entries are initialized to 0. Then it picks Qbits random vector Q and sends it to the module. The attacker observes the set of indices ind ⊆ [1, N] corresponding to the encrypted templates asked by the module. It updates its table T as follows, according to its query Q and the response ind:

X : Dep T (qr, X) ∈ A mi
for each i ∈ [1, N] and j ∈ [1, Q], it decrements the entry T [i][j] if Q[j] = 0, and increments it if Q[j] = 1.
At the end of the attack, the N quantizations are guessed from the signs of the counters. The number of queries made to the module is the crucial point in the attack above (and generally in other black-box attacks against biometric systems [START_REF] Bringer | Blackbox security of biometrics (invited paper)[END_REF]). Our extended model enables to introduce a bound on the number of actions allowed to be performed. We now use this model to integrate such a bound in the formal architecture description. Let A mi-e (n) TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 131 be the following architecture, for some n ≥ 1:

A mi-e (n) := Has I (BR), Has In addition to the dependence of A mi , the dependence relations indicates that the leakage is conditioned by a specific link mapping between the outsourced ciphertexts and the stored quantizations: Dep mi-e T (qr, {ind (N•Q) , qs (N•Q) }). Furthermore, the module may learn the entire database ebr in a number of queries depending on the size of the database and the number of indices asked by the module: Dep mi-e M (ebr, {sebr ( N/C ) }).

Strengthened variants of the architecture

Now, based on some counter-measures of the attacks indicated in [START_REF] Bringer | Blackbox security of biometrics (invited paper)[END_REF], we express several variants of the architecture A mi-e . For each variant, the deductive rules D for the property language L P are used to show that, for some conditions on the parameters, the quantizations qr are protected.

Variant 1

As a first counter-measure, the module could ask the entire database at each invocation. It is rather inefficient, and, in some sense, runs against to initial motivation of its design. However, this can be described within the language L A , and, in practice, can be manageable for small databases. This architecture, denoted A mi-e1 , is given by A mi-e (n) for some n ≥ 1, except that Dep mi-e1 T := Dep mi T . It is now possible to prove that the quantizations are protected, even in presence of several executions of the protocols. Since the relations Dep T no longer contains a dependence leading to qr, an application of (HN) becomes possible and gives the expected property.

TRANSACTIONS ON DATA PRIVACY 11 (2018)

X : Dep T (qr, X) ∈ A mi-e1 Has (n) T (qr) ∈ A mi-e1 j : Receive (n) T,j (S, {qr}) ∈ A mi-e1 T : Compute (n) T (qr = T ) ∈ A mi-e1 ∀n : A Has T (qr (n) ) HN A Has none T (qr)

Variant 2

In the precedent variant, the effect of the counter-measure is the withdrawal of the dependence relation. We now consider architectures where such a dependency is still given, but where counter-measures are used to prevent a critical bound on the number of queries to be reached. A first measure is to block the number of attempts the terminal can make. The module can detect it and refuse to respond. This architecture, denoted A mi-e2 , is given by A mi-e (B), for some B N • Q. As a result, the Has none i (qr) property can be derived. In particular one must show that A mi-e2 Has T (ind (N•Q) ), in order to prevent the dependence rule H5 to be applied.

S : Receive

(B) T,M (S, {ind}) ∈ A mi-e2 Has (B) T (ind) ∈ A mi-e2 B < N • Q T : Compute (B) T (ind = T ) ∈ A mi-e2 A mi-e2 Has T (ind (N•Q) )
An application of HN enables to conclude.

Dep mi-e2 T (qr, {ind (N•Q) }) ∈ A mi-e2 Has (B) T (qr) ∈ A mi-e2 j : Receive (B) T,j (S, {qr}) ∈ A mi-e2 A mi-e2 Has T (ind (N•Q) ) T : Compute (B)
T (qr = T ) ∈ A mi-e2 A mi-e2 Has T (qr (1) ) HN A mi-e2 Has none T (qr)

Variant 3

In the precedent variant, the terminal cannot accumulate enough information since he cannot query the module enough times to derive a useful knowledge. We now describe a variant where the terminal has no bound on the number of times it asks the module, but where the system is regularly reinitialised, so that the accumulated information becomes useless.

The leakage of the system runtime is dependent on some association between the quantizations qr and the encrypted database ebr; namely the association π that maps the quantization qr[i] = Quant(BR[π(i)]) to the encrypted template from which it has been computed ebr[π(i)] = Enc(BR[π(i)]). Once this mapping is changed, the information is canceled. For instance the database can be randomly permuted after B queries to the secure module.

Formally, this is caught by adding a Reset primitive to the architecture. Let A mi-e3 be the architecture defined as A mi-e3 := A mi-e2 ∪{Reset}. The semantics of the Reset events ensures that no more than B values of ind will be gathered by the terminal for a fixed mapping. The proof that A mi-e3 Has none T (qr) is as the proof that A mi-e2 Has none T (qr).

TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 133

Related works

Privacy concerns related to the use of biometric data has attracted a lot of attention in the media (for instance, with the introduction of a fingerprint identity sensor in iPhones) and among lawyers and policy makers 5 . Most studies in the computer science community are done on a case by case basis and at a lower level than the architectures described here. For instance, [START_REF] Tang | A formal study of the privacy concerns in biometric-based remote authentication schemes[END_REF] proposes a security model for biometric-based authentication taking into account privacy properties -including impersonation resilience, identity privacy or transaction anonymity -and applies it to biometric authentication. The underlying proofs rely on cryptographic techniques related to the ElGamal public key encryption scheme. Other works such as [START_REF] Kanak | BioPSTM: a formal model for privacy, security, and trust in template-protecting biometric authentication[END_REF][START_REF] Lai | Privacy-security trade-offs in biometric security systems -Part I: single use case[END_REF][START_REF] Lai | Privacy-security trade-offs in biometric security systems -Part II: multiple use case[END_REF] develop formal models from an information theoretic perspective relying on specific representations of biometric templates akin to error correcting codes.

As far as formal approaches to privacy are concerned, two main categories can be identified: the qualitative approach and the quantitative approach. Most proposals of the first category rely on a language that can be used to define systems and to express privacy properties. For example process calculi such as the applied pi-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] have been applied to define privacy protocols [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols: A taster[END_REF]. Other studies [START_REF] Barth | Privacy and contextual integrity: Framework and applications[END_REF][START_REF] Moritz | S4P: A generic language for specifying privacy preferences and policies[END_REF] involve dedicated privacy languages. The main departure of the approach advocated in this paper with respect to this trend of work is that we reason at the level of architectures, providing ways to express properties without entering into the details of specific protocols. Proposals of the second category rely on privacy metrics such as k-anonymity, l-diversity, or -differential privacy [START_REF] Dwork | Differential privacy[END_REF] which can be seen as ways to measure the level of privacy provided by an algorithm. Methods [START_REF] Mcsherry | Privacy integrated queries: an extensible platform for privacy-preserving data analysis[END_REF] have been proposed to design algorithms achieving privacy metrics or to verify that a system achieves a given level of privacy. The contributions on privacy metrics are complementary to the work described in this paper. We follow a qualitative (or logical) approach here, proving that a given privacy property is met (or not) by an architecture. As suggested in the next section, an avenue for further research would be to cope with quantitative reasoning as well, using inference systems to derive properties expressed in terms of privacy metrics.

Several authors [START_REF] Sada G Ürses | Engineering Privacy by Design[END_REF][START_REF] Kerschbaum | Privacy-preserving computation (position paper)[END_REF][START_REF] Le | design: A formal framework for the analysis of architectural choices[END_REF][START_REF] Mulligan | Bridging the gap between privacy and design[END_REF][START_REF] Spiekermann | Engineering privacy[END_REF] have already pointed out the complexity of "privacy engineering" as well as the "richness of the data space" [START_REF] Sada G Ürses | Engineering Privacy by Design[END_REF] calling for the development of more general and systematic methodologies for privacy by design. For example, [START_REF] Kerschbaum | Privacy-preserving computation (position paper)[END_REF][START_REF] Maffei | Security and privacy by declarative design[END_REF] point out the complexity of the implementation of privacy and the large number of options that designers have to face. To address this issue and favour the adoption of these tools, [START_REF] Kerschbaum | Privacy-preserving computation (position paper)[END_REF] proposes a number of guidelines for the design of compilers for secure computation and zero-knowledge proofs whereas [START_REF] Fournet | ZQL: A compiler for privacy-preserving data processing[END_REF] provides a language and a compiler to perform computations on private data by synthesizing zero-knowledge protocols. None of these proposals addresses the architectural level and makes it possible to get a global view of a system and to reason about its underlying trust assumption.

Conclusion

This work is the result of a collaboration between academics, industry and lawyers to show the applicability of the privacy by design approach to biometric systems and the benefit of formal methods to this end. Indeed, even if privacy by design becomes a legal obligation in the European Union [36] its application to real systems is far from obvious. We have presented in the same formal framework a variety of architectural options for privacy preserving biometric systems. We also have introduced an extension of this formal framework in order to catch the leakage due to the system runtime. One of the main advantages of the approach is to provide formal justifications for the architectural choices and a rigorous basis for their comparison. Table 1 summarizes the main properties of the architectures reviewed in the first part of this paper. One of the most interesting pieces of information is the trust assumptions which are highlighted by the model. The first line shows that A ed is the architecture in which the strongest trust in put in the terminal that does not have to trust any other component apart from the issuer and is able to get access to br. Architecture A hsm is a variant of A ed ; it places less trust in the terminal that has to trust the hardware security module to perform the matching. A hom is the architecture in which the terminal is less trusted: it has to trust the issuer, the hardware security module and the server for all sensitive operations and its role is limited to the collection of the fresh biometric trait and the computation of the fresh template. Architecture A moc is similar to this respect but all sensitive operations are gathered into a single component, namely the smart card. It should be clear that no solution is inherently better than the others considering that extra, technical or non technical (organizational, economic, etc.) constraints may have to be taken into account and, depending on the context of deployment and the technology used, some trust assumptions may be more reasonable than others. From the strict privacy point of view however, the match on card architecture provides the best guarantees since only the secure module has to be trusted and this module hosts the matching operation and has exclusive access to the biometric reference template. In any event, the most important in the design process is to be able to understand the underlying trust assumptions of a particular choice of architecture and the consequences in terms of privacy. Components are: user U, terminal T, server S, secure module M (used as a generic name for a hardware security module or a card C), issuer I.

A trust relation (i, j) means that component i trusts component j.

Table 1: Comparison between architectures

A benefit of the formal approach followed in this paper is that it can provide the foundations for a systematic approach to privacy by design. A proof of concept implementation of a system to support designers in their task has been proposed in [START_REF] Antignac | Trust driven strategies for privacy by design[END_REF]. In this system, the user can introduce his privacy and integrity requirements (as well as any requirements imposed by the environment such as the location of a given operation on a designated component) and choose different options for the distribution of the operations and the trust assumptions. Architectures can be initially defined in a purely informal way and then translated into a formal model. A tool integrating the approach can be used by designers to build and TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 135 verify architectures. Designers without any knowledge or even interest in formal methods can use the non formal part of the framework. They can explore the design space based on initial inputs provided in a non formal language and analyse the suggested architectures based on their graphical representations. Designers who want to obtain formal guarantees can try to prove properties of their architectures, either automatically or with the help of a verification tool integrated within the design environment.

As stated above, we focus on the architectural level in this paper. As a result, we do not cover the full development cycle. Preliminary work has been done to address the mapping from the architecture level to the protocol level to ensure that a given implementation, expressed as an applied pi-calculus protocol, is consistent with an architecture [START_REF] Ta | Privacy by design: On the conformance between protocols and architectures[END_REF]. As far as the formal approach is concerned, it would also be interesting to study how it could be used in the context of future privacy certification schemes. This would be especially interesting in the context of the European General Data Protection Regulation [36] which promotes not only privacy by design but also privacy seals.

Figure 2 Figure 2 :

 22 Figure 2: Graphical representations

Figure 3 :

 3 Figure 3: Classical architectures with an encrypted database

A

  ed := Has I (br), Has U (rd), Has T (thr), Compute I (ebr = Enc(br)), Receive S,I ({Attest I (ebr = Enc(br))}, {ebr}), Receive T,S ({Attest I (ebr = Enc(br))}, {ebr}), T rust T,I , V erif y T (Attest I (ebr = Enc(br))), Receive T,U ({}, {rd}), Compute T (bs = Extract(rd)), Compute T (br = Dec(ebr)), Compute T (dec = µ(br , bs, thr)), Receive U,T ({}, {dec}) The properties of the encryption scheme are captured by the dependence and deductive relations. The dependence relations are: (ebr, {br}) ∈ Dep I , and {(bs, {rd}), (dec, {br , bs, thr}), (br , {ebr}), (br, {ebr})} ⊆ Dep T . Moreover the deductive algorithm relation contains: {ebr = Enc(br)} {br = Dec(ebr)}.

A

  hsm := Has I (br), Has U (rd), Has M (thr), Compute I (ebr = Enc(br)), Receive S,I ({Attest I (ebr = Enc(br))}, {ebr}), Receive T,S ({Attest I (ebr = Enc(br))}, {ebr}), T rust T,I , V erif y T (Attest I (ebr = Enc(br))), Receive T,U ({}, {rd}), Compute T (bs = Extract(rd)), Receive M,T ({}, {bs, ebr}), Compute M (br = Dec(ebr)), Compute M (dec = µ(br , bs, thr)), V erif y T ({Attest M (dec = µ(br , bs, thr))}), T rust T,M , Receive T,M (A, {dec}), V erif y T ({Attest M (br = Dec(ebr))})

Figure 4 :

 4 Figure 4: Comparison over encrypted data with homomorphic encryption

  br), ebs = Enc(bs), edec = Hom-µ(ebr, ebs, thr)} {Dec(edec) = µ(br, bs, thr)} (1) The dependence relations include the following: {(bs, {rd}), (ebs, {bs})} ⊆ Dep T ; (ebr, {br}) ∈ Dep I ; {(br, {ebr}), (bs, {ebs}), (dec, {edec})} ⊆ Dep M . Architecture A hom is defined as fol-TRANSACTIONS ON DATA PRIVACY 11 (2018) Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures 121 lows: A hom := Has I (br), Has U (rd), Has S (thr), Compute I (ebr = Enc(br)), Receive S,I ({Attest I ({ebr = Enc(br)})}, {ebr}), Receive T,U ({}, {rd}), Compute T (bs = Extract(rd)), Compute T (ebs = Enc(bs)), Receive S,T ({}, {ebs}), Compute S (edec = Hom-µ(ebr, ebs, thr)), Receive T,S (A, {edec}), V erif y T (Attest I ({ebr = Enc(br)})), V erif y T (Attest S ({edec = Hom-µ(ebr, ebs, thr)})), T rust T,S , T rust T,I , Receive M,T ({}, {edec}), Compute M (dec = Dec(edec)), Receive T,M ({Attest M ({dec = Dec(edec)})}, {dec}), T rust T,M , V erif y T (Attest M ({dec = Dec(edec)})), Receive U,T ({}, {dec})

Figure 5 :

 5 Figure 5: Biometric verification using the Match-On-Card technology In this architecture, the terminal is assumed to trust the smart card. This trust assumption is justified by the fact that the card is a tamper-resistant hardware element. This architecture is simpler than the previous ones but not always possible in practice (for a combination of technical and economic reasons) and may represent a shift in terms of trust if the smart card is under the control of the user. More formally, the MOC architecture is composed of a user U, a terminal T, and a card C. The card C attests that the templates br and bs are close (with respect to the threshold thr): A moc := Has C (br), Has U (rd), Has C (thr), Receive T,U ({}, {rd}), Compute T (bs = Extract(rd)), Receive C,T ({}, {bs}), Compute C (dec = µ(br, bs, thr)), Receive U,T ({}, {dec}), Receive T,C ({Attest C (dec = µ(br, bs, thr))}, {dec}), V erif y T ({Attest C (dec = µ(br, bs, thr))}), T rust T,C

  j } The data structure List over a set S denotes the finite ordered lists of elements of S, size(L) denotes the size of the list L, and () is the empty list. For a non-empty list L = (e 1 , . . . , e n ) ∈ S n where size(L) = n ≥ 1, L[m] denotes the element e m for 1 ≤ m ≤ n, last(L) denotes L[n], and append(L, e) denotes the list (e 1 , . . . , e n , e) ∈ S n+1 . Let σ := (σ 1 , . . . , σ N ) denote the global state (i.e. the list of states of all components) defined over (State ⊥ ) N and σ v i and σ pk i denote, respectively, the variable and the knowledge state of the component C i .

Figure 7 :

 7 Figure 7: Architecture of the extension of the Match-On-Card technology to biometric identification. The dotted red line indicates the location of the comparison.

A

  mi := Has I (BR), Has U (rd), Has M (C), Has M (THR), Compute I (ebr = Enc(BR)), Compute I (qr = Quant(BR)), Compute T (bs = Extract(rd)), Compute T (sebr = EGet(ebr, ind)), TRANSACTIONS ON DATA PRIVACY 11 (2018) The issuer encrypts the templates and computes the quantizations, which is expressed by the dependencies: Dep mi I := {(ebr, {BR}), (qr, {BR})}. The terminal and module computations are reflected in the dependencies as well: Dep mi T := {(bs, {rd}), (qs, {bs})}, (sebr, {bs, ind})}. The dependency relation of the module reflects its ability to decrypt the templates: Dep mi M := {(ind, {qs, qr, C}), (sbr, {sebr}), (dec, {sbr, bs, THR}), (BR, {ebr})}.

  Has T (qr) ∈ A mi j, S : Receive T,j (S, {qr}) ∈ A mi T : Compute T (qr = T ) ∈ A mi A Has T (qr) HN A Has none T (qr)

U

  (rd), Has M (C), Has M (THR), Compute

I

  (ebr = Enc(BR)), Compute

I

  (qr = Quant(BR)), Compute

T

  (bs = Extract(rd)), Compute

T

  (sebr = EGet(ebr, ind)), Compute

T

  (qs = Quant(bs)), Compute

M

  (ind = QComp(qs, qr, C)), Compute (n) M (sbr = Dec(sebr)), Compute

M

  (dec = µ(sbr, bs, THR)), Receive(n) S,I ({Attest I (ebr = Enc(BR))}, {ebr}), Receive (n) T,U ({}, {rd}), Receive (n) T,S ({Attest I (ebr = Enc(BR))}, {ebr}), Receive (n) M,T ({}, {qs}), Receive (n) M,I ({Attest I (qr = Quant(BR))}, {qr}), Receive (n) T,M ({}, {ind}), Receive (n) M,T ({}, {sebr, bs}), Receive (n) T,M ({}, {dec}), T rust T,I , T rust M,I , T rust T,M , V erif y (n) T (Attest I (ebr = Enc(BR))), V erif y (n) T ({Attest M (dec = µ(sbr, bs, THR))}), V erif y (n) M (Attest I (qr = Quant(BR))), V erif y (n)T ({Attest M (sbr = Dec(ebr))})

  I), (T, M), (T, S)

  his deductive system i . Another relation, Dep i , is used to take into account dependencies between variables. Dep i (Y, X ) means that if C i can obtain the values of each variable in the set of variables X , then it may be able to derive the value of Y . The absence of such a relation is an assumption that C i cannot derive the value of Y from the values of the variables in X . It should be noted that this dependency relation is associated with a given component: different components may have different capacities. For example, if component C i is the only component able to decrypt a variable ev to get the clear text v, then Dep i (v, {ev}) holds but Dep j (v, {ev}) does not hold for any j = i.

  1. The same rule can be applied here to prove A hom Has M (ebr) exploiting the fact that neither (br, {edec}) nor (br, {dec}) belong to Dep M .

TRANSACTIONS ON DATA

PRIVACY 11 (2018)

Julien Bringer, Hervé Chabanne, Daniel Le Métayer, Roch Lescuyer

Except for the Session event.

Except for Trust primitives, which cannot be instantiated into events because they are global assumptions.TRANSACTIONS ONDATA PRIVACY 11 (2018)

For example with a proposal adopted by the French Senate in May 2014 to introduce stronger requirements for the use of biometrics.

This work has been partially funded by the French ANR-12-INSE-0013 project BIOPRIV and the European FP7-ICT-2013-1.5 project PRIPARE. Earlier and partial versions of this work appeared in FM 2015 [10] and ISC 2015 [11] conferences.


domain: math shs

text:
Rahim Kouki
email: rahim.kouki@gmail.com

Yassine Hachaïchi
email: hachaichi.ens@gmail.com

Polynomial approximation: From history to teaching

Keywords: Taylor approximation, dialectic tool-object, syntax, semantics

Introduction and research problem

Our motivation for engaging in this research project relies on recurrent students' difficulties in the appropriation of the concept of Taylor approximation. Despite the richness of this concept as a tool in many fields of application (e.g calculation of limits, local study of a function and the study of physical phenomena), for what we know, there is little research on this topic in mathematics education. Beyond the lack of comprehension of the notion of convergence for Taylor series [START_REF] Martin | Differences between experts 'and students' conceptual images of mathematical structure of Taylor series convergence[END_REF], we hypothesize that the articulation between syntax and semantics is not clear for students, creating a fuzzy area that prevents them from being able to apply Taylor approximation as a tool in applied mathematics. In this paper, we summarize the main results of our epistemological investigation and the first element of a didactic study of teaching material on this topic, in order to identify paths for improving its teaching and learning.

Theoretical framework

Throughout our epistemological and didactic investigations, we refer to the dialectics between semantics (graphic interpretation, dynamic interpretation and numerical approximation) and syntax (the different formulations of the Taylor approximation), including their articulation with the toolobject dialectic [START_REF] Douady | Tool, Object, Setting, Window: Elements for Analysing and Constructing Didactical Situations in Mathematics[END_REF] and the registers of semiotic representations [START_REF] Duval | A Cognitive Analysis of Problems of Comprehension in the Learning of Mathematics[END_REF]. (this approach is developed and used in Kouki, to appear).

Epistemological investigation

We outline the evolution of the mathematical object known as "Taylor approximation" through a historical and epistemological investigation. Our study emphasizes the co-existence of different types of techniques mainly with geometric, algebraic and dynamic origins that contributed to the emergence and development of this object (Kouki, Belhaj Amor, & Hachaïchi, 2016).

Our research identifies key moments in the development of infinitesimal calculus and local approximations which led to the calculus as it is taught nowadays. In particular, the works of Roberval, Euler, Fermat, Leibniz, Newton, until Taylor and Weierstrass are significant in the development of Taylor approximations.

Didactic investigation

Based on our epistemological investigation, we have conducted a didactic study of the Tunisian curriculum, textbooks and course handouts on Taylor approximation. The Tunisian curriculum, three handwritten courses and four handbooks were analyzed. Through this study, we confront the various dimensions of this concept revealed by the epistemological investigation with those that are present in teaching materials.

This study supports the hypothesis that there are gaps in the teaching of Taylor approximation. In particular, some of them are due to insufficiencies of graphical representations and numerical approximation, corresponding to a deficit of semantic work, the emphasis being put on the syntax.

Conclusion

The epistemological and didactical investigations summarized in this paper are part of a larger project aiming at developing propositions for enhancing the teaching and learning of Taylor approximation. This enhancement can help to foster an appropriation of the concept allowing to use it in the various applications undergraduate students could meet in further studies, in particular in applied mathematics.

Proceedings of CERME10