Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures
Julien Bringer Herve Chabanne Daniel Le Metayer Roch Lescuyer

Theoretical studies of superconductivity in doped  BaCoSO
    Jiangping Hu
    December 30, 2023
=========================================================




This work aims to show the applicability, and how, of privacy by design approach to biometric systems and the benefit of using formal methods to this end. Starting from a general framework that has been introduced at STM in 2014, that enables to define privacy architectures and to formally reason about their properties, we explain how it can be adapted to biometrics. 
The choice of particular techniques and the role of the components (central server, secure module, biometric terminal, smart card, etc.) in the architecture have a strong impact on the privacy guarantees provided by a biometric system.
In the literature, some architectures have already been analysed in some way. However, the existing proposals were made on a case by case basis, which makes it difficult to compare them and to provide a rationale for the choice of specific options.
In this paper, we describe, on different architectures with various levels of protection, how a general framework for the definition of privacy architectures can be used to specify the design options of a biometric systems and to reason about them in a formal way.





§ INTRODUCTION



Applications of biometric recognition, as the most natural tool to identify or to authenticate a person, have grew over the years. They now vary from criminal investigations and identity documents to many public or private usages, like physical access control or authentication from a smartphone toward an internet service provider. Such biometric systems involve two main phases: enrolment and verification (either authentication or identification) <cit.>. Enrolment is the registration phase, in which the biometric traits of a person are collected and recorded within the system.
In the authentication mode, a fresh biometric trait is collected and compared with the registered one by the system 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 discriminative features, leading to what is called a biometric template. 

With the increased use of biometric systems, and more recently with the development of personal data protection regulations, the issues related to the protection of the privacy of the used biometric traits have received particular attention. As leakage of biometric traits may lead to privacy risks, including tracking and identity theft, privacy by design approach is often needed.

As a security technical challenge, it has attracted a lot of research works since at least 15 years and a wide-array of well-documented primitives, such as encryption, homomorphic encryption, secure multi-party computation, hardware security, template protection etc.,  are known in the litterature. With those building tools, various architectures have been proposed to take into account privacy requirements in the implementation of privacy preserving biometric systems. Some solutions involve dedicated cryptographic primitives such as secure sketches <cit.> and fuzzy vaults <cit.>, others rely on adaptations of existing cryptographic tools <cit.> or the use of secure hardware solutions <cit.>.
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.

Here, we aim to show how to use and adapt a general framework that has been introduced in <cit.> for the formal definition and validation of privacy architectures.  The goal is 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 achieved privacy properties.

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 even becoming more and more often legally compelled, as for instance in European Union with the General Data Protection Regulation <cit.> entering into force. 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.

This work, which has been conducted in particular within the French ANR research project BioPriv <cit.>, an interdisciplinary project involving lawyers and computer scientists, can be seen as an illustration of the feasibility of the privacy by design approach in an industrial environment. A step in this direction has been described in <cit.> which introduces a system for defining privacy architectures and reasoning about their properties. In Section <ref>, we provide an outline of this framework. Then we show how this framework can be used to apply a privacy by design approach to the implementation of biometric systems. In Sections <ref> to <ref>, 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 <ref>. 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 <cit.>.
To adress this issue, in Section <ref>, we propose an extension of the formal framework, in which information leaks spanning over several sessions of the system can be expressed. In Section <ref>, we apply the extended model to analyse biometric information leakage in several variants of biometric system architectures.

Finally, Section <ref> sketches related works and Section <ref> concludes the paper with suggestions of avenues for further work.





§ GENERAL APPROACH



The work presented in <cit.> 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 taken 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 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 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 <cit.> relies on a dedicated epistemic logic.
Indeed, because privacy is closely connected with the notion of knowledge, epistemic logics <cit.> form an ideal basis to reason about privacy properties but standard epistemic logics based on possible worlds semantics suffer from a weakness (called “logical omniscience” <cit.>) 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 Term of terms T defined as follows, where c represents constants (c ∈ Const), X variables (X ∈ Var) and F functions (F ∈ Fun):

    [               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);                                                                                               |           Verify_i (St)                       |              Trust_i, j;                         ];                                                                                                                                                                                                                                                                                                                                                                                                                                                       ;                                                                                        [                [6mm]St                ::= Pro                      |                    Att                    Att    ::= Attest_G ({Eq});                    Pro    3l::= Proof_i ({P})                     Eq ::= Pred (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 Pred := { =, ∈}.
Compute_G (X = T) means that the set of components G can compute the term T and assign its value to X and Trust_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, namely attestations: Attest_i ({Eq}) is the declaration by the component i that the properties in {Eq} hold; and proofs: Proof_i ({P}) is the delivery by C_i of a set of proofs of properties.
Verify_i is the verification by component C_i of the corresponding statements (proof or authenticity).
In any case, the architecture level does not provide details on how a verification is done.
The verification of an attestation concerns the authenticity of the statement only, not its truth that C_i may even not be able to carry out itself.
In practice, it could be the verification of a digital signature.

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_i^none (X)                                         |                                K_i (Prop)                                         |                                 φ_1 ∧ φ_2                                                                                    ;                                      Prop                                       ::= 7lPred (T_1, …, T_n)  |  Prop_1  ∧ Prop_2;                                           ]

Has_i(X) and Has_i^none(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 <cit.> that makes it possible to avoid the logical omniscience 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 his deductive system ▹_i.

Another relation, Dep_i, is used to take into account dependencies between variables.
Dep_i (Y, 𝒳) means that if C_i can obtain the values of each variable in the set of variables 𝒳, 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 X from the values of the variables in 𝒳.
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.

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 <cit.>.
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 <ref>).
The semantics S (φ) of a property φ is defined as the set of architectures meeting φ.
For example, A ∈ S (Has_i^none (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 <ref>.





§ 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 , , etc. rather than indexed variables C_i to denote components.
By abuse of notation, we will use component names instead of indices and write, for example, Receive_𝖴, 𝖳 ({}, {𝚍𝚎𝚌}).
Type letters , , etc. denote variables.
The set of components of an architecture is denoted by 𝒥.

The variables used in biometric system architectures are the following:




  * A biometric reference template  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  provided by the user during the verification phase.

  * A fresh template  derived from  during the verification phase.

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

  * The output  of the verification which is the result of the matching between the fresh template  and the enrolled templates , considering the threshold .

 
Two components appear in all biometric architectures: a component 𝖴 representing the user, and the terminal  which is equipped with a sensor used to acquire biometric traits.
In addition, biometric architectures may involve an explicit issuer , enrolling users and certifying their templates, a server  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  to store the enrolled templates (and in some cases to perform the matching).
Figure <ref> introduces some graphical representations used in the figures of this paper.



In this paper, we focus on the verification phase and assume that enrolment has already been done.
Therefore the biometric reference templates are stored on a component which can be either the issuer (Has_𝖨 (𝚋𝚛)) or a smart card (Has_𝖢 (𝚋𝚛)).
A verification process is initiated by the terminal  receiving as input a raw biometric data  from the user .
 extracts the fresh biometric template  from  using the function Extract ∈ Fun.
All architectures A therefore include Receive_𝖳, 𝖴 ({}, {𝚛𝚍}) and Compute_𝖳 (𝚋𝚜 = Extract (𝚛𝚍)) and the Dep_𝖳 relation is such that (𝚋𝚜, {𝚛𝚍}) ∈ Dep_𝖳.
In all architectures A, the user receives the final decision 𝚍𝚎𝚌 (which can typically be positive or negative) from the terminal: Receive_𝖴, 𝖳 ({}, {𝚍𝚎𝚌}) ∈ A.
The matching itself, which can be performed by different components depending on the architecture, is expressed by the function μ∈ Fun which takes as arguments two biometric templates and the threshold 𝚝𝚑𝚛.



§ APPLICATION OF THE FRAMEWORK TO  SEVERAL ARCHITECTURES FOR BIOMETRIC SYSTEMS WITH VARIOUS PROTECTION LEVELS



 §.§ 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 <ref> shows an architecture A_𝖾𝖽 in which reference templates are stored in a central database and the decryption of the references and the matching are done inside the terminal.
The second part of the figure shows an architecture A_𝗁𝗌𝗆 in which the decryption of the references and the matching are done on a dedicated hardware security module.
Both architectures are considered in turn in the following paragraphs.





  §.§.§ Use of an encrypted database.


The first architecture A_𝖾𝖽 is composed of a user , a terminal , a server  managing an encrypted database  and
an issuer  enrolling users and generating the encrypted database .
The set Fun 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
Ω := {𝚎𝚋𝚛 = Enc (𝚋𝚛),
𝚋𝚛' = Dec (𝚎𝚋𝚛),
𝚋𝚜 = Extract (𝚛𝚍),
𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛)},
and the architecture is defined as:

    A_𝖾𝖽 := {   
    Has_𝖨 (𝚋𝚛), Has_𝖴 (𝚛𝚍), Has_𝖳 (𝚝𝚑𝚛),
    Compute_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛)),
    
       
    Receive_𝖲, 𝖨 ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛))}, {𝚎𝚋𝚛}),
    
       
    Receive_𝖳, 𝖲 ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛))}, {𝚎𝚋𝚛}),
    Trust_𝖳, 𝖨,
    
       
    Verify_𝖳 (Attest_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛))),
    Receive_𝖳, 𝖴 ({}, {𝚛𝚍}),
    
       
    Compute_𝖳 (𝚋𝚜 = Extract (𝚛𝚍)),
    Compute_𝖳 (𝚋𝚛' = Dec (𝚎𝚋𝚛)),
    
       
    Compute_𝖳 (𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛)),
    Receive_𝖴, 𝖳 ({}, {𝚍𝚎𝚌})
    }

The properties of the encryption scheme are captured by the dependence and deductive relations.
The dependence relations are:
(𝚎𝚋𝚛, {𝚋𝚛}) ∈ Dep_𝖨, and
{(𝚋𝚜, {𝚛𝚍}), (𝚍𝚎𝚌,
{𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛}),
(𝚋𝚛', {𝚎𝚋𝚛}), (𝚋𝚛, {𝚎𝚋𝚛})} ⊆ Dep_𝖳.
Moreover the deductive algorithm relation contains:
{𝚎𝚋𝚛 = Enc (𝚋𝚛)}▹{𝚋𝚛 = Dec (𝚎𝚋𝚛)}.

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 (𝚋𝚛), which can be proven using 
Rule  (the same property holds for 𝚋𝚛'):



Has_𝖲 (𝚋𝚛) ∉A_𝖾𝖽
  ∄𝒳: (𝚋𝚛, 𝒳) ∈ Dep_𝖲
  ∄ T: Compute_𝖲 (𝚋𝚛 = T) ∈ A_𝖾𝖽
∄ j ∈𝒥, ∄ S, ∄ E, Receive_𝖲, j (S, E) ∈ A_𝖾𝖽∧𝚋𝚛∈ E

A_𝖾𝖽⊢ Has_𝖲^none (𝚋𝚛)


It is also easy to prove, using  and , that the terminal has access to 𝚋𝚛': Has_𝖳 (𝚋𝚛').

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 𝚎𝚋𝚛) and the computations that the terminal can perform by itself (through Compute_𝖳 and the application of ▹):



Verify_𝖳 ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛))}) ∈ A_𝖾𝖽
Trust_𝖳, 𝖨∈ A_𝖾𝖽

A_𝖾𝖽⊢ K_𝖳 (𝚎𝚋𝚛 = Enc (𝚋𝚛))




{𝚎𝚋𝚛 = Enc (𝚋𝚛)}▹{𝚋𝚛 = Dec (𝚎𝚋𝚛)}
A_𝖾𝖽⊢ K_𝖳 (𝚎𝚋𝚛 = Enc (𝚋𝚛))

A_𝖾𝖽⊢ K_𝖳 (𝚋𝚛 = Dec (𝚎𝚋𝚛))




Compute_𝖳 (𝚋𝚛' = Dec (𝚎𝚋𝚛)) ∈ A_𝖾𝖽

A_𝖾𝖽⊢ K_𝖳 (𝚋𝚛' = Dec (𝚎𝚋𝚛))


Assuming that all deductive relations include the properties (commutativity and transitivity) of the equality,  can be used to derive:
A_𝖾𝖽⊢ K_𝖳 (𝚋𝚛 = 𝚋𝚛').
A further application of  with another transitivity rule for the equality allows us to obtain the desired integrity property:



A_𝖾𝖽⊢ K_𝖳 (𝚋𝚛 = 𝚋𝚛')
Compute_𝖳 (𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛)) ∈ A_𝖾𝖽

A_𝖾𝖽⊢ K_𝖳 (𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛))

A_𝖾𝖽⊢ K_𝖳 (𝚍𝚎𝚌 = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛))





  §.§.§ 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_𝗁𝗌𝗆 pictured in the second part of Figure <ref>.

In addition to the user , the issuer , the terminal , and the server , the set of components contains a hardware security module .
The terminal does not perform the matching, but has to trust .
This trust can be justified in practice by the level of security provided by the HSM  (which can also be endorsed by an official security certification scheme).
The architecture is described as follows in our framework:

    A_𝗁𝗌𝗆 := {   
    Has_𝖨 (𝚋𝚛), Has_𝖴 (𝚛𝚍), Has_𝖬 (𝚝𝚑𝚛),
    Compute_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛)),
    
       
    Receive_𝖲, 𝖨 ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛))}, {𝚎𝚋𝚛}),
    
       
    Receive_𝖳, 𝖲 ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛))}, {𝚎𝚋𝚛}),
    Trust_𝖳, 𝖨,
    
       
    Verify_𝖳 (Attest_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛))),
    Receive_𝖳, 𝖴 ({}, {𝚛𝚍}),
    
       
    Compute_𝖳 (𝚋𝚜 = Extract (𝚛𝚍)),
    Receive_𝖬, 𝖳 ({}, {𝚋𝚜, 𝚎𝚋𝚛}),
    
       
    Compute_𝖬 (𝚋𝚛' = Dec (𝚎𝚋𝚛)),
    Compute_𝖬 (𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛)),
    
       
    Verify_𝖳 ({Attest_𝖬 (𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛))}),
    Trust_𝖳, 𝖬,
    
       
    Receive_𝖳, 𝖬 (𝒜, {𝚍𝚎𝚌}),
    Verify_𝖳 ({Attest_𝖬 (𝚋𝚛' = Dec (𝚎𝚋𝚛))})
    }

where the set of attestations 𝒜 received by the terminal from the module is
𝒜 := {Attest_𝖬 (𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛)), Attest_𝖬 (𝚋𝚛' = Dec (𝚎𝚋𝚛))}.

The trust relation between the terminal and the module makes it possible to apply rule  twice:



Verify_𝖳 ({Attest_𝖬 (𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛))}) ∈ A_𝗁𝗌𝗆
  Trust_𝖳, 𝖬∈ A_𝗁𝗌𝗆
A_𝗁𝗌𝗆⊢ K_𝖳 (𝚍𝚎𝚌 = μ (𝚋𝚛', 𝚋𝚜, 𝚝𝚑𝚛))




Verify_𝖳 ({Attest_𝖬 (𝚋𝚛' = Dec (𝚎𝚋𝚛))}) ∈ A_𝗁𝗌𝗆
Trust_𝖳, 𝖬∈ A_𝗁𝗌𝗆

A_𝗁𝗌𝗆⊢ K_𝖳 (𝚋𝚛' = Dec (𝚎𝚋𝚛))


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 ,  make it possible to derive:
A_𝗁𝗌𝗆⊢ K_𝖳 (𝖻𝗋 = Dec (𝖾𝖻𝗋)).
Then two successive applications of  regarding the transitivity of the equality lead to:
A_𝗁𝗌𝗆⊢ K_𝖳 (𝚍𝚎𝚌 = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛)).

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



Has_𝖳 (𝚋𝚛) ∉A_𝗁𝗌𝗆
  
∄𝒳: (𝚋𝚛, 𝒳) ∈ Dep_𝖳
  
∄ T: Compute_𝖳 (𝚋𝚛 = T) ∈ A_𝗁𝗌𝗆
[.9] ∄ j ∈𝒥, ∄ S, ∄ E, Receive_𝖳, j (S, E) ∈ A_𝗁𝗌𝗆∧𝚋𝚛∈ E

A_𝗁𝗌𝗆⊢ Has_𝖳^none (𝚋𝚛)





 §.§ Enhancing protection with homomorphic encryption



In both architectures of Section <ref>, 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 <cit.> 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 <ref> presents an architecture A_𝗁𝗈𝗆 derived from A_𝗁𝗌𝗆 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 𝚎𝚋𝚜).
The server also owns an encrypted reference template 𝚎𝚋𝚛.
The comparison, i.e. the computation of the distance between the templates, is done by the server, leading to the encrypted distance 𝚎𝚍𝚎𝚌, 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_𝗁𝗈𝗆 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) <cit.> as in the solution described in <cit.> 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 <cit.>).
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:

    {𝚎𝚋𝚛 = Enc (𝚋𝚛),
    𝚎𝚋𝚜 = Enc (𝚋𝚜),
    
    𝚎𝚍𝚎𝚌 = Hom-μ (𝚎𝚋𝚛, 𝚎𝚋𝚜, 𝚝𝚑𝚛)
    }▹{Dec (𝚎𝚍𝚎𝚌) = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛)}

The dependence relations include the following:
{(𝚋𝚜, {𝚛𝚍}),
(𝚎𝚋𝚜, {𝚋𝚜}) }⊆ Dep_𝖳;
(𝚎𝚋𝚛, {𝚋𝚛}) ∈ Dep_𝖨;
{(𝚋𝚛, {𝚎𝚋𝚛}),
(𝚋𝚜, {𝚎𝚋𝚜}),
(𝚍𝚎𝚌, {𝚎𝚍𝚎𝚌})}⊆ Dep_𝖬.
Architecture A_𝗁𝗈𝗆 is defined as follows:

    A_𝗁𝗈𝗆   
    := {
    Has_𝖨 (𝚋𝚛), Has_𝖴 (𝚛𝚍), Has_𝖲 (𝚝𝚑𝚛),
    Compute_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛)),
    
       
    Receive_𝖲, 𝖨 ({Attest_𝖨 ({𝚎𝚋𝚛 = Enc (𝚋𝚛)})}, {𝚎𝚋𝚛}),
    Receive_𝖳, 𝖴 ({}, {𝚛𝚍}),
    
       
    Compute_𝖳 (𝚋𝚜 = Extract (𝚛𝚍)),
    Compute_𝖳 (𝚎𝚋𝚜 = Enc (𝚋𝚜)),
    
       
    Receive_𝖲, 𝖳 ({}, {𝚎𝚋𝚜}),
    Compute_𝖲 (𝚎𝚍𝚎𝚌 = Hom-μ (𝚎𝚋𝚛, 𝚎𝚋𝚜, 𝚝𝚑𝚛)),
    
       
    Receive_𝖳, 𝖲 (𝒜, {𝚎𝚍𝚎𝚌}),
    Verify_𝖳 (Attest_𝖨 ({𝚎𝚋𝚛 = Enc (𝚋𝚛)})),
    
       
    Verify_𝖳 (Attest_𝖲 ({𝚎𝚍𝚎𝚌 = Hom-μ (𝚎𝚋𝚛, 𝚎𝚋𝚜, 𝚝𝚑𝚛)})),
    Trust_𝖳, 𝖲,
    
       
    Trust_𝖳, 𝖨,
    Receive_𝖬, 𝖳 ({}, {𝚎𝚍𝚎𝚌}),
    Compute_𝖬 (𝚍𝚎𝚌 = Dec (𝚎𝚍𝚎𝚌)),
    
       
    Receive_𝖳, 𝖬 ({Attest_𝖬 ({𝚍𝚎𝚌 = Dec (𝚎𝚍𝚎𝚌)})}, {𝚍𝚎𝚌}),
    Trust_𝖳, 𝖬,
    
       
    Verify_𝖳 (Attest_𝖬 ({𝚍𝚎𝚌 = Dec (𝚎𝚍𝚎𝚌)})),
    Receive_𝖴, 𝖳 ({}, {𝚍𝚎𝚌})
    }

where the set 𝒜 of attestations received by the terminal from the server is:
𝒜 := {Attest_𝖨 ({𝚎𝚋𝚛 = Enc (𝚋𝚛)}), Attest_𝖲 ({𝚎𝚍𝚎𝚌 = Hom-μ (𝚎𝚋𝚛, 𝚎𝚋𝚜, 𝚝𝚑𝚛)})}.

In order to prove that the terminal can establish the integrity of the result 𝚍𝚎𝚌, we can proceed in two steps, proving first the correctness of 𝚎𝚍𝚎𝚌 and then deriving the correctness of 𝚎𝚍𝚎𝚌 using the properties of homomorphic encryption.
The first step relies on the capacities of component 𝖳 and the trust assumptions on components 𝖨 and 𝖲 using rules  and  respectively.



Compute_𝖳 (𝚎𝚋𝚜 = Enc (𝚋𝚜)) ∈ A_𝗁𝗈𝗆

A_𝗁𝗈𝗆⊢ K_𝖳 (𝚎𝚋𝚜 = Enc (𝚋𝚜))




Verify_𝖳 ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (𝚋𝚛))}) ∈ A_𝗁𝗈𝗆
Trust_𝖳, 𝖨∈ A_𝗁𝗈𝗆

A_𝗁𝗈𝗆⊢ K_𝖳 (𝚎𝚋𝚛 = Enc (𝚋𝚛))




Verify_𝖳 ({Attest_𝖲 (𝚎𝚍𝚎𝚌 = Hom-μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛))}),
Trust_𝖳, 𝖲∈ A_𝗁𝗈𝗆

A_𝗁𝗈𝗆⊢ K_𝖳 (𝚎𝚍𝚎𝚌 = Hom-μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛))


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 (<ref>)) :



LHS_1 ▹{Dec (𝚎𝚍𝚎𝚌) = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛)}
∀ Eq ∈ LHS_1: A_𝗁𝗈𝗆⊢ K_𝖳 (Eq)

A_𝗁𝗈𝗆⊢ K_𝖳 (Dec (𝚎𝚍𝚎𝚌) = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛))


The desired property is obtained through the application of rules  and  exploiting the trust relation between 𝖳 and 𝖬 and the transitivity of equality.



Verify_𝖳 ({Attest_𝖬 (𝚍𝚎𝚌 = Dec (𝚎𝚍𝚎𝚌))}) ∈ A_𝗁𝗈𝗆
Trust_𝖳, 𝖬∈ A_𝗁𝗈𝗆

A_𝗁𝗈𝗆⊢ K_𝖳 (𝚍𝚎𝚌 = Dec (𝚎𝚍𝚎𝚌))





A_𝗁𝗈𝗆⊢ K_𝖳 (Dec (𝚎𝚍𝚎𝚌) = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛))
  A_𝗁𝗈𝗆⊢ K_𝖳 (𝚍𝚎𝚌 = Dec (𝚎𝚍𝚎𝚌))

A_𝗁𝗈𝗆⊢ K_𝖳 (𝚍𝚎𝚌 = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛))


As far as privacy is concerned, the main property that A_𝗁𝗈𝗆 is meant to ensure is that no component (except the issuer) has access to the biometric references.
Rule  makes it possible to prove that , , and  never get access to , as in Section <ref>.
The same rule can be applied here to prove A_𝗁𝗈𝗆⊬ Has_𝖬 (𝚎𝚋𝚛) exploiting the fact that neither (𝚋𝚛, {𝚎𝚍𝚎𝚌}) nor (𝚋𝚛, {𝚍𝚎𝚌}) belong to Dep_𝖬.



 §.§ 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 <cit.> (also called com­pa­rison-on-card), 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 <ref>).



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 , a terminal , and a card .
The card  attests that the templates 𝚋𝚛 and 𝚋𝚜 are close (with respect to the threshold 𝚝𝚑𝚛):

    A_𝗆𝗈𝖼 := {   
    Has_𝖢 (𝚋𝚛), Has_𝖴 (𝚛𝚍), Has_𝖢 (𝚝𝚑𝚛),
    Receive_𝖳, 𝖴 ({}, {𝚛𝚍}),
    
       
    Compute_𝖳 (𝚋𝚜 = Extract (𝚛𝚍)),
    Receive_𝖢, 𝖳 ({}, {𝚋𝚜}),
    
       
    Compute_𝖢 (𝚍𝚎𝚌 = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛)),
    Receive_𝖴, 𝖳 ({}, {𝚍𝚎𝚌}),
    
       
    Receive_𝖳, 𝖢 ({Attest_𝖢 (𝚍𝚎𝚌 = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛))}, {𝚍𝚎𝚌}),
    
       
    Verify_𝖳 ({Attest_𝖢 (𝚍𝚎𝚌 = μ (𝚋𝚛, 𝚋𝚜, 𝚝𝚑𝚛))}),
    Trust_𝖳, 𝖢}

Using rule , it is easy to show that no component apart from 𝖢 gets access to 𝚋𝚛.
The proof of the integrity property relies on the capacities of component 𝖳 and the trust assumption on component 𝖢 using rules  and  respectively.





§ EXTENSION OF THE FRAMEWORK TO INFORMATION LEAKAGE




 §.§ 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. <cit.>), we now propose an extension of the formal framework sketched in Section <ref>, in which the information leaking through several executions can be expressed.

We highlights the difference with the framework introduced in Section <ref> without repeating their common part.
The term language we use is now the following.

    [                              T                            ::=                             X̃                              |                              c                              | F (X̃_1, …, X̃_m, 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.

    [ [                             [7mm]A                                ::=                              5l{R};                                  R                                ::=                      Has_i^(n) (X)                                  |                          Has_i (c)                                  | 3lReceive_i, j^(n) ({St}, {X}∪{c});                                                                     |                         Trust_i, j                                  |                              Reset                                  |              Compute_G^(n) (X = T)                                  |                Verify^(n)_i ({St});                                    ];                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   ;                                                                                                                                                                                                                                                                        [            [7mm]St                ::=                Pro                  |                Att                                                                         Att                ::=    Attest_i ({Eq});                Pro                ::=    6lProof_i ({P})                 Eq                ::= Pred (T_1, …, T_m);                  P                ::=                Att                  |                 Eq;                    ] ]

The superscript notation ^(n) denotes that a primitive can be carried out at most n ∈ (ℕ∖{0}) ∪{∞} times by the component(s) – where (∀ n' ∈ℕ: n' < ∞).
We assume that n is never equal to 0.
𝗆𝗎𝗅 (α) 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 event[Except for the Session event.] is an instantiation of an architectural primitive[Except for Trust primitives, which cannot be instantiated into events because they are global assumptions.].
The notion of successive sessions is caught by the addition of a Session event[Computations can involve different values of the same variables from different sessions.] .
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.



    [                                θ                              ::=                          𝖲𝖾𝗊 (ϵ);                                ϵ                              ::=                      Has_i (X:V)                                |                        Has_i (c)                                | 3lReceive_i, j ({St}, {X:V}∪{c});                                                                 |                          Session                                |                            Reset                                |                Compute_G (X = T)                                |                  Verify_i ({St});                                  ]

An event can instantiate variables X with specific values V.
Constants always map to the same value.
Let Val be the set of values the variables and constants can take.
The set Val_ is defined as Val ∪{} where ∉Val 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 <cit.>.
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.

    [                       State_                            = (State_V × State_P) ∪{Error};                      State_V                            =     Var ∪ Const →𝖫𝗂𝗌𝗍 (Val_);                      State_P                            =            {Eq}∪{Trust_i, j} ]

The data structure 𝖫𝗂𝗌𝗍 over a set S denotes the finite ordered lists of elements of S,
𝗌𝗂𝗓𝖾 (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 𝗌𝗂𝗓𝖾 (L) = n ≥ 1, L[m] denotes the element e_m for 1 ≤ m ≤ n, 𝗅𝖺𝗌𝗍 (L) denotes L [n], and 𝖺𝗉𝗉𝖾𝗇𝖽 (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
σ_i^v and σ_i^pk denote, respectively, the variable and the knowledge state of the component C_i.

The variable state assigns values to variables and to constants (each constant is either undefined or taking a single value).
σ_i^v (X) [m] (resp. σ_i^v (c) [m]) denotes the m-th entry of the variable state of X ∈ Var (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, {Trust_i, j |  ∃ C_j: Trust_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: Trace × (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 θ∈ Trace, 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.

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:
𝗅𝖺𝗌𝗍 (σ_i^v (X)) := V.
This effect is denoted by σ_i^v [X / V]:

    S_E (Has_i (X:V), σ) =
    S_E (Receive_i, j (S, {X:V}), σ) =
    σ[σ_i / (σ_i^v[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 / (σ_i^v[X / V], σ^pk_i ∪{X = T})] 
        if the condition on the computation holds,
    σ[σ_i / Error]  otherwise,

where V := ε(T, ∪_C_i ∈ Gσ_i^v).
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: 𝗌𝗂𝗓𝖾({m  |  σ_i^v (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 (Verify_i (Proof_j (E)), σ)     = σ[σ_i/ (σ_i^v, σ_i^pk∪ new^pk_Proof)] 
        if the proof is valid, 
    σ[σ_i / Error]  otherwise,
    
    
    S_E (Verify_i (Attest_j (E)), σ)     = σ[σ_i / (σ_i^v, σ_i^pk∪ new^pk_Attest)] 
        if the attestation is valid, 
    σ[σ_i / Error]  otherwise.

The new knowledge new^pk_Proof and new^pk_Attest are defined as:

    new^pk_Proof    := {Eq  |  Eq ∈ E  ∨ ([ ∃ C_k: Attest_k (E') ∈ E  ∧ Eq ∈ E';                 ∧ Trust_i, k∈σ_i^pk ])} and
    
    new^pk_Attest    := {Eq  |  Eq ∈ E  ∧ Trust_i, j∈σ_i^pk}.

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, {Trust_i, j |  ∃ C_j: Trust_i, j∈ A})],

where the new variable state upd^v is such that σ_i^v (X) := 𝖺𝗉𝗉𝖾𝗇𝖽 (σ_i^v (X), ) for all variables X ∈ Var, and σ_i^v (c) := 𝖺𝗉𝗉𝖾𝗇𝖽 (σ_i^v (c), 𝗅𝖺𝗌𝗍 (σ_i^v (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 𝗌 (σ), which indicates the number of sessions.
In the initial state, 𝗌 (σ) := 1, and at each Session event, 𝗌 (σ) 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                  ::= 5lPred (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 φ∈ℒ_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 <ref>.
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 ⊢φ.



  * Let us assume that A ⊢ Has_i (X^(n)), and that the derivation tree is of depth 1.
By definition of 𝒟, such a proof is obtained by application of (), () or ().
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 𝒟, such a proof is obtained by application of (), (), (), () or ().
In each case, starting from a state σ' ∈ S_i (A) such that 𝗌 (σ') ≥ 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  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 𝒟, such a proof is obtained by application of () or ().

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 σ_i^v (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.

In the second case, we have that (Y, {X_1^(n_1), …, X_m^(n_m), c_1, …, c_q}) ∈ Dep_i, that ∀ l ∈ [1, m]: A ⊢ Has_i (X_l^(n_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 ().
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^(1)_i (X).
However, since () was applied, we have A ⊬ Has^(1)_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) (), (), or () (after an eventual application of ()).
In the last case, the proof shows how to exhibit a derivation tree to obtain A ⊢ Has_i (X^(n)) (the () 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 ().


  * 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 (), (), (), () or ().


  * 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 <cit.> aims at extending the MOC technology (cf. Section <ref>) 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 <cit.>.
The reference 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 𝚚𝚜 and sends them to the secure module.
Then, the module proceeds to a comparison between the fresh quantization and all enrolled quantizations 𝚚𝚛.
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 𝚒𝚗𝚍 of those c nearest quantized versions 𝚚𝚛 of the enrolled templates). This gives the module the access to the set 𝚜𝚎𝚋𝚛 of the c encrypted templates. The module decrypts them, and compares them with the fresh template 𝚋𝚜.
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 <ref> 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, 𝚎𝚋𝚛, 𝚚𝚛) = n, Range (𝚛𝚍, thr, 𝚋𝚜, 𝚚𝚜, 𝚍𝚎𝚌) = 1, and Range (𝚒𝚗𝚍, 𝚜𝚎𝚋𝚛, 𝚜𝚋𝚛) = c.
The set Fun 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_𝖨 (br)).
A verification process is initiated by the terminal  receiving as input a raw biometric data  from the user .
 extracts the fresh biometric template  from  using the function Extract ∈ Fun.
The architecture then contains, as other biometric systems, Receive_𝖳, 𝖴 ({}, {𝚛𝚍}) and Compute_𝖳 (𝚋𝚜 = Extract (𝚛𝚍)) and the Dep_𝖳 relation is such that (𝚋𝚜, {𝚛𝚍}) ∈ Dep_𝖳.
The user receives the final decision 𝚍𝚎𝚌 from the terminal: Receive_𝖴, 𝖳 ({}, {𝚍𝚎𝚌}).
To sum up, the architecture is described as follows in the framework of Section <ref>:

    A    ^𝗆𝗂 := {
    Has_𝖨 (br),
    Has_𝖴 (𝚛𝚍),
    Has_𝖬 (c),
    Has_𝖬 (thr),
    
       
    Compute_𝖨 (𝚎𝚋𝚛 = Enc (br)),
    Compute_𝖨 (𝚚𝚛 = Quant (br)),
    
       
    Compute_𝖳 (𝚋𝚜 = Extract (𝚛𝚍)),
    Compute_𝖳 (𝚜𝚎𝚋𝚛 = EGet (𝚎𝚋𝚛, 𝚒𝚗𝚍)),
    
       
    Compute_𝖳 (𝚚𝚜 = Quant (𝚋𝚜)),
    Compute_𝖬 (𝚒𝚗𝚍 = QComp (𝚚𝚜, 𝚚𝚛, c)),
    
       
    Compute_𝖬 (𝚜𝚋𝚛 = Dec (𝚜𝚎𝚋𝚛)),
    Compute_𝖬 (𝚍𝚎𝚌 = μ (𝚜𝚋𝚛, 𝚋𝚜, thr)),
    
       
    Receive_𝖲, 𝖨 ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (br))}, {𝚎𝚋𝚛}),
    Receive_𝖳, 𝖴 ({}, {𝚛𝚍}),
    
       
    Receive_𝖳, 𝖲 ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (br))}, {𝚎𝚋𝚛}),
    Receive_𝖬, 𝖳 ({}, {𝚚𝚜}),
    
       
    Receive_𝖬, 𝖨 ({Attest_𝖨 (𝚚𝚛 = Quant (br))}, {𝚚𝚛}),
    Receive_𝖳, 𝖬 ({}, {𝚒𝚗𝚍}),
    
       
    Receive_𝖬, 𝖳 ({}, {𝚜𝚎𝚋𝚛, 𝚋𝚜}),
    Receive_𝖳, 𝖬 ({}, {𝚍𝚎𝚌}),
    
       
    Trust_𝖳, 𝖨,
    Trust_𝖬, 𝖨,
    Trust_𝖳, 𝖬,
    Verify_𝖳^ (Attest_𝖨 (𝚎𝚋𝚛 = Enc (br))),
    
       
    Verify_𝖳^ ({Attest_𝖬 (𝚍𝚎𝚌 = μ (𝚜𝚋𝚛, 𝚋𝚜, thr))}),
    
       
    Verify_𝖬^ (Attest_𝖨 (𝚚𝚛 = Quant (br))),
    Verify_𝖳^ ({Attest_𝖬 (𝚜𝚋𝚛 = Dec (𝚎𝚋𝚛))})
    }

The issuer encrypts the templates and computes the quantizations, which is expressed by the dependencies:
Dep_𝖨^𝗆𝗂 := {(𝚎𝚋𝚛, {br}),
(𝚚𝚛, {br})}.
The terminal and module computations are reflected in the dependencies as well:
Dep_𝖳^𝗆𝗂 := {(𝚋𝚜, {𝚛𝚍}),
(𝚚𝚜, {𝚋𝚜})},
(𝚜𝚎𝚋𝚛, {𝚋𝚜, 𝚒𝚗𝚍})}.
The dependency relation of the module reflects its ability to decrypt the templates:
Dep_𝖬^𝗆𝗂 := {(𝚒𝚗𝚍, {𝚚𝚜, 𝚚𝚛, c}),
(𝚜𝚋𝚛, {𝚜𝚎𝚋𝚛}),
(𝚍𝚎𝚌, {𝚜𝚋𝚛, 𝚋𝚜, thr}),
(br, {𝚎𝚋𝚛})}.
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 <ref> is insufficient to consider the leakage of the sensitive biometric data stored inside the module.
In A^𝗆𝗂, we would like that the terminal gets no access to the quantizations: A^𝗆𝗂∈ Has^none_𝖳 (𝚚𝚛).
It is indeed possible to derive A^𝗆𝗂⊢ Has^none_𝖳 (𝚚𝚛), thanks to the () rule.
According to the notations of <cit.>, where Has_i (X) stands for Has_i (X^(1)) in this paper, we have:


∄ X: Dep_𝖳 (𝚚𝚛, X) ∈ A^𝗆𝗂
Has_𝖳 (𝚚𝚛) ∉A^𝗆𝗂
∄ j, S: Receive_𝖳, j (S, {𝚚𝚛}) ∈ A^𝗆𝗂
∄ T: Compute_𝖳 (𝚚𝚛 = T) ∈ A^𝗆𝗂
A ⊬ Has_𝖳 (𝚚𝚛)

A ⊢ Has^none_𝖳 (𝚚𝚛)


This corresponds to the intuition saying that quantizations are protected since they are stored in a secure hardware element.

However, an attack (described in <cit.>) 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 q-bits random vector Q and sends it to the module.
The attacker observes the set of indices 𝚒𝚗𝚍⊆ [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 𝚒𝚗𝚍:
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 <cit.>).
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^𝗆𝗂-𝖾 (n) be the following architecture, for some n ≥ 1:

    A^𝗆𝗂-𝖾    (n) := {
    Has_𝖨 (br),
    Has_𝖴^(n) (𝚛𝚍),
    Has_𝖬 (c),
    Has_𝖬 (thr),
    
       
    Compute_𝖨^(n) (𝚎𝚋𝚛 = Enc (br)),
    Compute_𝖨^(n) (𝚚𝚛 = Quant (br)),
    
       
    Compute_𝖳^(n) (𝚋𝚜 = Extract (𝚛𝚍)),
    Compute_𝖳^(n) (𝚜𝚎𝚋𝚛 = EGet (𝚎𝚋𝚛, 𝚒𝚗𝚍)),
    
       
    Compute_𝖳^(n) (𝚚𝚜 = Quant (𝚋𝚜)),
    Compute_𝖬^(n) (𝚒𝚗𝚍 = QComp (𝚚𝚜, 𝚚𝚛, c)),
    
       
    Compute_𝖬^(n) (𝚜𝚋𝚛 = Dec (𝚜𝚎𝚋𝚛)),
    Compute_𝖬^(n) (𝚍𝚎𝚌 = μ (𝚜𝚋𝚛, 𝚋𝚜, thr)),
    
       
    Receive_𝖲, 𝖨^(n) ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (br))}, {𝚎𝚋𝚛}),
    Receive_𝖳, 𝖴^(n) ({}, {𝚛𝚍}),
    
       
    Receive_𝖳, 𝖲^(n) ({Attest_𝖨 (𝚎𝚋𝚛 = Enc (br))}, {𝚎𝚋𝚛}),
    Receive_𝖬, 𝖳^(n) ({}, {𝚚𝚜}),
    
       
    Receive_𝖬, 𝖨^(n) ({Attest_𝖨 (𝚚𝚛 = Quant (br))}, {𝚚𝚛}),
    Receive_𝖳, 𝖬^(n) ({}, {𝚒𝚗𝚍}),
    
       
    Receive_𝖬, 𝖳^(n) ({}, {𝚜𝚎𝚋𝚛, 𝚋𝚜}),
    Receive_𝖳, 𝖬^(n) ({}, {𝚍𝚎𝚌}),
    
       
    Trust_𝖳, 𝖨,
    Trust_𝖬, 𝖨,
    Trust_𝖳, 𝖬,
    Verify_𝖳^(n) (Attest_𝖨 (𝚎𝚋𝚛 = Enc (br))),
    
       
    Verify_𝖳^(n) ({Attest_𝖬 (𝚍𝚎𝚌 = μ (𝚜𝚋𝚛, 𝚋𝚜, thr))}),
    
       
    Verify_𝖬^(n) (Attest_𝖨 (𝚚𝚛 = Quant (br))),
    
       
    Verify_𝖳^(n) ({Attest_𝖬 (𝚜𝚋𝚛 = Dec (𝚎𝚋𝚛))})
    }

In addition to the dependence of A^𝗆𝗂, the dependence relations indicates that the leakage is conditioned by a specific link mapping between the outsourced ciphertexts and the stored quantizations:
Dep_𝖳^𝗆𝗂-𝖾 (𝚚𝚛, {𝚒𝚗𝚍^(n·q), 𝚚𝚜^(n·q)}).
Furthermore, the module may learn the entire database  in a number of queries depending on the size of the database and the number of indices asked by the module:
Dep_𝖬^𝗆𝗂-𝖾 (𝚎𝚋𝚛, {𝚜𝚎𝚋𝚛^(⌈n / c⌉)}).



 §.§ Strengthened variants of the architecture


Now, based on some counter-measures of the attacks indicated in <cit.>, we express several variants of the architecture A^𝗆𝗂-𝖾.
For each variant, the deductive rules 𝒟 for the property language ℒ_P are used to show that, for some conditions on the parameters, the quantizations  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 ℒ_A, and, in practice, can be manageable for small databases.
This architecture, denoted A^𝗆𝗂-𝖾1, is given by A^𝗆𝗂-𝖾 (n) for some n ≥ 1, except that Dep_𝖳^𝗆𝗂-𝖾1 := Dep_𝖳^𝗆𝗂.
It is now possible to prove that the quantizations are protected, even in presence of several executions of the protocols.
Since the relations Dep_ no longer contains a dependence leading to , an application of () becomes possible and gives the expected property.


∄ X: Dep_𝖳 (𝚚𝚛, X) ∈ A^𝗆𝗂-𝖾1
Has_𝖳^(n) (𝚚𝚛) ∉A^𝗆𝗂-𝖾1
∄ j: Receive_𝖳, j^(n) (S, {𝚚𝚛}) ∈ A^𝗆𝗂-𝖾1
∄ T: Compute_𝖳^(n) (𝚚𝚛 = T) ∈ A^𝗆𝗂-𝖾1
∀ n: A ⊬ Has_𝖳 (𝚚𝚛^(n))

A ⊢ Has^none_𝖳 (𝚚𝚛)





  §.§.§ 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^𝗆𝗂-𝖾2, is given by A^𝗆𝗂-𝖾 (b), for some b≪n·q.
As a result, the Has^none_i (𝚚𝚛) property can be derived.
In particular one must show that A^𝗆𝗂-𝖾2⊬ Has_𝖳 (𝚒𝚗𝚍^(n·q)), in order to prevent the dependence rule  to be applied.


∄ S: Receive_𝖳, 𝖬^(b) (S, {𝚒𝚗𝚍}) ∈ A^𝗆𝗂-𝖾2
Has_𝖳^(b) (𝚒𝚗𝚍) ∈ A^𝗆𝗂-𝖾2
b < n·q
∄ T: Compute_𝖳^(b) (𝚒𝚗𝚍 = T) ∈ A^𝗆𝗂-𝖾2
A^𝗆𝗂-𝖾2⊬ Has_𝖳 (𝚒𝚗𝚍^(n·q))


An application of  enables to conclude.


Dep_𝖳^𝗆𝗂-𝖾2 (𝚚𝚛, {𝚒𝚗𝚍^(n·q)}) ∈ A^𝗆𝗂-𝖾2
Has_𝖳^(b) (𝚚𝚛) ∉A^𝗆𝗂-𝖾2
∄ j: Receive_𝖳, j^(b) (S, {𝚚𝚛}) ∈ A^𝗆𝗂-𝖾2
A^𝗆𝗂-𝖾2⊬ Has_𝖳 (𝚒𝚗𝚍^(n·q))     ∄ T: Compute_𝖳^(b) (𝚚𝚛 = T) ∈ A^𝗆𝗂-𝖾2
A^𝗆𝗂-𝖾2⊬ Has_𝖳 (𝚚𝚛^(1))

A^𝗆𝗂-𝖾2⊢ Has^none_𝖳 (𝚚𝚛)





  §.§.§ 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  and the encrypted database ; namely the association π that maps the quantization 𝚚𝚛[i] = Quant (br[π (i)]) to the encrypted template from which it has been computed 𝚎𝚋𝚛[π (i)] = Enc (br[π (i)]).
Once this mapping is changed, the information is cancelled.
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^𝗆𝗂-𝖾3 be the architecture defined as A^𝗆𝗂-𝖾3 := A^𝗆𝗂-𝖾2∪{Reset}.
The semantics of the Reset events ensures that no more than b values of  will be gathered by the terminal for a fixed mapping.
The proof that A^𝗆𝗂-𝖾3⊢ Has^none_𝖳 (𝚚𝚛) is as the proof that A^𝗆𝗂-𝖾2⊢ Has^none_𝖳 (𝚚𝚛).





§ RELATED WORKS



Generally speaking, while the privacy of biometric data has attracted a lot of attention in the news (for instance, with the introduction of a fingerprint sensor in the new iphone) and among lawyers and policy makers[For example with a proposal adopted by the French Senate in May 2014 to introduce stronger requirements for the use of biometrics.], it has not triggered such a strong interest in the computer science community so far.
Most studies in this area are done on a case by case basis and at a lower level than the architectures described here.
For instance, <cit.> 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.
<cit.> develop formal models from an information theoretic perspective relying on specific representations of biometric templates close 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 which can be used to define systems and to express privacy properties.
For example process calculi such as the applied pi-calculus <cit.> have been applied to define privacy protocols <cit.>.
Other studies <cit.> 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 <cit.> which can be seen as ways to measure the level of privacy provided by an algorithm.
Methods <cit.> have been proposed to design algorithms achieving privacy metrics or to verify that a system achieves a given level of privacy.
These 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 <cit.> have already pointed out the complexity of “privacy engineering” as well as the “richness of the data space”<cit.> calling for the development of more general and systematic methodologies for privacy by design.
<cit.> 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, <cit.> proposes a number of guidelines for the design of compilers for secure computation and zero-knowledge proofs whereas <cit.> provides a language and a compiler to perform computations on private data by synthesising 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 <cit.> 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 <ref> is a recap chart 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_𝖾𝖽 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 .
Architecture A_𝗁𝗌𝗆 is a variant of A_𝖾𝖽; it places less trust in the terminal that has to trust the hardware security module to perform the matching.
A_𝗁𝗈𝗆 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_𝗆𝗈𝖼 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 and, depending on the context of deployment and the technology used, some trust assumptions may be more reasonable than others.
In any case, it is of prime importance to understand the consequences of a particular choice in terms of trust.



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 <cit.>.
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.
When an architecture has been built, the system can try to verify the required properties with or without the help of the designer.

As stated above, we focused on the architectural level.
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 <cit.>.
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 <cit.> which promotes not only privacy by design but also privacy seals.







plain


