compliance.tex

% !Tex spellcheck = en_GB
\documentclass[runningheads,10pt]{llncs}

% Config

\usepackage{amsmath}
\numberwithin{equation}{section}

% https://tex.stackexchange.com/questions/42619/x-mark-to-match-checkmark
\usepackage{pifont}% https://ctan.org/pkg/pifont
\newcommand{\cmark}{\ding{51}}%
\newcommand{\xmark}{\ding{55}}%

\input{./config/packages.tex}
\input{./config/macros.tex}

% Add DRAFT watermark to the document
\usepackage[printwatermark]{xwatermark}
\newwatermark[allpages,color=gray!25,angle=45,scale=3.5,xpos=0,ypos=0]{DRAFT}

\title{{\textsf{Pistis}}: Privacy Preserving Compliant Transaction System}

\author{Antoine Rondelet \and Michal Zajac}
\institute{Clearmatics, UK \\
\email{ar@clearmatics.com}, \email{michal.zajac@clearmatics.com}}
\date{\today}

%\setcounter{tocdepth}{2}
\begin{document}
\maketitle

\begin{abstract}
  Recent surge in adoption of cryptoassets, by both retail and institutional
  investors, has lead to increased scrutiny from law makers and regulators.
  This increasing development and use of privacy-preserving technologies on
  blockchain systems raises a ``privacy vs compliance'' dilemma between
  designing systems providing strong privacy guarantees -- necessary to conduct
  any type of non-trivial business activity and fundamental to preserve
  individuals' financial freedom -- and the need for transparency to ensure
  regulatory compliance.

  In this paper we introduce \emph{Privacy Preserving Compliant Transaction
    System} (PPCTS) which assure that blockchain-traded assets can be traded
  privately, yet, in compliance with their regulatory frameworks. To that end we
  identify key actors that may take part in regulating such assets, list the key
  properties of a PPCTS, define a UC-model ideal functionality of such systems,
  and propose protocols that implement it.

\keywords{zero-knowledge proofs, regulatory compliance, digital cash, Ethereum,
  Zeth, privacy}

\vspace*{1em}

\textbf{Disclaimer:} The content of this work does not constitute legal advise.
\end{abstract}

\section{Introduction}\label{sec:intro}

The recent global developments in payment systems and financial technologies
coupled with the emergence and increased adoption of blockchain and
decentralised protocols present a wide set of opportunities as well as numerous
challenges.

Market structures, trading technologies and financial instruments have steadily
evolved over the centuries, forcing regulators across jurisdictions to 
continuously adapt existing frameworks to maintain high confidence in the 
financial system, protect its stability as well as its consumers.

\michals{4.10}{Refer to that later -- regulators need to keep financial system stable and protect its customers, hence ``regulatability'' is a must and our solution allows it.}

In the United Kingdom, for instance, the introduction of the Banking Act
(1979)~\cite{1979-uk-dev} -- in response to economic turbulence (1973--1975) due
to loosely controlled credit
allocation~\cite{Chapter10RegulatoryandOtherChangesintheUKBankingMarket} -- was
quickly followed by subsequent regulations, some of which aiming to detect and
prevent procedures by which money acquired from criminal activity could be
dissimulated and appear as being lawfully acquired (i.e.~so-called ``money
laundering''~\cite{si-1993-1933,2001-c-24,si-2003-3075}\footnote{See~\cite{ML-law}
for an overview of the evolution of AML regulations in the UK.}).  More
recently, and in light of the weaknesses revealed by the 2008--2009 financial
crisis, the UK regulatory framework has been reshaped, with, notably, the
dissolution of the Financial Services Authority (FSA) in
2013\footnote{Initially founded in 2001} and the creation of the Financial
Conduct Authority (FCA), Financial Policy Committee (FPC) and the Prudential
Regulation Authority (PRA). As of today, and as illustrated in~\cite[Chapter
1]{journey-to-fca}, the Bank of England (BoE) administers monetary policy,
influencing interest rates, inflation and employment, and also plays a key role
-- via its subsidiary, the PRA and the FPC -- in the regulation of financial
markets, along with the FCA -- supervised by HM Treasury.

While sound local financial regulations are key to keep domestic markets robust,
stable and trusted, criminal activities are frequently carried out on a large
scale. Local actions and systems to \emph{detect and report} suspicious activity to
law enforcement -- via Suspicious Activity Reports (SARs)\footnote{SARs are processed
  by the National Crime Agency (NCA) in the UK\cite{nca-sars,intro-to-sars} and by
  Financial Crimes Enforcement Network (FinCEN) in the US} -- are often criticised as
being very costly and offering few results~\cite{ML-law}.  \michals{4.10}{Another
  thing to refer -- in our system policy assigners define what is allowed and what's
  not. This allows for some degree of automatization of fraud / criminal activity
  prevention -- we allow application to have much stricter rules than they can be
  defined just for a casual wire transfer. More precisely, we allow users to remain
  anonymous, transfer funds quickly and privately, but on the other hand, policy
  assigners assign compliance policies that are at least as strict as compliance
  policies for classical non-anonymized fund transfer options.}

Moreover, the increasing development of fast cross-border communication technologies
and the patchwork of heterogeneous jurisdictions significantly increase the
difficulty to bring activities related to money laundering and financing terrorism
down. In an attempt to mitigate such issues, an intergovernmental organization, the
Financial Action Task Force (FATF), was created in 1989. This organization has
developed recommendations and standards in order to foster coordinated global
response to prevent organised crime, corruption and terrorism~\cite{fatf-about}.
\michals{4.10}{General comment -- when we provide some background on how financial
  markets are regulated / oversight, we should also state how our functionalities /
  PPCTS follows that regulatory approach. That is, we should not only give the reader
  a general background, but a background that is directly relevant to our solution
  and show how it is relevant.}

Nevertheless, despite the establishment of such organizations, along with the
signature of various ``Memorandums of Understanding''
(MoUs) e.g.~\cite{mou-fsa-sec,mou-fsa-cftc} (see also
e.g.~\cite{fca-sec-coop,fca-cftc-coop}) -- to ease
cross-jurisdiction investigations -- gathering evidence for investigating
illegal cross-border conduct remains a major challenge, particularly when
blocking or secrecy laws are involved, which may be unwelcomed by governmental
authorities in other countries~\cite{role-sec}.

\subsection{Regulating cryptoassets}

Recent surge in adoption of cryptoassets (by both retail and institutional
investors) has led to increased scrutiny from law makers and regulators.
Cryptocurrency projects like Diem--formerly known as Libra--present
``unprecedented taxation challenges''~\cite{Law2020Facebook}, and the increasing
development and use of privacy-preserving technologies on blockchain systems
(e.g.~\cite{DBLP:journals/corr/abs-1904-00905,EPRINT:BAZB19,aztec-protocol,zcash-protocol})
raises a ``privacy vs compliance'' dilemma between designing systems providing
strong privacy guarantees (necessary to conduct any type of non-trivial
business activity and fundamental to preserve individuals' financial freedom
which is at the core of democracy), and the need for transparency to ensure
regulatory compliance.

Despite the inherent transparency of various blockchains (which is leveraged by
several companies and projects e.g.~\cite{elliptic-company,chainanalysis-company,bitcoin-abuse} to understand payment flows
within the systems) reports suggest that such systems have ``offered exceptional
scalability to ransomware operations''~\cite{tails-ransoms} and are used for
illicit activities online~\cite{analysis-darknet}.
%
Interestingly, empirical evidence suggest that privacy-enabling cryptocurrencies
are only used in minority to carry out fraudulent activity on the
darknet~\cite{RR-4418-ECC}. However, it is important to bear in mind that this
landscape is evolving astoundingly fast and what holds true today may not remain
true tomorrow. In an attempt to conciliate the use of privacy enabling
cryptocurrencies with regulatory compliance, some suggested to implement
risk-based Anti-Money Laundering (AML), Countering Financing of Terrorism (CFT),
and Know-Your-Customers (KYC) processes on Virtual Asset Services Providers
(VASPs)~\cite{perkinscoie_report,fatf-vasp}. These approaches, articulated
around the thesis that VASPs (e.g.~cryptocurrency exchanges) act as necessary
gateways criminals need to go through to ``wash and convert'' unlawfully
acquired cryptocurrencies to fiat monies (like GBP, EUR or USD) may not hold true indefinitely.

The dramatic expansion of the cryptocurrencies user base\footnote{As of Q3
  2020,~\cite{cryptoasset-benchmark} estimated a total of up to 101 million
  unique users across 191 million accounts opened at service providers, while
  two years prior, a similar study estimated the number of identity-verified
  cryptoasset users at about 35 million globally.}  leading to broader
  acceptance of cryptocurrencies as means of payment (see
  also~\cite{bloomberg-zug-crypto-tax,bbc-btc-legal-tender}) represent an
  impediment for regulators who try to regulate the ever-mutating blockchain
  industry without altering financial innovation\footnote{E.g.~bills like the
  Stable Act~\cite{stable-act-draft} which intend to regulate stablecoin
  issuers (bank charters and reserves requirements) are seen as ``innovation
  killers'' by opponents.}.  Even if having ``legal tender'' in almost no
  jurisdictions (except El Salvador, at the time of
  writing~\cite{bbc-btc-legal-tender}), cryptoassets with large user bases can
  lead to a large number of (truly) peer-to-peer transfers which associated
  funds may never be redeemed and converted to fiat money, hence failing to
  flow through the checks implemented by centralized services such as
  exchanges.
  Furthermore, various KYC checks could also be bypassed by carrying out
  off-chain transactions of cryptoassets via the exchange of ``hardware
  sticks'' bearer instruments (e.g.~Zeth Bearer Instruments~\cite{zbi-article}) or, by using blockchain transaction
  relays~\cite{zeth-relay} as a way to escape on-chain surveillance tools for
  instance. Finally, the patchwork of heterogeneous cryptocurrency regulations
  around the world can still be leveraged to escape strict regulations by
  turning to VASPs located in advantageous jurisdictions, or by designing
  instruments that may not fall strictly under a regulator's
  jurisdiction\footnote{In the US for instance, the Security and Exchange
  Commision's (SEC) jurisdiction is over securities, while the Commodity
  Futures Trading Commission (CFTC) has jurisdiction over derivatives such as
  futures and swaps (further to the Dodd-Frank Act~\cite{cftc-dodd-frank}).
  Such separation of concern between the SEC and the CFTC poses a challenge
  with regard to regulating cryptoassets as it may be unclear which assets
  (e.g.~stablecoins, synthetic assets, blockchain-based derivatives, ``utility
  tokens'', NFTs etc.) should be treated as securities or not (see ``Howey Test''~\cite{sec-howey})}.

\subsection{Parties involved in regulatory compliance on blockchain systems}
Before discussing solutions and designs for the compliance verification, it is
crucial to answer the following question: \emph{Who are the parties involved in
compliance verification process?}  We list below the set of actors that may be
obliged to participate in such process. Importantly, the nature of
the transacting parties -- highly regulated entities like banks, retail traders etc. --
may require different compliance checks involving potentially different
regulators (see~\cref{sec:intro}).

\subsubsection{Regulatory bodies.}
The role of such regulatory bodies is to act as standard-setters~\cite{role-sec}, in
order to define the set of recommendations and rules that financial actors need to
follow in a given (set of) jurisdiction(s). This established set of standards is then
used as a basis for further activities, ranging from \emph{supervision} to
\emph{enforcement} to \emph{authorisation} to only name a few.\footnote{See
  e.g.~\url{https://www.fca.org.uk/publications/corporate-documents/our-approach}}

\subsubsection{(Financial) Services Providers.}
\paragraph{Centralized VASPs.} Despite a lack of consensus around
cryptocurrency regulations\footnote{See
  e.g.~\url{https://complyadvantage.com/blog/cryptocurrency-regulations-around-world/}
  for more details}, cryptocurrency exchanges allowing consumers to buy and sell
cryptoassets tend to implement standard processes that consist in identifying
and verifying users, maintaining records, and complying with AML/CFT reporting
obligations. Such obligations can vary from one jurisdiction to another and may
include, among others, suspicious transaction or activity reporting, enhanced
procedures for high transaction amounts etc.  Moreover, customized checks may
additionally be carried out depending on the risk profile of the cryptoassets
traded, as well as the VASPs' jurisdictions. Trading privacy preserving
cryptocurrencies, for instance, may require additional customer checks.

\paragraph{Smart contract (DApp) providers.} Implementers of decentralized
applications (DApps) are providing state transitions allowing network users to
transact on a blockchain system (such state transitions may be: ``stablecoins
functionalities'', ``decentralized exchanges'' etc.).  Such applications are
hosted on each of the nodes of the decentalized blockchain network, and are thus
not executed within a well-defined jurisdiction.  Instead, the associated code
is hosted and executed on all blockchain nodes worldwide, which poses a
challenge for regulation. Nevertheless, such applications \emph{may} be provided
by organizations registered within a specific jurisdiction, providing an avenue
for local regulators. It is important to note, however, that anonymous groups of
developers may still deploy applications to public blockchain networks.

In the next sections, we will argue that DApps deployed or operated by registered
organizations may implement privacy-preserving compliance checks at the protocol
level; providing a robust complement to regulatory compliance checks implemented
on centralized venues (e.g.~centralized exchanges).  Such compliance checks may
be added to the provided state transition on the blockchain, allowing to
automate part of the process, preventing fraudulent state transitions and
lessening burdensome reconciliations\footnote{Since the state of a blockchain is
  immutable, it is useful to prevent fraudulent state transitions from being
  executed and added to the chain in order to keep a compliant state at any
  point in time, reducing reconciliation procedures and associated costs.}.

\paragraph{Blockchain developers and operators.} Establishing the regulatory regime
of blockchain systems is a tedious task, especially due to the potential lack of
central coordinating entity. As proposed in a draft document by the
FATF~\cite{fatf-va-sixth-draft} (further amended~\cite{fatf-vasp-updated}), governance token holders or developers of blockchain
systems may be considered as VASPs, and hence subject to their regulatory
regimes. While it is not possible to foresee tomorrow's regulations, it seems that if
the early FATF recommendations were to be followed, there could be a convergence between
the so-called \emph{permissionless} and \emph{permissioned} blockchains. In other
words, if there exist a regulated VASP behind the development of every blockchain
systems, chances are that KYC and Customer Due Diligence (CDD) processes will be
implemented in order to onboard users on the systems, for example, it may be
necessary to modify the Ethereum account address creation routine to ensure that new
accounts have been created w.r.t.~KYC and CDD.

Permissionless blockchain protocols, allowing ad-hoc on/off-boarding on the system, have flourished
in the last years and observed steep increase in retail and institutional adoption
\cite{eib-bond-ethereum,occ-blockchain}. It is unclear whether the current
situation -- relying on centralized VASPs to act as safeguards or gateways to prevent
fraudulent conversions of funds between fiat and cryptocurrencies -- will persist or
mutate. In the rest of this document, we focus exclusively on permissionless
blockchains. We further consider blockchains with an expressive execution environment
allowing to deploy and execute smart contracts (e.g.~EVM
chains\footnote{i.e.~blockchains using the Ethereum Virtual Machine.
  See~\cite{eth-docs-evm} for more details.}).

\paragraph{Blockchain services providers.} While blockchain protocols act as
the backbone on which DApp services are deployed, it is also important to note
that a myriad of businesses have been created beyond the strict boundaries of
blockchains, forming entire ``off-chain'' ecosystems. Such services may
either be:
\begin{itemize}
\item[\emph{custodial},] like wallet providers, securing the cryptographic
  keys of their users; or
\item[\emph{non-custodial},] like transaction relays, which receive messages
  from their users and relay them to the blockchain, cf.~\cite{zeth-relay}; or
  blockchain bridges, which connect multiple blockchain systems,
  e.g.~\cite{btcrelay,rainbow-bridge}
\end{itemize}

It seems fair to assume that custodial services providers must be subject to
stricter regulations, since they control the users' funds. On the other hand,
loose regulations around non-custodial services may constitute an open door for
fraudulent activity, e.g.~unregulated flows of liquidity from one blockchain to
another etc. For simplicity, we do not consider the regulatory regime for these
service providers in the rest of this document.

\begin{remark}
  We note that, CDD checks are generally carried out by verifying legal
  documents owned by the service customer (identity check using passports, proof
  of fund provenance using payslips or bank statements etc.) \emph{which are
    ill-suited for information disclosure minimization}. For example, the broker
  probably does not need to know the city of birth of a customer, nor their
  precise age. Instead it may simply know that the customer is legally
  authorized to trade. On the other hand, cryptographic tools make it possible
  to carry out such compliance checks with minimal information
  disclosure.
\end{remark}

\subsubsection{Transacting parties.}
Beyond financial services providers and regulatory bodies, we now consider two
categories of users: those using existing services provided by regulated third
parties (e.g.~DApps, exchanges etc), and those who do not.  While the former
user class -- \emph{blockchain services users} -- is subject to AML/CFT/KYC
processes implemented by the service of interest (and must then provide multiple
pieces of information), the latter user class -- \emph{native blockchain users}
-- may simply join the permissionless network on an ad-hoc basis, and are thus
exempt of such KYC checks.  In fact, native blockchain users can either simply
transact native assets (e.g.~ETH) on the platform without using any DApp
services, and/or may leverage the smart-contracts capabilities of the underlying
blockchain to seal self-enforcing legally binding agreements with other users as
a substitute of legal (paper) contracts. (In such case, the cryptographic
signature attached to the blockchain transaction executing the smart-contract
acts as the digital equivalent as an ``ink signature'' on a (paper) contract.)

In the rest of the document, we will treat all smart contracts as DApps, and
focus on the relations between service providers, their users and the
regulatory bodies.

%%%%%%%

% \color{gray}
% \subsection{Cryptographic toolkit to build blockchain-based compliant systems}
% \michals{26.08}{I vote for removing this section from the paper. It brings little and slows reader down. AC and ZK proofs can be described along the way, view keys are not used, hence may be discarded.}

% \paragraph{Anonymous credentials}
% Identity verification is ubiquitous in our society. Whether it is to enter a
% pub, access an online service, or open a bank account, it is always necessary
% to show some credentials (and/or perform tasks -- like a captcha\footnote{An
% individual's ability to perform some task (i.e.~the \emph{Capability} mental
% model~\cite{rwot-models-identity}) is useful in the context of defining the
% individual's Identity. See~\cite{rwot-models-identity} for more information
% about the various dimensions and mental models of \emph{Identity}}). While the
% exchange and display of ``paper credentials'' (e.g.~passports) is common today,
% such credentials are not adequate for online processing, prone to forgeries,
% and do not provide an avenue for information disclosure minimalization. These
% obstacles are particularly concerning for the end users, as well as for
% services providers\footnote{In fact, ``data'' is often nicknamed as the
% ``digital oil'' and mostly seen as a source of income for companies (since
% large datasets can be used to ``train'' machine learning algorithms/refine
% models that generate business value, and/or can simply be sold to
% third-parties). Nevertheless, besides being an asset, ``data'' is also a
% liability. Data breaches in online services expose customers of the services
% and may greatly impact the reputation of the affected businesses.}. To that
% end, it is natural to turn to the use of cryptographic tools such as
% \emph{anonymous credentials}~\cite{C:Chaum83a} when designing scalable
% (privacy-preserving) systems. Instead of exchanging scans of paper credentials,
% PDF documents, or any other material, disclosing, in full, potentially
% sensitive information; cryptographic solutions using anonymous credentials may,
% instead, be used to prove facts (cryptographically) about pieces information in
% a privacy preserving manner. For instance, anonymous credentials constructions
% can be used in due diligence processes, for KYC/AML procedures etc.
% 
% \paragraph{Zero-knowledge proof systems (see~\cref{crypto-preliminaries:zkps})}\label{val-candidates:ssec:zkcp}
% Beyond the potential use of ``general purpose'' zero-knowledge proof systems
% (i.e.~proof systems covering wide complexity classes) for the design of
% anonymous credentials (see, e.g.~\cite{DBLP:journals/corr/abs-2006-05201}), such
% cryptographic primitives may be used --- more broadly --- to generate
% Zero-Knowledge Compliance Proofs (ZKCPs), that show that a user uses a service
% in a compliant fashion (e.g.~a user's transaction follows the rules of the
% system, provided that ``the rules of the system'' are encoded in an adequate
% algebraic form).
% 
% As flexibility is generally required in a system\footnote{E.g.~to account for
% multiple user classes (e.g.~retail traders vs institutional traders on an
% exchange) which may be subject to different regulatory regimes (e.g.~depending
% on their legal status and trade activity on a system) and different service
% rules, or to account for changing regulations}, different proof systems may be
% used to support different compliance policies within a single service. For
% instance, ``universal'' Succinct Non-interactive ARguments of Knowledge
% (SNARKs) (e.g.~\cite{EPRINT:GabWilCio19,CCS:MBKM19}) or ``transparent'' SNARKs,
% so-called Zero-Knowledge Scalable Transparent ARguments of Knowledge (STARKs)
% may be used here. However, QAP-based SNARKs such as~\cite{EC:Groth16} may also
% be leveraged to design systems with flexible compliance policies, by using
% \emph{universal circuits}~\cite{STOC:Valiant76} or by using recursive proof
% composition~\cite{TCC:Valiant08} for instance. These solutions offer different
% tradeoffs and must be selected, by protocol designers, in a way that optimizes
% for the necessary parameters during the design of the protocols.
% 
% Finally, we note that processing ZKCPs on-chain may allow to delegate part of
% the auditing task (i.e.~ZKCP verification) to a smart contract. Although this
% model has limitations\footnote{Using a publicly verifiable NIZK on a blockchain
% system still leaks information about the validity of the proofs, which may leak
% information about the behavior of the user on the system. Furthermore, the
% storage cost of adding cryptographic proofs to the chain data needs to be
% considered.}, this setting could be used as an automated SARs filling system.
% If the contract rejects the submitted ZKCP, then it could mark the transaction
% as non-compliant and emit an event that can be consumed by a off-chain process
% running on a regulator's system, to allow regulators to react appropriately.
% 
% \begin{example}[ZKCP on-chain]
% Consider a privacy-preserving transaction system where transactions which value
% exceeds $\$ 10,000$ require a special permission while other transactions are
% proceeded with no such delay\footnote{Such mechanism may be useful to regulate
% the amount on ``cash''-type transactions on-chain.}. The system may be designed
% such that a user of a DApp must provide a \emph{range proof} proving that the
% private amount transferred via the on-chain service is below an authorized
% threshold\footnote{Informally, a range proof is a (zero-knowledge) proof that a
% secret value lies in a given interval.}. If the proof verifies correctly (on
% the smart contract), then the transaction is fully executed by the
% smart-contract, and the blockchain state is modified accordingly. If the range
% proof does not verify correctly however (i.e.~the transferred amount is above
% $\$ 10,000$), the transaction execution is aborted (i.e.~no further changes are
% made to the blockchain state), and the user may contact the DApp operator to
% provide additional pieces of information about the transaction so that it may
% be signed by the service operator and re-submitted for inclusion to the chain.
% Such approach prevents non-compliant state transitions on blockchain services,
% while automating part of the compliance process via smart contracts and
% cryptographic checks.
% \end{example}
% \color{black}

%%%%%%%
\subsection{State of the art}
\michals{27.08}{For now we have here only parts moved from other sections. Need
  to expand}

\michals{6.09}{Give an introduction for this section}

Below we discuss some prior approaches to compliance and privacy-preserving
transacting systems.

\paragraph{View keys}\label{val-candidates:ssec:data-reveal}
In contexts where an operator must be granted the right to monitor all activity
happening on a given service, it is possible to use so-called \emph{view keys}.
Regardless of the derivation method employed to generate the keys, this approach
aims to keep users' data (e.g.~transaction details) private to the rest of the
user set, while allowing full disclosure of user's activity to a service
operator. Such approach obviously raises issues related to users' privacy and
\emph{key custody} -- the service operator must ensure that the key material is
adequately protected to prevent unintended use of the view keys. This often
necessitates to extend the service's infrastructure with Hardware Security
Modules (HSMs), employ multi-party computation techniques (e.g.~``key
splitting''), and set strict access control policies (e.g.~to prevent ``insider
attacks'').

\paragraph{On Damgård et al \cite{EPRINT:DGKOS20}.}
Our work relies on Damgård et al \cite{EPRINT:DGKOS20} who defines
UC-functionality for privacy preserving transacting system. The system allows
users to create multiple (yet limited number of) accounts, such that it is
infeasible for an external spectator to tell which user posses which
accounts. On the other hand, if the user behaves dishonestly then a qualified
set of so-called anonymity revokers can reveal its credentials and remove it and
all its accounts from the system.

In this paper we rely on this solution. However, as explained in
\cref{sec:our-solution}, we extend it considerably. One of the most important
improvement being including compliance checks into the system.

\subsection{Our contribution}
\label{sec:our-contribution}

As initially alluded to in~\cite{DBLP:journals/corr/abs-2008-05958}, compliance
predicates can be used along with modern zero-knowledge proof system in order
to conciliate the use of privacy-preserving protocols with regulatory
compliance. In fact, arguing about predicate satisfaction in zero-knowledge can
lead to efficient design for auditable digital-cash/private transfers on
blockchain systems.

In this paper, we propose several considerations and tools for the design of
privacy-preserving blockchain-based compliance protocols\footnote{The
work~\cite{zkp-and-law}, published while writing this manuscript, further
proposes to use zero-knowledge proofs as a way to solve so-called
``Verification Dilemmas'' in multiple legal contexts. What we describe here as
a privacy/compliance paradox can be phrased as a Verification Dilemma.}. We
start by considering the various settings by which compliance can be enforced
on blockchain systems. Then, we describe a protocol that automates and
facilitates privacy-preserving compliance checks on blockchains like
Ethereum~\cite{ethyellowpaper}. We base our solution directly on the work of
Dåmgard et al.\cite{EPRINT:DGKOS20}, however we provide it with the following
improvements:

\paragraph{Private policies.}
Our most important contribution is to allow for private compliance policies
both on the accounts as well as on the transactions. More precisely,
in~\cite{EPRINT:DGKOS20} each user has a private list of attributes $\AL$ that
is signed by an identity provider (to assure that users cannot set these
attributes as they like), and each of the user's accounts has a specified
publicly-known policy $\comppolicy$, such that $\comppolicy(\AL) = \true$,
i.e.~the policy is fulfilled by the user's attributes. Unfortunately, we note
that despite the use of zero-knowledge proof systems to prove that some private
data satisfies some properties/constraints, there is always a tradeoff between
the information leaked by the system, and the statement that is being proven.
For example, consider a trading platform that should only be available to EU
citizens (i.e.~$\comppolicy$ here is of the form ``is EU citizen?'' and returns
true or false depending on the input data). The platform operator may, for
instance, hold a set of public keys from identity issuers from all 27
countries, and expect users to provide a message signed by one of the
authorized identity issuer to create an account. Nevertheless, such an approach
leaks (one of) the nationality(ies) of the user via the signature of the
identity issuer. So, even if the message signed perfectly blinds the user's
sensitive credential data, the protocol uses very restrictive predicates that
leak valuable information about the user to the platform (and more importantly,
to potential network adversaries!). Such leakages are particularly important
since they may accrue as the system is used for prolonged period, and may be
correlated with other data sources (e.g.~other leakages on the system) to carry
out de-anonymization attacks. The first step towards finding a solution to this
problem is to acknowledge that leakages still occur even when using
cryptographic tools such as zero-knowledge proof systems. Even if
$\comppolicy(\AL) = \true$ is proven in zero-knowledge, the ``verification
bit'' is disclosed to the verifier (i.e.~disclosed to the public if a scheme is
publicly verifiable). As such, the design of the statements to prove is of
particular importance. To stop leaking the citizenship in our example, it may
be more appropriate for the trading platform operator to leverage ring
signatures with the set of identity issuers. That way the signature on the user
message only proves that one EU member has issued valid credentials to this
user, without disclosing the particular issuer. That is, system designers must
design sufficiently sophisticated predicates to safely provide access to their
services to users while empowering them with privacy and minimal information
disclosure\footnote{A general good practice is to design a predicate (to prove
in zero-knowledge) as a decision tree that branches with each OR clause in the
policy (i.e.~see a policy as a logical disjunction). This allows users to use
their private data to evaluate the appropriate branch to true, redeeming the
whole policy valid, without disclosing the evaluation path in the tree.}. This
is all the more important in the context of blockchain-based services
(e.g.~DApps) as user messages (i.e.~transactions) are routed on a broadcast
network before being included to a public ledger. Poor policy design from the
DApp providers exposes their end-users to the whole network.

In this paper we propose a mechanism allowing users to \emph{hide} the
compliance policy they prove, effectively minimizing information leakages on
the system and better safeguarding users' sensitive personal and transactional
data.

\paragraph{Transaction checks.}
Contrary to \cite{EPRINT:DGKOS20}, which focuses exclusively on an identity
layer, we allow, in our ideal functionality (and protocol), users to show
predicate satisfaction on their transaction data. This makes it possible to
prove compliance on privacy-preserving state transitions such as $\zeth$, which
brings Zerocash-type~\cite{SP:BCGGMT14} privacy to Ethereum\footnote{As noted
in~\cite{DBLP:journals/corr/abs-1904-00905} the difference between
account-based and UTXO-based blockchains is of particular importance with
regard to information leakages. The privacy guarantees in $\zeth$ are weaker
than these in Zerocash due to the need to pay for gas. More on that later.}.

\paragraph{On the gas model.}
The gas model introduced in Ethereum \cite{ethyellowpaper}, and relevant to
most smart contract enabled blockchains, is a security
mechanism that protects the network against adversaries trying to execute
non-halting programs. The mechanism is quite simple and effective as it prices
every computational (and memory manipulation) step of a smart contract,
effectively requiring the network users to pay for executing state transitions
on the system. While it is easy to see how such an approach solves the attack
vector abovementioned (i.e.~attackers trying to run non-halting
programs on the network would see their account balance emptied and the
computation would stop afterwards), this mechanism comes with major
drawbacks. One such issue is that the gas model constitutes an impediment to
user privacy on smart-contract chains. Since executing a smart-contract
requires to hold funds to be able to pay for each instruction executed,
end-users must call a smart contract from a funded account
(either funded via p2p transactions with other peers or via a VASP like an
centralized exchange). Inevitably, this means that at least one other party on
the network (VASP or another peer) knows additional information about the
holder of the account and can use such information to carry out de-anonymization
attacks on the network. To mitigate the tension between the need for gas and
the need for privacy, we extend our model to introduce
a collection of parties called \emph{relays} (denoted $\relay$) which append
information on the ledger on behalf of a user~\cite{zeth-relay}.

\begin{remark}
  We note that the need for an incentive structure assumed by Damgard et
  al.~\cite[Section 3.4]{EPRINT:DGKOS20} to make sure that no account
  holder can create more accounts than they are allowed, is not necessary if we
  design a PPCTS for a specific DApp on a smart contract chain. In this
  setting, no party may be required to report duplicated accounts as the
  account creation logic may partially be delegated to a smart contract which 
  would simply automatically reject the addition of an existing account entry
  by malicious account holders.
\end{remark}

Our proposed modifications on top of Dåmgard et al.'s \emph{identity-layer}
allow us to design a PPCTS, as defined in \cref{sec:capts}.

\section{PPCTS}
\michals{26.08}{Should be made a subsection of an introduction?}
\label{sec:capts}

Below, and when clear from context, we informally use the term \emph{verifier}
to denote the actor that asks pieces of information (e.g.~a service) to a
\emph{prover} (e.g.~a user or customer) and decides to either deem the received
pieces of information as admissible (or correct) or not.

\subsection{Desired properties}
\label{sec:desired_properties}
We list below the desired properties of a PPCTS:
\begin{description}
\item[{Completeness.}] An honest compliance verifier should always accept a
correct proof of compliance from an honest and compliant prover.

\item[{Soundness.}] It should be infeasible for a non-compliant prover to
convince the verifier to accept non-complying pieces of information as adequate
evidence of compliance, e.g.~an invalid transaction.

\item[{Efficiency.}] The compliance process must be efficient in order to
preserve the overall system's performances, i.e.~proving compliance and
verifying it must be efficient.

\item[{Reliability.}] If the system cannot verify the compliance it should
fail safe. That is, when a proof of compliance cannot be obtained, the system
should behave as if the compliance was not satisfied.

\item[{Robustness.}] The regulatory compliance checks must not \emph{only}
rely on trusted third parties and must not be easy to bypass.

This property is particularly important on distributed ledgers since KYC checks
implemented at specific gateways (e.g.~``exchanges/brokers'') may easily be
bypassed by using decentralized alternatives (decentralized exchanges, buying
assets on a purely peer-to-peer basis etc.)

\item[{Security.}] Implementing compliance processes must not undermine the
overall security of the system and of its users.

For instance, the PPCTS should not represent an attack vector on the system --
carrying out compliance checks must not put users' funds at risk -- and must be
designed around the same (or weaker) security assumptions as the system on which
it is built. Past events have demonstrated how (commercial) customer databases
and KYC checks carried out by hardware manufacturers and/or service providers
may translate into personal information leakages (e.g.~as consequences of cyber
attacks) about the user base, which may undermine users' personal
security/safety, e.g.~\cite{forbes-ledger-hack,ledger-hack-fear}, affecting the
breached service's reputation at the same time.  \michals{18.08}{How it is
  related to privacy?}\antoines{25.08}{It is not directly related. Sure a
  privacy preserving system will have less data to expose in the event of a
  breach on the service, but here the focus is on the security boundary of the
  system, which is to make sure that a flaw in the PPCTS cannot be used to break
  the whole system.}

\item[{Adaptability.}] PPCTS should be easy to extend and composable with
other systems.

In light of the quickly changing (legal and technological) environment due to
the fast-paced innovation in the blockchain ecosystem these properties are
especially imporant. In fact, regulators may adjust their guidance, or service
operators may decide to update their terms and services to collect more data
about their users (e.g.~transaction-related or personal pieces of information),
it should be possible for the parties involved in compliance verification to
provide and verify new pieces of information by relying on the infrastructure
and techniques already implemented in the PPCTS.

\item[{Privacy preservation.}] Compliance processes should not reveal any
additional information except the fact that the proven compliance policy holds.
\end{description}
\michals{26.08}{New structure here -- statement + description. Used
  ``paragraph'' envirionment, but not sure about it (p-graphs allow to easily
  distinc statement from description)}
\michals{26.08}{Important and missing -- showing that our PPCTS follow these
  rules}
\michals{26.08}{Important and missing II -- defining the above rules for our PPCTS.}

\subsection{Interactions between actors}

In light of the diversity in the set of actors, the set of messages exchanged
between a service user and a service provider may greatly vary depending on the
nature of the service, and depending on the user. While some of the pieces of
information related to regulatory compliance may be exchanged directly on the
blockchain (e.g.~cryptographic commitments, ciphertexts, etc.), other pieces of
information need to be exchanged via off-chain interactions. For instance, a
regulatory body may publish a set of recommendations and guidelines, that
service providers need to follow, on its website (off-chain). A user may want
to gain access to a blockchain-hosted service, and thus may exchange pieces of
information with the service operator (off-chain) to satisfy the KYC procedures
of the service. In response to the user's registration, a service may modify
the state the blockchain to grant the user access to the service, and/or may
simply carry out off-chain modifications to the service's state and send a
confirmation message (off-chain) to the user. While using the service, a user
may post data on the blockchain, which may be used by the service operator as
input to its monitoring processes.

It is important to remember, however, that blockchains are not ``mere
distributed databases''. In fact, a blockchain acts as ``source of truth'' to
which adding data is generally an expensive operation. Once added to the
immutable blockchain state, the cost of keeping a piece of data under consensus
(as part of the blockchain state) is paid by the whole network (see,
e.g.~\cite{zeth-state-simulation2021}). As such, not all pieces of information
are fit for inclusion on a blockchain system. For instance, adding Personally
Identifiable Information (PII) to immutable ledgers is not desired as it
violates data regulations in certain jurisdictions (e.g.~GDPR). More broadly,
appending pieces of information to a blockchain requires to send a message to a
public broadcast channel, which constitutes challenges with regard to
information leakages minimization in the context of privacy preserving
protocols (e.g.~as we saw, the mere fact of sending a zk-proof of a publicly
verifiable NIZK on a blockchain leaks the ``verification bit'' which provides
information about the instance/witness pair of the user).

\section{Protocol overview}

\subsection{The actors}
\paragraph{User $\user$.}
A user is a party using the system. That is, a party that wants to have their
transactions (i.e.~blockchain virtual machine state transtions) $\tx$ to be
processed by the system. To that end the user first obtains their application
identity from the identity module and (possibly anonymously) registers a number
of accounts which are then used to transact. Transactions provided by the user
are verified for their their validity and compliance. The latter may require
from the user additional data, like a proof that transactions follows the policy
assigned by the policy assigner, or interaction with the policy assigner
themself. Furthermore, if the user misbehaves they need to take into account
possible consequences like their identity reveal and accounts block. This is
possible since information required to reveal user's personal data or block
their accounts are given to a set of anonymity revokers, who working
collectively may disclose them.

\paragraph{Relay $\relay$.}
A relay is a party who provides other users with anonymity services. More
precisely, a relay acts as a proxy to the blockchain. It receives fees from
users in exchange for submitting transactions to the ledger on their behalf. By
submitting transactions from its ledger account, the relay pays for the gas
associated to the transactions and allows the end-users to stay anonymous
(i.e.~transact without a funded account on the ledger). Such relayed
transactions may, for instance, be used by users to fund a newly created ledger
account. Users may stay anonymous to the relay by making sure that no
information in the message sent to the relays (e.g.~transactions payloads) can
be used to de-anonymize them. To that end a number of privacy-preserving
techniques may be employed, like encryption, cryptographic commitments,
zero-knowledge proofs, and communications via anonymous communication networks. The incentivization structure of relays is outside of the scope of this 
document. For now, we assume that the relays can receive fees via off-chain or on-chain mechanisms. For discussions on relay mechanisms and incentivization, see e.g.~\cite{zeth-relay}.

\paragraph{Policy assigner $\polas$.}
The policy assigner is a party which provides the users of the system with
compliance policies that have to be followed by transactions the users send.
This makes the application owner -- VASP -- a natural candidate to fulfill that
role as well.

\paragraph{Anonymity revoker $\ar$.}
Anonymity revokers make a set of parties which role is to keep encrypted users'
credentials and their accounts' details. When a user behaves dishonestly, what
has to be agreed by at least some threshold of the anonymity revokers, then
these credential and account details are revealed to prevent the misbehaving
party from a further use of the system. Alternatively, an honest user should not
worry having their credential revealed in case of a dishonest anonymity revoker,
as any set that counts less than a threshold anonymity revokers can tell nothing
about the stored user's data.

\paragraph{Identity provider $\idprov$.}
Identity providers are parties who check real-life credential of users and
provides them with anonymized credential ready to be used in the system.

\paragraph{Application owner $\owner$.}
In the real world, the application owner is a party
that sets-up the transacting smart contract, picks which identity providers and
policy assigners should be available in the contract. The application owner is a
gate-keeper who prevents users, identity providers and policy assigners with bad
reputation to join the system. Here we also assume that the application owner
sets up the parameters for cryptographic primitives used in the system, like
encryption scheme, signature scheme, non-interactive zero-knowledge proofs,
where it picks the refence strings as well. (Alternatively, one could set up a
collective that jointly sets up the parameters and reference string via an MPC.)

\subsection{The protocol briefly explained}
From a high level, a user proceeds as follows (see~\ref{appendix:unrolled}
for more information). First, a user $\user$ retrieves
anonymity revokers' public keys and use them to threshold-encrypt its PRF key $\key$
that will be later used to create user's accounts.

\paragraph{Getting new identity.}
In the next step, the user interacts with a chosen identity provider $\idprov$ to get
an identity that will be used in the transacting system. To that end, it provides the
identity provider with an attribute list $\al$ which contains all data required to
get identity on the system. The identity provider checks $\al$ by either
non-cryptographic means (e.g.~relying on user's national ID or, in case of
institutions, its company register's entry), or using cryptographic credential scheme
with credential signed by a trusted entity. Importantly, we require the identity
provider to be able to identify the user so legal actions could be imposed on it if
it misuses the system. The user also shows $\idprov$ a public key of its choice
$\pcred$ and shows knowledge of the corresponding secret key $\scred$. If all the
checks are accepted, the identity provider signs $\scred$, user's key $\key$ that
will be used to create new system accounts and attribute list $\al$. Since we want
these values (possibly except of $\al$) to remain private, the signature is
blind. That is, the identity provider does not know what it signs, however, since we
also require that the user provides $\idprov$ with a zero-knowledge proof that it
picked data to be signed honestly, the identity provider may securely do that without
doubting on the validity of the data signed. We denote the signature by
$\signature_{id}$.

\paragraph{Getting compliance policy.} Before the user starts to transact it also
needs a compliance policy. Transactions the user is going to perform will need to
fulfill that policy. To that end, the user turns to a policy assigner $\polas$ and
defines how it wants to use the transacting system. Given that information $\polas$
picks a policy for $\user$. This step can be realized in multiple ways -- the policy
may be assigned based on interaction or there may be a public information what
policies are assigned to which set of actions and which type of users. To confirm
that the user is allowed to perform the required set of actions the policy assigner
picks a predicate $\alpolicy$ which has to be fulfilled by the user's attribute list
$\al$. That is, we require $\alpolicy (\al)$ to hold.  To assure that $\al$ remains
private a zero-knowledge proof is used to show that predicate. Importantly, $\polas$
also checks that $\al$ is the same list of attributes that was signed by the identity
provider. Eventually, the policy assigner picks a compliance policy $\comppolicy$ and
sends it to $\user$ along with its signature $\signature_{comp}$ which certifies
authenticity of the policy, i.e.~assures that no malicious user can pick its own
policy $\comppolicy'$ and use it instead of the assigned $\comppolicy$.

If the user wants to use the system in multiple ways \hl{...}
\michals{28.10}{We started a discussion on that. We considered two options
  here. Either the user gets multiple identities and single policy per identity or we
  allow only one identity per user and multiple policies. AFAIR, we were leaning
  towards the latter option. However, now I think that maybe the first option is
  slightly better. It allows to revoke more user's accounts if it misbehaves. That
  is, by default we revoke all accounts per identity. If the user has multiple
  identities then we cannot revoke all its accounts. Obviously (?) the user can set up
  multiple identities with multiple identity providers. (Maybe there is a way to
  prevent that, like each of the identity provider could hold a register of
  credentials hashes $h$ of registered users. Then we could use MPC or PIR (private
  information retrieval) methods to allow identity providers to privately query other
  IPs' databases to check whether a concrete hash $h$ was registered there). Another
  argument for the multiple policies per single identity is more philosophical
  one. The user wants to get multiple policies, so we should allow that by changing
  PA specification. Getting multiple policies by getting multiple identities seems
  like unnecessarily complication. OTOH, if the user wants to perform different
  activity then a different attribute list may be required -- these things are
  verified by the identity provider. In that case having multiple identities per user
makes sense.}

\paragraph{Creating new accounts.} Given identity and policy, the user can create
accounts that will be used to send and receive transactions. $\user$ starts by
threshold-encrypting its public credentials $\pcred$ and computes the account
identifier by running a PRF with a key $\key$ on index $x$. Index $x$ numerates the
accounts created by the user, it takes values from $1$ to $\maxacc$, where the latter
is the upperbound for a number of accounts the user can make. Then the user computes
a policy digest $\policydig$ which assures that the compliance policy tied with the
account is the same as the compliance policy the user got from the policy
assigner without revealing the policy itself. Eventually, the user
computes zero-knowledge proof to certify that
\begin{inparaenum}[(1)]
\item the above computation has been done correctly;
\item it knows a valid $\scred$ corresponding to $\pcred$;
\item has a valid signature from the identity provider that assures validity of
  attribute list $\al$;
\item it has a valid compliance policy assigned by a policy assigner.
\end{inparaenum}

Importantly, the zero-knowledge proof the user is showing assures that it in fact got
the compliance policy from the policy assigner and the identity from the identity
provider. That is, it excludes the attack where a malicious user $\user^*$ obtains an
identity from the identity provider, but then gets a compliance policy from another
user $\user$ (or vice versa) and for such policy creates a new account. Such attack
to be successful requires $\user^*$ to know $\user$'s secret key $\scred$ and the
signature it got from its identity provider. (If $\user^*$ knew $\user$'s signature
from the identity provider then it could impersonate $\user$.)


\paragraph{Sending transactions.} Eventually, the user is allowed to send
transactions. To that end, $\user$ computes zero-knowledge proofs which show validity
of the transaction (regarding the rules of the transacting system, e.g.~assuring that
funds used in the transaction were not created out-of-thin-air etc.) and transaction
compliance with the assigned compliance policy.

Proposed system allows users to send non-compliant transactions if they have been
approved by the corresponding policy assigner. Also, to protect privacy of the user,
transactions can be send via a {\pistis{}} relay who is just another system user. In
general, relays can be used whenever user is tasked to publish some information on
blockchain.

\paragraph{Revoking user's accounts.} If misbehaviour of a user $\user$ is detected, its
identity can be revealed and accounts blocked.  Threshold encryption allows
large-enough set of anonymity revokers to decrypt encryptions of user credentials
$\pcred$ and key $\key$. The former allows the identity provider that provided
$\user$ with its identity to reveal information that identifies it. The latter allows
anonymity revokers to mark and block all accounts created by the user. Importantly,
threshold encryption scheme may be set such that no single anonymity revoker may be
allowed to reveal user's identity, what is a desired property since an anonymity
revoker may be corrupted. On the other hand, no particular anonymity revoker is
necessary to decrypt the credentials (that is, it is only required that a big-enough
set of anonymity revokers cooperates), what prevents failure of decryption due to
anononymity revoker unavailability (e.g.~the revoker may be off-line).

\subsection{\pistis{} is a PPCTS}
Here we briefly state how we define the properties required for a PPCTS,
cf.~\cref{sec:desired_properties}, for \pistis{} and argue that they are
fulfilled.

\begin{description}
\item[{Completeness.}] Completeness of \pistis{} holds from the completeness of
  zero-knowledge proof system.

\item[{Soundness.}] Similarly to the above, soundness of \pistis{} relies on
  soundness of the zero-knowledge proof system.

\item[{Efficiency.}] Efficiency of the compliance process is assured by using
  efficient proof systems, in our case -- zkSNARKs, which are efficiently
  provable and verifiable; moreover, the proofs compounds of a constant number
  of elements despite the size of the statement.

\item[{Reliability.}] This property is assured as $\PPCTS$ functionality
  $\func{\PPCTS}$ which $\pistis$ implements does not change its state if the
  provided transaction is non-compliant and the policy assigner does not
  approved it.

\item[{Robustness.}]
  Design of $\pistis$ assures that no non-compliant transaction can be processed
  unless arbitrarily accepted by the policy assigner given that zero-knowledge proof
  systems that $\pistis$ uses are sound. That holds if the proof systems' structured
  reference strings (SRS) were generated honestly. This can be provided by using
  secure multi-party computation (MPC) of the SRS-s, i.e.~computing SRS-s be a set of
  mutually distrusting parties. Depending on the MPC protocols used, it can be
  guaranteed that the SRS-s are computed honestly if at least one of the parties is
  honest.

\item[{Security.}]
  This property is assured as $\pistis$ does not process nor utilize user's secret data
  from Layer 1, like e.g.~a secret key related to a Layer 1 account.
%
  Obviously, knowledge of such key may be necessary to execute $\pistis$. For
  example, if $\pistis$ is a smart contract on Ethereum, the user uses its
  secret key to make EVM state transitions related to executing $\pistis$'s
  commands. However, no system's command takes as input users secret key, nor
  requires its knowledge.

\item[{Adaptability.}]
  $\pistis$ is adaptable and customizable in a number of aspects. First of all,
  $\pistis$ protocol is composed of a number of idealized functionalities, like
  NIZK, threshold encryption scheme, PRF, functionality of secure parameter
  generation. Each of these functionalities may be implented independenly, using
  various cryptographich primitives, etc. Security properties of $\pistis$
  guarantees that the protocol will remain secure as long as each of the
  functionalities' implementations are done securely.
  Furthermore, the $\pistis$ realizes a UC-functionality of PPCTS, hence it can
  be securely composed with other UC functionalities.

  From the practical point of view, $\pistis$ does not rely on functionalities that
  are specific to a single blockchain. Hence, although it was created with EVM-compatible blockchains in mind, it is practically blockchain-oblivious.

  \michals{2.09}{Argument for that point. Pistis is a smart contract and is, to
    an extend, ledger-neutral. However, I am not sure how we can compose it with
  other elements. What would be that elements? Oracles? But then, wouldn't we
  rely security of the system on them? I.e. wouldn't we rely security of the
  system on some external components we don't control?}

\item[{Privacy preservation.}] This is assured since the only things revealed
  during transactions are: transaction $\tx$, which in our case hides such
  elements as transaction's sender, receiver and amount, transaction auxiliary
  data $\paux$ and policy digest $\policydig$. Furthermore, the sole
  fact that the transaction is processed does not mean it follows a compliance
  policy assigned to the sender (as it may be approved by the policy
  assigner). Also the compliance policy is not revealed at all -- the only
  public information about the policy is that some transaction follows it (shown
  using a zero knowledge proof) and its digest which is computed using a
  pseudo-random function.
\end{description}

\section{Cryptographic preliminaries and primitives}\label{crypto-preliminaries:zkps}

\subsection{Notation}
Let $\secpar \in \NN$ be the security parameter. We assume that all algorithms
described receive as an implicit parameter the security parameter written in
unary, $1^{\secpar}$. %All algorithms are modeled as Turing machines.
An efficient algorithm is a probabilistic Turing machine running in polynomial
time, we write $\ppt$ to denote a such algorithms. We denote by $\rand{\adv}$ a
random variable describing randomness tape of algorithm $\adv$. We write
$r \sample \rand{\adv}$ to denote concrete randomness given to $\adv$. Although
we usually do not explicitly describe the randomness a $\ppt$ algorithm $\adv$
is given, we may sometimes do it, in which case we write $\adv(x; r)$, which
should be interpreted as ``algorithm $\adv$ runs on input $x$ and randomness
$r$''.

For distribution families $\family{A} = \smallset{A(\secpar)}_{\secpar \in
\NN}, \family{B} = \smallset{B(\secpar)}_{\secpar \in \NN}$ write $\family{A}
\approx_{\eps(\secpar)} \family{B}$ if the statistical distance between
$\family{A}$ and $\family{B}$ is upper-bounded by $\eps(\secpar)$. We say that
a function $f\colon \NN \to \RR$ is \emph{negligible} if it vanishes faster
than the inverse of any polynomial, i.e. for every $c \in \NN$ there exists an
integer $x'$ such that for all $x > x'$, we have $\abs{f(x)} < 1/x^c$. We write
$\negl[]$ (resp.~$\poly[]$) to denote a negligible (resp.~polynomial) function.
For a string $x$ of length $n$ we write $\length{x} = n$.

We denote by $\REL \in \smallset{0,1}^{\ast} \times \smallset{0,1}^{\ast}$ a
polynomial-time decidable binary relation, which associated NP language is
defined as $\LAN_{\REL} = \smallset{x\ |\ \exists w\ s.t.\ (x,w) \in \REL}$.
Furthermore, we sometimes abuse notation and write $\REL(\inp, \wit) = 0$ if
$(\inp, \wit) \not\in \REL$ and $\REL(\inp, \wit) = 1$ if $(\inp, \wit) \in
\REL$.

% Furthermore, we denote by $P_{\REL} \colon \smallset{0,1}^{\ast} \times
% \smallset{0,1}^{\ast} \to \smallset{0,1}$ the predicate associated to $\REL$
% which takes two binary strings $(x, w)$ as input and returns 1 (i.e.~$\true$)
% if $(x, w) \in \REL$ and 0 (i.e.~$\false$) otherwise \footnote{Informally a
% predicate $P_{\REL}$ defines the set of rules/conditions $(x,w)$ must follow
% for $x$ to be accepted in the language $\LAN_{\REL}$.}.
In what follows, we refer to a \emph{compliance policy}, as a set of
established rules, a financial transaction needs to satisfy and comply with in
order to be deemed acceptable. Formally, the compliance policy $\comppolicy$ is
a predicate which can be evaluated to eiher $0$ ($\false$) or $1$ ($\true$).

For a (finite, abelian, cyclic) group $\GRP$ we denote by $\gnone{1}$ its
generator. We use additive notation, that is,
$\gnone{a} + \gnone{b} = \gnone{a + b}$ and $a \gnone{b}= \gnone{ab}$. Denote by
$\pair: \GRP_1 \times \GRP_2 \to \GRP_T$ a bilinear pairing, that is for
$\gone{a} \in \GRP_1, \gtwo{b} \in \GRP_2, \gtar{ab} \in \GRP_T$ holds
$\pair(\gone{a}, \gtwo{b}) = \gtar{ab}$. Alternatively, we write
$\gone{a} \bullet \gtwo{b} = \gtar{ab}$. We specify algorithm $\ggen$ that given
security parameter $\secparam$ outputs public parameters $\pp$ that compounds of
description of groups $\GRP_1, \GRP_2, \GRP_T$, their generators and bilinear
pairing between them. We assume that $\ggen$ is run once and for all, that is
all of the involved parties, all algorithms, get $\pp$ as input.

We use UC model by Canetti \cite{EPRINT:Canetti00}. In our description of ideal
functionalities, protocols and simulators we sometimes abuse notation and state
that some dataset $\dataset{D}$ contains tuples with party $\party$, or that
party $\party$ is an input to a procedure. In that case, it should be understand
that we do not store, nor pass the whole party $\party$, i.e.~all its tapes and
description, but only its \emph{unique} identifier $\partyid{\party}$.

\subsubsection{Signature scheme}
A digital signature scheme $\SIG$ consists of 3 algorithms $(\kgen, \sig,
\verify)$ such that:
\begin{description}
  \item[$\kgen(\secparam)$:] outputs a keypair, made of a public and a secret
  key $(\pk, \sk)$;
  \item[$\sig(\sk, m)$:] given as input the secret key $\sk$ and message $m$,
  outputs a signature $\signature$;
  \item[$\verify(\pk, \signature, m)$:] verifies whether a signature
  $\signature$ is a valid signature for message $m$ under the key $\pk$.
\end{description}

Furthermore, a signature scheme must be complete and secure (i.e. unforgeable).
\begin{description}
  \item[Completeness.] A valid signature $\signature$ for message $m$ should
  always be accepted by an honest verifier, that is:
  \[
  \condprob{\verify(\pk, \signature, m) = 1}{(\pk, \sk) \sample
  \kgen(\secparam), \signature \sample \sig(\sk, m)} = 1.
  \]
  \item[Existential unforgeability.] It should be intractable for a $\ppt$
  adversary $\adv$ to produce a signature, without knowing the signing key
  $\sk$, on a message that has not been signed yet. More precisely, $\adv$ has
  negligible probability of winning the game described in \cref{fig:euf}.
\end{description}

\begin{figure}
\centering
\fbox{
\procedure{EUF-CMA}
{(\pk, \sk) \sample \kgen(\secparam)\\
(m', \signature') \gets \adv^{\oracleo_{\sk}}(\pk)\\
\pcif \verify(\pk, m', \signature') = 1 \land (m', \signature') \not\in Q \\
\pcind \pcreturn 1\\
\pcreturn 0}} \caption{Existential unforgeability of a signature scheme. Oracle
$\oracleo_\sk$ takes as input messages $m$ and outputs corresponding signatures
$\signature$; pair $(m, \signature)$ is then assigned to list $Q$.}
\label{fig:euf}
\end{figure}

\subsubsection{Zero-knowledge proofs}
A zero knowledge proof system $\proofsystem$ for a family of polynomial-time
decidable binary relations $\RELGEN = \smallset{\REL}$, is a tuple of 4
algorithms $(\kgen, \prover, \verifier, \simulator)$ that has the following
properties.
\begin{description}
\item[Completeness.]  We say that a proof system is \emph{complete} if a proof
  for a true statement produced by an honest prover is always accepted by an
  honest verifier, that is for all $\REL \in \RELGEN$ and
  $(\inp, \wit) \in \REL$
\[
\condprob{\verifier(\REL, \srs, \inp, \zkproof) = 1}{\srs \sample
\kgen(\REL), \zkproof \sample
\prover(\REL, \srs, \inp, \wit)} = 1.
\]

\item[{Zero knowledge.}]
A proof system is \emph{zero-knowledge} if the verifier seeing a proof for a
statement $\inp$ learns nothing besides the veracity of the statement.
Formally, we require that there exists a $\ppt$ simulator $\simulator$ that
equipped with a trapdoor $\td$ for any $\inp \in \LAN_\REL$ provides a
simulated proof that is indistinguishable from a proof output by an honest
user. That is,
\[
\fset{\prover(\REL, \srs, \inp, \wit)}_{(\srs, \td) \sample
\kgen(\REL), (\inp, \wit)} \approx_\eps \fset{\simulator(\REL,
\srs, \td, \inp)}_{(\srs, \td) \sample \kgen(\REL), (\inp, \wit)}.
\]

\item[{Soundness.}]
A proof system is \emph{sound} if a dishonest prover, who tries to convince a
verifier of the veracity of a false statement, has negligible chances to
succeed. That is, for all $\REL \in \RELGEN$ and all $\ppt$ adversaries $\adv$
\[
\condprob{\verifier(\REL, \srs, \inp, \zkproof) = 1}{(\srs, \td) \sample
\kgen(\REL), (\inp, \wit, \zkproof) \sample \adv(\REL, \srs), \inp
\not\in \LAN_\REL} \leq \negl.
\]

\item[{Knowledge soundness.}]
In some cases we require from the proof system to be \emph{knowledge sound}.
Intuitively, knowledge soundness holds when a $\ppt$ is able to produce a valid
proof for a statement only when it knows the statement's witness. More
precisely, for any $\ppt$ adversary $\adv$ there exists a $\ppt$ extractor
$\ext_\adv$ such that
\[
\Pr
\left[
\begin{aligned}
& \verifier(\REL, \srs, \inp, \zkproof) = 1 \\
&  \land \REL(\inp, \wit) \neq 1
\end{aligned}
\,\left |\,
\begin{aligned}
& (\srs, \td) \sample \kgen(\REL), {r \sample \rand{\adv}} \\
& (\inp, \wit, \zkproof) \sample
\adv(\REL, \srs; r), \wit \gets \ext_\adv(\REL, \srs, r)
\end{aligned}
\right. \right] \leq \negl.
\]

\item[{Simulation extractability.}]
Unfortunately, knowledge soundness is often not sufficient to prevent attacks
in real-life applications (e.g.~a knowledge-sound proof system does not assure
that a malicious user cannot get a valid proof from an honest prover, maul it,
and present this mauled proof as their own). Simulation extractability is a
stronger notion that prevents such attacks. Formally, a proof system is
simulation extractable if for any $\ppt$ adversary $\adv$ there exists a $\ppt$
extractor $\ext_\adv$ such that
\[
\Pr
\left[
\begin{aligned}
& \verifier(\REL, \srs, \inp, \zkproof) = 1 \\
& \land \REL(\inp, \wit) \neq 1
\end{aligned}
\,\left | \,
\begin{aligned}
& (\srs, \td) \sample \kgen(\REL), (\inp, \wit, \zkproof) \sample
\adv^{\oracleo}(\REL, \srs; r), \\
& (\inp, \zkproof) \not\in Q, \wit \gets \ext_\adv(\REL, \srs, r)
\end{aligned}
\right.
\right]
\leq \negl
\]
where, $\oracleo$ on $\adv$'s input $\inp$ responds with a simulated proof
$\zkproof$ for $\inp$; $Q$ is a list of all instances $\inp$ submitted by $\adv$
along with the oracle's responses $\zkproof$.
\end{description}

We call a proof system \emph{universal} if $\kgen$ depends only on the security
parameter $\secpar$, not the concrete relation $\REL$ itself. That is, a single
SRS $\srs$ can be used for all relations $\REL \in \RELGEN$ of a given
size. For the sake of efficiency, a universal proof system may have specified
additional SRS generating algorithm $\kgens$ which takes $\srs$ output by
$\kgen$ and produces a specialized SRS $\srss$ that allows both the prover and
verifier to make and verify proofs more efficiently.

\begin{remark}[On transaprent NIZKs]
We note that the definitions above focus on SRS-based NIZKs, however other
approaches are possible. For example, one could use so-called transparent
zero-knowledge proof systems which are made non-interactive in the
random-oracle model~\cite{CCS:BelRog93} via the Fiat--Shamir
transformation~\cite{C:FiaSha86}. In that case, the $\kgen$ algorithm may just
return an empty string. Also, in that case, the simulator does not learn the
trapdoor corresponding to the SRS. Zero-knowledge of Fiat--Shamir based NIZKs
relies on programmability of the random oracle. More precisely, the simulator
is able to program the oracle to return $y$, picked by $\simulator$, when it is
given $x$.

It is argued sometimes that random oracle-based NIZKs can be instantiated using
a hash function. Such statements have to be taken with a pinch of salt as zero
knowledge requires either the hash function programmability or use of much less
efficient transformations than Fiat--Shamir's.
\end{remark}

\subsubsection{Threshold encryption scheme}

We give the definition of the threshold encryption scheme following
\cite{EPRINT:DGKOS20}.

%\begin{definition}
A $(\threshold, \noofparties)$-threshold encryption scheme $\TENC = (\kgen,
\enc, \dec, \combine)$ over a message space $M$ compounds the following
algorithms:
\begin{description}
  \item[$\kgen(\secparam)$:] takes security parameter and returns a pair of a
  public and secret keys $(\pk, \sk)$.
  \item[$\enc(\vec{\pk}, m)$:] encrypts message $m \in M$ using a vector of
  public keys $\vec{\pk} = (\pk_i)_{i \in \range{1}{\noofparties}}$, such that
  any $(\threshold + 1)$-sized set of $\pk_i$ owners should be able to decrypt
  it. Denote by $\ciphertext_i$ the share of $m$ encrypted using $\pk_i$.
  \item[$\dec(\sk_i, \ciphertext_i)$:] A party who knows a secret key $\sk_i$
  corresponding to a public $\pk_i$ decrypts $\ciphertext_i$ and publishes the
  decrypted share $\varshare_i$.
  \item[$ \combine(\vec{\pk}, \ciphertext, \smallset{\varshare_i}_{i \in I'})$:]
  Takes a subset $I' \subset \smallset{1, \ldots, \noofparties}$ of size at
  least $\threshold + 1$ and outputs either a message $m$ or $\bot$.
\end{description}
%\end{definition}

We further define below the notion of a secret sharing scheme.
%
%\begin{definition}[Secret sharing scheme]
A $(\threshold, \noofparties)$-secret sharing scheme $\SS$ is made of the
following algorithms
\begin{description}
  \item[$\share_{\threshold, \noofparties}(m)$:] Which on input a secret
  message $m$ produces $\noofparties$ shares $\vec{\varshare} = (\varshare_1,
  \ldots, \varshare_\noofparties)$ such that for any subset $I \subset
  \smallset{1, \ldots, \noofparties}$ of size at least $\threshold + 1$ is able
  to reconstruct $m$ from $\smallset{\varshare_i}_{i \in I}$. Importantly, $m$
  remains random even when a subset of shares of size smaller than $\threshold
  + 1$ is known.
  \item[$\reconstruct_{\threshold, \noofparties}(\smallset{\varshare_i}_{i \in
  I'})$:] For $I' \subset \smallset{1, \ldots, \noofparties}$ of size at least
  $\threshold + 1$ it reconstructs the shared message $m$.
\end{description}
%\end{definition}

\paragraph{Share-and-Encrypt paradigm.}
A $(\threshold, \noofparties)$-threshold encryption scheme $\TENC$ can be
instantiated using a public key encryption scheme $\ENC = (\kgen, \enc, \dec)$
and a secret sharing scheme $\SS = (\share_{\threshold, \noofparties},
\reconstruct_{\threshold, \noofparties})$. Let $I = \smallset{1, \ldots,
\noofparties}$, then $\TENC$ can be instantiated as follows:
\begin{description}
  \item[$\TENC.\kgen(\secparam)$:] For each $i \in I$ return $(\pk_i, \sk_i)
  \sample \ENC.\kgen(\secparam)$.
  \item[$\TENC.\enc(\vec{\pk}, m)$:] Compute $\vec{\varshare} \sample
  \SS.\share(\threshold, \noofparties, m)$ and $\ciphertext_i \sample
  \ENC.\enc(\pk_i, \varshare_i)$. Send $\ciphertext_i$ to party $i$.
  \item[$\TENC.\dec(\sk_i, \ciphertext_i)$:] Decrypt and publish the share
  $\varshare_i \gets \ENC.\dec(\sk_i, \ciphertext_i)$.
  \item[$\TENC.\combine(\vec{\pk}, \smallset{\ciphertext_i}_{i \in I},
  \smallset{\varshare_i}_{i \in I'}):$] For a set $I' \subset I$ of size at
  least $\threshold + 1$ combine the decrypted shares by running $m \gets
  \SS.\reconstruct_{\threshold, \noofparties}(\smallset{\varshare_i}_{i \in
  I'})$.
\end{description}

We additionaly require that the threshold encryption scheme we use is
\emph{partialy decryption simulatable}~\cite{EPRINT:DGKOS20}. More precisely, a
  $(\threshold, \noofparties)$ threshold encryption scheme is
  $(\threshold, \noofparties)$-partial decryption simulatable if there exists an
  efficient algorithm $\simpart$ such that for all $\ppt$ adversaries $\adv$
  \[
    \abs{\prob{\ngame{\adv}{pds}(\secpar, \threshold, \noofparties) = 1}  -
      \frac{1}{2}} \leq \negl,
  \]
  for $\ngame{\adv}{pds}(\secpar, \threshold, \noofparties)$ as defined at
  \cref{fig:game_pds}.
%\end{definition}

\begin{figure}
   \centering
   \fbox{\procedure{$\ngame{\adv}{pds}(\secpar, \threshold, \noofparties)$}{C
       \gets \adv(\secpar, \threshold, \noofparties) \\
       \pcfor i \in \range{1}{\noofparties}\\
       \pcind (\sk_i, \pk_i) \sample \kgen(\secparam)\\
       (R, m_0, m_1) \gets \adv(\smallset{\pk_i}_{i \in [\noofparties]},
       \smallset{\sk_i}_{i \in C})\\
       b \sample \bin\\
       c_0 \sample \enc(\vec{\pk}_R, m_0)\\
       c_1 \sample \enc(\vec{\pk}_R, m_1)\\
       \pcif b = 0 \pcthen\\
       \pcind \pcfor i \in R \setminus C\\
       \pcind \pcind \mu_i \gets \dec(\vec{\sk}_R, c_0) \\
       \pcelse\\
       \pcind \pcfor i \in R \cap C  \\
       \pcind \pcind \mu_i \gets \dec(\vec{\sk}_R, c_1) \\
       \pcind \pcfor i \in R \setminus C\\
       \pcind \pcind \mu_i \gets \simpart(\threshold, \noofparties,
       \vec{\pk}_R, c_0, \smallset{\mu_j}_{j \in \in R \cap C}, m_0)\\
       b' \gets \adv(c_b, \smallset{\mu_j}_{j \in R \setminus C})\\
       \pcif b = b' \land \abs{m_0} = \abs{m_1} \land \abs{R \cap C} \leq
       \threshold \land R \subset [\noofparties] \land C \subset [\noofparties]
       \\
       \pcthen \pcreturn 1 \pcelse \pcreturn 0}}
  \caption{Partial decryption simulatability game}
  \label{fig:game_pds}
\end{figure}

\subsubsection{Pseudorandom functions}

%\begin{definition}[$\prf$ function family]
\newcommand{\pcfamilystyle}[1]{\mathcal{#1}} \newcommand{\cF}{\pcfamilystyle{F}}
A function family $\prf = \smallset{\prf_k: A \to B}_{k \in K}$ is called
\emph{pseudorandom} if for a set of keys $K \in \bin^{\secpar}$, function $h$
randomly picked from all functions mapping $A$ to $B$, any $\ppt$ adversary
$\adv$ holds
\[
\abs{\condprob{\adv^{\prf_k}(\secparam) = 1}{k \sample K} -
\condprob{\adv^{h}(\secparam) = 1}{k \sample
K}} \leq \negl.
\]
%\end{definition}

Additionally, in our case we follow \cite{EPRINT:DGKOS20} and require from the
$\prf$ that it is \emph{weakly robust}. That is, no $\ppt$ adversary $\adv$,
given should be able to come with a key $\key^*$ and function input $x^*$ that
collides with some other function. More precisely, we call a $\prf$ \emph{weakly robust} if
\[
\condprob{\exists (x, y) \in Q, \prf_{\key^*} (x^*) = y}{\key \sample K, (x^*, \key^*) \gets
\adv^{\prf_\key}} \leq \negl,
\]
where $Q$ is a list of all queries and their responses send by the adversary to
$\prf_\key$.
%\end{definition}

\section{The protocol}
\subsection{Primitives' instantiations}
\paragraph{Zero-knowledge proof systems}
\michals{27.08}{Which zkSNARK?}

The choice of zkSNARK used to prove relations is of great importance for efficiency
of the system and should be done separately for each system instantiation after
considering how the system is supposed to be used. The main trade-off here is between
using a universal on non-universal zkSNARK. The latter, like \cite{EC:Groth16} is
more efficient, but requires a separate SRS for each of the proven relation. This is
especially troublesome if one desires the compliance policy relation $\REL_{comp}$ or
attribute list relation $\REL_{al}$ to be universal relations, i.e.~a single
relations that may be used to prove virtually any statement, for any compliance
policy or attribute list predicate. However, if one designs a system that has a
single compliance policy and single attribute list policy, then use of a more
flexible proof system is not necessary.

However, when a more general and customizable system is required, one may greatly
benefit if it chooses a universal proof system like, e.g.
Plonk~\cite{EPRINT:GabWilCio19}, Sonic~\cite{CCS:MBKM19}, Marlin~\cite{EC:CHMMVW20},
Lunar~\cite{EPRINT:CFFQR20}, Basilisk~\cite{C:RafZap21}. Although less efficient than
\cite{EC:Groth16}, each of these systems allows to have a single universal SRS for
\emph{all} relations (however, efficiently proving or verifying a proof requires a
specialized SRS which can be computed from the universal SRS by each of the parties
separately), which reduces greatly the number of required reference strings.

\michals{27.08}{Give description of the proof system -- here or in the appendix}
\begin{description}
\item[$\REL_{val}$] which takes $((\tx, \paux_{tx}), (\saux_{tx}))$ and returns
  $1$ if the transaction $\tx$ is valid from the transacting system point of
  view.
\item[$\REL_{comp}$] which verifies that the transaction submitted by the user
  complies with the compliance policy it got assigned \textbf{or} the user
  knows a policy assigner's signature on the transaction. More precisely,
  \[
    \REL_{comp} = \left\{
      \begin{aligned}
        & ((\tx, \paux_{tx}, \pk_{\polas}, \policydig), \\
        & (\comppolicy, \signature_{comp}, \signature_{tx}, \key, r))
      \end{aligned}
      \,\left|\,
        \begin{aligned}
%          & \ldots \\
          & \policydig = \tprf_{\key}(\comppolicy, \signature_{comp}, r),
          \SIG.\verify(\pk_{\polas}, \signature_{comp}, \comppolicy) = 1\\
          & \comppolicy(\tx, \paux_{tx}) = 1
          \lor \SIG.\verify(\pk_{\polas}, \signature_{tx}, (\tx, \paux)) = 1
        \end{aligned}
      \right.  \right\}
  \]
\item[$\REL_{acc}$] which pair of public and secret key $(\pk_{acc},
  \sk_{acc})$ associated with the account has to fulfil. The relation highly
  depends on the ledger. Intuitively, the secret key should allow user to sign
  and send transactions, while the public key should allow others to verify
  signatures and transactions send by the user.
\item[$\REL_{newacc}$] which verifies that the account has been created using
  correct user's secrets and the party which creates the account has
  correctly assigned identity and policy. More precisely,
  \[
    \REL_{newacc} = \left\{
      \begin{aligned}
        &((\cuser, \aux_{acc}, \idprov, \pk_{acc}, \pk_{\polas}, \pk_{\idprov},
        \policydig, \vec{\pk_{\ar}}), \\
        & (\signature_{id}, r_{tenc}, \pcred, \scred, \key, \\
        &\sk_{acc}, \comppolicy, \signature_{comp}, r_{pd}, \AL, x, \alpolicy, \signature_{al}))
      \end{aligned}
      \, \left| \,
        \begin{aligned}
          & \BSIG.\verify(\pk_\idprov, \signature_{id}, (\scred, \key, \AL)) =
          1
          \\
          & \aux_{acc} = \prf_{\key}(x), \text{ for some } x \in
          \range{1}{\maxacc}\\
          & \cuser = \TENC.\enc((\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}),
          \pcred; r_{tenc}),\\
          & \REL_{acc}(\pk_{acc}, \sk_{acc}) = 1,  \REL_{user}(\pcred, \scred) = 1, \\
   %       & \pccom{\text{check correctness of the  policy digest}}\\
          &  \policydig = \tprf_{\key}(\comppolicy, \signature_{comp}, r_{pd}),\\
          &  \SIG.\verify(\pk_{\polas}, \signature_{comp}, (\comppolicy, \pcred)) = 1, \\
          & \SIG.\verify(\pk_\polas, \signature_{al}, (\alpolicy, \pcred)) = 1, \alpolicy (\al) = 1
        \end{aligned}
        \right.\right\}.
    \]
\item[$\REL_{user}$] which public and secret credentials of the user have to
  fulfil. That is,
  \(
    \REL_{user} = \left\{
      (\pcred, \scred)
    \right\}
\) Following \cite{EPRINT:DGKOS20} we require that $\REL_{user}$ is a hard relation.
\item[$\REL_{sign}$] that user's signature has to fulfil, more precisely
  \[
    \REL_{sign} = \left\{
      \begin{aligned}
        & (\pk_\user, \pk_{\idprov}, \vec{\pk_\ar}, \signature_1, c, \AL, \pp),\\
        & (\sk_\user, \key, r', r)
      \end{aligned}
      \,\left|\,
        \begin{aligned}
          & \REL_{user}(\pk_\user, \sk_\user) = 1 \\
          & \signature_1 = \prepsign(\pk_\idprov, (\sk_\user, \key, \AL), r')\\
          & c = \TENC.\enc(\vec{\pk_\ar}, \key; r)
        \end{aligned}
      \right.\right\}
  \]
  \item[$\REL_{al}$] which shows that user's attribute list $\AL$ satisfies predicate
    $\alpolicy$ requested by policy assigner $\polas$ before the compliance policy
    can be assigned, that is
    \[
      \REL_{al} = \left\{
        \begin{aligned}
          & (\pAL, \pk_\idprov, \pcred, c, \pk_{polas}),\\
          & (\sAL, \signature_{id}, \scred, \key, \alpolicy)
        \end{aligned}
         \,\left|\,
          \begin{aligned}
            & (\pAL, \sAL) \gets \AL, \alpolicy (\AL) = 1,             \\
            & \BSIG.\verify (\pk_{id}, \signature_{id}, (\scred, \key, \AL)) =
            1, \\
            & \REL_{user} (\pcred, \scred) = 1, c = \enc(\pk_{polas}, \alpolicy)
        \end{aligned}
          \right.
        \right\}
      \]
    \item[$\REL_{sig}, \REL_{bsig}, \REL_{enc}, \REL_{tenc}$] which determine
      relations between public and secret key of a signature scheme $\SIG$, blind
      signature scheme $\BSIG$, encryption scheme $\ENC$ and threshold encryption
      scheme $\TENC$.
  \end{description}

  \begin{remark}[Combining statements]
    We note that some of the relations above could be combined and proven 
    together for the sake of efficiency.
  \end{remark}

  \begin{remark}[On universal relations]
    Depending on application, relations $\REL_{al}$ and $\REL_{comp}$ may be
    universal -- each of them may be used to show any $\npol$ relation. However, they
    are used to show specific relations -- $\alpolicy, \comppolicy$ that are
    accounted for when the proven instance is set. That is, for $\REL_{al}$ proven
    relation $\alpolicy$ is set as a part of the instance. For $\REL_{comp}$ the
    relation $\comppolicy$ remains hidden (as it is private) but the $\REL_{comp}$
    instance contains uniquely determined $\comppolicy$'s, so called, policy digest
    $\policydig$.
  \end{remark}

  \subsubsection{Threshold encryption scheme}
  Following \cite{EPRINT:DGKOS20} we build the threshold encryption scheme using a
  Shamir's secret sharing scheme with a CLT \cite{AC:CasLagTuc18} encryption
  scheme. The latter relies on a so-called CL framework \cite{RSA:CasLag15} which
  composes of two algorithms $\sgen$ and $\solve$ defined as follows\footnote{Both CL
    framework and CLT encryption scheme definitions were taken from \cite{EPRINT:DGKOS20}}:
  \begin{description}
  \item[$\sgen (\secparam, q)$:]
    \begin{enumerate}
    \item Take a security parameter $\secpar$
    and prime $q$ and produce the following:
    \begin{description}
    \item [$\hGGG$]  a finite abelian group of order $\hat{n} \gets q \cdot
      \hat{s}$. The bitsize of $\hat{s}$ is a function of $\secpar$, $\gcd (q,
      \hat{s}) = 1$. It is required that valid encodings of elements in $\hGGG$ can
      efficiently be recognized.
    \item [$\GGG$]  a cyclic subgroup of $\hGGG$ of order $n \gets q \cdot s$ where
      $s$ divides $\hat{s}$.
    \item [$\HHH$]  the unique cyclic group of order $q$ generated by $\hgenerator$.
    \item [$\GGG^q$]  the subgroup of $\GGG$ of order $s$. Since $\HHH \subset \GGG$,
      it holds that $\GGG \simeq \GGG^q \times \HHH$.
    \item [$\tilde{s}$]  an upper bound for $\hat{s}$.
    \item [$\ggenerator, \hgenerator, \ggenerator_q$]  generators of $\GGG, \HHH,
      \hGGG$, $\ggenerator \gets \hgenerator + \ggenerator_q$.
    \end{description}
    \item Return $\pp \gets (\hGGG, \GGG, \HHH, \tilde{s}, \ggenerator, \hgenerator, \ggenerator_q)$. 
  \end{enumerate}
\item[$\solve (q, \pp, X)$:] Solves discrete logarithm problem in $\HHH$.
  \end{description}

  Finally the encryption scheme is defined as follows. \michals{10.1}{I skip for now description of SSS as it is
    very standard but describing it takes time}
  \begin{description}
  \item[$\sgen (\secparam, 1^\mu):$]
    \begin{enumerate}
    \item sample a $\mu$-bit prime $q$;
    \item $\pp \sample \ggen (\secparam, q)$; 
    \item return $\pp$;
    \end{enumerate}
  \item[$\kgen (\pp)$:]
    \begin{enumerate}
    \item sample $\alpha \sample \mathcal{D}_q$, $y \sample \alpha \cdot \ggenerator_q$;
    \item set $\pk \gets y$, $\sk \gets \alpha$;
    \item return $(\pk, \sk)$;
    \end{enumerate}
  \item[$\enc (\pk, m)$:]
    \begin{enumerate}
    \item sample $r \sample \mathcal{D}_q$;
    \item return $(r \cdot \ggenerator_q, m \cdot \hgenerator + r \cdot y)$;
    \end{enumerate}
  \item[$\dec (\sk, (\grpelement{c}_1, \grpelement{c}_2)$:]
    \begin{enumerate}
    \item compute $\grpelement{m} \gets \grpelement{c}_2 - \alpha \cdot \grpelement{c}_1$;
    \item return $\solve(q, \pp, \grpelement{m})$;
    \end{enumerate}
  \end{description}

  Here $\mathcal{D}_q$ is a distribution that is $\negl$-close (in terms of
  statistical distance) to the uniform distribution over elements of $\GGG^q$.

\subsubsection{(Blind) signature scheme}

Similarly to \cite{EPRINT:DGKOS20} we use Poincheval-Sanders
\cite{RSA:PoiSan16} signature scheme as a blind signature scheme. We also use
it when a standard signature scheme is required.
\begin{description}
  \item[$\sgen(\secparam)$:] Sample $\pp := (p, \GRP_1, \GRP_2, \GRP_T, \pair,
    \gone{1}, \gtwo{1})$.
  \item[$\kgen(\pp)$:] Given $\pp$
    \begin{enumerate}
    \item For $i \in \range{1}{\ell}$, sample $x, y_i \sample \FF_p$.
    \item Compute $\gone{x}, \gtwo{x}, \gone{y_i}, \gtwo{y_i}$ for $i \in
    \range{1}{\ell}$.
    \item Output $\pk = \gone{x}, \gtwo{x}, \smallset{\gone{y_i},
      \gtwo{y_i}}_{i \in \range{1}{\ell}}$ and $\sk = \gone{x}$.
    \end{enumerate}
  \item[$\prepsign(\pk , m = (m_1, \ldots, m_\ell))$:]
    \begin{enumerate}
    \item Sample $r \sample \FF_p$.
    \item Compute $\signature_1 = \gone{r} + \sum_{i = 1}^{\ell} m_i
    \gone{y_i}$
    \end{enumerate}
  \item[$\blindsign(\sk, \signature_1)$:]
    \begin{enumerate}
    \item Sample $\alpha \sample \FF_p$,
    \item Output $\signature_2 = (\gone{\alpha}, \alpha \cdot \gone{x +
    \signature_1})$.
    \end{enumerate}
  \item[$\unblind(\signature_2, r)$:]
    \begin{enumerate}
    \item Parse $\signature_1$ as $\grp{a}, \grp{b}$ and compute $\signature' =
      (\grp{a}, \grp{b} - r \cdot \grp{a})$.
    \item Randomize $\signature'$ by choosing $r' \sample \FF_p$ and computing
      $\signature = r' \signature'$.
    \item Return $\signature$.
    \end{enumerate}
  \item[$\verify(\pk, m = (m_1, \ldots, m_\ell), \signature)$:]
    \begin{enumerate}
    \item Parse signature $\signature$ as $(\signature_1, \signature_2)$.
    \item Output $1$ if:
      \begin{itemize}
      \item $\signature_1 \neq \gone{1}$, and
      \item $\signature_1 \bullet \gtwo{x} + \sum_{j = 1}^{\ell}\gtwo{y_j} =
        \signature_2 \bullet \gtwo{1}$.
      \end{itemize}
    \end{enumerate}
\end{description}

\subsubsection{Pseudorandom function}
In our scheme we use two pseudorandom functions, which we denote $\prf$ and
$\tprf$.  First, similarly to \cite{EPRINT:DGKOS20}, we use Dodis-Yampolskiy
\cite{PKC:DodYam05} PRF. More precisely, let $\gone{1}$ be generator of an
order-$p$ group $\GRP_1$. On input $x$ and key $\key \sample \FF_p$, $\prf =
\gone{\frac{1}{\key + x}}$.

Security of this function holds only for small domains, that is however enough
as the maximum number of accounts the user can set up is bounded by $\maxacc$.
The function is also weakly robust.
% \michals{12.08}{Need to check  -- DY PRF is secure for polynomially many
%   inputs. Is it a case here? I.e. we not only pass to the PRF the account
%   number (as in Damgard et al) but also $\pcred$ which may take exponentially
%   many arugments. Probably we could just use some hash function (assuming it
%   is a PRF) instead.}

Second, we use as $\tprf$ a hash function $\hash$ assuming it is a weakly
robust PRF. Note that we cannot use Dodis-Yampolskiy's PRF here as it is secure
only against small domains, what is not the case for $\tprf$. We propose to use
here MiMC \cite{AC:AGRRT16} hash function as it combines well with (most)
zkSNARKs. (That is, proving statements regarding MiMC is usually much more
efficient -- for the prover -- than showing statements for, say, SHA3.)

\subsubsection{Data objects}
Following \cite{EPRINT:DGKOS20} we define the following data objects held by
the system users:

\begin{description}
\item[User certificate ($\uc$)] After registration at an identity provider the
  user gets a certificate containing
  \begin{itemize}
  \item Public and secret identity credentials $\pcred$ and $\scred$;
  \item PRF key $\key$;
  \item Attribute list $\AL$; we note the public and secret part of the attribute
    list by $\pAL$ and $\sAL$ respectively. Importantly, it may hold that
    $\pAL = \emptyset$;
  \item Identity provider's signature on $(\scred, \key, \AL)$.
  \end{itemize}
\item[Account creation information ($\aci$)] The user equipped with an identity
  from the identity provider and $\uc$ can create new accounts. The
  corresponding data object $\aci$ is posted on the ledger and contains:
  \begin{itemize}
  \item $\auxacc$, the (unique) account registration ID;
  \item $\cuser$, the threshold encryption of public credentials $\pcred$;
  \item Identifier $\idprov$ of the identity provider who provided the user
    with the identity;
  \item Account public key $\pk_{acc}$;
  \item $\zkproof$, a zero-knowledge proof that certifies that the account has
    been created by an authorized user.
  \end{itemize}
\item[Identity Provider's Information on User ($\ipiu$)] which is a data stored
  by the identity provider after granting identity to a user. The data set
  contains:
  \begin{itemize}
  \item Identifier $\user$ of the user and its public credentials $\pcred$;
  \item Set of the anonymity revokers who keeps encryption of the user's PRF
    key $\ckey$.
  \end{itemize}
\end{description}
Additionally, since our protocol also allows users to append transactions to
the ledger, we specify the following data object:
\begin{description}
\item[Transaction data ($\txdata$)] which contains all transaction-related
  information that are to be posted on the ledger. That is,
  \begin{itemize}
  \item transaction description $\tx$, \antoines{23.08}{What's that? If we have
  the originator and ``public tx data'' in the field below, what do we have in
  the ``tx description''? In practical terms, do you mean the ``gasPrice'' and
  other fields making up the tx object? If we don't want to get down the
  ``implementation level'', I find this bullet confusing here as its intent is
  not very clear. Not clear how that relates to the other fields mentioned
  below.}
  \item auxiliary public transaction data $\paux_{tx}$,
%  \item transaction sender account identifier $\auxacc$,
  \item transaction originator policy assigner's $\polas$ public key $\pk_\polas$ and a compliance policy
    digest $\policydig$,
  \item zero-knowledge proofs for transaction validity and transaction
  compliance.
\item Account identifier digest $\auxacc$.
  \end{itemize}
\end{description}

\subsection{Functionality and protocol for $\PPCTS$}

\begin{funcbox}{Application functionality $\func{\PPCTS}$} We identify the
  following parties: identity providers $\partyset{I} = \smallset{\idprov_1,
  \ldots, \idprov_\noofidprov}$, anonymity revokers $\partyset{AR} =
  \smallset{\ar_1, \ldots, \ar_\noofar}$, users $\partyset{U} =
  \smallset{\user_1, \ldots, \user_\noofu}$, application owner $\owner$, relays
  $\partyset{R} = \smallset{\relay_1, \ldots, \relay_\noofr}$, $\partyset{R}
  \subseteq \partyset{U}$, and policy assigners $\partyset{PA} =
  \smallset{\polas_1, \ldots, \polas_\noofpolas}$.  The functionality is
  parameterized by
  \begin{itemize}
  \item values $\noofar, \noofidprov, \noofpolas$ and threshold $\thresholdar$;
  \item relation $\RELacc$ that an account private key-public key pair has to
    fulfill;
  \item relation $\RELval$ that a transaction has to fulfill to be considered
    valid according to the rules of the transacting system;
  \item maximal number of accounts $\maxacc$ a user can open.
  \end{itemize}
  Flag $\ready$ is initially set to $\false$.

  \paragraph{Initialization}
  On $(\initialize)$ from a party $\party \in \partyset{I} \cup \partyset{AR}
  \cup \partyset{PA} \cup \owner \cup \partyset{R}$ output to $\adv$
  $(\initialized, \party)$. When all parties are initialized set flag $\ready =
  \true$.

  \paragraph{Identity issuance}
  On $(\issueIdentity, \idprov, \AL)$ from user $\user$, and $(\issueIdentity,
  \user)$ from $\idprov$:
  \begin{itemize}
  \item if $\ready = \false$, ignore;
  \item if there is already stored $(\issuedIdentity, \user, \idprov, \auxid)$
    then ignore; else send $(\issueIdentity)$ (or $(\issueIdentity, \user,
    \idprov, \AL)$ if $\idprov$ is corrupted) to $\adv$.
  \item Upon receiving $(\issueIdentity, \auxid)$ from $\adv$: if there already
    is stored tuple $(\identityIssued, \relay, \idprov', \aux'_{id})$ for
    $\aux'_{id} = \auxid$; or $\auxid = \bot$, then abort; otherwise, store
    $(\identityIssued, \user, \idprov, \auxid)$.
  \item Output $(\identityIssued, \auxid)$ to $\adv$.
  \end{itemize}

  \paragraph{Attribute check}
  On $(\checkAttributes, \polas)$ from the user and $(\checkAttributes, \user, \alpolicy)$
  from the policy assigner
  \begin{itemize}
  \item if $\ready = \false$, ignore;
  \item if there is no $(\issuedIdentity, \user, \cdot, \cdot)$ stored, then ignore;
  \item if $\alpolicy (\AL) = 0$ then return to user, policy assigner, and the
    adversary $(\attributesNotValid)$ and exit
  \item else send to the adversary $(\attributesValid)$ and to the user
    $(\attributesValid, \alpolicy)$
  \item store $(\attributesValid, \user, \alpolicy)$.
  \end{itemize}
  
  \paragraph{Policy issuance}
  On $(\issuePolicy, \polas, \AL)$ from user $\user$, and $(\issuePolicy,
  \user, \alpolicy, \comppolicy)$ from $\polas$:
  \begin{itemize}
  \item if there is no $(\attributesValid, \user, \alpolicy)$ then ignore; else 
  \item if there is already stored
    $(\policyAssigned, \user, \polas, \comppolicy, \ldots)$ then ignore; else
    send $(\issuePolicy, \polas)$  to $\adv$.
  \item Store $(\policyAssigned, \user, \polas, \alpolicy, \comppolicy)$;
    if $\polas$ or $\user$ is corrupted, send
    $(\policyAssigned, \pcred, \AL, \user, \polas, \allowbreak \alpolicy,
    \comppolicy)$ to $\adv$.
  \end{itemize}

\paragraph{Account creation}
  On $(\createAccount, \auxid, \polas, \pkacc, \skacc)$ from
  user $\user$
  \begin{itemize}
  \item If $\ready = \false$ or $\RELacc (\pkacc, \skacc) \neq 1$ ignore.
  \end{itemize}
  Else,
  \begin{itemize}
  \item If $\auxid = \bot$, then abort, else read $(\identityIssued, \user,
    \idprov, \auxid, \polas)$ and abort if there is no such entry;
  \item Check whether there is $(\policyAssigned, \user, \polas,
      \comppolicy, \alpolicy)$ entry stored, and abort if there is not the case.
  \item Output $(\createAccount, \pkacc, \idprov, \polas)$ to $\adv$;
  \item On $(\createAccount, \auxacc, \policydig)$ from $\adv$, if $\auxacc =
    \bot$, $\policydig = \bot$ or there is already an account with the same
    $\auxacc$ or $\policydig$, then abort, else
    \begin{itemize}
    \item store $(\accountCreated, \polas, \comppolicy, \policydig,
      \auxacc, \pkacc, \skacc)$,
    \item set $\cnt(\auxid) \gets \cnt(\auxid) + 1$,
    \item add $(\auxacc, \policydig, \pkacc, \idprov, \polas)$
      to the buffer and the adversary;
    \end{itemize}
  \item Return $(\accountCreated, \auxacc, \policydig)$ to $\user$.
\end{itemize}
  
  \paragraph{Shielded account creation}
  On $(\createAccountShielded, \auxid, \polas, \pkacc, \skacc,   \relay)$ from
  user $\user$ and $(\createAccountShielded, \pkacc)$ from $\relay$.
  \begin{itemize}
  \item If $\ready = \false$ or $\RELacc (\pkacc, \skacc) \neq 1$ ignore.
  \end{itemize}
  Else,
  \begin{itemize}
  \item If $\auxid = \bot$, then abort, else read $(\identityIssued, \user,
    \idprov, \auxid, \polas)$ and abort if there is no such entry;
  \item Check whether there is $(\policyAssigned, \user, \polas,
      \comppolicy, \alpolicy)$ entry stored, and abort if there is not the case.
  \item Output $(\createAccountShielded, \pkacc, \idprov, \polas)$ to $\adv$;
  \item On $(\createAccountShielded, \auxacc, \policydig)$ from $\adv$, if $\auxacc =
    \bot$, $\policydig = \bot$ or there is already an account with the same
    $\auxacc$ or $\policydig$, then abort, else
    \begin{itemize}
    \item store $(\accountCreated, \polas, \comppolicy, \policydig,
      \auxacc, \pkacc, \skacc)$,
    \item set $\cnt(\auxid) \gets \cnt(\auxid) + 1$,
    \item add $(\auxacc, \policydig, \pkacc, \idprov, \polas, \relay)$
      to the buffer and the adversary;
    \end{itemize}
  \item Return $(\accountCreatedShielded, \auxacc, \policydig)$ to $\user$ and $\relay$.
\end{itemize}

  \paragraph{Account and transaction retrieval}
  On $(\retrieve)$ from a party $\party \in \partyset{U} \cup \partyset{AR}
  \cup \partyset{I} \cup \owner \cup \partyset{PA} \cup \partyset{R}$ output a
  list of all accounts and transactions stored in $\listvar{tx}$.

  \paragraph{Sending transaction} On input $(\sendTransaction,
  \tx, \pauxtx, \sauxtx, \auxacc, \polas, \policydig, \relay)$ from user
  $\user$:
  \begin{itemize}
  \item If there is no $(\accountCreated, \auxid, \polas', \comppolicy,
    \auxpol', \policydig', \auxacc', \skacc', \user)$ such that $\auxacc =
    \auxacc'$, $\skacc = \skacc'$, $\polas = \polas'$, $\auxpol = \auxpol'$ and
    $\policydig = \policydig'$, then abort.
  \item If $\RELval((\tx, \pauxtx), \sauxtx) \neq 1$ then abort
  \item Else read $\comppolicy$ and send $(\sendTransactionBegins, \auxacc,
    (\tx, \pauxtx))$ to $\adv$.
  \item Verify that $\comppolicy(\tx, \pauxtx) = 1$ and if that is not the case, send
    $(\allowTransaction, \tx, \pauxtx)$ to $\polas$ and $\adv$. \pccom{We allow the
      adversary to learn when a user tries to send non-complying transaction.}
    \begin{itemize}
    \item On $(\allowed, \tx, \pauxtx)$ from $\polas$ send $(\allowed)$ to
      $\adv$ and $\user$, then proceed;
    \item On $(\notAllowed, \tx, \pauxtx)$ from $\polas$ send $(\notAllowed)$
      to $\adv$ and $\user$ and exit.
    \end{itemize}
  \item Send $(\sendTransaction, \tx, \pauxtx, \auxacc, \polas, \policydig,
    \relay)$ to $\adv$;
  \item Return ($\transactionSent)$ to $\adv$ and add $(\tx,
    \paux_{tx}, \auxacc, \polas, \policydig)$ to the buffer.
  \end{itemize}

  \paragraph{Shielded sending transaction} On input
  $(\sendTransactionShielded, \tx, \pauxtx, \sauxtx, \auxacc, \polas, \policydig, \relay)$ from
  user $\user$ and $(\sendTransactionShielded, \tx)$ from $\relay$:
  \begin{itemize}
  \item If there is no $(\accountCreated, \auxid, \polas', \comppolicy,
    \auxpol', \policydig', \auxacc', \skacc', \user)$ such that $\auxacc =
    \auxacc'$, $\skacc = \skacc'$, $\polas = \polas'$, $\auxpol = \auxpol'$ and
    $\policydig = \policydig'$, then  abort.
  \item If $\RELval((\tx, \pauxtx), \sauxtx) \neq 1$ then abort
  \item Else read $\comppolicy$ and send $(\sendTransactionShieldedBegins, \auxacc,
    (\tx, \pauxtx))$ to $\adv$.
  \item Verify that $\comppolicy(\tx, \pauxtx) = 1$ and if that is not the
    case, send $(\allowTransaction, \tx, \pauxtx, \relay)$ to $\polas$ and $\adv$. \pccom{We allow the
    adversary to learn when a user tries to send non-complying transaction.}
    \begin{itemize}
    \item On $(\allowed, \tx, \pauxtx)$ from $\polas$ send $(\allowed)$ to
      $\adv$ and $\user$, then proceed;
    \item On $(\notAllowed, \tx, \pauxtx)$ from $\polas$ send $(\notAllowed)$
      to $\adv$ and $\user$ and exit.
    \end{itemize}
  \item Send $(\sendTransactionShielded, \tx, \pauxtx, \auxacc, \polas, \policydig,
    \relay)$ to $\adv$ and $\relay$;
  \item Return ($\shieldedTransactionSent)$ to $\adv$ and $\relay$ and add $(\tx,
    \paux_{tx}, \auxacc, \polas, \policydig)$ to the buffer.
  \end{itemize}

  \paragraph{Buffer release} \pccom{Publishes the newly created
    transactions} \\
  On $(\releaseTransBuffer, f)$ from $\adv$:
  \begin{itemize}
  \item If $f$ is not a permutation or its range size does not equal the number
    of tuples in the buffer, abort;
  \item remove all tuples from the buffer and add them in the permuted
    order (according to $f$) to the list $\listvar{tx}$.
  \end{itemize}

  \paragraph{Revoking accounts}
  On $(\revokeAccount, \auxacc)$ from an identity provider $\idprov$ and a set
  of anonymity revokers $\smallset{\ar_i}_{i \in I}$:
  \begin{itemize}
  \item If there is no tuple $(\accountCreated, \cdot, \cdot, \auxacc, \cdot)$
    then abort. Otherwise read $(\accountCreated, \auxid, \auxpol, \auxacc,
    \skacc)$.
  \item If $\abs{I} \leq \thresholdar$ or there is no tuple $(\identityIssued,
    \user, \idprov, \auxid, \polas, \auxpol)$ abort;
  \item Otherwise return $(\accountRevoked, \auxacc, \user)$ to $\idprov$ and
    $\smallset{\ar_i}_{i \in I}$.
  \end{itemize}

  \paragraph{Tracing malicious accounts}
  On $(\traceAccounts, \user)$ from $\idprov$ and $\smallset{\ar_i}_{i \in I}$:
  \begin{itemize}
  \item If $\user$ has no identity registered using $\idprov$, i.e. there is no
    tuple $\identityIssued, \user, \idprov, \cdot, \cdot, \cdot, \cdot)$, then
    abort. Otherwise read the value $\auxid$ from the tuple.
  \item If $\abs{I} > \thresholdar$, then return a list of all $\auxacc$-s that
    there is a tuple $(\accountCreated, \auxid, \cdot, \auxacc, \cdot)$.
  \end{itemize}
\end{funcbox}


\begin{protbox}{Application protocol $\prot{\PPCTS}$}
  \paragraph{Used ideal functionalities}
  \begin{description}
  \item[$\func{pp}$] outputs the public parameters for the signature scheme and the
    threshold encryption scheme.
  % \item[$\func{srs}$] that provides common reference strings to cryptographic
  %   primitives used in the protocol;
  \item[$\func{reg}$] which provides the users with public keys of anonymity
    revokers, policy assigners and other parties that take part in the protocol.
  \item[$\func{ledger}$] implements the following $\variable{validate}$
    predicate: the predicate accepts if a NIZK proof $\zkproof$ is valid and if
    $\auxacc$ has not been seen before.
  \item[$\func{idpol}$] is responsible for issuing users' identities. The functionality
    is parametrized by
    \begin{itemize}
    \item Signature scheme $\SIG = (\sgen, \kgen, \sign, \verify)$
    \item Blind signature scheme
      $\BSIG = (\sgen, \kgen, \blindsign, \sign, \verify)$;
    \item $(\thresholdar, \noofar)$-threshold encryption scheme $\TENC = (\sgen, \kgen, \enc, \dec)$
    \item Encryption scheme $\ENC = (\sgen, \kgen, \enc, \dec)$
    \item Relation $\REL_{sig}(\pk, \sk)$ which verifies whether
      $(\pk, \sk) \in \IM(\SIG.\kgen)$.
    \end{itemize}
  \item[$\func{nizk}$] NIZK functionalities parametrized by relations (each
    relation parametrizes different instance of the functionality):
    \begin{itemize}
    \item set of relations $\smallset{\REL_{al}}$, each of $\REL_{al}$ tells whether an
      attribute list of the user fulfils a predicate required by the policy assigner;
    \item$\REL_{val}$ which tells whether a transaction is valid according to the
      transacting system;
    \item$\REL_{comp}$ which tells whether a policy digest has been correctly
      computed for the compliance policy assigned to the user and that the
      transaction complies with the assigned compliance policy or the policy
      assigner approved the transaction by signing it.
    \item$\REL_{newacc}$ which tells whether account has been created using
      correct user's secrets and the policy digest has been computed correctly.
    \end{itemize}
  \end{description}

  \paragraph{Setup}
  \begin{itemize}
  \item On input $(\initialize, \ldots)$ from any party $\party \in \partyset{I} \cup
   \partyset{AR} \cup \partyset{U} \cup \owner \cup \partyset{R} \cup \partyset{PA}$
    \begin{itemize}
    \item Generate public parameters by running $\func{pp}^{\SIG, \BSIG, \ENC, \TENC, \secpar}$
      and obtain parameters $\pp$.
    \end{itemize}
  \end{itemize}

  \paragraph{The protocol description for a user $\user$.}
  \begin{description}
    
  \item[Identity issuance] On input $(\issueIdentity, \idprov, \AL)$
    \begin{itemize}
    \item Retrieve the identity provider's public key $\pk_{\idprov}$ and anonymity
      revokers' public keys $\smallset{\pk_{\ar_i}}_{i = 1}^{\noofar}$ using the
      $\func{reg}$ functionality.
    \item Generate key pair $(\pcred, \scred)$ satisfying $\REL_{user}$.
    \item Call $\func{idpol}$ on $(\initialize, (\pcred, \scred), \AL)$;
    \item Choose a random $\prf$ key $\key$ and encrypt it $\ckey =
      \TENC.\enc((\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}), \key; r_{key})$.
    \item Call identity issuance functionality $\func{idpol}$ on input
      $(\issueIdentity, (\ckey, \key, r_{key}, (\pk_{\ar_1}, \ldots,
      \pk_{\ar_{\noofar}}), \allowbreak \AL, (\pcred, \scred), \idprov)$
    \item After receiving the response $\signature_{id}$ from $\func{idpol}$ set
      $\auxid = (\idprov, \AL, \scred, \signature_{id}, \key)$.
    \item Return $(\identityIssued, \auxid)$.
    \end{itemize}

  \item[Attribute check] On input $(\checkAttributes, \polas)$
     \begin{itemize}
     \item Call $\func{idpol}$ on $(\checkAttributes, \polas)$.
     \item On $(\attributesNotValid, \user, \polas, \alpolicy)$ return the message to
       $\user$ and abort.
     \item On $(\attributesValid, \user, \polas, \alpolicy)$ store $\alpolicy$
       and return $(\attributesValid, \user, \polas, \alpolicy)$ to $\user$.
     \end{itemize}

   \item[Policy issuance] On input $(\issuePolicy, \polas, \AL)$
     \begin{itemize}
     \item send $(\issuePolicy, \polas, \AL)$ to the functionality $\func{idpol}$;
     \item obtain policy $\comppolicy$ and its signature $\signature_{comp}$;
     \item store $(\pcred, \polas, \comppolicy, \signature_{comp})$;
     \item return $(\policyAssigned, \user, \polas, \alpolicy, \comppolicy)$ to $\user$.
     \end{itemize}

  \item[Account creation] On input  $(\createAccount, \auxid, \polas,
    \pkacc, \skacc)$
    \begin{itemize}
    \item Compute threshold encryption of the public credentials, i.e.~compute
      $\cuser \gets \TENC.\enc((\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}), \pcred;
      r_{pcred})$.
    \item Compute account identifier $\auxacc \gets \prf_\key(x)$, for $x$ being the
      index of the newly created account.
    \item Compute policy digest $\policydig = \tprf_\key(\comppolicy,
      \signature_{comp}, r_{pd})$ for some random $r_{pd}$.
    \item Obtain $\polas$'s public key $\pk_\polas$ using $\func{reg}$.
    \item Make a proof that the values above have been computed correctly, i.e.~run
      $\func{nizk}^{\REL_{newacc}}$ on input
      $(\proveStatement, (\cuser, \aux_{acc}, \idprov, \pk_{acc}, \pk_{\polas},
      \pk_{\idprov} \policydig, \vec{\pk_\ar}), (\signature_{id}, r_{tenc}, \pcred,
      \scred, \key, \sk_{acc}, \comppolicy, \signature_{comp}, r_{pd}, \AL, x, \alpolicy,
      \signature_{al}) )$ and obtain a proof $\zkproof_{newacc}$.
    \item Let $\aci = ((\cuser, \auxacc, \idprov, \pk_{acc}), \zkproof_{newacc})$, send
    $(\createAccount, \aci)$ to $\func{ledger}$ 
  \item Return $(\accountCreated, \auxacc, \policydig)$.
    \end{itemize}
    
  \item[Shielded account creation] On input  $(\createAccountShielded, \auxid, \polas,
    \pkacc, \skacc, \relay)$
    \begin{itemize}
    \item Compute threshold encryption of the public credentials, i.e.~compute
      $\cuser \gets \TENC.\enc((\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}), \pcred;
      r_{pcred})$.
    \item Compute account identifier $\auxacc \gets \prf_\key(x)$, for $x$ being the
      index of the newly created account.
    \item Compute policy digest $\policydig = \tprf_\key(\comppolicy,
      \signature_{comp}, r_{pd})$ for some random $r_{pd}$.
    \item Obtain $\polas$'s public key $\pk_\polas$ using $\func{reg}$.
    \item Make a proof that the values above have been computed correctly, i.e.~run
      $\func{nizk}^{\REL_{newacc}}$ on input
      $(\proveStatement, (\cuser, \aux_{acc}, \idprov, \pk_{acc}, \pk_{\polas},
      \pk_{\idprov} \policydig, \vec{\pk_\ar}), (\signature_{id}, r_{tenc}, \pcred,
      \scred, \key, \sk_{acc}, \comppolicy, \signature_{comp}, r_{pd}, \AL, x, \alpolicy,
      \signature_{al}) )$ and obtain a proof $\zkproof_{newacc}$.
    \item Let $\aci = ((\cuser, \auxacc, \idprov, \pk_{acc}), \zkproof_{newacc})$, send
    $(\createAccount, \aci)$ to the relaying party $\relay$ via $\func{amt}$.
    \item Send $(\retrieve)$ to $\func{ledger}$ and obtain ledger $L$.
    \item If $L$ contains $\aci$, store $(\aci, \sk_{acc})$ and return
      $(\accountCreatedShielded, \auxacc, \policydig)$ else abort.
    \end{itemize}

  \item[Account and transaction retrieval] On input $(\retrieve)$ call $\func{ledger}$ on
    input $(\retrieve)$. After receiving $(\retrieve, L)$ from the
    functionality, output $L$.

  \item[Sending transactions] On input $(\sendTransaction,  \tx, \pauxtx,
    \sauxtx, \auxacc, \skacc, \polas, \signature_{comp})$:
    \begin{itemize}
    \item Call $\func{nizk}^{\REL_{val}}$ on input $(\proveStatement,
      \inp_{val} = (\tx, \paux_{tx}), (\saux_{tx}))$ to show validity of the
      transaction and obtain proof $\zkproof_{val}$.
    \item For transactions that does not comply with the assigned compliance policy
      \begin{itemize}
      \item Call $\func{smt}$ on
        $(\allowTransaction, \tx, \paux_{tx}, \zkproof_{val}, \auxacc, \pk_{acc}, \policydig, \polas,
        \relay)$.
      \item On $(\notAllowed, \tx, \paux_{tx})$ abort.
      \item On $(\allowed, \signature_{tx}, \tx, \paux_{tx})$ continue.
      \end{itemize}
    \item Call $\func{nizk}^{\REL_{comp}}$ on
      $(\proveStatement, \inp_{comp} = (\tx, \paux_{tx}, \pk_{\polas}, \policydig),
      (\comppolicy, \signature_{comp}, \signature_{tx}, \key, r_{pd}))$ to show that
      the transaction fulfils the compliance policy $\comppolicy$ and obtain proof
      $\zkproof_{comp}$.
    \item Let
      $\txdata = (\tx, (\inp_{val}, \zkproof_{val}), (\inp_{comp},
      \zkproof_{comp}))$,
    \item Send $(\append, \txdata)$ to $\func{ledger}$.
    \item Return $(\transactionSent, \txdata)$.
    \end{itemize}

  \item[Sending shielded transactions] On input $(\sendTransactionShielded,  \tx, \pauxtx,
    \sauxtx, \auxacc, \skacc, \polas, \signature_{comp}, \relay)$:
    \begin{itemize}
    \item Call $\func{nizk}^{\REL_{val}}$ on input $(\proveStatement,
      \inp_{val} = (\tx, \paux_{tx}), (\saux_{tx}))$ to show validity of the
      transaction and obtain proof $\zkproof_{val}$.
    \item For transactions that does not comply with the assigned compliance policy
      \begin{itemize}
      \item Call $\func{smt}$ on
        $(\allowTransaction, \tx, \paux_{tx}, \zkproof_{val}, \auxacc, \pk_{acc}, \policydig, \polas,
        \relay)$.
      \item On $(\notAllowed, \tx, \paux_{tx})$ abort.
      \item On $(\allowed, \signature_{tx}, \tx, \paux_{tx})$ continue.
      \end{itemize}
    \item Call $\func{nizk}^{\REL_{comp}}$ on
      $(\proveStatement, \inp_{comp} = (\tx, \paux_{tx}, \pk_{\polas}, \policydig),
      (\comppolicy, \signature_{comp}, \signature_{tx}, \key, r_{pd}))$ to show that
      the transaction fulfils the compliance policy $\comppolicy$ and obtain proof
      $\zkproof_{comp}$.
    \item Let
      $\txdata = (\tx, (\inp_{val}, \zkproof_{val}), (\inp_{comp},
      \zkproof_{comp}))$,
    \item Send $(\append, \txdata)$ to the relay party $\relay$ via $\func{amt}$.
    \item Send $(\retrieve)$ to $\func{ledger}$ and obtain ledger $L$.
    \item If $L$ contains $\txdata$ and return $(\transactionSent, \txdata)$, else abort.
    \end{itemize}
    %\end{itemize}
  \end{description}

  \paragraph{The protocol description for relays $\relay$}
  \begin{description}
  \item[Shielded funding accounts] On input $(\createAccount, \pkacc)$ from a relay
    $\relay$,
    \begin{itemize}
    \item append $\aci$ to the ledger by running $(\append, \aci)$ at
      $\func{ledger}$
    \item Return $(\accountCreated, \auxacc, \policydig)$
    \end{itemize}
    
  \item[Shielded sending transactions] On input $(\sendTransaction, \tx)$ from a
    relay $\relay$
    %, either
    \begin{itemize}
    \item send $(\sendTransaction)$ to $\user$ by calling $\func{smt}$/
    \item get $(\pauxtx, \auxacc, \pk_{\polas}, \comppolicy, \zkproof_{comp},
      \zkproof_{val})$ from the user,
    \item verify the zero knowledge proofs, i.e.~call $\func{nizk}^{\REL_{comp}}$ on
      $(\verifyProof, (\tx, \pauxtx, \pk_{\polas}, \comppolicy),
      \zkproof_{comp})$ and $\func{nizk}^{\REL_{val}}$ on $(\verifyProof, (\tx,
      \pauxtx), \zkproof_{val})$.
    \item if some of the proofs do not verify, abort
    \item else set $\txdata \gets (\tx, \pauxtx, \pk_{\polas}, \comppolicy,
      \zkproof_{comp}, \zkproof_{val})$
    %\item ignore, or
    \item send $(\append, \txdata)$ to the ledger $\func{ledger}$.
    \item Return $(\shieldedTransactionSent)$.
    \end{itemize}
  \end{description}

  \paragraph{The protocol description for identity providers $\idprov$-s and
    anonymity revokers $\ar$-s.}
  \begin{description}
  \item[Initialization] On input $(\initialize)$ from party $\idprov \in
    \smallset{\idprov_1, \ldots, \idprov_\noofidprov}$ obtain SRS $\srs$ from
    $\func{keygen}^{\SIG.\kgen, \secpar}$ generate key pair $(\sk_\idprov,
    \pk_\idprov) \sample \SIG.\kgen(\secparam)$ and send $(\initialize,
    (\sk_\idprov, \pk_\idprov))$ to $\func{idpol}$.

    On input $(\initialize)$ from party $\ar \in \smallset{\ar_1, \ldots,
    \ar_\noofar}$, get public parameters $\pp$ from $\func{pp}^{\ggen,
    \secparam}$, generate key pair $(\pk_\ar, \sk_\ar) \sample
    \TENC.\kgen(\secparam)$ by calling $\func{keygen}^{\TENC.\kgen, \secpar}$
    and send $(\register, (\pk_\ar, \sk_\ar))$ to $\func{reg}$.

  \item[Identity issuance] On input $(\issueIdentity, \user)$ from an identity
    provider $\idprov$, call $\func{idpol}$ with input $(\issueIdentity, \user,
    (\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}))$. Given the response $(\pcred,
    \AL, \cuser)$ from the functionality, set $\ipiu = (\user, \pcred, \AL,
    \cuser)$.

  \item[Retrieving] On input $(\retrieve)$ call $\func{ledger}$ on input
    $(\retrieve)$. After receiving $(\retrieve, L)$ from the functionality
    output $L$.

  \item[Revoking account] On input $(\revokeAccount, \auxacc)$ from an identity
    provider $\idprov$ and $\smallset{\ar_i}_{i \in I}$, for $\abs{I} >
    \thresholdar$ the anonymity revokers proceed as follows:
    \begin{itemize}
    \item Call $\func{ledger}$ on input $(\retrieve)$;
    \item After receiving $(\retrieve, L)$ from $\func{ledger}$, search $L$ for
      user's dataset $\aci$ that contains $\auxacc$.
    \item Decrypt $\cuser$ jointly by calling $\TENC.\dec$.
    \item Combine the shares to reveal public credentials of the user $\pcred$.
    \end{itemize}
    Identity provider $\idprov$ proceeds as follows:
    \begin{itemize}
    \item Read the identity provider identity $\idprov'$ from the decrypted
      dataset $\aci$.
    \item Ignore if $\idprov \neq \idprov'$.
    \item Else, locate $\ipiu = (\user, \auxacc, \AL, \cuser)$ and return
      $\user$.
    \end{itemize}

  \item[Tracing account] On input $(\trace, \user)$ from an identity provider
    $\idprov$ and $\smallset{\ar_i}_{i \in I}$, for $\abs{I} > \thresholdar$,
    \begin{itemize}
    \item Identity provider locates $\ipiu = (\user, \auxacc, \AL, \cuser)$
      containing $\user$ and sends $\ckey$ to anonymity revokers via
      $\func{smt}$.
    \item Each anonymity revoker decrypts its share of user's key $\key_i$ and
      call $\func{mpcprf}$ on $(\compute, \key_i, \pcred)$ and receive all
      account identifiers that can be generated by the user, i.e.~$\prf_\key
      (x)$, for $x \in \range{1}{\maxacc}$.
    \end{itemize}
  \end{description}

  \paragraph{The protocol description for policy assigners $\polas$.}
  \begin{description}
  \item[Initialization] On input $(\initialize)$ from a policy assigner
    $\polas \in \smallset{\polas_1, \ldots, \polas_\noofpolas}$ obtain public
    parameters $\pp$ from $\func{pp}^{\ggen, \secpar}$, generate key pairs
    $(\SIG.\pk_\polas, \SIG.\sk_\polas) \sample \SIG.\kgen(\secparam)$,
    $(\ENC.\pk_\polas, \ENC.\sk_\polas) \sample \ENC.\kgen(\secparam)$ and send
    $(\initialize, (\SIG.\pk_\polas, \SIG.\sk_\polas), (\ENC.\pk_{\polas},
    \ENC.\sk_{\polas}))$ to $\func{idpol}$.
  \item[Attributes check] On input $(\checkAttributes, \user, \alpolicy)$ from
    $\polas$ call $\func{idpol}$ on $(\checkAttributes, \user, \alpolicy)$ and return
    its output.
  \item[Policy issuance] On input $(\issuePolicy, \user, \comppolicy)$ from
    user policy assigner $\polas$ call functionality $\func{idpol}$ on input
    $(\issuePolicy, \user, \comppolicy)$ and get $(\policyAssigned,
    \comppolicy)$
  \item[Conditional transaction approval:] On input $(\allowTransaction, \tx,
    \paux_{tx}, \auxacc, \pk_{acc}, \policydig, \polas)$ from user $\user$,
    reply via $\func{smt}$ with either $(\allowed, \signature_{tx}, (\tx,
    \paux_{tx}))$, where $\signature_{tx} = \SIG.\sign(\sk_{\polas}, (\tx,
    \paux_{tx}))$, or $(\notAllowed, (\tx, \paux_{tx}))$.
  \end{description}
\end{protbox}


\subsubsection{Security proof and the simulator description}
\begin{simbox}{Simulator $\simulator_{\PPCTS}$} The simulator internally emulates all 
  functionalities that are specified in the protocol $\prot{\PPCTS}$.
  
  \paragraph{Initialization}
  \begin{enumerate}
    \item The simulator initiates all functionalities it simulates and generates all
     necessary keys and parameters they use. That is, it runs $\func{pp}$ to generate
     public parameters.
  \item Honest user $\user$. On $(\initialized, \user)$ from the functionality:
    \begin{itemize}
    \item  Add $\user$ to the set of initialized parties
      $\partyset{Init}$.
  \item Call $\func{idpol}$ on $(\initialize)$. 
    \end{itemize}
  \item Dishonest user $\user$. On any first message from an uninitialised dishonest user
    $\user$
    \begin{itemize}
    \item Call $\func{\PPCTS}$ on $(\initialize)$ on behalf of $\user$.
    \item Add $\user$ to $\partyset{Init}$.
    \end{itemize}

  \item Honest policy assigner $\polas$. On $(\initialized, \polas)$ from the functionality:
    \begin{itemize}
    \item Pick randomly $(\SIG.\pk, \SIG.\sk) \in \REL_{sig}$ and $(\ENC.\pk,
      \ENC.\sk) \in \REL_{enc}$.
    \item Call $\func{idpol}$ on $(\initialize, (\SIG.\pk, \SIG.\sk), (\ENC.\pk, \ENC.\sk))$.
    \item Add $((\SIG.\pk, \SIG.\sk), (\ENC.\pk, \ENC.\sk))$ to list $\listvar{polas, pk}$ and $
      \polas$ to $\partyset{Init}$
    \item Register $((\SIG.\pk, \SIG.\sk), (\ENC.\pk, \ENC.\sk))$ at $\func{reg}$ 
    \end{itemize}

  \item Dishonest policy assigner $\polas$. On $(\initialize, (\SIG.\pk, \SIG.\sk), (\ENC.\pk, \ENC.\sk))$ from a
    dishonest user $\polas$ sent to $\func{idpol}$
    \begin{itemize}
    \item Check that $\REL_{sig}(\SIG.\pk, \SIG.\sk) = 1$ and
      $\REL_{enc}(\ENC.\pk, \ENC.\sk) = 1$, abort if that is not the case.
    \item Output $\fail$ if $(\pk, \sk) \in \listvar{polas, pk}$. \pccom{The
        adversary broken hardness of relation $\REL_{sig}$.}
    \item Else store $(\pk, \sk)$.
    \item Sent $(\initialize)$ to $\func{\PPCTS}$ on behalf of $\polas$ and add the
      party to $\partyset{Init}$.
    \end{itemize}

  \item Honest identity provider $\idprov$. On $(\initialized, \idprov)$ from the functionality:
    \begin{itemize}
    \item Pick randomly $(\pk, \sk) \in \REL_{sig}$.
    \item Call $\func{idpol}$ on $(\initialize, (\pk, \sk))$.
    \item Add $(\pk, \sk)$ to $\listvar{idprov, pk}$ and $\idprov$ to
      $\partyset{Init}$.
    \item Register $(\pk, \sk)$ at $\func{reg}$
    \end{itemize}

  \item Dishonest identity provider $\idprov$. On $(\initialize, (\pk, \sk))$
    sent to $\func{idpol}$ by a dishonest user $\idprov$:
    \begin{itemize}
    \item Check that $\REL_{sig}(\pk, \sk) = 1$, and abort if that is not the
      case.
    \item If $(\pk, \sk) \in \listvar{idprov, pk}$ output $\fail$. \pccom{The
        adversary broken hardness of relation $\REL_{sig}$.}
    \item Send $(\initialize)$ to $\func{\PPCTS}$ on behalf of $\idprov$ and add the
      party to $\partyset{Init}$
    \end{itemize}

  \item Honest anonymity revoker $\ar$. On $(\initialized, \ar)$ sent to the
    functionality
    \begin{itemize}
    \item Pick $(\pk, \sk) \in \REL_{tenc}$.
    \item Send $(\pk, \sk)$ to $\func{reg}$.
    \item Call $\func{idpol}$ on $(\initialize, (\pk, \sk))$.
    \end{itemize}

  \item Dishonest anonymity revoker $\ar$. On $(\initialize, (\pk, \sk))$ from the
    functionality $\func{idpol}$
    \begin{itemize}
    \item Check that $\REL_{tenc} (\pk, \sk) = 1$ and abort if that is not the case.
    \item Call $\func{\PPCTS}$ on $(\initialize)$ and add the party to the set of
      initialized parties $\partyset{Init}$3.
    \end{itemize}
  \end{enumerate}

  Importantly, if simulator gets a message from a non-initialized party, it ignores
  it (except the message is sent to initialize the party). 
  % \end{description} \item[Identity issuance]

  \paragraph{Identity issuance}
  \michals{13.12}{Should we add case of both honest parties?}
  \michals{5.1}{No if the functionality doesn't leak anything to the adversary}
  \begin{enumerate}
  \item Passively corrupted $\idprov$, honest $\user$. On $(\issueIdentity, \user, \idprov, \AL)$ from $\func{\PPCTS}$,
    \begin{itemize}
    \item Pick
      randomly $(\pcred, \scred)$ accordingly to $\REL_{user}$ and compute $\ckey$ being a
      dummy encryption of $0$.
  \item Emulate $\func{idpol}$ for $\idprov$ and output $(\pcred, \ckey)$
    to $\idprov$. \michals{12.1}{Should we output $\AL$ to the identity provider here?}
  \item Add $\ckey$ to $\listvar{ckey}$, $\pcred$ to $\listvar{user, pcred}$, and
    $((\user, \AL, \idprov), (\ckey, \pcred, \AL)$ to $\listvar{issue}$.
  \end{itemize}
\item Malicious $\user$, honest $\idprov$. On corrupted $\user$'s call $(\issueIdentity, (\ckey, \key, r,
      (\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar})), \AL, (\pcred, \scred),
      \idprov)$.
  \begin{itemize}
    \item Abort if $\ckey$ is not a valid encryption of
      key $\key$ under public keys $(\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar})$
      and randomness $r$; or $\REL_{user}(\pcred, \scred) \neq 1$.
    \item  Output $\fail$ if the ciphertext or the public key
      have been already registered, i.e.~when $\ckey \in \listvar{ckey}$ or
      $\pcred \in \listvar{user, pcred}$. \pccom{That is, the adversary
      produced a ciphertext identical to a ciphertext produced by the
      simulator, breaking security of the encryption scheme; or it produced the
      same public key $\pcred$ breaking hardness of relation $\REL_{user}$.}
  \item Otherwise, call $\func{\PPCTS}$ with $(\issueIdentity, \idprov, \AL)$,
    compute the signature $\signature_{id}$ by internally emulating the honest
    $\idprov$. Return $\aux_{id} = (\idprov, \AL, \scred, \signature_{id}, \key)$
    to $\user$.
    \item Add $(\signature_{id}, (\scred, \key, \AL),
      \idprov)$ to $\listvar{sign}$.
    \end{itemize}
  \end{enumerate}

  \paragraph{Attribute check}
  \begin{enumerate}
  \item Honest user $\user$ and policy assigner $\polas$. \pccom{The simulator does not
      need to do anything as this procedure does not leak anything to the adversary.}
    % On $(l_{al}, \pAL, \pk_{idprov},
    % \pk, l_{enc}, \pk_{\polas})$ from the 
    
  \item Honest user $\user$ and malicious policy assigner $\polas$. On
    $(\checkAttributes, \user, \alpolicy)$ sent by $\polas$ to $\func{idpol}$
    \begin{itemize}
    \item call $\func{\PPCTS}$ on $(\checkAttributes, \user, \alpolicy)$ on behalf of
      $\polas$;
    \item call $\func{idpol}$ on $(\checkAttributes, \polas)$ on behalf of the user.
    \end{itemize}
    
  \item Malicious user $\user$ and honest policy assigner $\polas$. On
    $(\checkAttributes, \polas)$ sent by $\user$ to $\func{idpol}$
    \begin{itemize}
    \item call $\func{\PPCTS}$ on $(\checkAttributes, \polas)$ on behalf of
      $\user$;
    \item on $(\attributesNotValid, \alpolicy)$ or
      $(\attributesValid, \user, \alpolicy)$ from $\func{\PPCTS}$ call
      $\func{idpol}$ on $(\checkAttributes, \user, \alpolicy)$ on behalf of $\polas$
    \end{itemize}
    
  \item Malicious $\user$ and policy assigner $\polas$. We do not allow both the user and
    policy assigner to be corrupted as that would allow the user to get any policy on any
    attribute list it wants.
  \end{enumerate}
  
  \paragraph{Policy issuance}
  \begin{enumerate}
  \item Passively corrupted $\polas$, honest $\user$.  On $\polas$'s call $(\issuePolicy, \user, \comppolicy, \alpolicy)$
      to the ideal functionality $\func{idpol}$ %, find which user
      % $\user$ uses public key $\pcred$ and
    \begin{itemize}
    \item Send $(\issuePolicy, \user, \alpolicy, \comppolicy)$ to $\func{\PPCTS}$.
    \item Simulate the $\func{idpol}$ functionality for $\polas$ and, for the policy
      $\comppolicy$ provided by $\polas$, output $(\policyAssigned)$ to $\polas$.
    \item Store $(\user, \polas, \comppolicy)$ to $\listvar{pol}$
    \end{itemize}
  \item Malicious $\user$, honest $\polas$. On corrupted $\user$'s call $(\issuePolicy, \polas, \AL)$ to
      $\func{idpol}$
    \begin{itemize}
    \item Invoke $\func{\PPCTS}$ on $(\issuePolicy, \polas, \AL)$.
    \item Learn the policy $\comppolicy$ sent to $\user$ by the policy assigner.
    \item Compute signature $\signature_{comp}$ on $(\comppolicy, \pcred)$ using
      previously picked signature scheme keys.
    \item Output $(\policyAssigned, \comppolicy, \signature_{comp})$ to $\user$.
    \end{itemize}
  \end{enumerate}

  \paragraph{Shielded account creation}\footnote{Analogously the simulator proceeds
    when non-shielded transaction is sent. In that case, interaction with relay is removed.} 
  \begin{enumerate}
  \item Malicious $\user$, honest relay $\relay$. On $(\sendAnonymously, \relay, \aci)$ sent to $\func{amt}$, where
      $\aci = (\inp_{newacc}=(\cuser, \auxacc, \idprov, \pk_{acc}, \pk_\idprov, \pk_\polas,
      \pk_{\idprov}, \policydig, \vec{\pk_\ar}),
      \zkproof_{newacc})$,
    \begin{itemize}
    \item Use $\func{nizk}^{\REL_{newacc}}$ to extract the witness
      $\wit_{newacc} = (\signature_{id}, r_{tenc}, \pcred, \scred, \key, \sk_{acc},
      \comppolicy, \signature_{comp}, r_{pd}, \AL, x, \alpolicy, \signature_{al})$ for
      $\inp_{newacc}$ or abort if the proof does not verify or there already is
      registered account
      $(\aux_{acc}, \cuser, \idprov, \pk_{acc}, \pk_\polas, \pk_\idprov, \policydig,
      \vec{\pk_{\ar}}, \zkproof) \in \listvar{acc}$.
    \item Output $\fail$ if at least one of the following holds:
      \begin{itemize}
      \item $(\signature_{id}, (\scred, \key, \AL), \idprov) \not\in \listvar{sig}$,
        \pccom{The adversary broke existential unforgeability of the signature
          scheme.}
      \item $\pcred \in \listvar{user,pcred}$ \pccom{The adversary broke hardness of
          relation $\REL_{user}$.}
      \item $\cuser \in \listvar{cuser}$, \pccom{The adversary broke semantic
          security of the encryption scheme.}
      \item $\auxacc \in \listvar{auxacc}$, \pccom{The adversary broke robustness of
          the PRF.}
      \item $x > \maxacc$. \pccom{The adversary broke soundness of NIZK for
          $\REL_{newacc}$.}
      \end{itemize}
    \item Otherwise, call $\func{\PPCTS}$ on
      $(\createAccount, \aux_{id}, \polas, \auxpol, \pk_{acc}, \sk_{acc},
      \relay)$ and, when prompted, input $\aux_{acc} = \prf_\key(x)$.
    \item Send $(\append, \aci)$ to the ledger functionality $\func{ledger}$.
    \end{itemize}

  \item Honest $\user$ and relay $\relay$. Upon receiving $(\createAccount, \pk_{acc}, \idprov,
      \polas)$ from the ideal functionality:
    \begin{itemize}
    \item Pick a random $\aux_{acc}$ from
      the PRF domain and forward it to the functionality.
      %\item If $\simulator$ gets $(\RelayDidNotApprove})$, it aborts.
    \item Add $\auxacc$ into $\listvar{auxacc}$, else abort.
    \item Prepare a statement
      $\inp_{newacc} = (\cuser, \aux_{acc}, \idprov, \pk_{acc}, \pk_{\idprov}, \pk_{\polas},
      \policydig, \vec{\pk_{\ar}})$ where $\ckey$ is an encryption of
      dummy.
    \item Get a simulated proof $\zkproof_{newacc}$ for $\inp_{newacc}$ by calling $\func{nizk}^{\REL_{newacc}}$ and
      append $(\inp, \zkproof)$ to the buffer of $\func{ledger}$.
    \item Add $(\inp_{newacc}, \zkproof_{newacc})$ to $\listvar{acc}$.
    \end{itemize}
    
  \item Honest $\user$, malicious relay $\relay$. On
    $(\createAccount, \pk_{acc}, \idprov, \polas)$ from the ideal functionality,
    \begin{itemize}
    \item Pick a random $\aux_{acc}$ from the PRF domain and forward it to
      the functionality.
    % \item On $(\append, \aci)$ from a dishonest $\relay$, send $(\relayApproved)$ to
    %   $\func{\PPCTS}$ and continue, else abort.
    \item Add $\auxacc$ into $\listvar{auxacc}$.
    \item Prepare statement $\inp_{newacc} = (\cuser, \aux_{acc}, \idprov, \pk_{acc}, \pk_{\polas},
      \pk_{\idprov}, \policydig, \vec{\pk_{\ar}})$ where
      $\ckey$ is an encryption of dummy.
    \item Get a simulated proof $\zkproof_{newacc}$ for $\inp_{newacc}$ by calling
      $\func{nizk}^{\REL_{newacc}}$ and append $(\inp, \zkproof)$ to the buffer of
      $\func{ledger}$.
    \item Add $(\inp_{newacc}, \zkproof_{newacc})$ to $\listvar{acc}$.
    \end{itemize}
    
  \item Malicious $\user$ and relay $\relay$. On $(\sendAnonymously, \relay, \aci)$, where
      $\aci = (\inp_{newacc}= (\cuser, \aux_{acc}, \idprov, \pk_{acc}, \pk_{\polas},
      \pk_{\idprov}, \policydig, \vec{\pk_{\ar}}), \zkproof_{newacc})$, send by
      $\user$ to $\func{amt}$:
    \begin{itemize}
    \item Use $\func{nizk}^{\REL_{newacc}}$ to extract the witness
      $\wit_{newacc} = (\signature_{id}, r_{tenc}, \pcred, \scred, \key, \sk_{acc},
      \comppolicy, \signature_{comp}, r_{pd}, \AL, x, \alpolicy, \signature_{al})$ for
      $\inp_{newacc}$ or abort if the proof does not verify or there already is
      registered account $(\inp_{newacc}, \zkproof_{newacc}) \in \listvar{acc}$.
    \item Output $\fail$ if at least one of the following holds:
      \begin{itemize}
      \item $(\signature_{id}, (\scred, \key, \AL), \idprov) \not\in
        \listvar{sig}$,
      \item $\pcred \in \listvar{user,pcred}$,
      \item $\cuser \in \listvar{cuser}$,
      \item $\auxacc \in \listvar{auxacc}$,
      \item $\auxacc \in \listvar{auxacc}$, or
      \item $x > \maxacc$.
      \end{itemize}
    \item Otherwise, call $\func{\PPCTS}$ on
      $(\createAccount, \aux_{id}, \polas, \aux_{pol}, \pk_{acc}, \sk_{acc}, \relay)$
      and, when asked, input $\aux_{acc} = \prf_\key(x)$.
    \item On $\func{ledger}$ call $(\append, \aci)$ from $\relay$
      % , send
    % $(\relayApproved)$ to $\func{\PPCTS}$ and continue, else abort.
    \end{itemize}
  \end{enumerate}

  \paragraph{Release}
  Emulate the command by simulating calls to $\func{ledger}$. That is, when the
  adversary invokes $(\releaseTransactionBuffer, f)$ add the permuted buffer to the
  list $\listvar{ledger}$ and then reset the buffer.

  \paragraph{Retrieving}
  Simulate the retrieve command in $\func{ledger}$ and give as output
  $\listvar{ledger}$.

  \paragraph{Shielded sending transactions}\footnote{Analogously the simulator proceeds
    when non-shielded transaction is sent. In that case, interaction with relay is removed.}
  \begin{enumerate}
  \item Honest $\user$, relay $\relay$ and policy assigner $\polas$. Upon receiving
    $(\sendTransactionBegins, \auxacc, (\tx, \paux_{tx}))$
    \begin{itemize}
    \item On $(\allowTransaction, \ldots, \polas, \ldots)$
      \begin{itemize}
      \item Send to $\polas$ message $(\allowTransaction, \ldots)$ via
        $\func{smt}$ on behalf of $\user$.
      \item On $(\allowed)$,
        \begin{itemize}
        \item Make a simulated signature $\signature_{tx}$ on $(\tx, \pauxtx)$
          on behalf of $\polas$,
        \item Send to $\user$ on behalf of $\polas$ message $(\allowed,
           \tx, \paux_{tx}, \signature_{tx})$ via $\func{smt}$. \pccom{$\polas$
          allowed transaction.}
        \end{itemize}
      \item On $(\notAllowed)$, send $(\notAllowed, \tx, \pauxtx)$ to $\user$
        via $\func{smt}$ on behalf of $\polas$ and exit.
      \end{itemize}
    \item On $(\sendTransaction, \ldots)$ from the functionality,
      \begin{itemize}
      \item Prepare simulated zero-knowledge proof for transaction validity,
        $\REL_{val}$ and compliance fulfillment $\REL_{comp}$. That is, show
        $\inp_{val} \in \LANG_{\REL_{val}}$ and $\inp_{comp} \in
        \LANG_{\REL_{comp}}$.
      \item Prepare $\txdata = (\tx, (\inp_{val}, \zkproof_{val}),
        (\inp_{comp}, \zkproof_{comp}))$.
      \item Send $(\sendTransaction, \txdata)$ to $\relay$ via $\func{amt}$.
      \item \comment{On $(\relayApproved)$ s}Send $(\append, \txdata)$ to $\func{ledger}$       
      %   on behalf of $\relay$,
      % \item Else exit.
      \end{itemize}
    \end{itemize}

  \item Malicious $\user$, honest relay $\relay$ and policy assigner $\polas$.
    \begin{itemize}
      \item  On
    $\user$ using $\func{smt}$ to send to $\polas$ message
    $(\allowTransaction, \tx, \paux_{tx}, \zkproof_{val}, \auxacc, \pkacc,
    \policydig, \polas, \relay)$ \pccom{The user's transaction does not follow the
      compliance policy and it has to ask the policy assigner for the permission.}
    \begin{itemize}
      \item Abort if $\zkproof_{val}$ is not acceptable;
      \item Else, extract the witness $\saux_{tx}$ from $\func{nizk}^{\REL_{val}}$,
        output $\fail$ if this fails.
      \item Call the functionality on
        $(\sendTransaction, \tx, \paux_{tx}, \saux_{tx}, \auxacc, \polas,
        \signature_{comp}, \policydig,
        \relay)$ on behalf of $\user$.
      \item On $(\notAllowed)$ from the functionality, send to $\user$ on
        behalf of $\polas$ message $(\notAllowed, \tx, \paux_{tx})$ via
        $\func{smt}$. \pccom{$\polas$ did not allowed the transaction.}
      \item On $(\allowed)$ from the functionality,
        \begin{itemize}
        \item Make a simulated signature $\signature_{tx}$ on $(\tx, \pauxtx)$
          on behalf of $\polas$,
        \item Send to $\user$ on behalf of $\polas$ message $(\allowed,
          \signature_{tx}, \tx, \paux_{tx})$ via $\func{smt}$. \pccom{$\polas$
          allowed transaction.}
        \end{itemize}
      \end{itemize}
    \item On input $(\sendAnonymously, \relay, \txdata)$ sent to $\func{amt}$
      by $\user$, read from $\txdata$: $\auxacc$, $\inp_{val} = (\tx,
      \paux_{tx}), \inp_{comp} = (\tx, \paux_{tx}, \polas, \policydig)$
      \pccom{User does not ask the policy assigner for a permission but
      directly goes to the relay}
    \begin{itemize}
      \item Abort if the provided proofs $\zkproof_{val}$ or $\zkproof_{comp}$
        do not verify.
      \item  Use $\func{nizk}^{\REL_{val}}$ and $\func{nizk}^{\REL_{comp}}$ to
        extract witnesses $\wit_{val} = (\saux_{tx})$ and $\wit_{comp} =
        (\comppolicy, \signature_{comp}, \signature_{tx}, \key, r)$ and output $\fail$
        is this fails.
      \item Output $\fail$ if $\signature_{comp}$ not in the list
        $\listvar{pol}$ or $\signature_{tx}$ not in the list $\listvar{tx}$.
      \item Call functionality on $(\sendTransaction, \tx, \paux_{tx}, \auxacc,
        \polas, \policydig, \signature_{comp}, \relay)$ if that has not been already done.
      \item \comment{On $(\relayApproved)$ from the functionality, c}Call $\func{ledger}$
        on behalf of the relay with input $(\append, \txdata)$.
      \end{itemize}
    \end{itemize}
  \item Honest $\user$ and policy assigner $\polas$, malicious relay $\relay$.
    \begin{itemize}
    \item On
      $(\allowTransaction, \tx, \pauxtx, \auxacc, \pkacc, \policydig, \polas,
      \relay)$ from the functionality,
      \begin{itemize}
      % \item Make a simulated proof $\zkproof_{val}$ for
      %   $\inp_{val} = (\tx, \paux_{tx}) \in \LAN_{\REL_{val}}$.
      \item Send $(\allowTransaction, \ldots)$ to $\polas$ on behalf of the user via
        $\func{smt}$.
      \item On $(\notAllowed)$ from the functionality, send
        $(\notAllowed, (\tx, \pauxtx))$ to $\user$ via $\func{smt}$ on behalf of
        $\polas$.
        \item On $(\allowed, \tx, \pauxtx)$ from the functionality,
          \begin{itemize}
          \item Prepare a simulated signature $\signature_{tx}$ for $\tx,
            \paux_{tx}$ on behalf of $\polas$,
          \item Send $(\allowed, \signature_{tx}, \tx, \pauxtx)$ to $\user$ via
            $\func{smt}$ on behalf of $\polas$.
          \end{itemize}
      \end{itemize}
    \item On $(\sendTransaction, \ldots)$ from the functionality,
      \begin{itemize}
      \item Prepare a simulated zero-knowledge proof $\zkproof_{val}$ for
        $\inp_{val} = (\tx, \paux_{tx}) \in \LAN_{\REL_{val}}$;
      \item Prepare a simulated zero-knowledge proof $\zkproof_{comp}$ for
        $\inp_{comp} = (\tx, \paux_{tx}, \pk_\polas, \auxpol) \in
        \LAN_{\REL_{comp}}$;
      \item Prepare $\txdata$.
      \item Send to $\relay$ via $\func{amt}$ message $(\sendTransaction,
        \txdata)$.
      % \item On $(\append, \txdata$) from $\relay$ sent to $\func{ledger}$, send
      %   $(\relayApproved)$ to $\func{\PPCTS}$.
      \end{itemize}
    \end{itemize}
  \item Malicious user $\user$ and relay $\relay$, honest policy assigner
  $\polas$.
    \begin{itemize}
    \item On input $(\allowTransaction, \tx, \pauxtx, \auxacc, \zkproof_{val}, \pkacc,
      \policydig, \polas, \relay)$ sent by $\user$ to $\polas$ via
      $\func{smt}$:
      \begin{itemize}
      \item Abort if $\zkproof_{val}$ is not acceptable.
      \item Use functionality $\func{nizk}^{\REL_{val}}$ to extract witness
        $\saux_{tx}$ for $(\tx, \pauxtx)$ and output $\fail$ if this fails.
      \item Call functionality on $(\sendTransaction, \tx, \paux_{tx},
        \saux_{tx}, \auxacc, \polas, \policydig, \signature_{comp}, \relay)$.
      \item On $(\notAllowed)$ from the functionality, send $(\notAllowed,
        (\tx, \pauxtx))$ to $\user$ via $\func{smt}$ on behalf of $\polas$.
      \item On $(\allowed)$ from the functionality,
        \begin{itemize}
        \item Prepare a simulated signature $\signature_{tx}$ for $\tx,
          \paux_{tx}$ on behalf of $\polas$,
        \item Send $(\allowed, \signature_{tx}, \tx, \pauxtx)$ to $\user$ via
          $\func{smt}$ on behalf of $\polas$.
        \end{itemize}
      \end{itemize}
    \item On input $(\sendAnonymously, \relay, \txdata)$ sent to $\func{amt}$
      by $\user$, read from $\txdata$: $\auxacc$, $\inp_{val} = (\tx,
      \paux_{tx}), \inp_{comp} = (\tx, \paux_{tx}, \polas, \policydig)$
      \begin{itemize}
      \item Abort if the provided proofs $\zkproof_{val}$ or $\zkproof_{comp}$ do not
        verify.
      \item Use $\func{nizk}^{\REL_{val}}$ and $\func{nizk}^{\REL_{comp}}$ to extract
        witnesses $\wit_{val} = (\saux_{tx})$ and
        $\wit_{comp} = (\comppolicy, \signature_{comp}, \signature_{tx}, \key, r)$,
        output $\fail$ if this fails.
      \item Output $\fail$ if $\signature_{comp}$ not in the list
        $\listvar{pol}$ or $\signature_{tx}$ not in the list $\listvar{tx}$.
      \item Otherwise, call functionality $\func{\PPCTS}$ on input
        $(\sendTransaction, \tx, \paux_{tx}, \saux_{tx}, \auxacc, 
        \polas, \policydig, \signature_{comp}, \relay)$ if that has not been done already.
      \end{itemize}
    % \item On $(\append, \txdata)$ sent by $\relay$ to $\func{ledger}$ send
    %   $(\relayApproved)$ to the functionality on behalf of $\relay$ and $\adv$.
    \end{itemize}
  \item Malicious $\relay$ and policy assigner $\polas$, honest user $\user$.
    \begin{itemize}
    \item On $(\allowTransaction, \ldots)$ from the functionality
      \begin{itemize}
     % \item Make a simulated proof $\zkproof_{val}$ for
     %    $\inp_{val} = (\tx, \paux_{tx}) \in \LAN_{\REL_{val}}$.
      \item Send $(\allowTransaction, \ldots)$ to $\polas$ via $\func{smt}$;
      \item On $(\allowed, \signature_{tx}, \tx, \pauxtx)$ from $\polas$
        \begin{itemize}
        \item Verify the signature and if it is correct send $(\allowed)$ to
        the functionality;
        \item Abort if the signature does not verify correctly;
        \end{itemize}
      \item On $(\notAllowed)$ from $\polas$, send $(\notAllowed)$ to the
          functionality and exit.
      \end{itemize}
    \item On $(\sendTransaction, \ldots)$ from the functionality
      \begin{itemize}
      \item Prepare a simulated zero-knowledge proof $\zkproof_{val}$ for
        $\inp_{val} = (\tx, \paux_{tx}) \in \LAN_{\REL_{val}}$;
      \item Prepare a simulated zero-knowledge proof $\zkproof_{comp}$ for
        $\inp_{comp} = (\tx, \paux_{tx}, \polas, \policydig) \in
        \LAN_{\REL_{comp}}$;
      \item Prepare $\txdata$ and send $(\sendTransaction, \txdata)$ via
        $\func{smt}$ on behalf of $\user$.
      % \item On $(\append, \txdata)$ sent by $\relay$ to $\func{ledger}$, send
      %   $(\relayApproved)$ to the functionality.
      \end{itemize}
    \end{itemize}
  \item Malicious policy assigner $\polas$, honest user $\user$ and relay
  $\relay$.
    \begin{itemize}
    \item On $(\allowTransaction, \tx, \paux_{tx}, \auxacc, \pkacc,
      \policydig)$ sent by the functionality:
      \begin{itemize}
      \item Send to $\polas$ message $(\allowTransaction, \tx, \paux_{tx},
        \auxacc, \pkacc, \policydig)$ via $\func{smt}$ on behalf of $\user$.
      \item On $(\allowed, \signature_{tx}, \tx, \pauxtx)$ sent by $\polas$ to
        $\user$ via $\func{smt}$,
        \begin{itemize}
          \item Verify the signature and if it is correct send $(\allowed)$ to
            the functionality;
          \item Abort if the signature does not verify correctly;
        \end{itemize}
      \item On $(\notAllowed, (\tx, \pauxtx))$, send $(\notAllowed)$ to the
        functionality and exit.
      \item Prepare a simulated zero-knowledge proof $\zkproof_{val}$ for
        $\inp_{val} = (\tx, \paux_{tx}) \in \LAN_{\REL_{val}}$;
      \item Prepare a simulated zero-knowledge proof $\zkproof_{comp}$ for
        $\inp_{comp} = (\tx, \paux_{tx}, \polas, \auxpol) \in
        \LAN_{\REL_{comp}}$;
      \item Collect $\txdata$ and send $(\sendTransaction, \txdata)$ to
        $\relay$ via $\func{amt}$ on behalf of $\user$.
      % \item On $(\relayApproved)$ from the functionality, send to
      %   $\func{ledger}$ message $(\append, \txdata)$ on behalf of $\relay$
      \end{itemize}
    \end{itemize}
  \end{enumerate}

  \paragraph{Revoking account}
  \begin{enumerate}
  \item Semi-honest $\idprov$, up to $\thresholdar$ malicious $\ar$, honest
    $\user$.
    \begin{itemize}
    \item When $\idprov$ and a qualified set of anonymity revokers inputs
      $\revokeAccount$, the simulator obtains $\aux_{acc}$ and $\user$ from the
      input and output of the functionality $\func{\PPCTS}$.
    \item The simulator, using $\aux_{acc}$ searches $\listvar{acc}$ and
      retrieves the corresponding $\ckey$.
    \item Similarly, the simulator uses $(\user, \idprov)$, searches
    $\listvar{issue}$ and retrieves the corresponding $\pcred$.
    \item The simulator equivocates the decryption of $\ckey$ using $\pcred$.
    \end{itemize}
  \item Malicious $\user$ and up to $\thresholdar$ malicious $\ar$-s.
    \begin{itemize}
    \item The simulator receives $\user$ and a list of accounts
      $\smallset{\aux_{acc}}$ from the ideal functionality.
    \item The simulator looks up the ciphertext $\cuser$ corresponding to the
      user $\user$ and emulates $\func{mpcprf}$ to output
      $\smallset{\aux_{acc}}$.
    \end{itemize}
  \end{enumerate}

  \paragraph{Tracing account}
  \begin{enumerate}
  \item Semi-honest $\idprov$ and up to $\thresholdar$ semi-honest $\ar$,
    honest $\user$.
    \begin{itemize}
    \item When the identity provider and the qualified set of anonymity
      revokers calls $(\trace)$, the simulator receives $\user$ and a lit
      $\listvar{auxacc}$ from the input and output of the main functionality.
    \item The simulator recovers $\cuser$ ciphertext.
    \item It programs the output of $\func{mpcprf}$ to be consistent with
    $\listvar{auxacc}$.
    \end{itemize}
  \item Malicious user $\user$ and up to $\thresholdar$ malicious anonymity
    revokers.
    \begin{itemize}
    \item The simulator receives $\user$ and list of accounts
      $\listvar{auxacc}$ from the ideal functionality.
    \item It looks up the ciphertext $\cuser$ corresponding to the user $\user$
      and emulates $\func{mpcprf}$ to output the list $\listvar{auxacc}$.
    \end{itemize}
  \end{enumerate}
\end{simbox}

\begin{theorem}
  Let $\SIG$ be a existentially unforgeable signature scheme, $\prf$ be a PRF,
  $\TENC$ be a semantically secure threshold encryption scheme which has
  partial decryption simulatability property. Then the protocol $\prot{\PPCTS}$
  UC-realizes $\func{\PPCTS}$ functionality in the $\smallset{\func{idpol},
  \func{ledger}, \func{srs}, \func{pp}, \func{idpol}, \func{nizk}, \func{smt},
  \func{amt}}$-hybrid model.
\end{theorem}

\begin{proof}
  The proof goes by game hoping. In the first game, the simulator has access to
  the ideal functionality $\func{\PPCTS}$ and provides a view indistinguishable
  from an execution of a real protocol $\prot{\PPCTS}$. The final game is the
  real-life protocol.
  \begin{description}
  \item[Hybrid 0.] In this hybrid the simulator behaves as described above.
  \item[Hybrid 1.]  In this hybrid the simulator never outputs $\fail$.
  \item[Hybrid 0 to Hybrid 1.]
    We argue  that the simulator described in the frame above outputs $\fail$
    with negligible probability only. More precisely, $\simulator$ return
    $\fail$ if
    \begin{itemize}
    \item $(\pk, \sk) \in \listvar{polas,pk}$ what happens only if the
      adversary breaks hardness of a hard relation $\REL_{sig}$.
    \item $(\pk, \sk) \in \listvar{idprov, pk}$ what happens only if the
      adversary breaks hardness of a hard relation $\REL_{sig}$.
    \item $\pcred \in \listvar{user, pcred}$ what happens only if the adversary
      breaks hardness of a hard relation $\REL_{user}$.
    \item $\ckey \in \listvar{ckey}$ what happens only if the adversary breaks
      semantic security of the encryption scheme.
    \item $(\signature_{id}, (\scred, \key, \AL), \idprov) \not\in
      \listvar{sig}$ what happens only if the adversary breaks existential
      unforgeability of the signature scheme.
    \item $\cuser \in \listvar{cpcred}$ what happens only if the adversary
      breaks semantic security of the encryption scheme.
    \item $\auxacc \in \listvar{auxacc}$ what happens only if the adversary
      breaks robustness of the PRF.
    \item $x \in \maxacc$ what happens only if the adversary breaks soundness
      of a proof system for $\REL_{newacc}$.
    \item $\signature_{comp} \in \listvar{pol}$ what happens only if the
      adversary breaks existential unforgeability of the signature scheme.
    \item $\signature_{tx} \in \listvar{tx}$ what happens only if the adversary
      breaks existential unforgeability of the signature scheme.
    \item it fails to extract a witness from an acceptable zero-knowledge proof
      produced by a malicious party.
    \end{itemize}
    All of these events have negligible probability, thus the probability that
    the hybrids are distinguishable is negligible as well.
  \item[Hybrid 2.] In this hybrid the simulator picks $\aux_{acc}$ in a way
    compliant with the protocol $\prot{\PPCTS}$. That is, it picks the PRF key
    $\key$ and for a user using credential $\pcred$ computes $\aux_{acc} =
    \prf_\key(x)$ for a counter $x \in \range{1}{\maxacc}$.
  \item[Hybrid 1 to Hybrid 2.] Assume that there is a distinguisher $\ddv$ who
    can distinguish both hybrids. That distinguisher can be used to distinguish
    an output of a PRF $\prf$ and a random bitstring. Hence, it can be used to
    break pseudorandomness of $\prf$.
  \item[Hybrid 3.] In this hybrid the simulator creates ciphertext $\cuser$ as
    in the real-life protocol, i.e.~it encrypts the real user's $\pcred$
    instead of a dummy.
  \item[{Hybrid 2 to Hybrid 3.}] The hybrids are indistinguishable as from the
    semantic security of the encryption scheme used to produce $\cuser$,
    encryption of $\pcred$ is indistinguishable from an encryption of a dummy.
  \item[{Hybrid 4.}] Similarly as in the previous hybrid, the simulator now
    changes the way that ciphertext $\ckey$ is produced. Instead of dummy, it
    encrypts now user's PRF key $\key$.
  \item[{Hybrid 2 to Hybrid 4.}] As previously, semantic security of the
    threshold encryption scheme assures indistinguishability of the hybrids.
  \item[{Hybrid 5.}] In this hybrid the simulator changes its behavior when the
    $(\revokeAccount)$ command is executed. That is, it processes threshold
    decryption of $\ckey$ which can now succeed as $\ckey$ contains a real
    user's key $\key$ and not a dummy.
  \item[{Hybrid 4 to Hybrid 5.}] Indistingushiability of the hybrids follows
    from the partial decryption simulatability of the threshold encryption
    scheme.
  \item[{Hybrid 6.}] In this hybrid the simulator changes its behavior when
    command $\traceAccounts$ is executed. That is, it outputs the real output
    of $\func{mpcprf}$ instead of programming its output. This is possible,
    since $\ckey$ consists of the real key not a dummy.
  \item[{Hybrid 5 to Hybrid 6.}] The indistinguishability of the hybrids is
    perfect as simulatability of $\func{mpcprf}$ is perfect.
  \item[{Hybrid 7.}] In the last hybrid the simulator changes its behavior when
    computing zero knowledge proofs. Now the simulator knows all parts of
    witnesses corresponding to the proven statements, thus it can compute the
    proofs honestly (using functionality $\func{nizk}$).
  \item[{Hybrid 6 to Hybrid 7.}] The hybrids are indistinguishable as in the
    zero-knowledge proof systems simulated proofs are indistinguishable from
    real ones. Now the simulator presents a view which is exactly the view of
    the execution of the real protocol.
  \end{description}
  Since all hops from one hybrid to another leaves the adversary with only
  negligible probability of distinguishing them, also the first and the final
  hybrids are distinguishable with negligible probability only. Hence, the
  simulator succeeds. \qed
\end{proof}

\subsection{Joint functionality for identity issuance and policy assignment}
\begin{funcbox}{Identity issuance functionality
    $\func{idpol}^{\BSIG, \SIG, \TENC, \ENC, \thresholdar, \noofar}$} The
  functionality is parametrized by
  \begin{itemize}
  \item Blind signature scheme $\BSIG$,
  \item Signature scheme $\SIG$
  \item $(\thresholdar, \noofar)$-Threshold encryption scheme $\TENC$,
  \item Encryption scheme $\ENC$.
  \item Hard relation $\REL$.
  \end{itemize}

  \paragraph{Setup}
  On $(\setupStart)$ from any party
  \begin{itemize}
  \item Generate public parameters by running
    $\pp_{idpol} \sample (\TENC.\sgen(\secparam), \BSIG.\sgen(\secparam), \SIG.\sgen
    (\secparam), \ENC.\sgen (\secparam))$;
  \item Send $(\setupReady, \pp_{idpol})$ to all parties and set
    $\flag{setupReady} = \true$.
  \end{itemize}


  \paragraph{Initialize}
  \subparagraph{Identity provider initialization}
  On input $(\initialize, \pk, \sk)$ from an identity provider $\idprov$,
  ignore if the party has been already initialized, or $\flag{setupReady} =
  \false$.
  \begin{itemize}
  \item If $\REL_{bsig}(\pk_{idprov}, \sk_{idprov}) = 1$, then store $(\idProvInitialized,
    \idprov, (\sk_{idprov}, \pk_{idprov}))$. Send $(\idProvInitialized, \idprov,
    \pk_{idprov})$ to $\idprov$ and $\adv$.
  \item set $\flag{ready} = \true$ if all identity providers were initialized.
  \end{itemize}

  \subparagraph{Policy assigner initialization} Upon input
  $(\initialize, (\SIG.\pk_\polas, \SIG.\sk_\polas), (\ENC.\sk_\polas,
  \ENC.\pk_\polas) )$ from a policy assigner $\polas$.
  \begin{itemize}
\item Ignore if
  \begin{itemize}
  \item $\polas$ has already been initialized,
  \item $\flag{setupReady} = \false$, or
  \item $(\SIG.\pk_{\polas}, \SIG.\sk_{\polas})$ does not fulfill the relation
    defined by $\SIG.\kgen(\pp_{pol})$;
  \item $(\ENC.\pk_{\polas}, \ENC.\sk_{\polas})$ does not fulfill the relation
    defined by $\ENC.\kgen(\pp_{pol})$;
  \end{itemize}
\item Else
  \begin{itemize}
  \item store $(\polas, (\SIG.\pk_{\polas}, \SIG.\sk_{\polas}), (\ENC.\pk_{\polas}, \ENC.\sk_{\polas}) )$,
  \item output $(\partyInitialized, \SIG.\pk_{\polas}, \ENC.\pk_{\polas}, \polas)$ to
    $\polas$ and $\adv$.
  \end{itemize}
\item If all policy assigners have been initialized, set $\flag{ready} =
\true$.
\end{itemize}

\subparagraph{User initialization}
On $(\initialize)$ from a user
\begin{itemize}
\item Ignore if
   \begin{itemize}
   \item $\user$ has been initialized;
   \item $\flag{setupReady} = \false$;
   \end{itemize}
 \item Else
   \begin{itemize}
   \item Output $(\partyInitialized)$ to $\adv$ and $\user$.
   \end{itemize}
 \end{itemize}

\paragraph{Identity issuance}
On input
$(\issueIdentity, (c, m, r, (\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar})), \aux_{sig},
(\sk_{\user}, \pk_{\user}), \idprov)$ from a user $\user$ and
$(\issueIdentity, \user, (\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}))$ from $\idprov$:
\begin{itemize}
\item If $\flag{ready} = \false$, then ignore;
\item If $\REL_{user}(\sk_{\user}, \pk_{\user}) = 0$ or
  $c \neq \TENC.\enc((\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}), m; r)$;
\item Else, compute
  $\signature_{id} \gets \BSIG.\sign((\sk_{\user}, m, \aux_{sig}), \sk_{\idprov})$;
\item Output $\signature_{id}$ to $\user$ and $(\pk_{\user}, c)$ to
  $\idprov$.
  %\michals{10.12}{$\aux$ here is the attribute list}
  \end{itemize}

 \paragraph{Attributes check}
 On input $(\checkAttributes, \polas)$ from user $\user$ and
 $(\checkAttributes, \user, \alpolicy)$ from policy assigner $\polas$.
 \begin{itemize}
 \item Read stored $\aux_{sig}$, abort if no $\aux_{sig}$ is stored for user $\user$.
 \item Send to adversary $(\length{\alpolicy}, \pAL, \pk_{idprov}, \pk, l_{enc} =
   \length{\ENC.\enc(\alpolicy)}, \pk_{\polas})$.
   \michals{5.1}{added some adversarial leakage, which the adversary learns in case
     of the protocol from the fact that the protocol leaks the statement proven in a
     NIZK way}
 \item If $\alpolicy (\aux_{sig}) = 0$ then send to $\user$
   $(\attributesNotValid, \user, \polas, \alpolicy)$ and to the adversary
   $(\attributesNotValid, \user, \polas)$ exit, else;
 \item Store $(\attributesValid, \user, \aux_{sig}, (\pk, \sk))$ and send
   $(\attributesValid, \user, \alpolicy, \polas)$ to the user and
   $(\attributesValid,  \user, \polas)$ to the adversary. \michals{4.1}{Added
     $\alpolicy$ to user's output, so the user learns what attribute policy it had
     assigned}
 \end{itemize}

\paragraph{Issue policy}
On input $(\issuePolicy, \polas, \aux_{sig})$ from user $\user$ and
$(\issuePolicy, \user, \comppolicy, \alpolicy)$ from $\polas$ (or
$(\issuePolicy, \user, \comppolicy, \alpolicy, \signature_{comp})$ if $\polas$ is
corrupted)
\begin{itemize}
\item Check whether $(\attributesValid,  \user, \aux_{sig}, (\pk, \sk))$ is stored and
  abort if it is not, in that case output $(\attributesNotVerified)$.
\item Send to adversary $(\length{\comppolicy})$.
\item Store $(\policyAssigned, \user, \polas, \comppolicy)$ and output
  $(\policyAssigned, \user, \polas)$ to the adversary.
\item If $\polas$ corrupted, verify that $\SIG.\verify(\pk_{\polas},
  \signature_{comp}, (\comppolicy, \alpolicy, \pk)) = 1$ and abort if that is not the case.
\item If $\polas$ not corrupted, compute $\signature_{comp} \gets
  \SIG.\sign(\sk_{\polas}, (\comppolicy, \alpolicy, \pk))$
\item Output $(\policyAssigned, \paux, \pk, \paux_{sig}, \length{\saux_{sig}})$ \michals{17.12}{Do we need to
    reveal so much about the party that got the policy assigned? Could we do without
    revealing, say $\pAL$ -- that is reveal it only to the policy assigner, but not
    to the adversary?} to $\adv$ (or
  $(\policyAssigned, \aux, \paux_{sig}, \saux_{sig}, \comppolicy, \alpolicy, \signature_{comp})$ if $\polas$ or
  $\user$ is corrupted); $(\policyAssigned)$ to $\polas$; and
  $(\policyAssigned, \comppolicy, \signature_{comp})$ to $\user$.
\end{itemize}
\end{funcbox}

\begin{protbox}{Protocol $\prot{idpol}^{\BSIG, \SIG, \TENC, \ENC, \thresholdar, \noofar}$}
  The protocol operates in the
  $\smallset{\func{smt}, \func{nizk}, \func{reg}}$-hybrid model and uses the
  following cryptographic primitives:
  \begin{itemize}
  \item Blind signature scheme $\BSIG$,
  \item Signature scheme $\SIG$
  \item $(\thresholdar, \noofar)$-Threshold encryption scheme $\TENC$,
  \item Encryption scheme $\ENC$.
  \item Hard relation $\REL$.
  \end{itemize}

  \paragraph{Setup}
  \begin{itemize}
  \item On input $(\setupStart)$ use $\func{pp}^{\TENC.\sgen, \secpar}$,
    $\func{pp}^{\ENC.\sgen, \secpar}$, $\func{pp}^{\BSIG.\sgen, \secpar}$,
    $\func{pp}^{\SIG.\sgen, \secpar}$ to generate public parameters $\pp$ and
    publicize it to all parties.
  \item Send $(\setupReady, \pp_{idpol})$ to all parties and set
    $\flag{setupReady} = \true$.
  \end{itemize}

  \paragraph{Initialize}
  \subparagraph{Identity provider initialization} On input
  $(\initialize, (\sk_{idprov}, \pk_{idprov}))$ the identity provide
  \begin{itemize}
  \item check if the key pair has correct distribution with respect to
    $\BSIG.\kgen(\pp)$ and ignore if that is not the case,
  \item else, store $(\sk_{idprov}, \pk_{idprov})$ and send
    $(\register, \sk_{idprov}, \pk_{idprov})$ to $\func{reg}$,
  \item output $(\partyInitialized, \pk_{idprov}, \idprov)$ to $\idprov$.
  \end{itemize}


  \subparagraph{Policy assigner initialization} On
  $(\initialize, (\SIG.\pk_{\polas}, \SIG.\sk_{\polas}), (\ENC.\pk_{\polas},
  \ENC.\sk_{\polas}))$ the policy assigner checks if the key pairs have correct
  distribution with respect to $\SIG.\kgen(\pp_{pol})$ and $\ENC.\kgen
  (\pp_{pol})$. If it does, store
  $(\SIG.\pk_{\polas}, \SIG.\sk_{\polas}), (\ENC.\pk_{\polas}, \ENC.\sk_{\polas})$
  and send to $\func{reg}$:
  \begin{itemize}
  \item $(\register, \SIG.\pk_{\polas}, \SIG.\sk_{\polas})$,
  \item $(\register, \ENC.\pk_{\polas}, \ENC.\sk_{\polas})$
  \end{itemize}
  Output $(\partyInitialized, \SIG.\pk_{\polas}, \ENC.\pk_{\polas}, \polas)$ to $\polas$.

  \subparagraph{User initialization} On
   $(\initialize, (\pk, \sk), \aux_{sig})$
  \begin{itemize}
  \item Check whether $(\pk, \sk) \in \REL$ and ignore if that is not the case.
  \item Register $\pk$ at $\func{reg}$ by sending $(\register, (\pk, \sk))$.
  \item Output $(\partyInitialized, \pk)$ to $\user$.
  \end{itemize}

  \paragraph{Identity issuance}
  \begin{itemize}
  \item On input $(\issueIdentity, (c, m, r, (\pk_{\ar_1}, \ldots,
    \pk_{\ar_\noofar})), \aux_{sig}, (\pk_\user, \sk_\user), \idprov)$ to the user
    $\user$ and an input $(\issueIdentity, \user, (\pk_{\ar_1}, \ldots,
    \pk_{\ar_\noofar}))$ to the identity provider:
    \begin{enumerate}
    \item The user
      \begin{itemize}
      \item gets $\pk_{idprov}$ from $\func{reg}$;
      \item Computes $\signature_1 = \prepsign(\pk_{idprov}, (\sk_{\user}, m,
        \aux), r')$;
      \item Sends $(\proveStatement, (\pk_{\user}, \signature_1, c, \aux_{sig}, \pp),
        (\sk_{\user}, m, r, r'))$ for relation $\REL_{sign}$; \pccom{The user shows
          that $c$ contains valid encryption of its credentials and it knows a valid
          secret key for its public key.}
      \item Upon receiving the proof $\zkproof$ from the functionality, sends
        $(\send, \idprov, (\pk_{\user}, \signature_1, c, \aux_{sig}, \pp),
        \zkproof)$ to $\func{smt}$;
      \end{itemize}
    \item Upon receiving $(\sent, \user, ((\pk_{\user}, \signature_1, c, \aux_{sig},
      \pp), \zkproof))$ from $\func{smt}$, the identity provider $\idprov$:
      \begin{itemize}
      \item Inputs $(\verifyProof, (\pk_{\user}, \signature_1, c, \aux_{sig}, \pp),
        \zkproof)$ to $\func{nizk}^{\REL_{sign}}$.
      \item If the NIZK functionality approves the proof, compute $\signature_2
        \gets \blindsign(\sk_{idprov}, \signature_1)$;
      \item Send $\signature_2$ to $\user$ using $\func{smt}$;
      \end{itemize}
    \item User $\user$ unblinds the signature by running
      $\unblind(\signature_2, r')$ and gets the signature $\signature$ on
      $(\sk_\user, m, \aux)$.
    \end{enumerate}
  \end{itemize}

\paragraph{Attributes check}
\subparagraph{User's actions} On
$(\checkAttributes, \polas)$.
On $(\alpolicy)$ sent by $\polas$ via $\func{smt}$,
  \begin{itemize}
  \item if $\alpolicy (\aux_{sig}) = 0$ then output $(\attributesNotValid, \user,
    \polas, \alpolicy)$; \michals{4.1}{Actually, I am not sure how this
      message should be handled. Do we need to send anything to the polas /
      functionality}
    \michals{4.1}{After consulting DGKOS20 -- what is returned in the protocol is
      what functionality returns to the calling party}
  \item else call $\func{nizk}^{\REL_{al}}$ on
    $(\proveStatement, ((\paux_{sig}, \pk_{\idprov}, \pk, c, \pk_{\polas}), (\saux_{sig},
    \alpolicy, \signature_{id}, \sk)))$ to get proof $\zkproof_{al}$;
  \item send $((\paux_{sig}, \pk_{\idprov}, \pk, c, \pk_{\polas}), \zkproof_{al})$ to
    the policy assigner using $\func{smt}$.
  \item get $(\attributesValid, \user, \polas, \alpolicy)$ from the policy assigner.
  \end{itemize}

  \subparagraph{Policy assigner's actions}
  On $(\checkAttributes, \user, \alpolicy)$
  \begin{itemize}
  \item if there is $(\alpolicy', \user)$ stored and $\alpolicy \neq alpolicy$ then abort
  \item send $(\alpolicy)$ to user $\user$ via $\func{smt}$;
  \item on $(\attributesNotValid, \user, \polas, \alpolicy)$ from $\user$, abort;
  \item get user's public key $\pk$ from $\func{reg}$;
  \item on $((\paux_{sig}, \pk_{\idprov}, \pk, c, \pk_{\polas}), \zkproof_{al})$ from
    user $\user$, call
    $\func{nizk}^{\REL_{al}} (\verifyProof, (\paux_{sig}, \pk_{\idprov}, \pk, c,
      \pk_{\polas}), \zkproof_{al}))$ and abort if the proof does not verify;
  \item abort if $\pk_{idprov}$ is not valid identity provider's public key; else
  \item send $(\attributesValid, \user, \polas, \alpolicy)$ to $\user$.
  \item save $(\alpolicy, \user)$.
  \end{itemize}

\paragraph{Policy issuance}
\subparagraph{User's actions} On
$(\issuePolicy, \polas, \aux_{sig})$
\michals{28.12}{Changed functionality input. Important, seems that we need idprov's
  signature on AL, otherwise a malicious user could generate it by its own.}
\begin{itemize}
\item Parse $\aux_{sig} = (\paux_{sig}, \saux_{sig})$, where $\paux_{sig}$ is the public part of the input
  and $\saux_{sig}$ the private part.
\item Send $(\issuePolicy)$ to $\polas$ using $\func{smt}$.
\item On $(\comppolicy, \signature_{comp})$ that $\polas$ sent by $\func{smt}$, store the
  message.
\end{itemize}

\subparagraph{Policy assigner actions} On $(\issuePolicy, \user, \comppolicy)$
\begin{itemize}
\item If $\user$ has no $\alpolicy$ assigned, then abort, else read $\alpolicy$.
\item Compute
  $\signature_{comp} \gets \SIG.\sign(\sk_{polas}, (\comppolicy, \alpolicy, \pk))$;
\item Send $(\comppolicy, \signature_{comp})$ to the user using $\func{smt}$.
\end{itemize}
\end{protbox}

\subsubsection{Security proof for $\prot{idpol}$}
\michals{4.1}{Need to check whether what protocol outputs matches with what ideal
  functionality outputs. For example, the protocol uses $\func{nizk}$ which reveals
  proven statement to the adversary -- we need to make sure that the functionality reveals
the same information.}
\begin{simbox}{Simulator $\simulator_{idpol}$}
  \paragraph{Setup}
  \begin{enumerate}
  \item Honest party $\party$, on $(\setupStart, \pp_{pol})$ from the
  functionality
    \begin{itemize}
    \item \hl{set up all simulated functionalities according to $\pp_{pol}$}
    \end{itemize}
  \item Dishonest party $\party$, on $(\generatePP)$ to $\func{pp}^{\ggen,
  \secpar}$.
    \begin{itemize}
    \item Send $(\setupStart)$ to the functionality.
    \end{itemize}
  \end{enumerate}

  \paragraph{Initialize}
  \michals{30.12}{Need to change that due to changes in the functionality inputs}
  \subparagraph{Identity provider initialization}
  \begin{enumerate}
  \item Honest $\idprov$ on $(\partyInitialized, (\pk_{idprov}))$
    \begin{itemize}
    \item Pick randomly $\sk_{idprov}$ and simulate calling $\func{reg}$ on
      $(\register, (\SIG.\sk_{idprov}, \SIG.\pk_{idprov}))$.
    \item Add $\idprov$ to the set of initialized parties.
    \end{itemize}
  \item Dishonest $\idprov$ on $(\register (\pk_{idprov}, \sk_{idprov}))$ sent by
    $\idprov$ to $\func{reg}$
    \begin{itemize}
    \item Ignore if $(\pk_{idprov}, \sk_{idprov}) \not\in \IM (\SIG.\kgen)$, the user
      has already been initialized, or $\flag{setupRead} = \false$.
    \item Else, input to $\func{\PPCTS}$ command $(\initialize, (\pk_{polas}, \sk_{polas}))$
    \end{itemize}
  \end{enumerate}

  \subparagraph{Policy assigner initialization}
  \begin{enumerate}
  \item Honest policy assigner $\polas$, on
    $(\partyInitialized, \SIG.\pk_{\polas}, \ENC.\pk_{polas}, \polas)$ from the functionality
    \begin{itemize}
    \item Pick randomly $\SIG.\sk_{\polas}$ and simulate calling $\func{reg}$ on
      $(\register, (\SIG.\pk_{\polas}, \SIG.\sk_{\polas}))$.
    \item Pick randomly $\ENC.\sk_{\polas}$ and simulate calling $\func{reg}$ on
      $(\register, (\ENC.\pk_{\polas}, \ENC.\sk_{\polas}))$.
    \item Add $\polas$ to the set of initialized parties
      $\partyset{Init}$. \michals{17.12}{Do we need to keep the party set Init?}
    \end{itemize}
  \item Dishonest policy assigner $\polas$, on
    $(\register, (\SIG.\pk_{polas}, \SIG.\sk_{polas})$ sent by $\user$ to $\func{reg}$,
    \begin{itemize}
    \item Ignore if $(\SIG.\pk_{polas}, \SIG.\sk_{polas}) \not\in \IM (\SIG.\kgen)$, the user has already been initialized, or
      $\flag{setupRead} = \false$.
    \end{itemize}
    On $(\register, (\ENC.\pk_{polas}, \ENC.\sk_{polas})$ sent by $\user$ to
    $\func{reg}$
    \begin{itemize}
    \item Ignore if $(\ENC.\pk_{polas}, \ENC.\sk_{polas}) \not\in \IM (\ENC.\kgen)$
    \item Else, input to $\func{\PPCTS}$ command
    $(\initialize, (\SIG.\pk_{polas}, \SIG.\sk_{polas}), (\ENC.\pk_{polas},
    \ENC.\sk_{polas}))$ and add $\user$ to the set of initialized parties.
    \end{itemize}
  \end{enumerate}

  \subparagraph{User initialization}
  \begin{enumerate}
  \item Honest user $\user$, on $(\partyInitialized, \pk)$
    \begin{itemize}
    \item Pick randomly $\sk$ and simulate calling $\func{reg}$ on $(\register, (\pk,
      \sk))$. \pccom{Note that with overwhelming probability $(\REL(\pk, \sk) = 0$
        hence the simulator has to simulate $\func{reg}$ instead of running it honestly}
    \end{itemize}
  \item Dishonest user $\user$, on $(\register, (\pk, \sk))$ sent by $\user$ to
    $\func{reg}$,
    \begin{itemize}
    \item Ignore if $(\pk, \sk) \in \REL$, the user has already been initialized, or
      $\flag{setupRead} = \false$.
    \item Else, input to $\func{\PPCTS}$ command $(\initialize, (\pk, \sk))$
    \end{itemize}
  \end{enumerate}

  \paragraph{Identity issuance}
  \begin{enumerate}
  \item Honest user $\user$ and identity provider $\idprov$. \michals{4.1}{Both in
      our functionality and in DGKOS20 the adversary learns nothing while honest user
    talks with an honest identity provider. OTOH DGKOS20 also doesn't consider a case
    of both parties honest.}
  \michals{5.1}{To my understanding, it is fine to not write a proof for
    honest-honest case as long as the adversary doesn't learn anything from the functionality}
\item Honest user $\user$ and malicious identity provider $\idprov$.
  \begin{itemize}
  \item on behalf of $\idprov$ send to $\func{idpol}$ input $(\issueIdentity, \user,
    (\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}))$;
  \item make a simulated signature $\signature_1$ and then a simulated proof
    $\zkproof$ for $(\pk_{\user}, \signature_1, c, \aux_{sig}, \pp)$ using
    $\func{nizk}^{\REL_{sign}}$;
  \item on $\signature_2$ sent by the identity provider, unblind the signature and
    obtain $\signature_{id}$.
  \item Output $\signature_{id}$ to $\user$.
  \end{itemize}
  \item Malicious user $\user$ and honest identity provider $\idprov$.
    \begin{itemize}
    \item On $(\proveStatement, (\pk_{\user}, \signature_1, c, \aux_{sig}, \pp),
      (\sk_{\user}, m, r, r'))$ sent by the user to $\func{nizk}^{\REL_{sign}}$, pass
      it to the functionality and return the proof $\zkproof$.
    \item Run extractor on $\zkproof, (\pk_{\user}, \signature_1, c, \aux_{sig},
      \pp)$ and reveal the witness. If the witness is invalid output $\fail$.
    \item Else, send to $\func{idpol}$ $(\issueIdentity, (c, m, r, (\pk_{\ar_1},
      \ldots, \pk_{\ar_{\noofar}})), \aux_{sig}, (\sk_{\user}, \pk_{\user}),
      \idprov)$ on behalf of $\user$.
    \item Get from $\func{idpol}$ signature $\signature_{id}$ and compute simulated
      signature $\signature_2$ which unblinded gives
      $\signature_{id}$. \pccom{Security of this step follows from the
        simulatability of the signature scheme}
      \michals{4.1}{Check this step -- does the simulator needs to know
        $\signature_{id}$ to compute $\signature_2$?}
    \end{itemize}
  \item Malicious user $\user$ and identity provider $\idprov$. We do not consider
    this case. If user and identity provider collude then the user could have
    assigned any identity it wants.
  \end{enumerate}

  \paragraph{Attributes check}
  \begin{enumerate}
  \item Honest user $\user$ and policy assigner $\polas$. On $(l_{alpolicy}, \pAL,
    \pk_{idprov}, \pk, l_{enc}, \pk_{\polas})$
    \begin{enumerate}
    \item On $(\attributesNotValid, \user,
    \polas)$ from the functionality \michals{5.1}{Do I need to reveal $\user$ here?}
    \begin{itemize}
    \item Pick random policy $\alpolicy'$ of length $l_{alpolicy}$.
    \item Using $\func{smt}$ send $(\alpolicy')$ to $\user$.
    \item Output $(\attributesNotValid, \user, \polas)$
    \end{itemize}
    \item On $(\attributesValid, \user, \polas)$
    \begin{itemize}
    \item Pick random policy $\alpolicy'$ of length $l_{alpolicy}$.
    \item Using $\func{smt}$ send $(\alpolicy')$ to $\user$.
    \item Compute simulated proof $\zkproof_{al}$ for statement
      $\REL_{al} ((\pAL, \pk_{idprov}, \pk, c, \pk_{\polas}), (\sAL, \alpolicy',
      \signature_{id}, \sk, \key))$, for some randomly picked
      $\sAL, \signature_{id}, \sk, \key$ and $c$ being an encryption of
      $\alpolicy'$,\michals{29.12}{Problem, the simulator picks randomly $\alpolicy'$
        but later has to make a zkproof that reveals $\alpolicy$.}
      \michals{30.12}{Solution -- put in the instance only encryption (under PA's
        public key) of the alpolicy}
    \item Send the proof to the policy assigner $\polas$.
    \item Simulate proof verification by $\polas$.
    \item If the proof verifies correctly, send $(\attributesValid, \user, \polas)$ to user
      $\user$.
    \end{itemize}
  \end{enumerate}

  \item Honest user $\user$ and malicious policy assigner $\polas$. On
    $(\alpolicy)$ sent by the policy assigner via $\func{smt}$.
    \begin{itemize}
    \item Input $(\checkAttributes, \user, \alpolicy)$ to the functionality
      $\func{\PPCTS}$ on behalf of $\polas$.
    \item On $(\attributesValid, \user, \polas)$ from the functionality
      \begin{itemize}
      \item compute simulated proof $\zkproof_{al}$ for statement
        $\REL_{al} ((\pAL, \pk_{idprov}, \pk, c, \pk_{\polas}), (\sAL, \alpolicy,
        \signature_{id}, \sk, \key))$, for some randomly picked
        $(\sAL, \alpolicy, \signature_{id}, \sk, \key)$ and
        $c = \ENC.\enc(\alpolicy)$
      \item Send the proof to the policy assigner $\polas$.
      \item If the proof verifies correctly, send
        $(\attributesValid, \user, \alpolicy)$ to user $\user$.
      \end{itemize}
      \item On $(\attributesNotValid, \user, \polas)$, output $(\attributesNotValid,
        \user, \polas)$ to the user.
      \end{itemize}

    \item Malicious user $\user$ and honest policy assigner $\polas$.
      \begin{enumerate}
      \item On $(\attributesNotValid, \user, \polas, \alpolicy)$
        \begin{itemize}
        \item Input to $\func{\PPCTS}$
          $(\checkAttributes, \polas, \AL, (\pk, \sk), (\pk_{id},
          \signature_{id}, \key))$ on behalf of user.
        \item Pick a random policy $\alpolicy'$ and send it via $\func{smt}$ to
          $\user$.
        \item On $(\attributesNotValid, \user, \polas)$ from the functionality, read
          $(\attributesNotValid, \user, \polas, \alpolicy)$ sent by the functionality
          to $\user$ and exit.
        \item Else, on $(\attributesValid,  \user, \polas)$ from the
          functionality, read $(\attributesValid, \user, \polas, \alpolicy)$
          sent by the functionality to $\user$. \michals{4.1}{That's how the
            simulator can learn $\alpolicy$ sent to a malicious party.}
        \item Make simulated proof $\zkproof_{al}$ for instance
          $(\paux_{sig}, \pk_{\idprov}, \pk, c, \pk_{\polas})$ using simulated
          functionality $\func{nizk}^{\REL_{al}}$, here $c$ is an encryption of
          $\alpolicy$ under $\polas$ public key.
        \end{itemize}
      \item On $((\paux_{sig}, \pk_{\idprov}, \pk, c, \pk_{\polas}), \zkproof_{al})$ sent to
        $\polas$
        \begin{itemize}
        \item Abort if the proof does not verify.
        \item Abort if $\pk_{idprov}$ is not a valid public key of the identity provider.
        \item Else, extract witness $(\saux_{sig}, \alpolicy, \signature_{id}, \sk)$ if
          this fails output $\fail$.
        \item Extract $\alpolicy$ from $c$.
        \item Send to $\func{idpol}$ input $(\checkAttributes, \polas)$.
        \item Send $(\attributesValid, \user, \polas, \alpolicy)$ to $\user$.
        \end{itemize}
      \end{enumerate}

  \item Malicious user $\user$ and policy assigner $\polas$. We do not allow both $\user$
    and $\polas$ to be corrupted at the same time. This would allow the adversary to have
    accepted attribute list that was not certified by the identity provider.
  \end{enumerate}

  \paragraph{Issue policy}
  \begin{enumerate}
  \item Honest user $\user$ and policy assigner $\polas$.
    \begin{itemize}
    \item Check if there is stored $(\alpolicy, \user)$; if not, abort; else read
      $\alpolicy$.
    \item Get $(l_{comppolicy})$ from $\func{idpol}$.
    \item Pick a random policy $\comppolicy'$ of size $l_{comppolicy}$.
    \item On $(\policyAssigned, \user, \polas)$ from $\func{idpol}$
      \begin{itemize}
      \item send $(\issuePolicy)$ to $\polas$ on behalf of $\user$;
      \item on behalf of $\polas$ compute
        $\signature_{comp} \gets \SIG.\sign(\sk_{polas}, (\comppolicy, \alpolicy,
        \pk))$
      \end{itemize}
    \end{itemize}

  \item Honest $\user$ and malicious policy assigner $\polas$.  On
    $(\comppolicy, \signature_{comp})$ sent by $\polas$ to $\user$ using $\func{smt}$;
    \begin{itemize}
    \item Call $\func{idpol}$ on $(\issuePolicy, \user, \comppolicy)$ on behalf of
      $\polas$.
    \item Send to $\polas$ via $\func{smt}$ $(\issuePolicy)$,
    \end{itemize}

  \item Malicious $\user$ and honest policy assigner $\polas$.  On
    $(\send, \polas, \issuePolicy)$ sent by $\user$ to $\polas$ by $\func{smt}$
    \begin{itemize}
    \item Call the functionality $\func{idpol}$ on $(\issuePolicy, \polas, \AL)$ for
      $\AL$ stored by the simulator.
    \item Abort if there is no stored $(\alpolicy, \user)$.
    \item Pick a random compliance policy $\comppolicy'$ and send
      $(\comppolicy', \signature_{comp} \gets \SIG.\sign(\sk_{polas}, (\comppolicy',
      \alpolicy, \pk)))$ via $\func{smt}$ to $\user$.
    \end{itemize}

  \item Malicious $\user$ and policy assigner $\polas$. We do not allow both $\user$ and
    $\polas$ to be corrupted at the same time.
  \end{enumerate}
\end{simbox}

\begin{theorem}[$\prot{idpol}$ securely realizes $\func{idpol}$]
  Let $\SIG$ be existentially unforgeable signature scheme, then $\prot{pol}$
  securely realizes $\func{idpol}$ in the $\smallset{\func{pp}, \func{srs},
  \func{reg}, \func{smt}}$-hybrid model.
\end{theorem}

\begin{proof}
  We note that, except the case of honest user and policy assigner, the
  simulator simulates perfectly as it only verify given signature (what is also
  done in $\func{idpol}$) and send input messages using $\func{smt}$. Hence, the
  adversary could only distinguish the real and ideal world in case of honest
  user and policy assigner. However, a adversary that tells whether
  $\func{smt}$ transfers a random message $m$ (resp.~$m'$) or user's
  credentials (resp.~assigned policy) breaks security of $\func{smt}$ what
  happens with negligible probability only. \qed
\end{proof}

\section{Conclusion}

\antoines{24.08}{TODO}

\bibliographystyle{alpha}
\bibliography{../cryptobib/abbrev1,../cryptobib/crypto,references}

\appendix
\section{Additional functionalities}
\paragraph{NIZK functionality} The functionality describes an ideal execution
of a NIZK system. That is, a valid statement is always accepted by the
functionality, no party can make the functionality accept an invalid statement,
no information about the statement's witness are revealed.

\begin{funcbox}{NIZK functionality $\func{nizk}^{\REL}$} Functionality is
  parametrised by a relation $\REL$.
  \begin{description}
  \item[Proving statements] On $(\proveStatement, \inp, \wit)$ from party
    $\party$:
    \begin{itemize}
    \item Check whether $(\inp, \wit) \in \REL$ and, if that is not the case,
      ignore.
    \item Else send $(\proveStatement, \inp)$ to $\adv$ and wait for answer
      $(\statementProven, \zkproof)$.
    \item Store $(\inp, \zkproof)$, send $(\statementProven, \zkproof)$ to
      $\party$.
    \end{itemize}
  \item[Verifying statements] On $(\verifyProof, \inp, \zkproof)$ from party
    $\party$:
    \begin{itemize}
    \item Check whether $(\inp, \zkproof)$ is stored. If not, send
      $(\giveWitness, \inp)$ to $\adv$.
    \item On answer $\wit$, check whether $(\inp, \wit) \in \REL$.  If that is
      the case store $(\inp, \zkproof)$.
    \item If there is $(\inp, \zkproof)$ stored, send $(\statementVerified,
      1)$.  Otherwise send $(\statementVerified, 0)$.
    \end{itemize}
  \end{description}
\end{funcbox}

\paragraph{SRS functionality}
The functionality assures secure generation of the SRS.
\begin{funcbox}{SRS functionality $\func{srs}^{\kgen, \kgens, \secpar}$}
  \begin{enumerate}
  \item On input $(\generateMasterSRS)$,
    \begin{itemize}
    \item generate $\srs \sample \kgen(\secpar)$,
    \item broadcast $\srs$ to all parties.
    \end{itemize}
  \item On input $(\generateSpecializedSRS, \REL)$
    \begin{itemize}
    \item generate $\srss \sample \kgens(\REL)$
    \item broadcast $\srss$ to all parties.
    \end{itemize}
  \end{enumerate}
\end{funcbox}

\michals{12.08}{Check! changed functionality to cover two part SRS generation}


\paragraph{Public parameter functionality}
The functionality assures secure generation of the public parameters. For a list of
protocols $p_1, p_2, \ldots$ the functionality runs $p_i.\sgen(\secparam)$ and outputs the
resulting public parameters.
\begin{funcbox}{Public parameters functionality $\func{pp}^{(p_1, p_2, \ldots, p_n), \secpar}$}
  On input $(\generatePP)$, if that is the first time this input has been given, generate
  $\pp_i \sample p_i.\sgen(\secparam)$, for $i \in \range{1}{n}$ and broadcast $\pp_i$ to
  all parties. Ignore further $(\generatePP)$ queries.
\end{funcbox}

\paragraph{Register functionality}
The functionality is responsible for receiving and storing users public and
secret keys. It assures that no party can change its key-pair and all the
parties retrieves the public keys they request.
\begin{funcbox}{Register functionality $\func{reg}$}
  \begin{description}
  \item[Registration] Upon receiving $(\register, \sk_\party, \pk_\party)$ from
    party $\party$, keep $(\party, \sk_\party, \pk_\party)$ and return
    $(\initialized, \party)$ if that is the first request from $\party$.
    Otherwise ignore.
  \item[Retrieval] Upon receiving $(\retrieve, \party')$ from some party
    $\party$ or the adversary, output $(\retrieve, \party', \pk_{\party'})$ to
    $\party$. $\pk_{\party'}$ is set to $\bot$ if no record $(\party',
    \sk_{\party'}, \pk_{\party'})$ exists.
  \end{description}
\end{funcbox}

\paragraph{Secure messaging functionality}
This functionality assures that two parties can securely -- confidentially and
robustly -- exchange messages.
\begin{funcbox}{Secure message transfer functionality $\func{smt}$} On input
  $(\send, \party', m)$ from a party $\party$:
  \begin{itemize}
  \item If both parties $\party$ and $\party'$ are honest, output $(\sent,
    \party, m)$ to $\party'$ and $(\sent, \party, \party', \abs{m})$ to $\adv$.
  \item Otherwise, output $(\sent, \party, \party', m)$ to $\adv$.
  \end{itemize}
\end{funcbox}

\paragraph{Anonymous messaging functionality}
The functionality behaves similarly to $\func{smt}$ however it offers extra
privacy as the recipient does need to learn who is the message sender. Importantly, the
receiver is able to send a response to the sender using the functionality.

\begin{funcbox}{Anonymous messaging functionality $\func{amt}$} On input
  $(\sendAnonymously, \party', mid, m)$ from a party $\party$:
  \begin{itemize}
  \item If both parties are honest, output $(\sentAnonymously, mid, m)$ to $\party'$
    and $(\sentAnonymously, \party', \abs{m})$ to the adversary. Store $(\party, \party', mid)$
  \item If the receiving party is corrupted, output $(\sentAnonymously,
    \party', mid, m)$ to $\adv$.
  \item If the sending party is corrupted, output $(\sentAnonymously, \party,
    \party', m, mid)$ to $\adv$.
  \end{itemize}
  On input $(\return, mid, m')$ from party $\party'$,
  \begin{itemize}
  \item Check whether there is $(\party, \party', mid)$ stored and abort if that is not
    the case;
  \item Else, send $(\returned, mid, m')$ to $\party$.
  \end{itemize}
\end{funcbox}
\paragraph{MPC PRF functionality}
The functionality allows the parties who hold shares of a PRF's secret key to
evaluate the function on given input.

\begin{funcbox}{PRF functionality $\func{mpcprf}$}
  % \michals{9.03}{We need this functionality to allow the simulator to know
  %   the secret keys of users. Otherwise it would not be able to tell which
  %   user's anonymity is to be revoken}
  The function interacts with parties $\party_1, \ldots, \party_\noofparties$
  and is parametrized by
  \begin{itemize}
  \item Constants $\threshold$, $\noofparties$, $\maxacc$;
  \item ($\threshold, \noofparties)$-secret sharing scheme $\SS$,
  \item PRF function $\prf$;
  \end{itemize}

  Upon input $(\compute, \key_i, \aux)$ from at least $\threshold + 1$ parties
  $\party_i$:
  \begin{itemize}
  \item Compute $\key = \reconstruct(\key_{i_1}, \ldots, \key_{i_{\threshold +
        1}})$;
  \item Evaluate $\prf_\key(x)$ on all $x \in \range{1}{\maxacc}$;
  \item Return the list of outputs to all requesters $\party_i$, $i \in
  \range{1}{\noofparties}$.
  \end{itemize}
\end{funcbox}

\paragraph{Ledger functionality}
The functionality describes how ideal execution of a ledger looks like. It
allows the parties to add content to the ledger and gives the adversary some
control on how the things waiting to be included into the ledger are ordered.
\begin{funcbox}{Ledger functionality $\func{ledger}$} The functionality is
  parametrized by a predicate $\valid$ and starts with empty list $L$ and
  variable $\buffer$ initially set to empty string $\eps$.
  \begin{description}
  \item[Append]
    On input $(\append, x)$ from a party $\party$, if $\valid(\state, (\buffer,
    x)) = 1$ then set $\buffer \gets (\buffer, x)$ and broadcast $(x, \party)$.
    \michals{10.05}{The broadcast is used to model the gas model which reveals
    the party that makes changes to the ledger.}
  \item[Retrieve]
    On input $(\retrieve)$ from a party $\party$ or $\adv$, return $(\retrieve,
    L)$ to the requestor if it is an honest party. In case the requestor is a
    corrupted party, return $(\retrieve, L, \buffer)$.
  \item[Buffer release]
    On input $(\releaseTransactionBuffer, f)$ from $\adv$, ignore if $f$ is not
    a permutation. Else, permute the buffer accordingly to $f$, i.e.~set
    $\buffer \gets f(\buffer)$, set $L \gets (L, \buffer)$ and $\buffer \gets
    \eps$.
  \end{description}

\end{funcbox}

\section{Assuring secure SRS generation}
In some scenarios one may assume that the numbr of regulators is limited. In
that case, the problem of trusted SRS generation seems feasible to handle using
the following approach: Assume that the proof system that the regulator $\rdv$
and the regulated party $\pdv$ use is Sub-ZK (subversion zero-knowledge,
i.e.~the zero-knowledge property holds even if the SRS is generated
maliciously, cf.~\cite{AC:BelFucSca16,AC:ABLZ17,PKC:Fuchsbauer18}).  Each
regulator $\rdv$ creates its own SRS which is then given to $\pdv$ who verifies
whether the SRS provides zero knowledge, and if that is the case, it uses it to
produce the proof.

We note that in such scenario both soundness and zero knowledge are preserved.
First, soundness holds since the regulator \emph{is interested} in getting
valid proofs for valid statements. Thus if it does not want to undermine its
efforts, it provides a SRS such that soundness holds and it keeps the
corresponding trapdoor secret.  Second, zero knowledge holds, since the
regulated party $\pdv$ can simply check the SRS for that property.
\section{Protocol instantiation with Zeth}

\newcommand{\genIDCreds}{\algostyle{GenIDCreds}} % Algorithm that generates the
  % identity credentials pair (pcred, scred) (a.k.a IDCred_{pub/sec} in DGKOS20)
\newcommand{\genAttributeList}{\algostyle{GenAttributeList}} % Algorithm that
  % generates the AL of choice for the user
\newcommand{\genPRFKey}{\algostyle{GenPRFKey}} % Algorithm that
  % generates the PRF key K (TODO: Take at random from the PRF key space
  % instead of introducing this uncessary macro)
\newcommand{\pkARs}{\variable{pkARs}} % Set of PKs from the selected Anonymity
  % Revokers.
\newcommand{\mBlind}{\variable{m_{blind}}} % Blinded message to sign
\newcommand{\sBlind}{\variable{\sigma_{blind}}} % Blind signature

% \newcommand{\RELidis}{\REL_{idis}} % Relation proven for the user registration

\procedure[linenumbering]{User registration}{%
\textbf{User} \<\< \textbf{Identity Provider} \\[0.2\baselineskip] [\hline]
  \< \pccomment{Public parameters} \< \< \< \\
  \< \srs \sample \nizk.\setup(\REL_{idis}, \secparam) \< \< \< \\
  \pccomment{Generate ID credentials pair} \\
  (\private{$\scred$}, \pcred) \sample \genIDCreds(\secparam) \<\< \\
  %
  \pccomment{Generate attribute list} \\
  \AL \gets \genAttributeList() \\
  %
  \pccomment{Generate PRF key} \\
  \private{$\prfkey$} \sample \genPRFKey(\secparam) \\
  %
  \pccomment{Collect ARs public keys} \\
  \pkARs \gets (\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}) \\
  %
  \pccomment{Threshold encrypt the PRF key ($\thresholdar$ out of $\noofar$)} \\
  % TODO: Cleanup notations here, add arguments to macro to get the t out of p
  % in the exponent and formally define t and p here (though these indices are
  % already used in the definitions section)
  \ckey \sample \TENC.\ENC^{\thresholdar, \noofar}_{\pkARs}(\prfkey) \\
  %
  \pccomment{Blind message to get signed by $\idprov$} \\
  \mBlind \gets \BSIG.\prepsign(\pk_\idprov, (\scred, \prfkey, \AL)) \\
  %
  \pccomment{Prove:} \\
  \pccomment{1. Knowledge of $\scred$} \\
  \pccomment{2. That $\scred$ is used to derive $\mBlind$} \\
  \pccomment{3. That $\ckey$ and $\mBlind$ are derived from $\prfkey$} \\
  \zkproof \sample \nizk.\prover(\srs, \\
    ((\pcred, \pkARs, \ckey), \private{$(\scred, \prfkey)$})) \\
  %
  \< \sendmessageright{top=\text{$(\user, \AL)$}} \< \< \< \\
  \< \sendmessageright{top=\text{$(\ckey, \pcred)$}} \< \< \< \\
  \< \sendmessageright{top=\text{$\mBlind$}} \< \< \< \\
  \< \sendmessageright{top=\text{$\zkproof$}} \< \< \< \\
  %
  \< \< \pccomment{Verify user attributes (abort if fails)} \\
  \< \< \verify(\user, \AL) \\
  %
  \< \< \pccomment{Verify proof of credential derivation (abort if fails)} \\
  \< \< \nizk.\verify(\srs, \zkproof, (\pcred, \mBlind, \pkARs, \ckey)) \\
  %
  \< \< \pccomment{Sign blinded message} \\
  \< \< \sBlind \gets \BSIG.\blindsign(\sk_\idprov, \mBlind) \\
  %
  \< \< \pccomment{Store $\ipiu$ to track user data} \\
  \< \< \ipiu \gets (\user, \pcred, \ar_1, \cdots, \ar_t, \ckey) \\
  %
  \< \sendmessageleft{top=\text{$\sBlind$}} \< \< \< \\
  %
  \pccomment{Unblind message} \\
  \signature_{idis} \gets \BSIG.\unblind(\sBlind) \\
  %
  \pccomment{Store $\uc$} \\
  \uc \gets (\pcred, \prfkey, \AL, \signature_{idis})
}

\newcommand{\dAppID}{\variable{DAppID}} % ID of the DApp the user wants to use
\newcommand{\dAppLevelID}{\variable{DAppLevelID}} % ID of the DApp level
  % corresponding to what the user wants to do on the DApp (e.g. users willing
  % to transact large amounts via Zeth may need to prove more complex
  % statements (proof of funds etc) than users using Zeth to transact amounts
  % in small ranges (e.g. amounts below $100))
\newcommand{\getAccountPolicy}{\algostyle{GetAccountPolicy}} % On input the
  % DApp ID and the Level ID, this function returns the account policy (i.e.
  % what the user needs to prove when creating new accounts for this DApp)
\newcommand{\getTxPolicy}{\algostyle{GetTxPolicy}} % On input the
  % DApp ID and the Level ID, this function returns the transaction policy (i.e.
  % what the user needs to prove when transacting through this DApp)
\newcommand{\accountpolicy}{\pcpolicystyle{P_{ACC}}} % Account policy (what needs to
  % be proven when creating new accounts from a registered identity)
\newcommand{\txpolicy}{\pcpolicystyle{P_{TX}}} % TX policy (what needs to be proven
  % when transacting on the system)

\procedure[linenumbering]{Get compliance policy}{%
  \textbf{User} \<\< \textbf{Policy Assigner (e.g. DApp operator)}
  \\[0.2\baselineskip] [\hline]
  \pccomment{Select the DApp to use} \\
  \dAppID \\
  \pccomment{Select the level (i.e.~how the user wants to use the DApp)} \\
  % E.g. I may want to use a DApp (e.g. Zeth) without KYC features. In this case
  % I don't get an account policy by the policy assigner, BUT the transaction
  % policy is very restricted (e.g. a very limited range proof [0, 100]).
  % (Note: The tx policy is different from the Zeth/DApp relation!)
  % If, however, use a DApp with high KYC checks, then the account policy
  % I receive will be very strict (need to prove lots of things everytime
  % I create a new account), and the transaction policy may be more loose,
  % e.g. it may be a wider range for the range proof ([0, 1000000]).
  \dAppLevelID \\
  \< \sendmessageright{top=\text{$(\dAppID, \dAppLevelID)$}} \< \< \< \\
  \< \< \alpolicy \gets \getAccountPolicy(\dAppID, \dAppLevelID) \\
  \< \< \comppolicy \gets \getTxPolicy(\dAppID, \dAppLevelID) \\
  \< \< \pccomment{In pratice SRSes for the statements (i.e.~policies)}
  \< \< \pccomment{to prove should also be exchanged. Else, we assume} \\
  \< \< \pccomment{that these SRSes are accessible to the user (e.g. via}\\
  \< \< \pccomment{an open registry of SRSes and associated MPC transcripts)} \\
  % TODO: Instantiate the Sign algo and explain the security guarantees it 
  % needs (EUF-CMA is enough here)
  \< \< \signature_{pal} \gets \sig(\alpolicy) \\ 
  \< \< \signature_{pcomp} \gets \sig(\comppolicy) \\
  \< \< \pccomment{The signature algorithm is assumed to be EUF-CMA} \\
  \< \sendmessageleft{top=\text{$((\alpolicy, \signature_{pal}),
  (\comppolicy, \signature_{pcomp}))$}} \< \< \<
}
% NOTE: In practice if the Policy is sent to the user by the PA (assume an R1CS
% or an SRS is sent to the user), the credential format will somehow be imposed 
% by the
% policy received (else the user would need to use his cred to prove an
% equivalent policy and prove the equivalence!). E.g. if the policy I send you
% is "age (an integer) is one of the roots of the polynomial (x - 1)(x - 2)(x -
% 3)(x - 4)...(x - 18)" to show that you are below 18 y.o., but the credential
% you got issued is based on an AL that is "under_18 = True", then you don't
% have the necessary witness (signed by the issuer) to generate the proof! So
% you need to go back to step 1 and generate another AL with "age = 17" (for
% e.g.) and re-trigger the Interactive Protocol with the IP to get your new AL
% signed and your new creds issued. So in practice, whether AL is generated by
% the user or whether it is granted in standard forms (e.g. digital passport as
% a set of standard attributes) by the IP will depend on the use case.

\newcommand{\genAccountKeys}{\algostyle{GenAccountKeys}} % TX policy
  % (what needs to be proven when transacting on the system)

\procedure[linenumbering]{User DApp account creation that satisfies
$\alpolicy$}{%
  \textbf{User} \<\< \textbf{Relay} \\[0.2\baselineskip] [\hline]
  \< \pccomment{Public parameters} \< \< \< \\
  \< \srs \sample \nizk.\setup(\REL_{newacc}, \secparam) \< \< \< \\
  \pccomment{Collect ARs public keys} \\
  \pkARs \gets (\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}) \\
  %
  \pccomment{Generate the account registration ID ($x$th account)} \\
  \auxacc \gets \prf_{\prfkey}(x) \\
  %
  \pccomment{Generate the anonymity revokation data} \\
  \cuser \sample \TENC.\ENC^{\thresholdar, \noofar}_{\pkARs}(\pcred) \\
  %
  \pccomment{Generate DApp account keypair (e.g.~$\zeth$ keypair)} \\
  (\skacc, \pkacc) \sample \zeth.\genAccountKeys(\secparam) \\
  %
  % Note: Depending on the DApp, posting pk_acc may be optional
  % Since we don't need it to verify Zeth transactions for instance
  %
  \pccomment{Generate ACI} \\
  \aci \gets (\auxacc, \cuser, \idprov, \pkacc, \accountpolicy) \\
  %
  \pccomment{Generate the zk-proof of valid account creation} \\
  \pccomment{Prove:} \\
  \pccomment{1. User had succesfully registered to $\idprov$} \\
  \pccomment{2. That $\accountpolicy(\AL)$ evaluates to $\true$} \\
  \pccomment{3. User knows $\skacc$ associated to $\pkacc$} \\
  \pccomment{4. User knows $\scred$ associated to $\pcred$} \\
  \pccomment{5. $\auxacc$, $\cuser$, $\ckey$ are correctly generated} \\
  \zkproof \sample \nizk.\prover(\srs, (\aci, \pkARs, \pk_\idprov),
  \private{$(\scred, \prfkey, x)$})) \\
  %
  \pccomment{Add the generated zkp to the ACI tuple} \\
  \aci \gets \aci || \zkproof \\
  %
  \< \sendmessageright{top=\text{$\aci$}} \< \< \< \\
  \< \< \pccomment{Add $\aci$ to the Ledger}
}

\newcommand{\getRegisteredACI}{\algostyle{GetRegisteredACI}} % Takes elements
  % (i.e. keys) of an ACI as input and returns the list of matching ACIs
\newcommand{\getRegisteredIPIU}{\algostyle{GetRegisteredIPIU}} % Takes elements
  % (i.e. keys) of an IPIU as input and returns the list of matching IPIU

\procedure[linenumbering]{Revoke account anonymity}{%
  \textbf{Anonymity revokers} \<\< \textbf{Identity provider}
  \\[0.2\baselineskip] [\hline]
  \pccomment{Select the target account identifier} \\
  \auxacc \\
  \pccomment{Find ACI corresponding to $\auxacc$ on the ledger} \\
  \aci \gets \getRegisteredACI(\auxacc) \\
  \pccomment{Collect ARs public keys} \\
  \pkARs \gets (\pk_{\ar_1}, \ldots, \pk_{\ar_\noofar}) \\
  \pccomment{Threshold decrypt $\cuser$ ($n > \thresholdar$ ARs collaborate))} \\
  \{\varshare_i\}_{i \in [n]} \gets \TENC.\dec^{t, \noofar}_{\pkARs}(\sk_i, \cuser) \\
  \pcred \gets \TENC.\combine^{t, \noofar}_{\pkARs}(\cuser, \{\varshare_i\}_{i \in [n]}) \\
  \< \sendmessageright{top=\text{$\pcred$}} \< \< \< \\
  \< \< \pccomment{Recover the $\ipiu$ of the user} \\
  \< \< \ipiu \gets \getRegisteredIPIU(\pcred) \\
  \< \sendmessageleft{top=\text{$\ipiu$}} \< \< \< \\
  \< \pccomment{The $\ipiu$ contains the ID of the user} \< \< \<
}

\procedure[linenumbering]{Trace user account}{%
  \textbf{Anonymity revokers} \<\< \textbf{Identity provider}
  \\[0.2\baselineskip] [\hline]
  \< \< \pccomment{Recover the $\ipiu$ of the suspected user} \\
  \< \< \ipiu \gets \getRegisteredIPIU(\pcred) \\
  \< \sendmessageleft{top=\text{$\ipiu$}} \< \< \< \\
  \pccomment{The relevant ARs decrypt the PRF key of the suspected user} \\
  \{\varshare_i\}_{i \in [n]} \gets \TENC.\dec^{t, \noofar}_{\pkARs}(\sk_i, \ckey) \\
  \prfkey \gets \TENC.\combine^{t, \noofar}_{\pkARs}(\cuser, \{\varshare_i\}_{i
  \in [n]}) \\
  \pccomment{Evalute the PRF on all account indices via an MPC protocol} \\
  \{{\auxacc}_i\}_{i \in [\maxacc]} \gets \prf_{{\prfkey}} (i)_{i \in [\maxacc]} \\
  \pccomment{All the user's account IDs are revealed} \\
  \pccomment{The ledger can be audited}
}

\procedure[linenumbering]{Send a transaction}{%
  \textbf{User} \<\< \textbf{Relay} \<\< \textbf{Policy Assigner}
  \\[0.2\baselineskip] [\hline]
  \pccomment{Create DApp payload (e.g. Zeth proof etc)} \\
  \pccomment{Create proof of tx compliance (i.e. $\txpolicy$ is satisfied)} \\
  \pccomment{or, seeks approval to the Policy assigner} \\
  \< \sendmessageright{top=\text{send payload to Relay}} \< \< \< \\
  \< \< \pccomment{Relays Tx on-chain} \< \< \< \\
  % TODO: Finish
}


\end{document}

% LocalWords:  prover's

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: