Reasoning About Privacy Properties of Architectures Supporting Group Authentication and Application to Biometric Systems

Abstract

This paper follows a recent line of work that advocates the use of formal methods to reason about privacy properties of system architectures. We propose an extension of an existing formal framework, motivated by the need to reason about properties of architectures including group authentication functionalities. By group authentication, we mean that a user can authenticate on behalf of a group of users, thereby keeping a form of anonymity within this set. Then we show that this extended framework can be used to reason about privacy properties of a biometric system in which users are authenticated through the use of group signatures.

1 Introduction

The privacy-by-design approach promotes the consideration of privacy requirements from the early design stage of a system. As an illustration of the importance of this topic, the General Data Protection Regulation adopted by the European trilogue (the European Commission, the European Parliament and the Council) in December 2015 [7] introduces privacy-by-design and privacy-by-default as legal obligations. Architectural choices have a strong effect on the privacy properties provided by a system. For this reason, the authors of [1] argue that key decisions regarding the design of a system should be taken at the architecture level. They introduce a formal framework for reasoning about privacy properties of architectures. The description of an architecture within this framework specifies the capacities of each component, the communications between them, the location of the computations and the data, and the trust relationships between the stakeholders. A dedicated privacy logic is used to express the privacy properties of the architectures. The use of formal methods enables precise definitions of properties and comparisons between architectures. It also makes it possible to provide a rigorous justification for the design choices.

As a first contribution of this paper, we propose an extension of this formal framework and show that it can be used to reason about properties of architectures supporting group authentication. By group authentication, we mean that a user can authenticate on behalf of a group of users. Several cryptographic primitives have been designed to achieve this goal. Our work provides the formal tools needed to reason about the properties of architectures involving these primitives, especially the guarantees that are provided in terms of privacy.

As a second contribution of this paper, we apply our extended framework to biometric systems. In a biometric system, users are authenticated with their biometric traits. The work of [3] uses the formal framework of [1] to reason about privacy properties of biometric architectures but it cannot deal with group signatures. We show that the extended framework can be used to reason about privacy properties of a biometric system in which users are authenticated by group signatures.

The interest of group signature in the context of biometrics has been shown in different contexts. For example, the biometric system architecture analysed in this paper was proposed in TURBINE [16], a European project which aimed at solving privacy concerns regarding the use of fingerprint biometrics for ID management. The application of this architecture was a pharmacy product research system. Pharmacists, for instance working at their selling desks, authenticate themselves to a pharmacy administration system. Authentication is based on a card owned by the employee, as well as its fingerprint. Thanks to the use of group signatures, a remote server (which does not get the fingerprint) is convinced that a valid enrolled user authenticates without knowing precisely who he is among the set of valid users (aka the employees).

Organization of the paper. Section 2 supplies an overview of the formal framework of [1]. Section 3 introduces our extension of this model. Section 4 presents the biometric architecture we are interested in, describes it within the architecture language of the formal framework, and analyses its privacy properties. Finally, we discuss in Sect. 5 some variants of the biometric architecture, before concluding in Sect. 6.

2 Reasoning About Privacy Properties of Architectures

In this section, we provide an overview of the framework introduced in [1] which is the foundation for our work. The interested reader can refer to [1] for a more complete description of the framework.

This framework relies on a dedicated epistemic logic for expressing privacy properties. Epistemic logics are good candidates to express privacy properties since they deal with the notion of knowledge. However, the standard possible worlds semantics for these logics lead to a well-known issue called the logical omniscience problem [9]. In a nutshell, any agent knows all the logical consequences of his knowledge. To get around this issue, the authors of [1] adopt an approach based on deductive algorithmic knowledge [13]. In this context, each component of an architecture is endowed with its own deductive capabilities.

Architectures are described with a dedicated architecture language. Then the semantics of a privacy property is defined as the architectures in which the property holds.

2.1 A Privacy Architecture Language

First of all, the functionality of a system is described by a set $\varOmega = \{X = T\}$ of equations over the following term language.

A term T might be a variable X ($X \in Var$), a constant c ($c \in Const$) or F a function applied to some variables ($F \in Fun$).

Then the architecture of a system is described by the following architecture language.

An architecture A is associated to a set of components $\mathcal {C} = \{C_1, \dots , C_{|\mathcal {C}|}\}$. In the architectural primitives, i and j stand respectively for $C_i$, $C_j$ and $G \subseteq \mathcal {C}$ denotes a set of components.

In the above syntax, $\{Z\}$ denotes a set of elements of category Z. Pred denotes a predicate, the set of predicates depending on the architectures to be considered. $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. $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$.

$Attest_i (\{Eq\})$ is the declaration by $C_i$ that the properties in $\{Eq\}$ hold and $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). $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$.

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.

All architectures are assumed to satisfy minimal consistency assumptions, in order to restrict the analysis to those which make sense. For instance, if a component sends a variable, we assume that this variable can be sent, computed or received by the component.

Events are instantiations of the architectural primitives (trust relations excepted). Traces are sequences of events, defined according to the following trace language.

$\mathsf {Seq} (\epsilon )$ denotes an ordered sequence of events $\epsilon$. When instantiating a primitive containing a variable X, the notation X : V means that the variable X receives the value V. Let Val be the set of values that the variables can take. $T^\epsilon$ is a term where values have been assigned to variables. The set $Val_\bot$ is defined as $Val \cup \{\bot \}$ where $\bot \not \in Val$ is a specific symbol used to denote that a variable has not been assigned.

As for architectures, only traces satisfying consistency assumptions are considered. $\langle \rangle$ denotes the empty trace (with no event).

A trace $\theta$ of events is said compatible with an architecture A if each event in $\theta$ (except the computations) can be obtained by instantiation of an element of A (Receive, Verify, etc.). Let T (A) be the set of traces which are compatible with an architecture A.

Each component $C_i$ is associated with a dependence relation $Dep_i$. For a variable Y and a set $\mathcal {X}$ of variables, $Dep_i (Y, \mathcal {X})$ – equivalently $(Y, \mathcal {X}) \in Dep_i$ – means that the value of Y can be obtained by the component $C_i$ if it gets access to the value of X, for each $X \in \mathcal {X}$.

Each component $C_i$ is also associated with a deductive system, noted $\triangleright _i$, allowing it to derive new knowledge. $\triangleright _i$ is defined as a relation between equations $\{Eq_1, \dots , Eq_n\} \triangleright _i Eq_0$, where equations over terms are defined according to the following syntax.

By a slight abuse of notations, Eq is an overloaded notation of the Eq definition in the language architecture, where conjunctions of equations are also possible.

Finally, the semantics of an architecture is defined from the traces of events. Each component is associated with a state. Each event in a trace of events affects the state of each component involved in the event. The semantics S(A) of an architecture A is defined as the set of states reachable by compatible traces.

2.2 A Privacy Logic

Privacy properties of architectures are expressed with the following language.

The knowledge operator $K_i$ represents the knowledge of the component $C_i$. The formula $Has_i$ represents the fact that $C_i$ can get access to variable X.

The semantics $S (\phi )$ of a property $\phi$ is defined as the set of architectures where $\phi$ is satisfied. The fact that a property $\phi$ is satisfied by a (consistent) architecture A is defined for each property as follows.

• A satisfies $Has_i (X)$ if there is a reachable state of $C_i$ in which X is not undefined.

• A satisfies $Has^{none}_i (X)$ if no compatible trace leads to a state in which $C_i$ assigns a value to X.

• A satisfies $K_i (Eq)$ if from all reachable states $C_i$ can deduce Eq.

• A satisfies $\phi _1 \wedge \phi _2$ if A satisfies $\phi _1$ and A satisfies $\phi _2$.

Based on the semantics of properties, [1] introduces a set of deductive rules which can be used to reason about privacy properties of architectures. This deductive system is shown correct and complete with respect to the semantics of the properties.

$A \vdash \phi$ denotes that $\phi$ can be derived from A – in other words, that there exists a derivation tree such that each step belongs to the axiomatics and the leaf is $A \vdash \phi$. A subset of this axiomatics, useful for this paper, is presented in Fig. (1a).

Fig. 1.

Axiomatics

3 Adding a Group Attestation to the Formal Model

As a first step to extend the architecture language of [1], we introduce the primitive $Attest_G (E)$ where G is a group of components and E a set of equations. This primitive generalizes $Attest_i (E)$ which involves a single component $C_i$. Section 3.1 defines the semantics of the traces containing these events and Sect. 3.2 extends the set of deductive rules.

3.1 Semantics of Traces

The semantics of a trace is defined by specifying, for each event, its effect on the states of the components.

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 the current knowledge of a component. In the initial state of an architecture A, denoted $Init^A = \langle Init^A_1, \dots , Init^A_{|\mathcal {C}|} \rangle$, the variables are undefined and the knowledge state only contains the trust primitives.

Let $\sigma$ denote the global state, and $\sigma _i$ denote the state of component i. The semantics of traces, denoted $S_T$, is defined recursively over sequences of events.

$$\begin{aligned} S_T (\langle \rangle , \sigma )&= \sigma \\ S_T (\epsilon \cdot \theta , \sigma )&= S_T (\theta , S_E (\epsilon , \sigma )). \end{aligned}$$

The function $S_E$, which defines the effect of the events, is defined for each type of event. The modification of a state is noted $\sigma [\sigma _i/(v, pk)]$ the variable and knowledge states of $C_i$ being replaced by v and pk respectively. $\sigma [\sigma _i /Error]$ denotes that the Error state is reached for component $C_i$. A component reaching an Error state is no longer involved in any action.

Restricting our attention to the events which contains a group attestation leads us to consider the events $Verify_i (Attest_G (E))$ and $Verify_i (Proof_j (E))$. The semantics of the verification events are defined according to the (implicit) semantics of the underlying verification procedures. In both cases, 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. Informally, a verification event containing a generalized attestation statement generates new knowledge only if all possible authors of the attestation are trusted by the verifying component $C_i$.

$$\begin{aligned} S_E (Verify_i (Proof_j (E)), \sigma ) =&{\left\{ \begin{array}{ll} \sigma [\sigma _i / Error] \quad \text {if the proof is not valid}, \\ \sigma [\sigma _i/ (\sigma _i^v, \sigma _i^{pk} \cup new^{pk}_{Proof})] \quad \text {otherwise}, \end{array}\right. } \end{aligned}$$

$$\begin{aligned} S_E (Verify_i (Attest_G (E)), \sigma ) =&{\left\{ \begin{array}{ll} \sigma [\sigma _i / Error] \quad \text {if the attestation is not valid}, \\ \sigma [\sigma _i / (\sigma _i^v, \sigma _i^{pk} \cup new^{pk}_{Attest})] \quad \text {otherwise}, \end{array}\right. } \end{aligned}$$

where the new knowledge $new^{pk}_{Proof}$ is defined as:

(1)

and the new knowledge $new^{pk}_{Attest}$ is defined as:

(2)

3.2 Axiomatics

The next challenge to deal with group attestation is the extension of the set of deductive rules and the proof of the correctness and completeness properties still hold. Our axioms for group attestation are presented in Fig. (1b). In the remaining of this section, we show that the correctness and the completeness of the axiomatics still hold with these new axioms.

Correctness. Let A be a consistent architecture and $\phi$ a property. The correctness theorem states that if there exists a derivation tree for this property ($A \vdash \phi$), then this property holds in the architecture ($A \in S (\phi )$).

The proof is made by induction on the depth of the tree $A \vdash \phi$. Let us restrict our attention to the cases where $(\mathsf {K4^{+}})$ and $(\mathsf {K5^{+}})$ are used. That is, let us assume that $A \vdash K_i (Eq)$, and that the derivation tree is of depth 1. By definition of the set of axioms, such a proof is obtained by application of (K1), (K3), $(\mathsf {K4^{+}})$ or $(\mathsf {K5^{+}})$. Let us focus on the $\mathsf {K4^{+}}$ and $\mathsf {K5^{+}}$ cases.

$\mathsf {K4^{+}}$. Let us assume that $Verify_i (Proof_j (E)) \in A$, $Attest_G$ ($E'$) $\in E$ and $\forall k \in G$: $Trust_{i, k} \in A$ for some i, j and G. Our goal is to prove that $\forall Eq \in E'$: $A \in S (K_i (Eq))$.

Let us consider a given state $\sigma ' \in S_i (A)$. By the architecture semantics, there exists a consistent trace $\theta '$, compatible with A, such that $\sigma ' = S_T (\theta ', Init^A)$. Two cases may happen. Either $\theta '$ contains an event $Verify_i (Proof_j (E))$ such that $Attest_G (E') \in E$, and we let $\theta := \theta '$, or it is not. In the latter case, we extend $\theta '$ into a trace $\theta$ such that $\theta$ contains such an event without breaking the consistency of the trace.

In either cases, there exists a trace $\theta$ which extends $\theta '$ and contains an event $Verify_i (Proof_j (E))$ such that $Attest_G (E') \in E$. Let $\sigma = S_T (\theta , Init^A)$. Since an Error state has not been reached (we have $\sigma ' \in S_i (A)$), and since $\forall k \in G: Trust_{i, k} \in \sigma _i^{pk}$ by definition of the initial state, then by the semantics of the group attestation (Eq. (1)) we have $\forall Eq \in E$: $Eq \in \sigma ^{pk}_i$.

By the definition of the architectures semantics, we deduce that $\sigma \in S (A)$. The prefix order over the traces together with the definition of the semantics of the trace induce a prefix order over the states, hence $\sigma \ge _i \sigma '$. By the reflexivity of the deductive algorithmic knowledge, we have $\forall Eq \in E'$: $\sigma ^{pk}_i \triangleright _i Eq$. By the semantics of the properties, we conclude that $\forall Eq \in E'$: $A \in S (K_i (Eq))$.

$\mathsf {K5^{+}}$. Let us assume that $Verify_i (Attest_G (E)) \in A$ and $\forall k \in G$: $Trust_{i, k} \in A$. We must show that $\forall Eq \in E$: $A \in S (K_i (Eq))$. Adaptation of the $\mathsf {K4^{+}}$ to the $\mathsf {K5^{+}}$ case is straightforward, invoking Eq. (2) of the trace semantics instead of Eq. (1).

Completeness. Let A be a consistent architecture and $\phi$ a property. The completeness theorem states that if the property holds in the architecture ($A \in S (\phi )$), then there exists a derivation tree for this property ($A \vdash \phi$).

The proof is made by induction over the definition of the property $\phi$. We restrict our attention here to the knowledge operator $K_i$. Let us assume that $A \in S (K_i (Eq))$ for a given component $C_i$ and equation Eq. We must show that $A \vdash K_i (Eq)$.

By the semantics of properties, $A \in S (K_i (Eq))$ means that $\forall \sigma ' \in S_i (A)$: $\exists \sigma \in S_i (A)$: $\sigma ^{pk}_i \triangleright _i Eq$. By the semantics of architectures, $\exists \theta \in T (A)$ such that ($\sigma = S_T (\theta , Init^A)$ and $\sigma ^{pk}_i \triangleright _i Eq$). By the semantics of the traces, this implies one among the following statements: either there exists $Compute_G (X = T^\epsilon ) \in \theta$ where $Eq := (X = T)$ and $C_i \in G$ and $T^\epsilon$ is obtained from T (by assigning values to variables); or there exists $Verify_i (Proof_j (E)) \in \theta$ where $Eq \in E$; or there exists $Verify_i (Proof_j (E)) \in \theta$ where $Attest_G (E') \in E$, $Eq \in E'$ and $\forall k \in G$: $Trust_{i, k} \in \sigma ^{pk}_i$ and $Eq \in E'$; or there exists $Verify_i (Attest_G (E)) \in \theta$, $Eq \in E$ and $\forall k \in G$: $Trust_{i, k} \in \sigma ^{pk}_i$.

By the compatibility of the traces, we deduce that: either $Compute_G (X) \in A$ where $Eq := (X = T)$ and $C_i \in G$; or $Verify_i (Proof_j (E)) \in A$ where $Eq \in E$; or $Verify_i (Proof_j (E)) \in A$ where $Attest_G (E') \in E$, $Eq \in E'$ and $\forall k \in G$: $Trust_{i, k} \in A$ and $Eq \in E'$; or $Verify_i (Attest_G (E)) \in A$, $Eq \in E'$ and $\forall k \in G$: $Trust_{i, k} \in A$. We conclude that $A \vdash K_i (Eq)$ by applying (respectively) (K1), (K3), $(\mathsf {K4^{+}})$ or $(\mathsf {K5^{+}})$.

4 Modelling a Biometric Architecture Supporting Group Authentication

4.1 A Biometric Architecture Using Group Signatures

Biometric systems involve two main phases: enrolment and verification (either authentication or identification) [10]. 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.

A group signature scheme [2] is an advanced cryptographic mechanism. It enables a user to sign messages on behalf of a group of users while staying anonymous inside this group. With a (public) verification algorithm, anyone can be convinced, given a group public key, a message, and a signature, that a certain member of the group authenticates the message.

The biometric system introduced in [4] aims at achieving some anonymity from the server’s point of view. The server is convinced that the authentication was successful for a certain enrolled user, but has no information about which among them. During the enrolment, a biometric reference is registered by the issuer. The issuer derives a user secret key from the biometric template and computes a group secret key, that is, a certificate attesting the enrolment inside the group. The user gets a card containing its biometric reference and the group certificate.

During the verification phase, the terminal gets a fresh capture of the biometric trait and computes a fresh template. A match between the fresh template and the reference is performed by the terminal. In case of success, the terminal derives the user secret key from the reference, produces a group signature thanks to the user secret key and the certificate (both are needed to produce a valid signature), and sends the signature to the server. The server checks the signature attesting that a registered user authenticates. If the signature is valid, the server is convinced of the correctness of the matching. However, it has no access to the biometric templates, neither to the identity of the user who authenticates.

4.2 Description Within the Formal Framework

For the sake of clarity, let us distinguish the biometric system and its formalization. We denote by $B_\mathsf {gs}$ the biometric system introduced in [4] and $A_\mathsf {gs}$ its definition within the formal framework, which we present below.

Fig. 2.

High-level view of the biometric system architecture using group signatures

Upper case sans serif letters in $A_\mathsf {gs}$ denote components. Components of the $A_\mathsf {gs}$ architecture are a set of N enrolled users $\mathcal {U} := \{\mathsf {U}_1, \dots , \mathsf {U}_N\}$ (each user $\mathsf {U}_i$ owning a card $\mathsf {C}_i$), a server S, an issuer $\mathsf {I}$ and a terminal modelled by two components $\mathsf {TM}$ and $\mathsf {TS}$. The issuer I enrols the users. The server S manages a database containing the enrolled templates. The terminal is equipped with a sensor used to acquire biometric traits. Formally, the terminal is split into two components TM and TS, corresponding respectively to its two functionalities. The matcher TM, acquires the fresh template and performs the comparison, and the signer TS authenticates on behalf of the group of users. As shown by the variants below, this distinction is motivated by the different trust assumptions a designer may consider.

Type letters denote variables. $\mathtt {br}_i$ denotes the biometric reference template of the user $\mathsf {U}_i$ built during the enrolment phase. $\mathtt {rd}$ denotes a raw biometric data provided by the user during the verification phase. $\mathtt {bs}$ denotes a fresh template derived from $\mathtt {rd}$ during the verification phase. A threshold $\mathtt {thr}$ is used during the verification phase as a closeness criterion for the biometric templates. The output $\mathtt {dec}$ of the verification is the result of the matching between the fresh template $\mathtt {bs}$ and the enrolled templates $\mathtt {br}$, considering the threshold $\mathtt {thr}$. $\mathtt {db}$ denotes the database of the registered biometric templates.

As in [3], we focus on the verification phase and assume that enrolment has already been done. The database $\mathsf {db}$ is computed by the issuer from all the references, using the function $DB \in Fun$. A verification process is initiated by the terminal receiving as input a raw biometric data $\mathtt {rd}$ from the user. The terminal, more precisely the TM component, extracts the fresh biometric template $\mathtt {bs}$ from $\mathtt {rd}$ using the function $Extract \in Fun$. The matching is expressed by the function $\mu \in Fun$ which takes as arguments two biometric templates and the threshold $\mathtt {thr}$. The terminal reads in the card the biometric template $\mathtt {br}$. The user receives the final decision $\mathtt {dec}$ of the matching from the terminal TM. Then the terminal, here the TS component, attests that the fresh template belongs to the set of enrolled templates.

The complete description of $A_\mathsf {gs}$ within the architecture language is as follows. Figure 2 sketches this description. When indices i are used, it is assumed that the corresponding primitive exists in $A_\mathsf {gs}$ for all users. For instance $Has_\mathsf {I} (\mathtt {br}_i) \in A_\mathsf {gs}$ implicitly means that $\forall \mathsf {U}_i \in \mathcal {U}$: $Has_\mathsf {I} (\mathtt {br}_i) \in A_\mathsf {gs}$.

To complete the description of $A_\mathsf {gs}$, it remains to define the dependence relations between the variables. The database is computed from all the references: $\forall j \in \mathcal {C}$: ($\mathtt {db}$, {$\mathtt {br}_1$, ..., $\mathtt {br}_N$}). Conversely, access to $\mathtt {db}$ gives access to all $\mathtt {br}_i$: $\forall j \in \mathcal {C}, \mathsf {U}_i \in \mathcal {U}$: $Dep_j$ ($\mathtt {br}_i$, {$\mathtt {db}$}). Moreover, $\forall j \in \mathcal {C}, \mathsf {U}_i \in \mathcal {U}$: we also have ($\mathtt {bs}$, {$\mathtt {rd}$}), ($\mathtt {dec}$, {$\mathtt {br}_i$, $\mathtt {bs}$}), ($\mathtt {dec}$, {$\mathtt {br}_i$, $\mathtt {rd}$}) $\in Dep_j$.

4.3 Trusting a Group of Users

In the biometric system architecture $A_\mathsf {gs}$, the group of users is trusted by the server, which is denoted $\forall \mathsf {U}_i \in \mathcal {U}$: $Trust_{\mathsf {S}, \mathsf {U}_i}$. However, the formalization does not define which cryptographic primitive is used in the concrete $B_\mathsf {gs}$ system. Let us discuss this point in more detail.

In a group signature scheme, users are typically not trusted, but a group manager, called the issuer, is trusted. When it enrols a user, the issuer provides a group secret key, aka a membership certificate – concretely, a signature of some secret user-specific data. In other words, it attests that the user is enrolled. Then the untrusted user proves that it is enrolled (by supplying a zero-knowledge proof of her user secret data and the corresponding membership certificate). In our case, the server does not trust the card, but trusts the issuer of the card. The card contains an attestation that the user was indeed enrolled by the issuer, here a certificate for a group signature, i.e., a group secret key.

The point to be noticed is that we do not model its internal machinery in our formal architecture. We only express the fact that the group is trusted. Whether this trust assumption is justified or not in practice is not part of the reasoning about architecture: it rather regards the justification of the choice of certain primitives to achieve the functionality. With the same trust assumption (all users are trusted), other primitives can be used, as ring signatures [14], where a member authenticates on behalf of a group without group manager.

The use of group signatures is a choice made at the protocol level. Checking the conformity between the protocols and the architecture is out of scope of this paper. This line of work has been initiated in [15].

4.4 Application of the Axiomatics

We now reason about the privacy properties of the $A_\mathsf {gs}$ architecture from the server point’s of view. $A_\mathsf {gs}$ should enable the server to be sure that a certain enrolled user authenticates, but the authenticated user is anonymous from the server’s point of view: $A_\mathsf {gs} \vdash K_\mathsf {S} (\mathtt {br}_i \in \mathtt {db})$. But the server should have no access to the templates: $A_\mathsf {gs} \vdash Has_\mathsf {S}^{none} (\mathtt {br}_i)$.

Regarding the template protection, the statement $A_\mathsf {gs} \vdash Has_\mathsf {S}^{none} (\mathtt {br}_i)$ is shown using rule HN. A subtlety here is the presence of the dependence between the biometric template $\mathtt {br}_i$ and the database $\mathtt {db}$. Therefore we first need to show $A \nvdash Has_\mathsf {S} (\mathtt {db})$.

Now HN can be applied.

$A_\mathsf {gs} \vdash Has_\mathsf {S}^{none} (\mathtt {bs})$ is also shown by an application of HN.

Since the server trusts the users, an application of $\mathsf {K5^{+}}$ shows that the server is ensured that some enrolled user authenticates.

5 Variants

Several variants [4] of the biometric system $B_\mathsf {gs}$ can be expressed and analyzed in our formal framework.

5.1 Lowering the Trust on the Group Signing Functionality

If the server trusts the matching functionality TM of the terminal but does not trust its signer functionality TS, then the component TS must supply a proof that some user is enrolled. The architecture, denoted $A_\mathsf {gs}^\mathsf {p}$, becomes:

An application of the new rule $\mathsf {K4^{+}}$ enable to prove that the server is ensured that some enrolled user authenticates.

5.2 Combination with Match-On-Card

In the $A_\mathsf {gs}$ architecture, the card is a plastic card. The biometric reference is just printed on it, together with a group secret key. To enhance the protection of the reference, a smart-card can be used instead of a plastic card, as in the Match-On-Card (MOC) technology [8, 11, 12]. The card stores the reference template, and the reference never leaves the card. During a verification, the card receives the fresh biometric template, carries out the comparison with its reference, and sends the decision back. The terminal trusts the smart card for the correctness of the matching. This trust is justified by the fact that the card is a tamper-resistant hardware element.

The $A_\mathsf {gs}$ architecture in which the plastic card is replaced by a smart-card performing a MOC is modelled as follows. In addition to the comparison, the card also computes the group authentication.

Using rule HN, it is easy to show that no component apart from I and $\mathsf {C}_i$ gets access to $\mathtt {br}_i$.

The terminal should be convinced that the matching is correct: $A_\mathsf {gs}^\mathsf {moc} \vdash K_\mathsf {TM} (\mathtt {dec} = \mu (\mathtt {br}_i, \mathtt {bs}, \mathtt {thr}))$. The proof relies on the trust placed by the server in the matching component TM of the terminal.

Regarding the group authentication, an application of $\mathsf {K5^{+}}$ shows that the server is ensured that some enrolled user authenticates.

5.3 Anonymity Revocation

As shown in [4], an additional mechanism can be used to revoke the anonymity of a group authentication if there is any legal need to do so. After the matching phase, the terminal has to encrypt the fresh template under the public key of a specific tracing authority, to sign all messages together, and to send the authentication result to the server. Then, at a later stage, the tracing authority may decrypt the template and check, with an access to the database of the issuer, that the templates were indeed close. This a posteriori check ensures a form of accountability which can be requested in certain contexts.

The formal model introduced in [1] includes an additional architectural primitive, called SpotCheck, which can be used to carry out a posteriori checks and therefore to describe the above variant. However, the model including the SpotCheck primitive is proven complete only when all the functions of the term language are at most unary. Since the comparison between templates, an essential operation of biometric systems, is inherently binary, we would then obtain a correct but incomplete system.

We leave for future work the definition of a formal model with a posteriori verifications which would be both correct and complete and would not suffer this arity restriction in the term language.

6 Conclusion

In this paper, we have analysed the privacy properties of a biometric system in which users can remain anonymous from the point of view of a remote server, while the server is still convinced that a valid user authenticates. Table 1 sums up the properties of the different architectures considered here. Architecture $A_\mathsf {gs}^\mathsf {moc}$ provides the best guarantees in terms of privacy. However, its deployment has a cost, since it requires that each user owns a card with powerful capabilities. Although quite demanding, these assumptions are not out of reach of the current technology [5]. The main variant $A_\mathsf {gs}$ is more realistic. The choice between $A_\mathsf {gs}$ and $A_\mathsf {gs}^\mathsf {p}$ depends on the trust placed on each component in a specific deployment. The possibility to express these trust assumptions in a formal way and to study their consequences is one of the main benefits of the framework presented here because it provides rigorous justifications to make well-informed design choices for the architecture of a system.

Table 1. Comparison between architectures