thesis/chap-GS-background.tex

In this Part, we will present two constructions for dynamic group signatures.
The construction that will be explained in \cref{ch:sigmasig} is an adaptation of the Libert, Peters and Yung short group signature in the standard model from classical pairing assumptions~\cite{LPY15} into the random oracle model to gain efficiency, while keeping the assumptions simple.
This gives us a constant-size group signature scheme that is shown to be competitive with other constructions based on less standard assumptions.
An implementation is available and detailed in \cref{ch:sigmasig}.

The second construction, described in \cref{ch:gs-lwe}, is a lattice-based dynamic group signature where the scheme from Ling, Nguyen and Wang~\cite{LNW15} for static groups has been improved to match requirements for dynamic groups.
This construction has been the first fully secure group signature scheme from lattices.

Before describing those scheme, let us recall in this Chapter the definition of dynamic group signatures and their related security definitions.

\section{Background} \label{sse:gs-background}
\addcontentsline{tof}{section}{\protect\numberline{\thesection} Historique}

Dynamic group signatures are a solution to allow a user to authenticate a message on behalf of a set of users it belongs to (the \textit{group}) that can be publicly verified while remaining anonymous inside its group.
On the other hand, the user remains accountable for the signatures it provides as there exists an authority, the \textit{opening authority}, that can lift the anonymity of a given signature using its own secret key.
In the dynamic setting, a group signature scheme has a second authority: the \textit{group manager}, that allows a user to enroll the group after an interaction with it.
These interactions are summarized in Figure~\ref{fig:gs-relations}.

The concept of group signatures was introduced by Chaum and van Heyst in 1991~\cite{CVH91}, but the works of Ateniese, Camenisch, Joye and Tsudik in 2001~\cite{ACJT00} were the first to provide scalable and secure group signatures.
In 2003, Bellare, Micciancio and Warinschi~\cite{BMW03} proposed a formal definition for \textit{static} group signatures, where the group is defined once and for all at the setup phase.
This model was extended to dynamic groups by Bellare, Shi and Zhang (BSZ) and Kiayias and Yung~(KY) in 2005~\cite{BSZ05,KY06}. Those two security models are slightly different, and we choose in this thesis to build our proofs in the~\cite{KY06} model as described in~\cref{sse:gs-definitions}.

The \cite{BMW03}~model summarize the security of a group signature scheme in two notions: \textit{anonymity} and \textit{traceability}.
The former notions models the fact that without the opening authority's secret, even if everyone colludes, no one can trace back a user from a signature; the latter sum up the fact that even if everyone is corrupted (even the opening authority), it is impossible to forge a valid signature that does not open to a valid user.

In the dynamically growing group setting, the \textit{group private keys issuing} phase is replaced by an interactive \textit{join} protocol where a user that wants to join the group interacts with the group manager.
In this context, the two notions of the BMW model are kept, and a third one is added: the ``\textit{non-frameability}''.
This notion expresses the impossibility to frame a group of honest users in order to provide a signature that opens to one on them, \textit{even if the group manager and the opening authority are colluding}.

One application of this primitive can be to handle anonymous access control for public transportation systems.
In order to commute, a person should prove the possession of a valid subscription to the transportation service.
Thus, at registration to the service, the commuter joins the group of \emph{users with a valid subscription} and when it takes the transport, it is asked to sign the timestamp of its entry in the name of the group.
In case of misbehavior, another entity --\,let say the police\,-- is able to lift the anonymity of the signatures logged by the reading machine.
Then, the public transportation company is unable to learn anything from seeing the signatures, except the validity of the subscription of a user, and on the other hand, the police does not have access to the logs except if the public transportation company hands them to it.

Other applications of group signatures can be advocated as authentication of low-range communications for intelligent cars or anonymous access control of a building.
As we can see, most applications necessitate the use of \textit{dynamically growing} groups in order to be meaningful.

Bootle, Cerulli, Chaidos, Ghadafi and Groth~\cite{BCC+16} rise the problem of revocation and proposed a model that handle the issues that arose from the introduction of revocation called ``\textit{fully-dynamic}'' group signatures, but as the main difficulty is to allow users to dynamically enroll to the group --\,as revocation has been known to be implemented in a modular manner~\cite{LLNW14}\,-- this approach is not considered here, even if it is of interest~\cite{LNWX17}.

\section{Formal Definition and Correctness} \label{sse:gs-definitions}
\addcontentsline{tof}{section}{\protect\numberline{\thesection} Définition formelle et correction}

This section recalls the syntax and the security definitions of dynamic  group signatures based on the model of Kiayias and Yung~\cite{KY06}.

%A \emph{group signature}  allows a group member to attest that a message was provided by a member of a \emph{group} without being altered during the process and preserving the \emph{anonymity} of the users.



\begin{figure}
  \centering
  \input fig-gs-relations
  \caption{Relations between the protagonists in a dynamic group signature
  scheme}
  \label{fig:gs-relations}
\end{figure}

In the setting of \emph{dynamic groups}, the syntax of group signatures includes
an interactive protocol which allows users to register as new members of the
group at any time. The syntax and the security model are those defined by
Kiayias and Yung~\cite{KY06}.
Like the very similar {BSZ} model~\cite{BSZ05}, the Kiayias-Yung
({KY}) model assumes an interactive \emph{join} protocol whereby a
prospective user becomes a group member by interacting with the group manager.
This protocol provides the user with a membership certificate, $\crt_i$, and a
membership secret, $\scr_i$.

%\paragraph{Syntax.}
We denote by $\Ngs \in \poly[\lambda]$ the maximal number of group members that the system will be able to handle.
\begin{definition}[Dynamic Group Signature]
  \index{Dynamic group signatures}
  A \emph{dynamic group signature} scheme consists of the algorithms or protocols $(\Setup, \mathsf{Join}, \Sign, \Verify, \Open)$ described as follows.

  \begin{description}
    \item[\textsf{Setup}$(1^\lambda,1^{\Ngs})$:] given a security parameter $\lambda$ and a maximal number of group members $\Ngs \in \mathbb{N}$, this algorithm is run by a \textit{trusted party} to generate a group public key $\gspk$, the group manager's private key $\mathcal{S}_{\GM}$ and the opening authority's private key $\mathcal{S}_{\OA}$.
      Each key is given to the appropriate authority while $\gspk$ is made public.
      The algorithm also initializes a public state $\mathsf{st}$ comprising a set data structure $\mathsf{st}_{\users}=\emptyset$ and a string data structure $\mathsf{st}_{\trans}= \epsilon$.\\
      In the following, all algorithms have access to the public parameters $\gspk$.
%
    \item[\textsf{Join}$^{\join_{\user}, \join_{\GM}}$:] is an \emph{interactive} protocol between the group manager GM and a user $\mathcal{U}_i$ where the latter becomes a group member.
      The protocol involves two interactive Turing machines $\join_{\user}$ and $\join_{\GM}$ that both take the group public key $\gspk$ as input.
      The execution $\langle \join_{\user}(\lambda,\gspk),\join_{\GM}(\lambda,\mathsf{st},\gspk,\mathcal{S}_{\GM}) \rangle$, ends with user $\mathcal{U}_i$ obtaining a membership secret $\scr_{i}$, that no one else knows, and a membership certificate $\crt_{i }$.
      If the protocol is successful, the group manager updates the public state $\mathsf{st}$ by updating the following state informations $\mathsf{st}_{\users}\coloneqq \mathsf{st}_{\users} \cup \{ i \}$ as well as $\mathsf{st}_{\trans}\coloneqq \mathsf{st}_{\trans} || ( i ,\transcript_i )$.
%
%\item[\textsf{Revoke}:] is a (possibly randomized) algorithm allowing the GM
%to generate an updated revocation list $RL_t$ for the new revocation period $t$.
%It takes as input a public key $\gspk$ and a set $\mathcal{R}_t \subset \mathsf{st}_{\users}$
%that identifies the users to be revoked.
%It outputs an updated revocation list $RL_t$ for period $t$.
%%
    \item[\textsf{Sign($\crt_i, \scr_i, M$)}:] given
%a revocation period $t$ with its revocation list $RL_t$,
      a membership certificate $\crt_{i }$, a membership secret $\scr_{i }$ and
      a message $M$, this \emph{probabilistic} algorithm outputs
      %$\perp$ if $i \in \mathcal{R}_t$ and
      a signature $\sigma$.
%
    \item[\textsf{Verify($\sigma, M$)}:] given a signature $\sigma$,
%a revocation period $t  $, the corresponding revocation list $RL_t$,
      a message $M$ and a group public key $\gspk$, this
      \emph{deterministic} algorithm returns either $0$ or $1$.
%
    \item[\textsf{Open($\mathcal{S}_{\OA}, M, \sigma$)}:] takes as input a
      message $M$, a valid signature $\sigma$ w.r.t.
      $\gspk$ %for the indicated revocation period $t$
      , the opening authority's private key $\mathcal{S}_{\OA}$ and the public
      state $\mathsf{st}$.
      It outputs  $i \in \mathsf{st}_{\users} \cup \{ \bot \}$, which is the identity of
      a group member or a symbol indicating an opening failure.
%
  \end{description}
  Each membership certificate contains a unique \emph{tag} that identifies the user.
\end{definition}

The correctness requirement basically captures that, if all parties
\emph{honestly} run the protocols, all algorithms are correct with respect to
their specification described as above.

%As mentioned in section~\ref{sec:art}
The Kiayias-Yung model~\cite{KY06} considers three security notions: the security against \textit{misidentification attacks} requires that, even if the adversary
can introduce users under its control in the group, it cannot produce a signature that traces outside the set of dishonest users. The notion of security against
\textit{framing attacks} implies that honest users can never be accused of having signed messages that they did not sign, even if the whole system conspired
against them. And finally the \textit{anonymity} property is also formalized by granting the adversary access to a signature opening oracle as in the models of~\cite{BSZ05}.

\paragraph{Correctness for Dynamic Group Signatures.}
Following the Kiayias-Yung terminology \cite{KY06}, we say that a public state
$\mathsf{st}$ is \textit{valid} if it can be reached from $\mathsf{st}=(\emptyset,\epsilon)$ by a
Turing machine having oracle access to $\join_{\GM}$. Also, a state $\mathsf{st}'$ is said
to \textit{extend} another state $\mathsf{st}$ if it is within reach from $\mathsf{st}$.

Moreover, as in \cite{KY06}, when we write
$\crt_{i}\leftrightharpoons_{\gspk} \scr_{i}$, it means that there exists
coin tosses $\varpi$ for $\join_{\GM}$ and $\join_{user}$ such that, for some valid
public state $\mathsf{st}'$, the execution of the interactive protocol
$\langle \join_{\user}(\lambda,\gspk),\join_{\GM}(\lambda,\mathsf{st}',\gspk,\mathcal{S}_{\GM}) \rangle_\varpi$
provides $\join_{\user}$ with $(i,\scr_{i },\crt_{i })$.

\begin{definition}[Correctness]
  A dynamic group signature scheme is correct if the following conditions are
  all
  satisfied:
%
  \begin{enumerate}[(1)]
%
    \item In a valid state $\mathsf{st}$, $|\mathsf{st}_{users}|=|\mathsf{st}_{trans}|$ always holds and
      two distinct entries of $\mathsf{st}_{trans}$ always contain certificates with
      distinct tag.
%
    \item If
      $\langle \join_{\user}(\lambda,\gspk),\join_{\GM}(\lambda,\mathsf{st},\gspk,\mathcal{S}_{\GM}) \rangle$
      is run by two honest parties following the protocol and
      $\langle i, \crt_{i }, \scr_{i } \rangle$ is obtained by $\join_{\user}$, then
      we have $\crt_{i} \leftrightharpoons_{\gspk} \scr_{i }$.
%
    \item For each %revocation period $t$ and any
      $(i, \crt_{i}, \scr_{i})$ such that $\crt_{i }
      \leftrightharpoons_{\gspk}  \scr_{i }$, satisfying condition 2, we have
      $ \mathsf{Verify}\big(\mathsf{Sign}(\gspk, \crt_{i }, \scr_{i
      },M),M,\gspk\big)=1$.
%
    \item For any outcome $(i, \crt_{i }, \scr_{i })$ of
      $\langle\join_{\user}(.,.  ),\join_{\GM}(.,\mathsf{st},.,. )\rangle$
      for some valid state information $\mathsf{st}$, if $\sigma =\mathsf{Sign}(\gspk,\crt_{i }, \scr_{i},M)$, then
      $\mathsf{Open}(M,\sigma,\mathcal{S}_{\OA},\gspk,\mathsf{st}')=i.$
%
  \end{enumerate}
  %
\end{definition}

\section{Associated Security Notions}
\addcontentsline{tof}{section}{\protect\numberline{\thesection} Notions de sécurité associées}
\label{sse:gs-sec-notions}

\subsection{Oracles for Security Experiments}
\addcontentsline{tof}{subsection}{\protect\numberline{\thesubsection} Oracles nécessaires à la définition des expériences de sécurité}

We formalize security properties via experiments where the adversary
interacts with a stateful interface $\mathcal{I}$ that maintains the following
variables:
%
\begin{itemize}
%
  \item $\mathsf{state}_{\mathcal{I}}$: is a data structure representing the
    state of  the interface as the adversary invokes the various oracles
    available in the attack games. It is initialized as
    $\mathsf{state}_{\mathcal{I}}=(\textsf{st},\gspk,\mathcal{S}_{\GM},
    %\linebreak[4]
    \mathcal{S}_{\OA}) \leftarrow \mathsf{Setup}(1^\lambda,1^\Ngs)$.
    It includes the (initially empty) set $\textsf{st}_{users}$ of group members and a
    dynamically growing database $\textsf{st}_{trans}$ storing the transcripts of
    previously executed join protocols.
%Finally,
%$\mathsf{state}_{\mathcal{I}}$  includes a counter
%$t$ (which is initialized to $0$) indicating the number of user revocation
%queries so far.
  \item $n=|\textsf{st}_{users}|<\Ngs$ denotes  the current cardinality of the group.
%
  \item $\mathsf{Sigs}$: is a database of signatures created by the signing
    oracle.  Each entry consists of a triple $(i,M,\sigma)$ indicating that
    message $M$ was signed by user $i$.
%
  \item $U^a$: is the set of users that were introduced by the adversary in the
    system in an execution of the join protocol.
%
  \item $U^b$: is the set of honest  users  that   the adversary, acting as a
    dishonest group manager, introduced in the system. For these users, the
    adversary obtains the transcript of the join protocol but not the   user's
    membership secret.
%
\end{itemize}

In attack games, adversaries are granted access to the
following oracles:

\begin{itemize}
%
  \item $Q_{\mathsf{pub}}$, $Q_{\mathsf{key\GM}}$ and $Q_{\mathsf{key\OA}}$: when
    these oracles are invoked, the interface looks up $\mathsf{state}_{\interface}$ and
    returns   the group public key $\gspk$,   the GM's private key
    $\mathcal{S}_{\GM}$ and the opening authority's private key
    $\mathcal{S}_{\OA}$ respectively.
%
  \item $Q_{\ajoin}$: allows the adversary to introduce  users under its control
    in the group. On behalf of the GM, the interface runs  $\join_{\GM}$ in
    interaction with the $\join_{\user}$-executing adversary who plays the role of
    the prospective user in the join protocol. If this protocol successfully
    ends, the interface increments $n$, updates $\mathsf{st}$ by inserting the new user
    $n$ in both sets $\mathsf{st}_{users}$ and $U^a$. It also sets
    $\mathsf{st}_{\trans}\coloneqq \mathsf{st}_{\trans} || ( n, \transcript_n )$.
%
  \item $Q_{\bjoin}$: allows the adversary, acting as a corrupted group manager,
    to introduce new honest group members of its choice. The interface
    triggers an execution of $\langle \join_{\user},\join_{\GM} \rangle$ and runs $\join_{\user}$ in
    interaction with the adversary who runs $\join_{\GM}$. If the protocol
    successfully completes, the interface increments $n$, adds user $n$  to
    $\mathsf{st}_{users}$ and $U^b$ and sets
    $\mathsf{st}_{\trans}\coloneqq \mathsf{st}_{\trans} || ( n, \transcript_n )$.
    It stores the   membership certificate $\crt_{n  }$
    and the membership secret $\scr_{n }$ in a \textit{private} part of
    $\mathsf{state}_{\interface}$.
%
  \item $Q_{\mathsf{sig}}$: given a message $M$,  an index $i$, the interface
    checks whether the private area of $\mathsf{state}_{\interface}$ contains a
    certificate $\crt_{i }$ and a membership secret $\scr_{i }$.    If no such elements $(\crt_i,\scr_i)$ exist or if $i \not\in U^b$, the
    interface returns $\bot$.  Otherwise, it outputs a signature $\sigma$ on
    behalf of user
    $i$
    and  also sets $\mathsf{Sigs} \leftarrow \mathsf{Sigs} || (i,M,\sigma)$.
%
  \item $Q_{\mathsf{open}}$: when this oracle is invoked on input of a valid
    pair $(M,\sigma)$,
    the interface runs  algorithm $\mathsf{Open}$ using the current state $\mathsf{st} $.
    When $S$ is a set of pairs of the form $(M,\sigma)$,
    $Q_{\mathsf{open}}^{\neg S}$ denotes a restricted  oracle that only applies
    the opening algorithm to pairs $(M,\sigma)$ which are not in $S$.
%
  \item $Q_{\mathsf{read}}$ and $Q_{\mathsf{write}}$: are used by  the adversary
    to read and write  the content of $\mathsf{state}_{\interface}$. At each
    invocation,  $Q_{\mathsf{read}}$ outputs the whole $\mathsf{state}_{\interface}$ but
    the public/private keys and the private part of $\mathsf{state}_{\interface}$ where
    membership secrets are stored after $Q_{\bjoin}$-queries. By using
    $Q_{\mathsf{write}}$,  the adversary can modify $\mathsf{state}_{\interface}$ at
    will as long as it does not  remove or alter elements of $\mathsf{st}_{users}$,
    $\mathsf{st}_{trans}$ or invalidate the public state $\mathsf{st}$: for example, the adversary
    is allowed to create dummy users  as long as it does not re-use already
    existing certificate tags.

\end{itemize}

Based on the above syntax,  the
security properties are formalized as follows.

\subsection{Security Against Misidentification Attacks}
\addcontentsline{tof}{subsection}{\protect\numberline{\thesubsection} Sécurité face aux attaques par identification incorrecte}
\label{sec:RGSdefsecMisId}
\index{Dynamic group signatures!Mis-identifications}

\begin{figure}[H]
  \centering
  \procedure{Experiment $\Exp{\textrm{mis-id}}{\adv}(\lambda)$}{%
    \mathsf{state}_{\interface}=(\mathsf{st},\gspk,\mathcal{S}_{\GM},\mathcal{S}_{\OA})
    \gets \mathsf{Setup}(1^\lambda,1^\Ngs)\\
    (M^\star,\sigma^\star) \leftarrow \adv(Q_{\mathsf{pub}},Q_{\ajoin},
    Q_{\mathsf{read}},Q_{\mathsf{keyOA}})\\
    \pcif \mathsf{Verify}(\sigma^\star,M^\star,\gspk)=0 \pcthen\\
    \pcind \pcreturn{0}\\
    i =\mathsf{Open}(M^\star,\sigma^\star,\mathcal{S}_{\OA}, \gspk,\mathsf{st}')\\
    \pcif i \not\in U^a \pcthen \\
    \pcind\pcreturn{1}\\
    \pcelse\\
    \pcind \pcreturn 0
  }
  \caption{Experiment for security against misidentification attacks.}
  \label{exp:mis-id}
\end{figure}

In a misidentification attack, the adversary can corrupt the opening authority
using the $Q_{\mathsf{keyOA}}$ oracle and introduce
malicious users in the group via $Q_{\ajoin}$-queries.
It aims at producing a valid signature $\sigma^\star$ that does not open to any
adversarially-controlled user.


\begin{definition} \label{def:mis-id}
  A dynamic group signature scheme is secure against \emph{misidentification
  attacks} if, for any $\ppt$ adversary $\adv$ involved in Experiment~$\Exp{\textrm{mis-id}}{\adv}(\lambda)$
  described in Figure~\ref{exp:mis-id}, we have:
  \[\advantage{\adv}{\mathrm{mis}\textrm{-}\mathrm{id}}(\lambda) \triangleq
    \Proba{\,\Exp{\mathrm{mis}\textrm{-}\mathrm{id}}{\adv}(\lambda)=1} \leq \negl[\lambda].\]
\end{definition}



\subsection{Non-Frameability}
\addcontentsline{tof}{subsection}{\protect\numberline{\thesubsection} Sécurité face aux attaques ciblées}
\label{sec:RGSdefsecMonFrame}
\index{Dynamic group signatures!Non frameability}

\begin{figure}[H]
  \centering
  \procedure{Experiment $\Exp{\mathrm{fra}}{\adv}(\lambda)$}{%
    \mathsf{state}_{\interface}=(\mathsf{st},\gspk,\mathcal{S}_{\GM},\mathcal{S}_{\OA})
    \gets \mathsf{Setup}(1^\lambda,1^\Ngs)\\
    (M^\star,\sigma^\star)
    \gets \adv(Q_{\mathsf{pub}},Q_{\mathsf{key}\GM},
      Q_{\mathsf{key}\OA}, Q_{\bjoin},%Q_{\mathsf{revoke}},
    Q_{\mathsf{sig}},	Q_{\mathsf{read}}, Q_{\mathsf{write}}) \\
    \pcif \mathsf{Verify}(\sigma^\star,M^\star,\gspk)=0 \pcthen\\
    \pcind \pcreturn 0 \\
    \pcif i=\mathsf{Open}(M^\star,\sigma^\star,\mathcal{S}_{\OA},
    \gspk,\mathsf{st}') \not \in U^b \pcthen\\
    \pcind \pcreturn 0\\
    \pcif
    \bigwedge_{j \in U^b \textrm{ s.t. } j=i~} (j,M^\star,\ast)
    \not\in \mathsf{Sigs} \pcthen \\
    \pcind \pcreturn 1\\
    \pcelse \\
    \pcind\pcreturn 0
  }
  \caption{Experiment for security against framing attacks.} \label{exp:frame}
 \end{figure}

Framing attacks consider the situation where the entire system  is colluding against some honest user.
The adversary can corrupt the group manager as well as the opening authority
(via oracles $Q_{\mathsf{key}\GM}$ and $Q_{\mathsf{key}\OA}$, respectively).
It can also introduce honest group members (via
$Q_{\bjoin}$-queries), observe the system while these users sign messages   and
create dummy users using $Q_{\mathsf{write}}$. %In addition, before the
%possible corruption of the group manager, the adversary can revoke
%group members at any time by invoking the $Q_{\mathsf{revoke}}$
%oracle. As a potentially corrupted group manager, $\A$ is allowed to
%come up with his/her own revocation list $RL_{t^\star}$ at the end of the game.
%We assume that anyone can publicly verify that $RL_{t^\star}$ is
%correctly formed ({\it i.e.}, that it could be a legitimate output of
%$\mathsf{Revoke}$) so that the adversary does not come up with
%an ill-formed revocation list.
%For consistency, if $\A$ chooses not to corrupt the GM, the produced
%revocation list $RL_{t^\star}$ must be the one determined by the history
%of $Q_{\mathsf{revoke}}$-queries.
The adversary eventually aims at framing an honest group member.

\begin{definition} \label{def:frame}
%
  A dynamic group signature scheme is secure against \emph{framing attacks} if,
  for any $\ppt$ adversary $\adv$ involved in the experiment~$\Exp{\mathrm{fra}}{\adv}(\lambda)$ described Figure~\ref{exp:frame}), it holds that
  \[ \advantage{\adv}{\mathrm{fra}}(\lambda)=\Proba{\Exp{\mathrm{fra}}{\adv}(\lambda)=1} \leq \negl[\lambda]. \]
%

\end{definition}

\subsection{Full Anonymity}
\addcontentsline{tof}{subsection}{\protect\numberline{\thesubsection} Anonymat complet}
\label{sec:RGSdefsecAnon}
\index{Dynamic group signatures!anonymity}

\begin{figure}[H]
  \centering
  \procedure{Experiment $\Exp{\textrm{anon}}{\adv,d}(\lambda)$}{
    \mathsf{state}_{\interface}=(\mathsf{st},\gspk,\mathcal{S}_{\GM},\mathcal{S}_{\OA})
    \gets \mathsf{Setup}(1^\lambda, 1^\Ngs)\\
    \big(aux,M^\star,(\scr_{0}^\star,\crt_{0}^\star),
    (\scr_{1}^\star,\crt_{1}^\star )\big)
    \gets \adv(\mathsf{play};\, Q_{\mathsf{pub}},Q_{\mathsf{key\GM}},
  %Q_{\mathsf{revoke}},
    Q_{\mathsf{open}},Q_{\mathsf{read}},Q_{\mathsf{write}})\\
  %\If{\neg(\crt_{b}^\star \leftrightharpoons_{\gspk} \scr_{b}^\star) for b\in\bit}
  %{\Return \bot\\}
  %\If{\crt_{0 }^\star = \crt_{1 }^\star }{\Return \bot\\}
    \pcif
    \neg((\crt_{0}^\star \leftrightharpoons_{\gspk} \scr_{0}^\star)
      \wedge (\crt_{1}^\star \leftrightharpoons_{\gspk} \scr_{1}^\star)
    \wedge (\crt_{0}^\star \neq \crt_{1 }^\star)) \pcthen\\
    \pcind\pcreturn \bot\\
  %Pick random d \gets \bit;
    \sigma^\star \leftarrow \mathsf{Sign}(\gspk,\crt_{d}^\star,
    \scr_{d}^\star,M^\star)\\
    d'\leftarrow \adv(\mathsf{guess};\,\sigma^\star,aux,Q_{\mathsf{pub}},
      Q_{\mathsf{key\GM}},Q_{\mathsf{open}}^{\neg \{ (M^\star, \sigma^\star)\}},
    Q_{\mathsf{read}},Q_{\mathsf{write}})\\
    \pcreturn d';
%  \If{d'=d}{\Return 1;}
%  \Return 0\;
  }
  \caption{Security experiments for (full-)anonymity game.} \label{exp:anon}
\end{figure}

The notion of anonymity is formalized by means of a game involving a two-stage
adversary. The first stage is called $\mathsf{play}$ stage and allows the
adversary $\adv$ to modify $\mathsf{state}_{\interface}$ via $Q_{\mathsf{write}}$-queries
and open arbitrary signatures by probing $Q_{\mathsf{open}}$.  When the
$\mathsf{play}$ stage ends, $\adv$ chooses a message $M^\star$ as well as two
pairs $(\scr_{0}^\star,\crt_{0}^\star)$ and $(\scr_{1}^\star,\crt_{1}^\star )$,
consisting of a valid membership certificate and a corresponding membership
secret.  Then, the challenger flips a coin $d \gets \bit$ and computes a
challenge signature $\sigma^\star$ using $(\scr_{d}^\star,\crt_{d}^\star)$.  The
adversary is given $\sigma^\star$ with the task of eventually guessing the bit
$d \in \bit$. Before doing so, it is allowed further oracle queries
throughout the second stage, called \textsf{guess} stage, but is restricted not
to query $Q_{\mathsf{open}}$ for $(M^\star,\sigma^\star)$.

\begin{definition} \label{def:anon}
%
A dynamic group signature scheme is fully anonymous if, for any $\ppt$ adversary
$\adv$
in the experiment~$\Exp{\mathrm{anon}}{\adv, d}(\lambda)$ described in Figure~\ref{exp:anon}, the following distance is negligible:
  \[\advantage{\adv}{\mathrm{anon}}\left( \lambda \right) \triangleq
  \left| \Proba{\,\Expt_{\adv, 1}^{\mathrm{anon}}(\lambda) = 1} -\Proba{\,\Expt_{\adv, 0}^{\mathrm{anon}}(\lambda) = 1} \right|\]

%
\end{definition}



%One can wonder why the \emph{revocation} is not in the \emph{dynamic group
%signature scheme} description, the reason is only pragmatic. It is a different
%problem to build a scheme that allows to revoke a group member than a scheme
%that allows inserting a group member~\cite{DP06}, and it has to be done in a
%case-by-case fashion.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%