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

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

► To cite this version:

Julien Bringer, Hervé Chabanne, Daniel Le Métayer, Roch Lescuyer. Reasoning About Privacy Properties of Architectures Supporting Group Authentication and Application to Biometric Systems. 30th IFIP Annual Conference on Data and Applications Security and Privacy (DBSec), Jul 2016, Trento, Italy. pp.313-327. [hal-01633672](https://hal.inria.fr/hal-01633672)

HAL Id: hal-01633672

https://inria.hal.science/hal-01633672

Submitted on 13 Nov 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Reasoning about Privacy Properties of
Architectures Supporting Group Authentication
and Application to Biometric Systems

Julien Bringer¹, Hervé Chabanne¹², Daniel Le Métayer³, and Roch Lescuyer¹

¹ Morpho, Issy-Les-Moulineaux, France

² Télécom ParisTech, Paris, France

³ INRIA, Université de Lyon, France

**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.

**Keywords:** Privacy by design, Formal methods, Biometric systems

# 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 architec-
tures 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 for-
mal 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 man-
agement. 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 Section 5 some variants of the biometric architecture, before concluding in Section 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 conse-
quences 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 $\Omega = \{X = T\}$ of equations over the following term language.

$$T ::= X \mid c \mid F(X_1, \dots, X_m)$$

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.

$$A ::= \{R\}$$

$$R ::= Has_i(X) \mid Receive_{i,j}(\{St\}, \{X\}) \mid Trust_{i,j} \\ \mid Compute_G(X = T) \mid Verify_i(\{St\})$$

$$St ::= Pro \mid Att \quad Att ::= Attest_i(\{Eq\})$$

$$Pro ::= Proof_i(\{P\}) \quad Eq ::= Pred(T_1, \dots, T_m)$$

$$P ::= Att \mid Eq$$

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

$$ \begin{array}{l} \theta ::= \mathbf{Seq}(\epsilon) \\ \epsilon ::= Has_i(X:V) \mid \mathit{Receive}_{i,j}(\{St\}, \{X:V\}) \\ \phantom{\epsilon ::=} \qquad \mid \mathit{Compute}_G(X = T^\epsilon) \mid \mathit{Verify}_i(\{St\}) \end{array} $$

$\mathbf{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_\perp$ is defined as $Val \cup \{\perp\}$ where $\perp \notin 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 $\vdash_i$, allowing it to derive new knowledge. $\vdash_i$ is defined as a relation between equations $\{Eq_1, \dots, Eq_n\} \vdash_i Eq_0$, where equations over terms are defined according to the following syntax.

$$ Eq ::= \mathit{Pred}(T_1, \dots, T_m) \mid Eq \wedge Eq $$

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.

$$ \phi ::= Has_i(X) \mid Has_i^{\mathit{none}}(X) \mid K_i(Eq) \mid \phi_1 \wedge \phi_2. $$

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_i^{none}(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 Figure (1a).

# 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 Section 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_1^A, \dots, Init_{|C|}^A \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
<figure><img src="image_2.png" /><figcaption>(a) Subset of the axiomatics of [1]</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>(b) Our extended axioms</figcaption></figure>

<caption>Fig. 1. Axiomatics</caption>

knowledge states of $C_i$ being replaced by $v$ and $pk$ respectively. $\sigma[\sigma_i/\text{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$.

$$S_E(Verify_i(Proof_j(E)), \sigma) = \begin{cases} \sigma[\sigma_i/\text{Error}] & \text{if the proof is not valid,} \\ \sigma[\sigma_i/(\sigma_i^v, \sigma_i^{pk} \cup new_{Proof}^{pk})] & \text{otherwise,} \end{cases}$$
$$S_E(Verify_i(Attest_G(E)), \sigma) = \begin{cases} \sigma[\sigma_i/\text{Error}] & \text{if the attestation is not valid,} \\ \sigma[\sigma_i/(\sigma_i^v, \sigma_i^{pk} \cup new_{Attest}^{pk})] & \text{otherwise,} \end{cases}$$

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

$$new_{Proof}^{pk} := \{Eq \mid Eq \in E \lor (\exists G \subseteq C : (Attest_G(E') \in E \land Eq \in E' \land \forall k \in G : \text{Trust}_{i,k} \in \sigma_i^{pk}))\}; \quad (1)$$

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

$$new_{Attest}^{pk} := \{Eq \mid Eq \in E \land \forall k \in G : \text{Trust}_{i,k} \in \sigma_i^{pk}\}. \quad (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 Figure (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 ($\mathbf{K}4^+$) and ($\mathbf{K}5^+$) 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 ($\mathbf{K}1$), ($\mathbf{K}3$), ($\mathbf{K}4^+$) or ($\mathbf{K}5^+$). Let us focus on the $\mathbf{K}4^+$ and $\mathbf{K}5^+$ cases.

$\mathbf{K}4^+$. Let us assume that $Verify_i(Proof_j(E)) \in A$, $Attest_G(E') \in E$ and $\forall k \in G: \text{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', \text{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, \text{Init}^A)$. Since an Error state has not been reached (we have $\sigma' \in S_i(A)$), and since $\forall k \in G:
$\mathit{Trust}_{i,k} \in \sigma_i^{pk}$ by definition of the initial state, then by the semantics of the group attestation (Equation (1)) we have $\forall Eq \in E: Eq \in \sigma_i^{pk}$.

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_i^{pk} \triangleright_i Eq$. By the semantics of the properties, we conclude that $\forall Eq \in E': A \in S(K_i(Eq))$.

K5$^+$. Let us assume that $\mathit{Verify}_i(\mathit{Attest}_G(E)) \in A$ and $\forall k \in G: \mathit{Trust}_{i,k} \in A$. We must show that $\forall Eq \in E: A \in S(K_i(Eq))$. Adaptation of the K4$^+$ to the K5$^+$ case is straightforward, invoking Equation (2) of the trace semantics instead of Equation (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_i^{pk} \triangleright_i Eq$. By the semantics of architectures, $\exists \theta \in T(A)$ such that $(\sigma = S_T(\theta, \mathit{Init}^A)$ and $\sigma_i^{pk} \triangleright_i Eq)$. By the semantics of the traces, this implies one among the following statements: either there exists $\mathit{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 $\mathit{Verify}_i(\mathit{Proof}_j(E)) \in \theta$ where $Eq \in E$; or there exists $\mathit{Verify}_i(\mathit{Proof}_j(E)) \in \theta$ where $\mathit{Attest}_G(E') \in E$, $Eq \in E'$ and $\forall k \in G: \mathit{Trust}_{i,k} \in \sigma_i^{pk}$ and $Eq \in E'$; or there exists $\mathit{Verify}_i(\mathit{Attest}_G(E)) \in \theta$, $Eq \in E$ and $\forall k \in G: \mathit{Trust}_{i,k} \in \sigma_i^{pk}$.

By the compatibility of the traces, we deduce that: either $\mathit{Compute}_G(X) \in A$ where $Eq := (X = T)$ and $C_i \in G$; or $\mathit{Verify}_i(\mathit{Proof}_j(E)) \in A$ where $Eq \in E$; or $\mathit{Verify}_i(\mathit{Proof}_j(E)) \in A$ where $\mathit{Attest}_G(E') \in E$, $Eq \in E'$ and $\forall k \in G: \mathit{Trust}_{i,k} \in A$ and $Eq \in E'$; or $\mathit{Verify}_i(\mathit{Attest}_G(E)) \in A$, $Eq \in E'$ and $\forall k \in G: \mathit{Trust}_{i,k} \in A$. We conclude that $A \vdash K_i(Eq)$ by applying (respectively) (K1), (K3), (K4$^+$) or (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
<figure><img src="image_4.png" /><figcaption>**Fig. 2.** High-level view of the biometric system architecture using group signatures</figcaption></figure>

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_{gs}$ the biometric system introduced in [4] and $A_{gs}$ its definition within the formal framework, which we present below.

Upper case sans serif letters in $A_{gs}$ denote components. Components of the $A_{gs}$ architecture are a set of $N$ enrolled users $U := \{U_1, \dots, U_N\}$ (each user $U_i$ owning a card $C_i$), a server $S$, an issuer $l$ and a terminal modelled by two
components TM and TS. The issuer $I$ enrolls 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. $br_i$ denotes the biometric reference template of the user $U_i$ built during the enrolment phase. $rd$ denotes a raw biometric data provided by the user during the verification phase. $bs$ denotes a fresh template derived from $rd$ during the verification phase. A threshold $thr$ is used during the verification phase as a closeness criterion for the biometric templates. The output $dec$ of the verification is the result of the matching between the fresh template $bs$ and the enrolled templates $br$, considering the threshold $thr$. $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 $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 $rd$ from the user. The terminal, more precisely the TM component, extracts the fresh biometric template $bs$ from $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 $thr$. The terminal reads in the card the biometric template $br$. The user receives the final decision $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_{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_{gs}$ for all users. For instance $Has_I(br_i) \in A_{gs}$ implicitly means that $\forall U_i \in U: Has_I(br_i) \in A_{gs}$.

$$
\begin{aligned}
A_{gs} &:= \{ Has_I(br_i), Has_U rd), Has_{TM} thr), \\
&\quad Compute_I(db = DB(br_1, \dots, br_N)), Compute_{TM}(bs = Extract rd), \\
&\quad Compute_{TM}(dec = \mu(br_i, bs, thr)), Trust_{S,U_i}, Trust_{S,TM}, Trust_{S,TS}, \\
&\quad Receive_I,U_i(\{Attest_{U_i}(br_i \in db)\}, \{\}\), Receive_{TM,U_i}(\{\}, \{rd\}), \\
&\quad Receive_{C_i,I}(\{Attest_{U_i}(br_i \in db)\}, \{br_i\}), Receive_{U_i,TM}(\{\}, \{dec\}), \\
&\quad Receive_{TM,C_i}(\{\}, \{br_i\}), Receive_{TS,TM}(\{\}, \{dec\}), \\
&\quad Receive_{TS,C_i}(\{Attest_{U_i}(br_i \in db)\}, \{br_i\}), \\
&\quad Receive_{S,TS}(\{Attest_U(br_i \in db)\}, \{\}), Verify_S(\{Attest_U(br_i \in db)\}) \}
\end{aligned}
$$

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

## 4.3 Trusting a group of users

In the biometric system architecture $A_{gs}$, the group of users is trusted by the server, which is denoted $\forall \mathbf{U}_i \in \mathcal{U}: \text{Trust}_{\mathcal{S}, \mathbf{U}_i}$. However, the formalization does not define which cryptographic primitive is used in the concrete $B_{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 enrolls 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_{gs}$ architecture from the server point's of view. $A_{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_{gs} \vdash K_{\mathcal{S}}(\mathbf{br}_i \in \mathbf{db})$. But the server should have no access to the templates: $A_{gs} \vdash \text{Has}_{\mathcal{S}}^{\text{none}}(\mathbf{br}_i)$.

Regarding the template protection, the statement $A_{gs} \vdash \text{Has}_{\mathcal{S}}^{\text{none}}(\mathbf{br}_i)$ is shown using rule **HN**. A subtlety here is the presence of the dependence between the biometric template $\mathbf{br}_i$ and the database $\mathbf{db}$. Therefore we first need to show $A \nvDash \text{Has}_{\mathcal{S}}(\mathbf{db})$.

$$ \frac{\begin{array}{l} \text{Has}_{\mathcal{S}}(\mathbf{db}) \notin A_{gs} \\ \exists \vec{X} : (\mathbf{db}, \vec{X}) \in \text{Dep}_{\mathcal{S}} \end{array}}{A_{gs} \nvDash \text{Has}_{\mathcal{S}}(\mathbf{db})} \qquad \begin{array}{l} \exists \mathcal{T}: \text{Compute}_{\mathcal{S}}(\mathbf{db} = \mathcal{T}) \in A_{gs} \\ \exists j, \exists \mathcal{S}, \exists \mathcal{E}: \text{Receive}_{\mathcal{S},j}(\mathcal{S}, \mathcal{E}) \in A_{gs} \wedge \mathbf{db} \in \mathcal{E} \end{array} $$
Now HN can be applied.

$$ 
\begin{array}{l}
\text{Has}_S(\mathbf{br}_i) \notin A_{\text{gs}} \qquad \exists T: \text{Compute}_S(\mathbf{br}_i = T) \in A_{\text{gs}} \\
\qquad \exists j, \exists S, \exists E: \text{Receive}_{S,j}(S, E) \in A_{\text{gs}} \wedge \mathbf{br}_i \in E \\
\hline
\text{HN} \frac{A_{\text{gs}} \vdash \text{Has}_S(\mathbf{br}_i)}{A_{\text{gs}} \vdash \text{Has}_S^{\text{none}}(\mathbf{br}_i)}
\end{array}
$$

$A_{\text{gs}} \vdash Has_S^{\text{none}}(\mathbf{bs})$ is also shown by an application of HN.

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

$$ K5^+ \frac{\text{Verif}_S(\text{Attest}_U(\mathbf{br}_i \in \mathbf{db})) \in A_{\text{gs}} \quad \forall U_i \in \mathcal{U} : \text{Trust}_{S,U_i} \in A_{\text{gs}}}{A_{\text{gs}} \vdash K_S(\mathbf{br}_i \in \mathbf{db})} $$

# 5 Variants

Several variants [4] of the biometric system $B_{\text{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_{\text{gs}}^p$, becomes:

$$ 
\begin{array}{l}
A_{\text{gs}}^p := A_{\text{gs}} \setminus \{ \\
\quad \text{Receive}_{S,T_S}(\{\text{Attest}_U(\mathbf{br}_i \in \mathbf{db})\}, \{\}), \text{Trust}_{S,T_S}, \\
\quad \text{Verify}_S(\{\text{Attest}_U(\mathbf{br}_i \in \mathbf{db})\}) \\
\quad \cup \{ \\
\quad \text{Receive}_{S,T_S}(\{\text{Proof}_{T_S}(\text{Attest}_U(\mathbf{br}_i \in \mathbf{db})), \{\}), \\
\quad \text{Verify}_S(\{\text{Proof}_{T_S}(\text{Attest}_U(\mathbf{br}_i \in \mathbf{db})), \{\})\}) \\
\} \}
\end{array}
$$

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

$$ K4^+ \frac{\text{Verif}_S(\text{Proof}_{T_S}(\text{Attest}_U(\mathbf{br}_i \in \mathbf{db}))) \in A_{\text{gs}}^p \quad \forall U_i \in \mathcal{U} : \text{Trust}_{S,U_i} \in A_{\text{gs}}^p}{A_{\text{gs}}^p \vdash K_S(\mathbf{br}_i \in \mathbf{db})} $$

## 5.2 Combination with match-on-card

In the $A_{\text{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 [12, 11, 8]. 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<sub>gs</sub> 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.

$$
\begin{align*}
A_{\text{gs}}^{\text{moc}} &:= \{ \text{Has}_I(\mathbf{br}_i), \text{Has}_{U_i}(\mathbf{rd}), \text{Has}_{\text{TM}}(\mathbf{thr}), \text{Trust}_{\text{TM},C_i}, \text{Trust}_{S,U_i}, \\
& \phantom{:=} \text{Compute}_I(\mathbf{db} = \text{DB}(\mathbf{br}_1, \dots, \mathbf{br}_N)), \text{Compute}_{\text{TM}}(\mathbf{bs} = \text{Extract}(\mathbf{rd})), \\
& \phantom{:=} \text{Compute}_{C_i}(\mathbf{dec} = \mu(\mathbf{br}_i, \mathbf{bs}, \mathbf{thr})), \text{Receive}_{I,U_i}(\{\text{Attest}_{U_i}(\mathbf{br}_i \in \mathbf{db})\}, \{\}\}, \\
& \phantom{:=} \text{Receive}_{C_i,I}(\{\text{Attest}_{U_i}(\mathbf{br}_i \in \mathbf{db})\}, \{\mathbf{br}_i\}), \text{Receive}_{\text{TM},U_i}(\{\}\}, \{\mathbf{rd}\}), \\
& \phantom{:=} \text{Receive}_{\text{TM},C_i}(\{\text{Attest}_{C_i}(\mathbf{dec} = \mu(\mathbf{br}_i, \mathbf{bs}, \mathbf{thr})), \text{Attest}_{U}(\mathbf{br}_i \in \mathbf{db})\}, \{\mathbf{dec}\}), \\
& \phantom{:=} \text{Receive}_{C_i,\text{TM}}(\{\}\}, \{\mathbf{bs}\}), \text{Receive}_{U_i,\text{TM}}(\{\}\}, \{\mathbf{dec}\}), \\
& \phantom{:=} \text{Receive}_{S,\text{TM}}(\{\text{Attest}_{U}(\mathbf{br}_i \in \mathbf{db})\}, \{\}\}), \text{Verify}_{S}(\{\text{Attest}_{U}(\mathbf{br}_i \in \mathbf{db})\}), \\
& \phantom{:=} \text{Verify}_{\text{TM}}(\{\text{Attest}_{C_i}(\mathbf{dec} = \mu(\mathbf{br}_i, \mathbf{bs}, \mathbf{thr}))\}) \}
\end{align*}
$$

Using rule HN, it is easy to show that no component apart from I and C<sub>i</sub> gets access to <b>br</b><sub>i</sub>.

The terminal should be convinced that the matching is correct: A<sub>gs</sub><sup>moc</sup> ⊢ K<sub>TM</sub>(dec = μ(<b>br</b><sub>i</sub>, <b>bs</b>, <b>thr</b>)). The proof relies on the trust placed by the server in the matching component TM of the terminal.

$$
\frac{\text{Verify}_{\text{TM}}(\text{Attest}_{C_i}(\text{dec} = \mu(\mathbf{br}_i, \mathbf{bs}, \mathbf{thr}))) \in A_{\text{gs}}^{\text{moc}}}{K5^+ \frac{\text{Trust}_{\text{TM},C_i} \in A_{\text{gs}}^{\text{moc}}}{A_{\text{gs}}^{\text{moc}} \vdash K_{\text{TM}}(\text{dec} = \mu(\mathbf{br}_i, \mathbf{bs}, \mathbf{thr}))}}
$$

Regarding the group authentication, an application of K5<sup>+</sup> 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 prim-
itive, called SpotCheck, which can be used to carry out a *posteriori* checks
and therefore to describe the above variant. However, the model including the
<table><thead><tr><th rowspan="2">Arch.</th><th colspan="2">Template protection</th><th rowspan="2">Trust relations</th></tr><tr><th>Components accessing the reference <i>br</i><sub><i>i</i></sub></th><th>Components accessing the query <i>bs</i></th></tr></thead><tbody><tr><td><i>A</i><sub>gs</sub></td><td>I, C, TM, TS</td><td>TM</td><td>(S, U<sub>i</sub>), (S, TS)</td></tr><tr><td><i>A</i><sup><i>p</i></sup><sub>gs</sub></td><td>I, C, TM, TS</td><td>TM</td><td>(S, U<sub>i</sub>)</td></tr><tr><td><i>A</i><sup><i>moc</i></sup><sub>gs</sub></td><td>I, C</td><td>TM, C</td><td>(S, U<sub>i</sub>), (TM, C<sub>i</sub>)</td></tr></tbody></table>

Components are: users $U_i$, terminal components TM and TS, server S, card C, issuer I. A trust relation $(i, j)$ means that component $i$ trusts component $j$.

<caption>**Table 1.** Comparison between architectures</caption>

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_{gs}^{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_{gs}$ is more realistic. The choice between $A_{gs}$ and $A_{gs}^{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.

# Acknowledgment

This work has been partially funded by the French ANR-12-INSE-0013 project BIOPRIV. Part of this work has been conducted within the Inria Project Lab on Privacy CAPPRIS [6].
References

1. Thibaud Antignac and Daniel Le Métayer. Privacy architectures: Reasoning about data minimisation and integrity. In Security and Trust Management - STM'14, volume 8743 of LNCS, pages 17-32. Springer, 2014.

2. Dan Boneh and Hovav Shacham. Group signatures with verifier-local revocation. In ACM Conference on Computer and Communications Security - CCS'04, pages 168-177. ACM Press, 2004.

3. Julien Bringer, Hervé Chabanne, Daniel Le Métayer, and Roch Lescuyer. Privacy by design in practice: Reasoning about privacy properties of biometric system architectures. In Formal Methods - FM'15, volume 9109 of LNCS, pages 90-107. Springer, 2015.

4. Julien Bringer, Hervé Chabanne, David Pointcheval, and Sébastien Zimmer. An application of the Boneh and Shacham group signature scheme to biometric authentication. In International Workshop on Security - IWSEC'08, volume 5312 of LNCS, pages 219-230. Springer, 2008.

5. Sébastien Canard and Marc Girault. Implementing group signature schemes with smart cards. In Smart Card Research and Advanced Application - CARDIS'02, pages 1-10. USENIX, 2002.

6. CAPPRIS. Collaborative Project on the Protection of Privacy Rights in the Information Society. Inria Project Lab on Privacy. https://cappris.inria.fr/.

7. European Parliament. European Parliament legislative resolution of 12 March 2014 on the proposal for a regulation of the European Parliament and of the Council on the protection of individuals with regard to the processing of personal data and on the free movement of such data. General Data Protection Regulation, Ordinary legislative procedure: first reading, 2014.

8. Michelle Govan and Tom Buggy. A computationally efficient fingerprint matching algorithm for implementation on smartcards. In Biometrics: Theory, Applications, and Systems - BTAS'07, pages 1-6. IEEE, 2007.

9. Joseph Y. Halpern and Riccardo Pucella. Dealing with logical omniscience. In Conference on Theoretical Aspects of Rationality and Knowledge TARK'07, pages 169-176, 2007.

10. Anil K. Jain, Arun Ross, and Salil Prabhakar. An introduction to biometric recognition. IEEE Trans. Circuits Syst. Video Techn., 14(1):4-20, 2004.

11. National Institute of Standards and Technology (NIST). MINEXII - an assessment of Match-On-Card technology, 2011. http://www.nist.gov/itl/iad/ig/minexii.cfm.

12. International Standard Organization. International standard iso/iec 24787:2010, information technology - identification cards - on-card biometric comparison, 2010.

13. Riccardo Pucella. Deductive algorithmic knowledge. J. Log. Comput., 16(2):287-309, 2006.

14. Ronald L. Rivest, Adi Shamir, and Yael Tauman. How to leak a secret. In Advances in Cryptology - ASIACRYPT'01, volume 2248 of LNCS, pages 552-565. Springer, 2001.

15. Vinh-Thong Ta and Thibaud Antignac. Privacy by design: On the conformance between protocols and architectures. In Foundations and Practice of Security - FPS'14, volume 8930 of LNCS, pages 65-81. Springer, 2015.

16. TURBINE. TrUsted Revocable Biometric IdeNtitiEs. Collaborative European project 216339 call FP7-ICT-2007-1, 2007. http://cordis.europa.eu/project/rcn/85447_en.html.