sapling-security-analysis/SaplingSecurityProof.tex

\def\notes{1}
\documentclass[11pt]{article}
%\usepackage[T1]{fontenc}
%\usepackage[letterpaper]{geometry}
%\geometry{verbose,tmargin=3cm,bmargin=3cm,lmargin=3cm,rmargin=3cm}
%\usepackage{verbatim}
\usepackage{amsfonts,amsmath,amssymb,amsthm}
%\usepackage{setspace}
\usepackage{xspace}%,enumitem}
%\usepackage{times}
\usepackage{fullpage}
%\usepackage{hyperref}
%\doublespacing
\usepackage{color}
\usepackage{mathrsfs}

%\usepackage{numdef}
%\usepackage{enumitem}
\usepackage{amsopn}
\usepackage{url,hyperref,enumitem}  
\providecommand{\sqbinom}{\genfrac{\lbrack}{\rbrack}{0pt}{}}
\DeclareMathOperator{\spn}{span}

\newif\ifdraft
%\drafttrue
\draftfalse
%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
\numberwithin{equation}{section} %% Comment out for sequentially-numbered
\numberwithin{figure}{section} %% Comment out for sequentially-numbered
\newtheorem{thm}{Theorem}[section]
\newtheorem{conjecture}[thm]{Conjecture}
\newtheorem{definition}[thm]{Definition}
\newtheorem{dfn}[thm]{Definition}
\newtheorem{lemma}[thm]{Lemma}
\newtheorem{remark}[thm]{Remark}
\newtheorem{proposition}[thm]{Proposition}
\newtheorem{corollary}[thm]{Corollary}
\newtheorem{claim}[thm]{Claim}
\newtheorem{fact}[thm]{Fact}
\newtheorem{openprob}[thm]{Open Problem}
\newtheorem{remk}[thm]{Remark}
\newtheorem{example}[thm]{Example}
\newtheorem{apdxlemma}{Lemma}
\newcommand{\question}[1]{{\sf [#1]\marginpar{?}} }
%\usepackage{babel}
\usepackage{tikz}

\makeatletter
\newcommand*{\circled}{\@ifstar\circledstar\circlednostar}
\makeatother

\newcommand*\circledstar[1]{%
  \tikz[baseline=(C.base)]
    \node[%
      fill,
      circle,
      minimum size=1.35em,
      text=white,
      font=\sffamily,
      inner sep=0.5pt
    ](C) {#1};%
}
\newcommand*\circlednostar[1]{%
  \tikz[baseline=(C.base)]
    \node[%
      draw,
      circle,
      minimum size=1.35em,
      font=\sffamily,
      inner sep=0.5pt
    ](C) {#1};%
}

\providecommand{\bd}[1]{\circled{#1}}


%Eli's macros
\newcommand{\E}{{\mathbb{E}}}
%\newcommand{\N}{{\mathbb{N}}}
\newcommand{\R}{{\mathbb{R}}}
\newcommand{\calF}{{\cal{F}}}
\newcommand{\inp}{\ensuremath{\mathsf{inp}}\xspace}
\newcommand{\inps}{\ensuremath{\overrightarrow{\mathsf{inp}}}\xspace}
\newcommand{\outs}{\ensuremath{\overrightarrow{\mathsf{out}}}\xspace}
\newcommand{\out}{\ensuremath{\mathsf{out}}\xspace}
\newcommand{\disp}[1]{D_{#1}}
%\newcommand{\spn}[1]{{\rm{span}}\left(#1\right)}
%\newcommand{\supp}{{\rm{supp}}}
\newcommand{\agree}{{\sf{agree}}}
\newcommand{\RS}{{\sf{RS}}}
\newcommand{\aRS}{{\sf{aRS}}}
\newcommand{\rrs}{R_{\aRS}}
\newcommand{\VRS}{V_\RS}
\newcommand{\set}[1]{\ensuremath{\left\{#1\right\}}\xspace}
\newcommand{\angles}[1]{\langle{#1}\rangle}
\newcommand{\condset}[2]{\set{#1 \mid #2 }}
\newcommand{\zo}{\set{0,1}}
\newcommand{\zon}{{\zo^n}}
\newcommand{\zom}{{\zo^m}}
\newcommand{\zok}{{\zo^}}
\newcommand{\eps}{\ensuremath{\epsilon}\xspace}
\newcommand{\e}{\eps}
%\newcommand{\d}{\delta}
\newcommand{\poly}{\ensuremath{\mathrm{poly}(\lambda)}\xspace}
\newcommand{\itone}{{\it{(i)}}\xspace}
\newcommand{\ittwo}{{\it{(ii)}}\xspace}
\newcommand{\itthree}{{\it{(iii)}}\xspace}
\newcommand{\itfour}{{\it{(iv)}}\xspace}
\newcommand{\cc}{{\rm{CC}}}
\newcommand{\rnk}{{\rm{rank}}}
\newcommand{\T}{T}
\newcommand{\I}{{\mathbb{I}}}
\ifdraft
\newcommand{\ariel}[1]{{\color{blue}{\textit{#1 --- ariel gabizon}}}}
\else
\newcommand{\ariel}[1]{}
\fi
\providecommand{\improvement}[1]{{\color{red} \textbf{#1}}}

\newcommand{\ate}[2]{\ensuremath{\mathsf{Ate_{opt}}(#1,#2)}\xspace}
\title{%
A security analysis of the Zcash Sapling Protocol}
\author{Ariel Gabizon \and Daira Hopwood}
\date{Zcash}
\begin{document}
\maketitle
 \mathchardef\mhyphen="2D

%\num\newcommand{\G1}{\ensuremath{{\mathbb G}_1}\xspace}
%\num\newcommand{\G2}{\ensuremath{{\mathbb G}_2}\xspace}
%\num\newcommand{\G11}{\ensuremath{\G1\setminus \set{0} }\xspace}
%\num\newcommand{\G21}{\ensuremath{\G2\setminus \set{0} }\xspace}
\newcommand{\grouppair}{\ensuremath{G^*}\xspace}

\newcommand{\Gt}{\ensuremath{{\mathbb G}_t}\xspace}
\newcommand{\F}{\ensuremath{{\mathbb F}_r}\xspace}
\newcommand{\help}[1]{$#1$-helper\xspace}
\newcommand{\randompair}[1]{\ensuremath{\mathsf{randomPair}(#1)}\xspace}
\newcommand{\pair}[1]{$#1$-pair\xspace}
\newcommand{\pairs}[1]{$#1$-pairs\xspace}
\newcommand{\pubvalsOf}[1]{\ensuremath{\mathrm{pub}(#1)}\xspace}
\newcommand{\pairone}[1]{\G1-$#1$-pair\xspace}
\newcommand{\pairtwo}[1]{\G2-$#1$-pair\xspace}
\newcommand{\sameratio}[2]{\ensuremath{\mathsf{SameRatio}(#1,#2)}\xspace}
\newcommand{\vecc}[2]{\ensuremath{(#1)_{#2}}\xspace}
\newcommand{\players}{\ensuremath{[n]}\xspace}
\newcommand{\ci}{\ensuremath{\mathrm{CI}}\xspace}
\newcommand{\pairvec}[1]{$#1$-vector\xspace}
\newcommand{\Fq}{\ensuremath{\mathbb{F}_q}\xspace}
\newcommand{\sigscheme}{\ensuremath{\mathscr S}\xspace}

\newcommand{\randpair}[1]{\ensuremath{\mathsf{rp}_{#1}}\xspace}
\newcommand{\randpairone}[1]{\ensuremath{\mathsf{rp}_{#1}^{1}}\xspace}

\newcommand{\randpairtwo}[1]{\ensuremath{\mathsf{rp_{#1}^2}}\xspace}%the randpair in G2

\newcommand{\pos}{\ensuremath{\mathsf{pos}}\xspace}
\newcommand{\rej}{\ensuremath{\mathsf{rej}}\xspace}
\newcommand{\acc}{\ensuremath{\mathsf{acc}}\xspace}
\newcommand{\sha}[1]{\ensuremath{\mathsf{COMMIT}(#1)}\xspace}
 \newcommand{\shaa}{\ensuremath{\mathsf{COMMIT}}\xspace}
 \newcommand{\comm}[1]{\ensuremath{\mathsf{comm}_{#1}}\xspace}
 \newcommand{\defeq}{:=}

\newcommand{\primeof}[1]{\ensuremath{#1 '}\xspace} 
\newcommand{\beforeout}[1]{\ensuremath{D^{\mathsf{out}}_{<#1}}\xspace}
\newcommand{\beforeoutprime}[1]{\ensuremath{D'^{\mathsf{out}}_{<#1}}\xspace}
\newcommand{\beforein}[1]{\ensuremath{D_{<#1}}\xspace}
\newcommand{\beforeinprime}[1]{\ensuremath{D'_{<#1}}\xspace}
%\renewcommand{\prime}[1]{\ensuremath{#1'}\xspace}
\newcommand{\inpwitness}{\ensuremath{\mathsf{inpwit}}\xspace}
\newcommand{\inpnote}{\ensuremath{\mathsf{inpnote}}\xspace}
\newcommand{\posnote}{\ensuremath{\mathsf{posnote}}\xspace}
\newcommand{\inpnotes}{\ensuremath{{\mathcal{I}}}\xspace}
\newcommand{\outnotes}{\ensuremath{{\mathcal{O}}}\xspace}
\newcommand{\outwitness}{\ensuremath{\mathsf{outwit}}\xspace}
\newcommand{\outnote}{\ensuremath{\mathsf{outnote}}\xspace}
\newcommand{\treehash}{\ensuremath{\mathsf{treehash}}\xspace}
\newcommand{\A}{\ensuremath{\vec{A}}\xspace}
\newcommand{\B}{\ensuremath{\vec{B}}\xspace}
\newcommand{\C}{\ensuremath{\vec{C}}\xspace}
\newcommand{\Btwo}{\ensuremath{\vec{B_2}}\xspace}
\newcommand{\treevecsimp}{\ensuremath{(\tau,\rho_A,\rho_A \rho_B,\rho_A\alpha_A,\rho_A\rho_B\alpha_B, \rho_A\rho_B\alpha_C,\beta,\beta\gamma)}\xspace}% The sets of elements used in simplifed relation tree in main text body
\newcommand{\rcptc}{random-coefficient subprotocol\xspace}
\newcommand{\rcptcparams}[2]{\ensuremath{\mathrm{RCPC}(#1,#2)}\xspace}
\newcommand{\verifyrcptcparams}[2]{\ensuremath{\mathrm{\mathsf{verify}RCPC}(#1,#2)}\xspace}

% \num\newcommand{\ex1}[1]{\ensuremath{ #1\cdot g_1}\xspace}
% \num\newcommand{\ex2}[1]{\ensuremath{#1\cdot g_2}\xspace}
 \newcommand{\pr}{\mathrm{Pr}}
 \newcommand{\powervec}[2]{\ensuremath{(1,#1,#1^{2},\ldots,#1^{#2})}\xspace}
%\num\newcommand{\out1}[1]{\ensuremath{\ex1{\powervec{#1}{d}}}\xspace}
%\num\newcommand{\out2}[1]{\ensuremath{\ex2{\powervec{#1}{d}}}\xspace}
 \newcommand{\nizk}[2]{\ensuremath{\mathrm{NIZK}(#1,#2)}\xspace}% #2 is the hash concatenation input
 \newcommand{\verifynizk}[3]{\ensuremath{\mathrm{VERIFY\mhyphen NIZK}(#1,#2,#3)}\xspace}
\newcommand{\protver}{protocol verifier\xspace} 
\newcommand{\mulgroup}{\ensuremath{\F^*}\xspace}
\newcommand{\lag}[1]{\ensuremath{L_{#1}}\xspace} 
\newcommand{\sett}[2]{\ensuremath{\set{#1}_{#2}}\xspace}
\newcommand{\omegaprod}{\ensuremath{\alpha_{\omega}}\xspace}
\newcommand{\lagvec}[1]{\ensuremath{\mathrm{LAG}_{#1}}\xspace}
\newcommand{\Z}{\ensuremath{\mathbb{Z}}\xspace}
\newcommand{\Ftwo}{\ensuremath{\mathbb{F}_{p^2}}\xspace}
\newcommand{\Ftwlth}{\ensuremath{\mathbb{F}_{p^{12}}}\xspace}
\newcommand{\Ffour}{\ensuremath{\mathbb{F}_{p^4}}\xspace}
\newcommand{\Fsix}{\ensuremath{\mathbb{F}_{p^{6}}}\xspace}

\newcommand{\coinset}{\ensuremath{{\cal C}}\xspace}
\newcommand{\serialnumset}{\ensuremath{\mathrm{SN}}\xspace}
\newcommand{\addrset}{\ensuremath{{\cal A}}\xspace}
\newcommand{\txset}{\ensuremath{{\cal T}}\xspace}
\newcommand{\valueset}{\ensuremath{{\cal V}}\xspace}
\newcommand{\ledgers}{\ensuremath{{\cal L}}\xspace}
\newcommand{\gd}{\ensuremath{\mathsf{g}}\xspace}

\newcommand{\snof}[1]{\ensuremath{\mathrm{sn}(#1)}\xspace}
\newcommand{\nfof}[1]{\ensuremath{\mathsf{nf}(#1)}\xspace}
\newcommand{\rkof}[1]{\ensuremath{\mathsf{rk}(#1)}\xspace}
\newcommand{\valueof}[1]{\ensuremath{\mathrm{v}(#1)}\xspace}
\newcommand{\addrof}[1]{\ensuremath{\mathrm{addr}(#1)}\xspace}
\newcommand{\equals}[4]{\ensuremath{\mathsf{equals}(#1,#2,#3,#4)}\xspace}
\newcommand{\coins}{\ensuremath{\mathrm{\mathbf{c}}}\xspace}
\newcommand{\vold}{\ensuremath{\mathrm{v^{old}}}\xspace}
\newcommand{\vbal}{\ensuremath{\mathrm{v^{bal}}}\xspace}
\newcommand{\bal}{\ensuremath{\mathrm{bal}}\xspace}
\newcommand{\rand}{\ensuremath{\mathrm{\mathsf{r}}}\xspace}
\newcommand{\vnew}{\ensuremath{\mathrm{v^{new}}}\xspace}
\newcommand{\ledger}{\ensuremath{\mathrm{L}}\xspace}
\newcommand{\values}{\ensuremath{\mathrm{\mathbf{v}}}\xspace}
\newcommand{\valuesof}[1]{\ensuremath{\values(#1)}\xspace}
\newcommand{\addrs}{\ensuremath{\mathrm{\mathbf{a}}}\xspace}
\newcommand{\addrsof}[1]{\ensuremath{\addrs(#1)}\xspace}

\newcommand{\sqoftexset}{{\cal S}\xspace}
\newcommand{\verifytx}[2]{\ensuremath{\mathsf{verify\mhyphen tx} (#1,#2)}\xspace}
\newcommand{\serialnumbersof}[1]{\ensuremath{\mathrm{sn}(#1)}\xspace}
\newcommand{\coinsof}[1]{\ensuremath{\coins(#1)}\xspace}
\newcommand{\seqofcoins}{\ensuremath{\coins^*}\xspace}
\newcommand{\txinput}{\ensuremath{\mathrm{x}}\xspace}
\newcommand{\txinputs}{\ensuremath{\mathrm{\mathbf{x}}}\xspace}
\newcommand{\seqoftxset}{\ensuremath{\txset^*}\xspace}
\newcommand{\tx}{\ensuremath{\mathsf{tx}}\xspace}
\newcommand{\aprand}{\ensuremath{\mathrm{pp}}\xspace}
\newcommand{\coin}{\ensuremath{\mathrm{c}}\xspace}
\newcommand{\ledgerset}{\ensuremath{\mathcal{L}}\xspace}
\newcommand{\uniqueledgerset}{\ensuremath{\mathcal{L}^{\mathrm{unique}}}\xspace}
\newcommand{\serialnums}{\ensuremath{\mathrm{\mathbf{sn}}}\xspace}

\newcommand{\txinputset}{\ensuremath{\mathcal{I}}\xspace}

\newcommand{\createtx}[2]{\ensuremath{\mathsf{create\mhyphen tx}(#1,#2)}\xspace}
\newcommand{\decodebykey}[3]{\ensuremath{\mathsf{decode}_{#3}(#1,#2)}\xspace}%#3 is sk
\newcommand{\decode}[2]{\ensuremath{\mathsf{decode}(#1,#2)}\xspace}
   
\newcommand{\key}{\ensuremath{\mathrm{sk}}\xspace}
\newcommand{\keyof}[1]{\ensuremath{\key(#1)}\xspace}
\newcommand{\keyset}{\ensuremath{{\mathcal K}}\xspace}


\newcommand{\adv}{\ensuremath{{\mathcal A}}\xspace}
\newcommand{\advprime}{\ensuremath{{\mathcal A'}}\xspace}
\newcommand{\advs}{\ensuremath{{\mathcal{A}}}\xspace}
\newcommand{\advaddrs}{\ensuremath{\addrs_{\adv}}\xspace}
\newcommand{\coinsofserialnums}[2]{\ensuremath{\coins(#1,#2)}\xspace}
\newcommand{\seq}{\ensuremath{\mathsf{r}}\xspace}
\newcommand{\querseq}{\ensuremath{\mathsf{q}}\xspace}
\newcommand{\sigquerseq}{\ensuremath{\mathsf{q^\sigma}}\xspace}
\newcommand{\schnorr}{\ensuremath{\mathsf{Schnorr}}\xspace}
\newcommand{\rawof}[1]{\ensuremath{\mathsf{raw(#1)}}\xspace}
\newcommand{\honest}{\ensuremath{\mathcal H}\xspace}
\newcommand{\ext}{\ensuremath{\mathcal \xi}\xspace}
\newcommand{\G}{\ensuremath{\mathbb{G}}\xspace}
\newcommand{\sigseq}{\ensuremath{\mathsf{\sigma}}\xspace}
\newcommand{\sk}{\ensuremath{\mathsf{sk}}\xspace}
\newcommand{\pk}{\ensuremath{\mathsf{pk}}\xspace}
\newcommand{\sigquer}{\ensuremath{\mathsf{q^\sigma}}\xspace}
\newcommand{\RO}{\ensuremath{\mathcal R}\xspace}
\newcommand{\ROsig}{\ensuremath{\mathcal R_{sig}}\xspace}
\newcommand{\sig}{\ensuremath{\sigma}\xspace}
\newcommand{\sign}{\ensuremath{\mathsf{sign}}\xspace}
\newcommand{\versig}{\ensuremath{\mathsf{verifySig}}\xspace}
\renewcommand{\sim}{\ensuremath{ {\mathcal S}}\xspace}
\newcommand{\simprv}{\ensuremath{\sim_{\mathsf{sign}}}\xspace}
\newcommand{\simro}{\ensuremath{\sim_{\RO}}\xspace}
\newcommand{\str}{\ensuremath{\mathrm{x}}\xspace}
\newcommand{\negl}{\ensuremath{\mathrm{negl}(\lambda)}\xspace}
\newcommand{\msg}{\ensuremath{\mathbf m}\xspace}
\newcommand{\dist}{\ensuremath{\mathrm{\pi}}\xspace}
\newcommand{\oracle}{\ensuremath{\mathscr O}\xspace}
\newcommand{\oracleprime}{\ensuremath{\mathscr O'}\xspace}
\newcommand{\g}{\ensuremath{\mathsf{g}}\xspace}

\section{Introduction}
The purpose of this note is to show that the Sapling protocol, that will be used for Zcash shielded (private) transactions as of the Sapling network upgrade, satisfies certain security properties. This document is not completely self contained and while reading it we recommend referring often to the Zcash protocol spec\cite{spec} for full details of the Sapling protocol.


A noteable property of the protocol is a separation of proving and signing authority. A ``delegated spender/prover'' creates transactions with the help
of a proof authorizing key (or just proving key for short), but the transaction is not valid until it is signed by the signer with the spending key, that roughly corresponds to the secret key when thinking of the proving key as a public key.

We informally describe the four properties we prove.

\begin{enumerate}
 \item \textbf{Non-malleability}: The delegated spender, after receiving a set of signatures on transactions of his choice, should not be able to create a new valid transaction, containing a nullifier appearing in one of the old transactions (overlapping nullifiers intuitively correspond to transactions from the same spending key). The way non-malleability is defined and proved here is inspired from the Zerocash paper\cite{zerocash}.
 \item \textbf{Indistinguishability}: An adversary should not be able to find two tupples (input notes, output notes) that are consistent in public data - meaning mainly that the amount going in or out of the shielded pool is the same, such that it is possible to distinguish from seeing the transaction which tupple it corresponds to.
 \item \textbf{Balance}: An adversary should not be able to construct a valid ledger (even when having full control of transactions inserted) such that the total amount coming out of the shielded pool is larger than what came in.
 \item \textbf{Spendability}: An adversary should not be able to send the honest party a note that was successfully received, but cannot be later spent (such an attack on \cite{zerocash} was found by Zooko Wilcox and coined ``Faerie Gold'' in \cite{spec}).
\end{enumerate}

Before getting into the Sapling protocol and these properties, we begin with preliminary definitions and results regarding signature schemes.







\section{Signature schemes}\label{sec:signatures}
%We assume all parties below have access to a random oracle \RO taking arbitrary strings as input and outputting uniform elements of \F.

When we say an algorithm \adv is \emph{efficient}, we mean it runs in time \poly for the ``security parameter'' $\lambda$.


 \begin{dfn}\label{dfn:sigscheme}
Let \G be a group of prime order $r$.
A signature scheme \sigscheme over \G in the random oracle model consists of algorithms $\sigscheme = (\sign,\versig,\sim= (\simprv,\simro))$
where $\sign,\versig$ are oracle machines with access to an oracle \RO taking as input arbitrary strings and returning uniform elements of \F.
Such that the following holds.
 \begin{itemize}
  \item The set of public/verification keys \set{\pk} is \G, and the set of private keys \set{\sk} is \F.
  \item For $\sk \in \F$, the verification key of \sk is $\pk= \sk\cdot g$ for a fixed generator $g\in \G$.
  \item We have the following ``zero-knowledge'' property:
 Fix any efficient \adv.
 Suppose that \adv interacts with \sim with two types of queries 
  \begin{enumerate}
   \item Queries \str, for an arbitrary string \str that are answered according to $\simro$.
   \item Queries $(\pk,\msg)$, answered according to $\simprv$.
  \end{enumerate}
Let $\dist_1$ be the distribution of the sequence of queries and replies to \adv.
Let $\dist_2$ be the distribution of the sequence of queries and replies to \adv when

\begin{enumerate}
 \item \RO takes the place of  $\sim_1$
 \item $\sign^{\RO}(\sk,\msg)$ is returned instead of $\sim_2(\pk,\msg)$ where \sk is the secret key corresponding to \pk.
\end{enumerate}
Then the distance between $\dist_1$ and $\dist_2$ is \negl.
\end{itemize}

We say \sigscheme is \emph{unforgeable w.r.t key randomization} if the following holds.
Fix any efficient \adv.
A party \oracle chooses uniform $\sk\in \F$ and sends $\pk = \sk\cdot g$ to \adv.
\oracle also initializes an empty set $T$.
\adv adaptively makes \poly queries of the form $(\alpha,\msg)$.
\oracle replies with $\sig\defeq \sign(\pk+\alpha\cdot g, \msg)$
and adds $(\alpha,\msg,\sig)$ to $T$.

Finally \adv outputs $(\alpha^*,\msg^*,\sig^*)$.
Let $\pk^*\defeq \pk+\alpha^*\cdot g$.
 Then the probability that 
  \begin{enumerate}
   \item $\versig(\pk^*,\msg^*,\sig^*)$, and 
   \item $(\alpha^*,\msg^*,\sig^*)\notin T$
  \end{enumerate}
is \negl.
\end{dfn}

% \begin{claim}
% If \sigscheme is simulation extractable with error $\eps$ it is also randomizable extractable with error $\eps+\negl$.
% \end{claim}
% \begin{proof}
% Have adv \adv against RE.
% Define the following \adv' against SE:
% \begin{enumerate}
%  \item Start by choosing uniformly \set{\sk_1,\ldots,\sk_\ell} and 
%  sending \set{\pk_1,\ldots,\pk_\ell} to \adv.
%  \item When \adv asks a query to \RO, answer it according to \simro.
%  \item When \adv asks a query $(\pk,\rho,\msg)$ to \honest, answer it with $\simprv(\pk+\rho\cdot g,\msg)$
% \item When \adv outputs $(\pk^*,\msg^*,\sig^*)$, output the same message.
%  \end{enumerate}
% Let \ext' be the extractor guaranteed to exist for \adv'.
% Now construct \ext for \adv as follows.
% \adv is executed, and the \ext is given $P=\set{P_1,\ldots,P_\ell}$,\seq,\querseq,\sigseq,\sigquerseq
% and its output $(\pk^*,\msg^*,\sig^*)$.
% 
% 
% Note that (\adv')'s output is determined by the value
% Note that the except for a negligible fraction of the time \adv succeeds relative to $\versig^{\RO}$ at the same
% \adv' succeeds relative to $\versig^{\simro}$.
% So \ext' is also a good extractor for \adv demonstrating the scheme has the $\eps'$ ``randomized extractability'' property for 
% $\eps' = \eps +\negl$.
% \end{proof}
% 
% 
 
 
 
 
 We assume our group \G has a hard DL problem; meaning that for any efficient \adv,
 given uniform $g,\sk\cdot g \in \G$ the probability of outputting \sk is \negl.
 
 We define the non-malleable version of Schnorr's signature scheme:
 
\paragraph{\underline{\schnorr:}} 
 \paragraph{Parameters:}
 Group \G of prime order $r$. Non-zero $g\in \G$.
 \paragraph{Signing:}
  Given message \msg and \sk, 
 \begin{itemize}
 \item Choose random $a\in \F$ and let $R\defeq a\cdot g$

  \item Compute $c\defeq \RO(R,\pk,\msg)$
  \item Let $u\defeq a+c\cdot \sk$.
  \item Define $\sign^{\RO}(\sk,\msg) \defeq (R,u)$.
 \end{itemize}
\paragraph{Verifying:}
 Given $\pk,\msg,\sig=(R,u)$, $\versig^{\RO}(\pk,\msg,\sig)$ 
 accepts iff:

\begin{itemize}
 \item Computing $c\defeq \RO(R,\pk,\msg)$; we have $u\cdot g = R+c\cdot \pk$.
\end{itemize}
\paragraph{Simulating:}
\begin{itemize}
\item $\simro(\str)$ checks if \str has been queried before; if so answers consistently, otherwise answers uniformly in \F and records the answer. 
 \item $\simprv(\pk,\msg)$: Choose uniform $c,u \in \F$. Define $R\defeq u\cdot g - c\cdot \pk$
 and $\str \defeq (R , \pk,\msg )$.
 Check if $\simro(\str)$ has been defined.
 If so, abort.  Otherwise define $\simro(\str)=c$ and return $(R,u)$.
\end{itemize}
\begin{remark}
 At times when we wish to change the parameter $g$ we work with from default to an element $h$,
 we will use it in the subscript, e.g. $sign_h^{\RO}(\sk,\msg)$.
 
 We refer by $\schnorr' = (\sign',\versig')$ to the Schnorr scheme where \pk is omitted from the computation of $c$.
\end{remark}
\begin{thm}\label{thm:schnorr-nf}
\schnorr is non-forgeable w.r.t randomization.
\end{thm}
\begin{proof}
Similarly to \cite{rerandSig},
we reduce to the non-forgeability of standard Schnorr (where the public key is not part of the signature \& without randomization)
that was proven in \cite{schnorrSecurity}.


Suppose we are given \adv interacting with \oracle as described above, and finally outputting $(\alpha^*,\msg^*,\sig^*)$.
We construct \advprime that interacts with \oracleprime which is a ``standard'' Schnorr oracle.

That is:
\begin{enumerate} 
\item \oracleprime begins by choosing a uniform $\sk\in \F$ 
\item \oracleprime computes $\pk = \sk\cdot g$ and sends \pk to \advprime. \oracleprime intializes an empty set $T'$.
\item \advprime sends queries \msg to \oracleprime and receives replies $\sig = \sign'_{\sk}(\msg)$. \oracleprime adds $(\msg,\sigma)$ to $T'$.
\item After all queries \advprime outputs $(\msg^*,\sig^*)$.
\end{enumerate}
\advprime wins if
\begin{itemize}
   \item $\versig'(\pk,\msg^*,\sig^*)$, and 
   \item $(\msg^*,\sig^*)\notin T'$
\end{itemize}
 
\advprime will simulate (\adv)'s interaction with \oracle using \oracleprime:
Given a query $(\alpha,\msg)$ of \adv, \advprime queries \oracleprime with $\msg'\defeq(\pk+\alpha\cdot g,\msg)$,
to receive reply $\sig'=(R,u')$ - \emph{this is a $\schnorr'$-signature of $\msg'$ with \sk, and we now convert this to a $\schnorr$-signature of $\msg$ with $\sk+\alpha$}.
Let $c\defeq \RO(R,\msg')=\RO(R,\pk+\alpha\cdot g, \msg)$. It sends $\sig\defeq (R,u\defeq u'+c\alpha)$ to \adv.


 We have 
\[u\cdot g = u'\cdot g +c\alpha\cdot g = R+c\cdot \pk +c\alpha\cdot g = R+ c\cdot (\pk+\alpha\cdot g) .\]
So we have $\versig(\pk+\alpha\cdot g,\msg,\sig)$.
Also $R$ is uniformly distributed, thus \advprime is answering (\adv)'s queries with the same distribution \oracle would have.

Note that the mapping $F(\alpha,\msg,\sig)\defeq (\msg',\sig')$
where $\msg'\defeq(\pk+\alpha\cdot g,\msg),\sig'\defeq (R,u-c\alpha)$ is injective.

% $T=\set{(\alpha,\msg,\sig)}$
Let $T$ be the set of tupples $(\alpha,\msg,\sig)$ such that \adv queried $(\alpha,\msg)$ and $\adv'$ answered \sig.
We have $T'= \sett{F(x)}{x\in T}$.

When \adv finally outputs $x^*=(\alpha^*,\msg^*,\sig^*)$;
\advprime outputs $F(x^*)$. 
As $F$ is injective $x^* \notin T$
implies $F(x^*)\notin T'$.

Denote $(m',\sigma')\defeq F(x^*)$.
From \cite{schnorrSecurity}'s results on unforgeability of $\schnorr'$, the probability that 
\begin{itemize}
   \item $\versig'(\pk,\msg',\sig')$, and 
   \item $(\msg',\sig')\notin T'$
\end{itemize}
is \negl.
Noting that $\versig'(\pk,\msg',\sig')\equiv \versig(\pk+\alpha\cdot g, \msg^*,\sig^*)$,
this means that the probability that
\begin{itemize}
   \item $\versig(\pk+\alpha\cdot g,\msg^*,\sig^*)$, and 
   \item $x^* \notin T$
\end{itemize}
is \negl.
This is exactly what we had to prove.
\end{proof}
\newcommand{\sample}{\ensuremath{\mathbf{sample}}\xspace}
\newcommand{\invert}{\ensuremath{\mathbf{invert}}\xspace}
\newcommand{\bigset}[2]{\ensuremath{W|_{#1\setminus #2}}\xspace}
\newcommand{\goodset}[2]{\ensuremath{W_{#1,#2}}\xspace}

\paragraph{Invertible group samplers}
We assume that for our group \G we have an efficient randomized procedure \sample that produces a group element in \G that is \negl-close to uniform,
such that there is an efficient deterministic algorithm \invert that given the output of \sample, produces w.p $1/\poly$
over the randomness of \sample, the randomness $r$ used in that execution. 

Note that when \G is an elliptic curve group over \F such a pair $(\sample,\invert)$
is having \sample try $\lambda$ iterations of: Choose random $x\in \F$, check if there exists some $(x,y)\in \G$, if so output one of the two such elements randomly; and otherwise try another random $x\in\F$.

\invert, given $(x,y)\in \G$, will output $(x,\mathsf{sign}(y))$, which will be correct in the case that the first iteration of \sample produced a good $x$, which happens w.p. approximately half.

We also need that \schnorr is a proof of knowledge of discrete log. For this,
we state the following theorem that is almost implicit in \cite{schnorrSecurity}, but we provide a proof for completeness.
\begin{thm}[Extractability of Schnorr]\label{thm:extractSchnorr}
Fix any integer function $\gamma=\gamma(\lambda)$ with $0\leq \gamma(\lambda)\leq 1$ for any $\lambda$.
There is an algorithm \ext with the following property.
Fix any efficient \adv and group element $\g\in\G$. Suppose that \adv produces w.p. $\gamma$
$(\pk,\msg,\sig)$ such that $\versig^{\RO}_{\g}(\pk,\msg,\sig)$.
Then, given the internal randomness used by \adv in the run and the vector \rand of replies of \RO,
\ext produces w.p $\gamma/2$ over (\adv)'s randomness, the randomness of \RO in answering (\adv)'s queries and its own randomness $s\in\F$ such that
$\pk = s\cdot \g$.
Furthermore, \ext's running time will be $F(\lambda,1/\gamma)$ where $F$ is a polynomial depending only on the running time of \adv.
\end{thm}

 \begin{proof}
 
  Assume first that \adv is deterministic. Let $Q=\poly$ be a bound on the number of queries to \RO made by \adv. When \adv is deterministic its execution is fully 
  determined by the vector $\rand \in \F^q$ of replies by \RO to its queries.  
  
  Recall that $\rand\in \F^Q$ denotes the $Q$ oracle replies to the queries of \adv to \RO.
  We call \rand \emph{good} if $\adv(\rand)$ outputs a verifying $(\pk,\msg,\sig)$.
  We assume for simplicity that whenever \rand is good \adv queries \RO at $(R,\pk,\msg)$ where $\sig = (R,u)$.
  (Otherwise \ext can simulate an altered \adv that asks this query whenever \rand is good and the query hasn't been made yet.)
  For good \rand we define the index $i(\rand)\in [Q]$ where the query $(R,\pk,\msg)$ was made. 
  For $i\in [Q]$ and $\rand\in\F^Q$ we define the subset \bigset{\rand}{i} of $\F^Q$ to be the set of $\rand' \in \F^Q$ that are equal to \rand outside of index $i$.
  We denote by \goodset{\rand}{i} the set of $\rand'\in \F^Q$ that are contained in \bigset{\rand}{i}, are good, and have $i(\rand')=i$.
   Note that there are at most $r^{Q-1}\cdot Q$ distinct sets \goodset{\rand}{i}.
 
 Note also that given two distinct elements $\rand\neq \rand'\in\goodset{\rand}{i}$, the executions $\adv(\rand),\adv(\rand')$ give us two valid signatures with the same public key \pk message \msg and first part $R$;
  and such two signatures enable computing \sk.
  
 Define the two functions
   \[ P = 4Q/\gamma, T=\lceil \ln 3\cdot 2 P \rceil.\]
  Given \rand and \adv, \ext does the following.
  \begin{enumerate}
  \item If \rand is not good, abort.
  \item If $\lambda$ is such that $r(\lambda)< 2P(\lambda)$, conduct a brute for search for \sk such that $\sk\cdot \g = \pk$.
   \item Otherwise, set $i=i(\rand)$. Sample $T$ elements $\rand\in \bigset{\rand}{i}$.
   \item Run \adv using each of the samples as \RO's reply vector. If one of the sampled elements is good and different from \rand, use it to compute and output \sk.
    \end{enumerate}
  We claim \ext retrieves \sk with probability at least $\gamma/2$. This claim will follow from two subclaims described below.
  Fix good \rand and let $i=i(\rand)$.
  Call \rand \emph{dense} if (it is good and) 
  \[|\goodset{\rand}{i}|\geq |\bigset{\rand}{i}|/P.\]
  We first show that given dense \rand, \ext succeeds w.p. at least $2/3$ over its inner randomness:
  The event that \ext fails implies that in $T$ samples of \bigset{\rand}{i}, it didn't find a distinct $\rand'\in \goodset{\rand}{i}$. This probability is bounded by
  \[(1-(1/P-1/r))^T \leq (1-1/2P)^T \leq e^{-T/2P}\leq 1/3.\]
  
  
  Next, we bound the probability of $\rand\in \F^Q$ not being dense:
  The number of such \rand is at most
  \[ r^{Q-1}Q \cdot \frac{r}{P}\leq \frac{r^Q\cdot Q}{P}.\]
  Thus the density of such elements is at most
  \[Q/P\leq \gamma/4.\]
  
  Now using these two subclaims, the probability of \ext succeeding to output \sk is at least the probability of \rand being dense, multiplied by the probability of \ext succeeding conditioned on \rand being dense. This gives success probability at least
  \[(3\gamma/4)\cdot (2/3) = \gamma/2.\]  
  
  
  Finally, if \adv is randomized, running \ext as above when \adv is fixed to whatever inner randomness it used and \ext received as input, gives the same success probability of \ext for randomized \adv.
  
  \end{proof}



%  For the proof of the theorem, note that we can think of \sim as uniform $(\seq, \sigseq) \in \F^{3Q}$ and answering queries accordingly.
%  (Perhaps aborting on the way.)
% \begin{thm}
% For any $\eps= 1/\poly$,  \schnorr is simulation extractable with error $\eps$.
% \end{thm}
% \begin{remark}
%  An important property of our definition and this theorem is that the ``extractor succeeds almost always when the prover succeeds'';
%  in contrast with, e.g., Theorem 3 of \cite{FKMV12}
% \end{remark}
% 
% \begin{proof}
%  The proof is similar to ones in \cite{PS00,firstMPC}.
%  
%  
%  Suppose \adv has made $Q$ queries  $q_1,\ldots,q_Q$ to $\simro$, receiving replies $\seq =\seq_1,\ldots,\seq_Q$;
%  and queries $\sigquer = \sigquer_1,\ldots,\sigquer_Q$ to \simprv receiving replies $\sigseq = \sigma_1,\ldots,\sigma_Q$.
% Suppose it has prouced $(\pk,\msg,\sig)$ such that
% $\versig^\simro(\pk,\msg,\sig)=\acc$
% 
% 
%  \newcommand{\rest}[2]{\ensuremath{#1|_{#2}}\xspace}
% \newcommand{\bigset}{\ensuremath{W|_{\seq\setminus j}}\xspace}
% \newcommand{\bigsetspecific}{\ensuremath{W|_{\seq\setminus j_s(\seq)}}\xspace}
% \newcommand{\smallset}{\ensuremath{W_{\seq,s}}\xspace}
% \newcommand{\alg}{\ensuremath{\mathsf{alg}}\xspace}
% \newcommand{\domainofsequence}{\ensuremath{[\rodomsize]^Q}\xspace}
% % \begin{claim}\label{clm:goodelems}
% % For any polynomial $P$, 
% %  there is an algorithm \alg that for a $(1-1/P(\log r))$-fraction of good \seq,
% %  obtains $\secrets(\seq)$ given \seq with probability $1-1/r$ in time \polylog.
% % \end{claim}
% 
% % Denote $S=\cup_{i\in\players}\secrets_i$, where $\secrets_i$ is the vector of variables $\tau_i,\rho_{A,i},\rho_{B,i},\alpha_{A,i},\alpha_{B,i},\alpha_{C,i},\gamma_i,\beta_i$.
% 
% Think of \sigseq, and \adv's randomness as fixed. We'll show that except for a $1/P$ fraction of $\seq \in \F^Q$,
% if $(\seq,\sigseq)$ is good we retrieve \sk except with probability $2^{-\lambda}$.
% Suppose that $\sig = (R,u)$.
% Let us call \seq $\sigseq$-good if   $(\seq,\sigseq)$ is good  
% Denote by $J\in [Q]$ the index such that $q_J = (\pk,\msg,R)$.
% % 
% % For good \seq and $s\in S$, we denote by $i_s(\seq)$
% % the index corresponding to $s$ in $I(\seq)$ and by $j_s(\seq)$
% % the index corresponding to $s$ in $J(\seq)$.
% % Note that for good \seq we always have $i_s(\seq)<j_s(\seq)$.
% 
% For $j\in [Q]$, and $\seq\in \F^Q$,
% we denote by \bigset the strings $\seq'\in \F^q$
% that are equal to \seq outside of $j$.
% For $\seq\in \F^Q$,
% we denote by \smallset the set of good $\seq'\in\F^q$ that are equal
% to \seq outside of $j$, and have $J(\seq')=J(\seq)$.
% Note that the set \smallset is determined by the index $j$
% and the values of \seq outside of $j$; thus, there are at most $\F^{Q-1}\cdot Q$ such distinct sets.
% Note also that $\smallset \subseteq \bigsetspecific$.
% 
% Now given good \seq, \sim does the following.
% Denote $P'\defeq 2P\cdot Q$.
% Letting $j\defeq J(\seq)$, \alg samples $2P'(\lambda)\cdot \lambda$ strings \seq' from \bigset.
% For each one he checks if $\seq'\in \smallset$ and if $\seq'_{j}\neq \seq_{j}$.
% If both checks hold, it means, that $\adv(\sigseq,\seq)=(\pk,\msg,(R,u))$ and $\adv(\sigseq,\seq')=(\pk,\msg,(R,u'))$ are two valid signatures of \msg under
% \pk. This means \ext can obtain $\sk$ using Schnorr's extractability property.
% 
% 
% Now the question is what is the probability of not finding a sequence \seq' enabling extraction of $\sk$.
% We claim this is at most $2^{-\lambda}$, when the density of \smallset in \bigset is at least $1/P'(\lambda)$:
% In this case the density of elements of \smallset such that $\seq'_{j}\neq \seq_{j}$ is at least $1/P'(\lambda)-1/r\geq 1/2P'(\lambda)$ for large enough $\lambda$.
% Thus, the probability that no such element \seq' is found is at most $(1-1/2P'(\lambda))^{ 2P'(\lambda)\cdot\lambda}\leq e^{-\lambda}$.
% 
% Now we must bound the density of good \seq that do not have this property.
% Each such \seq belongs to a set \smallset containing at most $r/P'(\lambda)$ elements.
% Thus, there at most 
% \[\frac{r \cdot r^{Q-1}\cdot Q}{P'(\lambda)} = \frac{r^Q\cdot Q^2}{P(\lambda)\cdot Q} = \frac{r^Q}{P(\lambda)}\]
% such elements, which is a $1/P(\lambda)$ fraction of the space.
% 
% In summary, for each value of \sigseq,
% if the fraction of values \seq such that $(\sigseq,\seq)$ is good is $\eps_\sigseq$.
% We succeed in extraction, except for a $1/P$-fraction of those.
% 
% 
% \end{proof}

\newcommand{\createaddr}{\ensuremath{\mathsf{createaddr}}\xspace}
\newcommand{\makeinput}{\ensuremath{\mathbf{makeinp}}\xspace}
\newcommand{\makeoutput}{\ensuremath{\mathbf{makeout}}\xspace}
\newcommand{\makerandomizedoutput}{\ensuremath{\mathbf{makerandomizedout}}\xspace}
\newcommand{\makeoutputandnote}{\ensuremath{\mathbf{makeoutputandnote}}\xspace}
\newcommand{\maketx}{\ensuremath{\mathbf{maketx}}\xspace}
\newcommand{\makerandomizedtx}{\ensuremath{\mathbf{makerandomizedtx}}\xspace}
\newcommand{\bindvaltx}{\ensuremath{\mathbf{bindval}}\xspace}
\newcommand{\signtx}[1]{\ensuremath{\mathbf{signtx}(#1)}\xspace}
\newcommand{\notecom}{\ensuremath{\mathbf{NC}}\xspace}
\newcommand{\valcom}{\ensuremath{\mathbf{VC}}\xspace}
\newcommand{\esk}{\ensuremath{\mathsf{esk}}\xspace}
\newcommand{\note}{\ensuremath{\mathsf{note}}\xspace}
\renewcommand{\notes}{\ensuremath{\overrightarrow{\mathsf{note}}}\xspace}
\newcommand{\noteenc}{\ensuremath{\mathsf{enc}}\xspace}
\newcommand{\epk}{\ensuremath{\mathsf{epk}}\xspace}
% \newcommand{\pk}{\ensuremath{\mathsf{pk}}\xspace}
\newcommand{\gr}{\ensuremath{\mathsf{g}_\mathbf{r}}\xspace}
\newcommand{\gsig}{\ensuremath{\mathsf{g}_{\mathbf{sig}}}\xspace}
\newcommand{\gnk}{\ensuremath{\mathsf{g}_{\mathbf{n}}}\xspace}
\newcommand{\gv}{\ensuremath{\mathsf{g}_{\mathbf{v}}}\xspace}
% \newcommand{\pk}{\ensuremath{\mathsf{pk}}\xspace}
\newcommand{\rawtx}{\ensuremath{\mathsf{raw_{tx}}}\xspace}
\newcommand{\pretx}{\ensuremath{\mathsf{pre\mhyphen tx}}\xspace}
\newcommand{\sigval}{\ensuremath{\sigma_{\mathsf{bind}}}\xspace}
\newcommand{\rcvs}{\ensuremath{\overrightarrow{\mathsf{rcv}}}\xspace}
\newcommand{\rcms}{\ensuremath{\overrightarrow{\mathsf{rcm}}}\xspace}
\newcommand{\pak}{\ensuremath{\mathsf{pak}}\xspace}
\newcommand{\ak}{\ensuremath{\mathsf{ak}}\xspace}
\newcommand{\akstar}{\ensuremath{\mathsf{ak}^*}\xspace}
\newcommand{\alphastar}{\ensuremath{\mathsf{\alpha}^*}\xspace}
\newcommand{\rcv}{\ensuremath{\mathsf{rcv}}\xspace}
\newcommand{\rk}{\ensuremath{\mathsf{rk}}\xspace}
\newcommand{\nk}{\ensuremath{\mathsf{nk}}\xspace}
\newcommand{\ovk}{\ensuremath{\mathsf{ovk}}\xspace}
\newcommand{\ivk}{\ensuremath{\mathsf{ivk}}\xspace}
\newcommand{\IVK}{\ensuremath{\mathbf{IVK}}\xspace}
\newcommand{\MPH}{\ensuremath{\mathbf{MPH}}\xspace}
\newcommand{\nsk}{\ensuremath{\mathsf{nsk}}\xspace}
\newcommand{\ask}{\ensuremath{\mathsf{ask}}\xspace}
\newcommand{\signallinputs}{\ensuremath{\mathsf{sign\mhyphen all\mhyphen inputs}}\xspace}
\newcommand{\spendverify}{\ensuremath{\mathsf{spendverify}}\xspace}
\newcommand{\pubinp}{\ensuremath{\mathrm{pub}}\xspace}
\newcommand{\wit}{\ensuremath{\mathsf{w}}\xspace}
\newcommand{\outstatement}[1]{\ensuremath{\mathsf{OUT}(#1)}\xspace}
\newcommand{\spendstatement}[1]{\ensuremath{\mathsf{SPEND}(#1)}\xspace}
\newcommand{\cm}{\ensuremath{\mathsf{cm}}\xspace}
\newcommand{\nf}{\ensuremath{\mathsf{nf}}\xspace}
\renewcommand{\path}{\ensuremath{\mathsf{path}}\xspace}
\newcommand{\cv}{\ensuremath{\mathsf{cv}}\xspace}
\newcommand{\rt}{\ensuremath{\mathsf{rt}}\xspace}
\newcommand{\prf}{\ensuremath{\pi}\xspace}
\renewcommand{\input}{\ensuremath{\mathsf{input}}\xspace}
\renewcommand{\output}{\ensuremath{\mathsf{output}}\xspace}
\newcommand{\inputs}{\ensuremath{\overrightarrow{\mathsf{input}}}\xspace}
\newcommand{\invals}{\ensuremath{\overrightarrow{\mathsf{v}}}\xspace}
\newcommand{\outvals}{\ensuremath{\overrightarrow{\mathsf{ov}}}\xspace}
\newcommand{\sigs}{\ensuremath{\overrightarrow{\mathsf{\sigma}}}\xspace}
\newcommand{\alphas}{\ensuremath{\overrightarrow{\mathsf{\alpha}}}\xspace}
\newcommand{\aks}{\ensuremath{\overrightarrow{\mathsf{ak}}}\xspace}
\newcommand{\asks}{\ensuremath{\overrightarrow{\mathsf{ask}}}\xspace}
\newcommand{\ivks}{\ensuremath{\overrightarrow{\mathsf{ivk}}}\xspace}
\newcommand{\sks}{\ensuremath{\overrightarrow{\mathsf{sk}}}\xspace}
\newcommand{\outputs}{\ensuremath{\overrightarrow{\mathsf{output}}}\xspace}
\newcommand{\rcm}{\ensuremath{\mathsf{rcm}}\xspace}
\newcommand{\val}{\ensuremath{\mathsf{v}}\xspace}
\newcommand{\outval}{\ensuremath{\mathsf{ov}}\xspace}
 \newcommand{\NF}{\ensuremath{\mathbf{NF}}\xspace}
 \newcommand{\KDF}{\ensuremath{\mathbf{KDF}}\xspace}
% \newcommand{\createaddr}{\ensuremath{\mathsf{createaddr}}\xspace}
\newcommand{\provoutput}{\ensuremath{\pi_{\mathsf{output}}}\xspace}
\newcommand{\provspend}{\ensuremath{\pi_{\mathsf{spend}}}\xspace}
\newcommand{\symencrypt}[2]{\ensuremath{\mathbf{ENC}_{#1}(#2)}\xspace}
\newcommand{\symdecrypt}[2]{\ensuremath{\mathbf{DEC}_{#1}(#2)}\xspace}
\newcommand{\sighash}{\ensuremath{\mathbf{sighash}}\xspace}
\newcommand{\outverify}{\ensuremath{\mathbf{outverify}}\xspace}
\newcommand{\MAXVAL}{\ensuremath{\mathsf{MAX}}\xspace}
\newcommand{\GH}{\ensuremath{\mathrm{GH}}\xspace}

\newcommand{\dec}{\ensuremath{\mathsf{\mathbf{dec}}}\xspace}
\newcommand{\np}{\ensuremath{\mathsf{np}}\xspace}
\newcommand{\ghash}{\ensuremath{\mathsf{GH}}\xspace}
\renewcommand{\d}{\ensuremath{\mathsf{d}}\xspace}
\newcommand{\secret}{\ensuremath{\mathsf{shared\mhyphen secret}}\xspace}
\newcommand{\jof}[1]{\ensuremath{#1_j}\xspace}
\section{Description of Sapling}
 \subsection{Basic components}
\subsection*{Functions, and their requirements:}
We do not explicitly state function domains and ranges; see the spec for more details.
Whenever discussing a function in the properties below, we always think of an infinite sequence of functions indexed by the security parameter $\lambda$.
\begin{enumerate}
 \item For any fixed values $\gd,\pk,\val$, and for any $\eps\geq 0$, $\notecom(\gd,\pk,\val,\rcm)$ is $\eps$-close to uniform when $\rcm$ is $\eps$-close to uniform.
 \item \notecom is collision resistant - i.e. the probability of finding $\note,\note'$ such that $\notecom(\note)=\notecom(\note')$ is \negl. \footnote{A caveat here is that this is true when the $\rcm$ parameter is thought of as a field element; in the actual circuit it is received as a string of bits where some elements of $\F$ have multiple representations; inspection of the proof shows that it suffices that CR w.r.t \rcm as a field element; same story with \rcv in \valcom.}
\item For any fixed \val and any $\eps\geq 0$, $\valcom(\val,\rcv)$ is $\eps$-close to uniform whenever \rcv is $\eps$-close to uniform. 
\item \valcom is collision-resistant.
\item \sighash is collision-resistant.
\item \IVK is collision-resistant.
\item \NF is collision resistant
%and has the structural property that $\NF(\nk,\note,\pos) = \RO(\nk,\notecom(\note),\pos)$ for some function \RO 
(see another requirement for the indistinguishability property in Section \ref{sec:indist}).
\end{enumerate}

\paragraph{Generators of \G}
We assume we are given generators $\gsig,\gnk,\gr,\gv$ that were sampled in a way that except w.p \negl
an efficient \adv cannot discover the discrete log relation between any two of them.

\subsection*{Statements:}
\underline{\textbf{\outstatement{\cv,\cm,\epk}:}}
I know $\note=(\gd,\pk,\val,\rcm),\rcv,\esk$ such that 
\begin{enumerate}
 \item $\cm = \notecom(\note)$.
 \item $\cv = \valcom(\val,\rcv)$.
 \item $\epk=\esk\cdot \gd$.
 \item $\gd$ has order greater than eight.
\end{enumerate}
\noindent
\underline{\textbf{\spendstatement{\rt,\cv,\nf,\rk}:}}
I know $\path,\pos,\note=(\gd,\pk,\val,\rcm),\cm,\rcv,\alpha,\ak,\nsk$ such that 
\begin{enumerate}
 \item $\cm = \notecom(\note)$.
 \item Either $\val=0$ (``dummy note''); or \path is a merkle path from \cm at position \pos to \rt.
 \item $\rk = \ak + \alpha \cdot \gsig$.
 \item Setting $\nk \defeq \nsk\cdot \gnk, \ivk \defeq \IVK(\ak,\nk)$; we have $\pk=\ivk\cdot \gd$.
 \item $\nf = \NF(\nk,\cm,\pos)$
\end{enumerate}

\subsection*{Components}
A \emph{note} is a tupple $\note = (\gd,\pk,\val,\rcm)$ where 
\begin{enumerate}
 \item $\gd,\pk \in \G$.
 \item $\val, \rcm \in \F$
 \item $\val \leq \MAXVAL$.
\end{enumerate}

An \emph{output base} $\output=(\gd,\pk,\val)$ is the same as a note excluding the \rcm component.
\begin{remark}
 It is convenient for us to define a note with \gd rather than its \GH-preimage \d as in the spec, as this is what's given as input to the circuits; there are minor non-exploitable issues with this, see e.g. https://github.com/zcash/zcash/issues/3490.
\end{remark}



For $\ivk \in \F$ we say \note \emph{belongs to \ivk} if $\pk =\ivk \cdot \g$.\\




An \emph{input base}, usually denoted \input, will consist of the values required to make an input in a Sapling transaction, except the spending key; namely $\input = (\note,\path,\pos,\pak)$ where
\begin{itemize}
 \item \note is a note
 \item \path is a path in a merkle tree beginning from a leaf of value $\cm=\notecom(\note)$.
 \item \pos is the position of \cm amongst the leaves of the Merkle tree (\pos is redundant here as it can be derived from \path, but convenient).
 \item \pak is a proving key to make SNARK spend proofs about the note.
\end{itemize}

We say \input is \emph{consistent with \rt} if \path ends at \rt.

A \emph{transaction input}, usually denoted \inp, is the final form in which an input appears in a transaction; \inp consists of 
\begin{enumerate}
 \item A value commitment \cv.
 \item A nullifier \nf.
 \item A Merkle root \rt of the tree containing the used note.
 \item A public key \rk that is (allegedly) a randomized version of the spent note's proving key \ak.
 \item A SNARK proof \prf for the statement \spendstatement{\rt,\cv,\nf,\rk}.
\end{enumerate}


\subsection{Methods}

We use the convention that $\ell$ denotes the number of inputs in a transaction, and $s$ the number of outputs.

\noindent
\underline{$\makeinput(\rt,\input=(\note,\path,\pos,\pak),\rcv,\alpha)$}

where \input is an input base consistent with \rt.

\begin{enumerate}
\item \cm = \notecom(\note)
 \item \nf = \NF(\nk,\note,\pos)
 \item Define $\rk\defeq \ak +\alpha\cdot \gsig, \cv\defeq  \val\cdot \gv+ \rcv\cdot \gr $.
 \item Let $\prf = \provspend(\cv,\rt,\nf,\rk;\note,\pak,\alpha,\path,\pos)$.
 \item Output $\inp=(\cv,\rt,\nf,\rk,\pi)$.
\end{enumerate}

\noindent
\underline{\makeoutput(\note=(\gd,\pk,\val,\rcm),\rcv)},
\begin{enumerate}
 \item Choose random $\esk\in \F$.
 \item Let $\cv\defeq \valcom(\val,\rcv) = \val\cdot \gv + \rcv\cdot \gr$.
 \item Let $\note = (\gd,\pk,\val,\rcm)$ and $\cm\defeq \notecom(\note)$.
 \item Let $\epk = \esk\cdot \gd$.
 \item Let $\noteenc = \symencrypt{\KDF(\esk\cdot \pk,\epk)}{\note}$
 \item Let $\prf = \provoutput(\epk,\cm,\cv;\note,\rcv,\esk)$.
 \item Output $(\cv,\cm,\epk,\prf,\noteenc)$
\end{enumerate}
\noindent
\underline{\makerandomizedoutput(\note=(\gd,\pk,\val),\rcv)},
\begin{enumerate}
 \item Choose random $\esk,\rcm\in \F$.
 \item Let $\cv\defeq \valcom(\val,\rcv) = \val\cdot \gv + \rcv\cdot \gr$.
 \item Let $\note = (\gd,\pk,\val,\rcm)$ and $\cm\defeq \notecom(\note)$.
 \item Let $\epk = \esk\cdot \gd$.
 \item Let $\noteenc = \symencrypt{\KDF(\esk\cdot \pk,\epk)}{\note}$
 \item Let $\prf = \provoutput(\epk,\cm,\cv;\note,\rcv,\esk)$.
 \item Output $(\cv,\cm,\epk,\prf,\noteenc)$
\end{enumerate}
\noindent
\underline{\bindvaltx(\rawtx=(\inps,\outs,\vbal),\rcvs)}

\begin{enumerate}
 \item Let $r\defeq\sum_{i=1}^\ell \rcv_i - \sum_{i=\ell+1}^{\ell+s}\rcv_i$
 \item Let $S\defeq\sum_{i=1}^\ell \cv_i - \sum_{i=\ell+1}^{\ell+s}\cv_i-\vbal\cdot \gv$
 \item Let $\sigval \defeq \sign_{\gr}(r,\sighash(\rawtx))$.
 \item Output $\pretx\defeq (\rawtx,\sigval)$.
\end{enumerate}

% \underline{\verifyinput{\inp=(\nf,\rt,\rk,\pi}}
\noindent
\underline{\signtx{\pretx=(\rawtx,\sigval),\asks,\alphas}}
\begin{enumerate}
 \item For each $i\in [\ell]$, let $\sigma_i\defeq \sign_{\gsig}(\ask_i+\alpha_i,\sighash(\rawtx))$
 \item Let $\sigs\defeq (\sig_1,\ldots,\sig_\ell)$.
 \item Output $(\rawtx,\sigs)$.
\end{enumerate}

Given $(\rt,\vbal)$ we say $(\inputs,\outputs)$ is \emph{consistent} with $\rt,\vbal$,

if
\begin{itemize}
 \item for each $j\in [\ell]$ $\input_j$ is consistient with \rt, i.e. \jof{\pak} is from $\notecom(\note_j)$ to \rt,
 \item $\sum_{j=1}^{\ell} \val_j-\sum_{j=\ell+1}^{\ell+s} \val_j=\vbal$.
 \item the positions \sett{\pos_j}{j\in [\ell]} are all distinct.
\end{itemize}


and \\
\noindent
\underline{\makerandomizedtx(\rt,\vbal,\inputs,\outputs)}

\noindent
where $\input_j = (\note_j,\pak_j,\path_j,\pos_j), \output_j =(\gd_j,\pk_j,\val_j)$
\begin{enumerate}
 \item Choose random $\rcvs\in \F^s$.
 \item For $j\in [\ell]$, $\inp_j = \makeinput(\rt,\input_j,\rcv_j)$
 \item For $j\in [s]$, $\out_j=\makeoutput(\output_j,\rcv_j)$
 \item $\pretx = \bindvaltx(\inps,\outs,\vbal)$.
 \item Choose random $\alphas\in \F^{\ell}$.
 \item Output $\tx = \signtx{\pretx,\ask,\alphas}$
\end{enumerate}

\noindent
\underline{\maketx(\inputs,\outputs,\rcvs,\ask,\pak)}
where $\input_j = (\val_j,\note_j,\pak_j,\path_j,\pos_j), \output_j =(\gd_j,\pk_j,\val_j,\rcm_j)$
\begin{enumerate}
\item Choose random $\alphas\in\F^{\ell}$.
 \item For $j\in [\ell]$, $\inp_j = \makeinput(\input_j,\rcv_j,\alpha_j,\pak)$
 \item For $j\in [s]$, $\out_j=\makeoutput(\output_j,\rcv_j)$
 \item Let $\vbal \defeq \sum_{i=1}^\ell\val_i - \sum_{j=\ell+1}^{\ell+s}\val_j$.
 \item $\pretx = \bindvaltx(\inps,\outs,\vbal,\rcvs)$.
 \item Let $\tx = \signtx{\pretx,\alphas,\ask}$
\end{enumerate}

\noindent
\underline{\verifytx{\ledger}{\tx}}

\begin{enumerate}
\item Suppose that $\tx=(\rawtx,\sigs)$.
\item For each $\inp_i =(\rt,\cv,\nf,\rk,\prf)\in \inps(\tx)$,
 \begin{itemize}
  \item Check that $\nf \notin \nfof{\ledger}\cup \set{\nfof{\inp_1},\ldots,\nfof{\inp_{i-1}}}$.
  \item Check that $\spendverify(\rt,\cv,\nf,\rk;\prf)$.
  \item Check that $\versig^{\RO}_{\gsig}(\rk,\sighash(\rawtx),\sig_i)$
 \end{itemize}
\item For each $\out = (\cv,\cm,\epk,\prf,\noteenc)\in\outs(\tx)$, check that  $\outverify(\cv,\cm,\epk;\prf)$
\item Let $S\defeq\sum_{i=1}^\ell \cv_i - \sum_{i=\ell+1}^{\ell+s}\cv_i-\vbal\cdot \gv$.
\item Check that $\versig^{\RO}_{\gr}(S,\sighash(\rawtx),\sigval)$.
\end{enumerate}


%where $\note =$ 





\section{Non-Malleability of Sapling w.r.t. delegated spenders}


We make the simplifying assumption when modelling non-malleability in this writeup; that \emph{there is only one spending key $(\ask,\nsk)$ of the honest signer  involved, and all addresses are diversifed addresses derived from this spending key}.
\subsection*{Modelling the adversary:}

We wish to show that the delegated spender cannot create any new transactions of her own.
We model this claim with the following non-malleability game:
We model the honest signer as an oracle \oracle that \adv interacts with as follows.
% 
% \paragraph{Create address queries}
% \oracle stores an initially empty set $K$ of secret keys to its addresses.
% When \adv issues a \createaddr query. \oracle
% \begin{enumerate}
%  \item Chooses random $\sk \leftarrow \keyset$
%  \item Adds $\sk$ to $K$.
%  \item Derives the corresponding proof authorizing key $\pak(\sk)$.
%  \item Sends \pak to \adv.
% \end{enumerate}


\oracle begins by choosing a new spending key $(\ask,\nsk)\leftarrow \keyset$ and sending the corresponding proof authorizing key
$\pak=(\ak,\nsk)$ to \adv.  Where $\ak=\ask\cdot \gsig$.


Afterwords, 
\adv can make \signallinputs queries to \oracle,
which intuitively correspond to asking for signatures on transactions whose inputs have spending key $(\ask,\nsk)$ (though see remark). 
\paragraph{Sign-all-inputs queries}% - $\signallinputs(\rawtx,\aks,\alphas)$}
\begin{enumerate}
 \item \adv sends $(\pretx=(\rawtx,\sigval),\alphas)$ to \oracle.
 Where $\rawtx = (\inps,\outs,\vbal)$
 \item \oracle checks if $\spendverify(\pubinp_i,\prf_i)$ holds for each $i\in [\ell]$ and otherwise aborts.
 \item  \oracle computes for $i\in [\ell]$, $\sig_i = \sign_{\gsig}(\ask+\alpha_i,\sighash(\rawtx))$.
 \item Let $\sigs\defeq (\sig_1,\ldots,\sig_\ell)$. \oracle return $\tx\defeq(\rawtx,\sigval,\sigs)$. 
\end{enumerate}
\begin{remark}
 The second item is another way of saying we assume \adv can only ask \oracle for signatures of transactions with legitimate spend proofs.
 Otherwise the proof currently fails as we need to be able to extract the witness from each input.
\end{remark}

% \textbf{\oracle must record its answers to previous \signallinputs queries and answer identically to repeating queries}
% \begin{remark}
% This requirement is needed for the non-malleability property stated in Claim \ref{clm:nmal}. Different signatures on repeating queries enable \adv to violate the claim by mixing and matching different signatures for the same raw transaction. Alternatives are to only demand the non-signature part is NM, or to have each $\sig_i$, also sign the previous signatures.
%  
% \end{remark}


\paragraph{Terminology:}
We refer below to a transaction \tx as $\tx=(\rawtx,\sigval,\sigs)$, where \sigs contains the $\ell$ input signatures and \sigval is as described above in 
\maketx{} 
that are added during \signallinputs \emph{and} the signature \sigval added in the last step of \maketx.

Non-malleability says, \adv should not be able to create a new valid transaction with inputs belonging to \oracle,
even after seeing transactions of its choice with inputs of \oracle. New will mean that the \rawtx part will be new.
(If we had changed the signature scheme to sign in order and have each signature sign the previous ones we could have required that
\tx including the signature part must be different from all previous transactions).

The way we formalize ``transaction with inputs of \oracle'' is that the transaction created by \adv contains 
overlapping nullifiers with the transactions signed previously by \oracle; precisely transactions that are outputs of \signallinputs queries.

\begin{remark}\label{rem:weirdstuff}
 A somewhat odd thing about the construction with the delegated spender, is that valid transactions signed by \oracle, do not exactly correspond to transactions whose inputs \oracle knows the spending key of. We can only say \oracle and \adv \emph{together} know the spending key.
 For example, given $(\ak,\nsk)$, \adv can choose random $s\in \F$, set $\ak' \defeq \ak + s\cdot \gsig$.   
 Now when \adv wants to sign an input in address $\ak'$, i.e. with some randomized key $\rk = \ak'+ \alpha \gsig  = \ak + (s+\alpha)\cdot \gsig$,
 it can give \oracle the randomization $\alpha' = s+\alpha$.
 
 A way to avoid these oddities is to have \oracle only sign transactions where he recognizes the nullifiers as belonging to a note of his.
 For our purposes here, we get a stronger result without this restriction by showing non-malleability holds when \oracle signs \emph{any} transaction.
\end{remark}



\paragraph{Some more terminology}
Given a validly formatted transaction $\tx=((\inps,\outs,\vbal), \sigval,\sigs)$,
we define 
\begin{itemize}
 \item \nfof{\tx} to be the set of nullifiers appearing in one of its inputs; so $\nfof{\tx}\defeq \sett{\nfof{\inp}}{\inp\in\inps}$.
\item \rkof{\tx} the set of randomized public keys appearing in inputs of \tx, so $\rkof{\tx}\defeq \sett{\rkof{\inp}}{\inp\in\inps}$.
\item $\rawof{tx}\defeq (\inps,\outs,\vbal)$. For a set $T$ of validly formed transactions we define $\rawof{T}\defeq \sett{\rawof{\tx}}{\tx\in T}$
\end{itemize}
\begin{claim}[Non-malleability w.r.t delegated spenders]\label{clm:nmal-sapling}
Fix any efficient \adv interacting with \oracle as described above.
Let $T=\set{\tx'}$ be the set of transactions that are replies of \oracle to \adv's \signallinputs queries.
The probability that \adv manages to output a ledger \ledger and transaction \tx such that

\begin{enumerate}
 \item	$\verifytx{\ledger}{\tx}=\acc$,
 \item  $\rawof{\tx}$ is not a prefix of an element of $T$.
 \item $\nfof{\tx} \cap \nfof{\tx'}\neq \emptyset$ for some  $\tx'\in T$.
\end{enumerate}
is \negl. 
\end{claim}
\begin{proof}
Let \adv be an algorithm that after interacting with \oracle as described above outputs \ledger,\tx.
Let \eps be the probability that \ledger, \tx satisfy the above, and assume for contradiction $\eps = 1/\poly$.

We construct \advprime that receives a randomized forgery challenge for \schnorr as described in Definition \ref{dfn:sigscheme},
and with probability $\eps-\negl$ either
\begin{itemize}
\item outputs a collision of \sighash
\item outputs a collision of \NF, 
 %\item outputs a collision of \notecom, 
 \item outputs a collision of \IVK, 
\item  Constructs a signature forgery for \schnorr w.r.t randomization.
\end{itemize}


Then, from CR of \sighash, \NF,\notecom,\IVK and Theorem \ref{thm:schnorr-nf} the claim follows.
%For convenience we use the abbreviation $\g=\gsig$ in the rest of this proof.
\advprime works as follows:
\begin{enumerate}
\item \advprime will receive a challenge \akstar for the signature scheme \schnorr sampled by the procedure \sample described in Section \ref{sec:signatures}.
 \item \advprime chooses random $\nsk\in \G$ and sends to \adv the proof authorizing key $\pak=(\nsk,\ak)$ 
 \ariel{note that here we need to make a spending key that is not from the same seed \sk}
 \item When \adv makes a \signallinputs query $(\rawtx,\alphas)$ \advprime first checks that the proofs in \rawtx are valid (as \oracle does in the description of \signallinputs queries) and then answers with \sigs where $\sig_i\defeq \simprv(\ak+\alpha_i\cdot \gsig,\msg)$. If during invocations to \simprv, \simro is queried on a point on which \adv queried \RO, \advprime aborts. (Note that the point queried by \simro is $(R,\rk,\msg)$ for a uniform $R$ chosen only during the execution of \simprv, so the probability such a point was already queried is \negl.)
 \item When \advprime makes a query to \RO, \adv answers according to \RO unless the query has already been answered according to \simro during invocations of \simprv in \signallinputs queries; in which case \advprime answers according to \simro. (This doesn't change the distribution of \RO from the perspective of \adv.)
 \item When \adv outputs \ledger, \tx: \advprime checks that it indeed satisfies the challenge - that is 
  $\verifytx{\ledger}{\tx}$; \tx contains an input \inp with $\nf=\nfof{\inp}$ being equal to $\nf(\inp')$ for some $\inp'\in \tx'$ for some $\tx'\in T$;
  appearing in one of the \signallinputs queries of \adv; and $\rawtx\notin \rawof{T}$. If not, \advprime aborts.
\item \advprime checks if  $\sighash(\rawtx)= \sighash(\rawtx'')$ for some $\tx''\in T$ with $\rawtx\neq \rawtx''$. If so it outputs $(\rawtx,\rawtx'')$ as a collision of \sighash.
\end{enumerate}

\textit{Explanation of where we are so far:} Denote by \rk and \sig the public key and signature in \inp. Let $\msg \defeq \sighash(\rawtx)$. \sig is a valid signature for message \msg and public key \rk, and \msg was never signed in reply to the \signallinputs queries by \oracle. To obtain a forgery w.r.t randomizatoin for the challenge \akstar, what is left is to find the \alphastar such that $\rk=\akstar+\alphastar\cdot \gsig$. The purpose of the next steps is to obtain such \alphastar or a collision of one of our CRH functions.
%  \item Denote from now by \rk and \sig the public key and signature in \inp. Let $\msg \defeq \sighash(\rawtx)$.
%  Since \msg is different from all the messages for which \adv received simulated signatured, \sig is a valid signature of \msg with key \rk. Thus, for \advprime to have a successful reply to the forgery challenge \akstar, it suffices 
%  
%  Let $R\defeq\set{\rk_1,\ldots,\rk_\ell}$ be the randomized public keys in the inputs of \tx,
%  and $R'\defeq \set{\rk'_1,\ldots,\rk'_{\ell}}$ be the randomized public keys in the inputs of $\tx'$.
%  \advprime checks if $R\cap R' \neq \emptyset$, i.e. $\rk_i=\rk'_j$ for some $i,j$.
% In such a case, since $\rk_i = \rk'_j=\akstar + \alpha'_j\cdot \gsig$ where $\alpha'_j$ was part of a query of \adv to \advprime; \advprime knows the discrete log $\alpha'_j$ of $\rk_i-\akstar$, and therefore can output the forgery w.r.t randomization of \ak $(\alpha'_j,\sighash(\rawtx),\sig_i)$.
\begin{enumerate}[resume]
 \item Otherwise, denote by $B$ the algorithm consisting of execution of all parties up to this point outputting \tx and \primeof{\tx}. Note that $B$'s randomness consists\footnote{We have not defined collision-resistant functions too formally. To be more accurate we assume all CRH functions are ``public'' in the sense that their seed is just a random string, and this randomness is also one of the inputs to $B$.} of that of $\adv,\advprime,\RO$ used up to this point and the randomness of $\sample$.
 Let \ext be the extractor guaranteed to exist for $B$ for the input \inp in \tx. Recall that \ext requires $B$'s internal randomness to produce a SNARK witness. \advprime can give \ext the randomness of \advprime,\adv,\RO used up to this point, but instead of using the actual randomness of \sample as input to \ext, \advprime uses the \invert method to obtain this randomness correctly from \ak with $1/\poly$ probability. Given this input, with probability $1/\poly - \negl= 1/\poly$, \ext outputs for the input \inp in \tx a witness $\wit=(\note,\pak=(\ak,\nsk),\alpha,\path,\pos)$.
 Similarly there is an extractor \primeof{\ext} for the input $\inp'$ in $\tx'$ giving us a witness $\wit'=(\note',\pak'=(\ak',\nsk'),\alpha',\path',\pos')$. If \ext or \primeof{\ext} fails \advprime aborts (note that the probability of both succeeding is $1/\poly$).
\item Let $\nk\defeq \nsk\cdot \gnk, \nk'\defeq \nsk'\cdot \gnk$.  We have \[\NF(\nk,\note,\pos) = \NF(\nk',\note',\pos')=\nf.\]
If $\nk\neq\nk',\note\neq\note'$ or $\pos\neq \pos'$, \advprime outputs $(\nk,\note,\pos), (\nk',\note',\pos')$ as a collision of \NF.
% \item Otherwise, we have $\notecom(\note)=\notecom(\note')=\cm$.
% If $\note \neq \note'$, \advprime outputs $\note,\note'$ as a collision of \notecom.

\item Otherwise we have $\note=\note'=(\gd,\pk,\val,\rcm)$.
Defining
$\ivk\defeq \IVK(\ak,\nk), \ivk'\defeq \IVK(\ak',\nk)$,
we have $\pk= \ivk\cdot \gd = \ivk'\cdot \gd$. 
Thus, $\ivk=\ivk'$.
(Important here that \ivk representation is unique and it is cause dfn of $\IVK$ has $mod\;\; 2^{\ell_{\ivk}=251}$.)
If $\ak\neq \ak'$, \advprime outputs $(\ak,\nk),(\ak,\nk')$ as a collision of \IVK.

\item Otherwise, we have $\ak=\ak'$.
 Now, \advprime knows $\alpha^*$ such that $\rk' = \ak^* + \alpha^*\cdot \gsig$, where $\ak^*$ was the forgery challenge from \oracle (as \adv used $(\alpha^*,\sighash(\rawtx'))$ in the \signallinputs query for \primeof{\tx} for input \primeof{\inp}).
And also $\rk' = \ak' + \alpha'\cdot \gsig$.
So $\ak=\ak'= \ak^* + (\alpha^*-\alpha')\cdot\gsig$.
And $\rk = \ak^* +(\alpha^*-\alpha'+\alpha)\cdot \gsig$.
Thus, in this case \advprime outputs $(\alpha^*-\alpha'+\alpha, \sighash(\rawtx), \sig )$ as a signature forgery w.r.t randomization of \akstar.
 
\end{enumerate}

\end{proof}
\newcommand{\tree}{\ensuremath{\mathsf{T}}\xspace}
\newcommand{\curnotes}{\ensuremath{\mathsf{N}}\xspace}

\newcommand{\maketransaction}{\ensuremath{\mathsf{maketransaction}}\xspace}
% \subsection{Modelling the outside adversary}
% 
% \underline{$\maketransaction(\inputs,\outputs,\vbal,\ask)$}:
% \begin{enumerate}
%  \item For $i\in [\ell]$, check where $\input_i$ appears in the compute $\input_i\defeq \makeinput({{\inp}}_i)$.
% \item Check that $\sum_{i=1}^\ell \val_i - \sum_{j=1}^s \outval_j=\vbal$.
% If this is the case then $(\inputs,\outputs,\vbal)$ is a \emph{valid input} to \maketransaction.
% Otherwise output \rej and abort.
%  \item For $j\in [s]$, compute $\output_j \defeq \makeoutput({\out_j})$.
%  \item Choose uniform $\rcvs\in \F^s$ and output $\signallinputs(\maketx{(\inputs,\outputs,\vbal,\rcvs)},\ask)$
%  
% \end{enumerate}
% 
% \oracle begins by choosing a uniform spending key $(\ask,\nsk)\in\keyset$.
% And generates the corresponding keys $\ak\defeq \ask\cdot \g ,\nk\defeq \nsk\cdot\g, \ivk \defeq\IVK(\ak,\nk)$. 
% \adv and \oracle initialize an empty set $T$ of diversified addresses.
% % \adv and \oracle initialize an empty merkle tree \tree
%  \adv and \oracle initialize an empty set of current notes \curnotes. 
% \adv can make two kinds of queries.
% 
% \paragraph{Get new diversified address queries}
% \begin{itemize}
% \item\oracle chooses $\gd\in \G$ according to the distribution \GH of the group hash output.
% \item\oracle then outputs the diversified address $(\gd,\pk \defeq \ivk\cdot \gd)$.
% \item \adv and \oracle add $(\gd,\pk)$ to the set of diversified addresses $T$.
% \end{itemize}
% \paragraph{Make transaction queries}
% \begin{itemize}
% \item \adv chooses extended input notes $\input_1,\ldots,\input_\ell\in\curnotes$.
% \item \adv chooses output notes $\output_1,\ldots,\output_s$, with $\output_j = (\gd_j,\pk_j,\val_j,\rcm_j)$, for $(\gd_j,\pk_j)\in T$.
% \item \adv Chooses uniform $\rcvs\in \F^{s+\ell}$.
% \item \adv sends $(\inputs,\outputs,\rcvs)$ to \oracle.
% % \item \oracle computes $\inputs$ with $\inp_j\defeq \makeinput(\input_j)$, and $(\note_j,\out_j)= \makeoutputandnote(\output_j)$.
% \item \oracle returns $\tx\defeq \maketx(\inputs,\outputs,\rcvs,\ask,\pak)$ to \adv.
% \item \adv and \oracle add $\output_j$ to \curnotes for each $j$ s.t. $(\gd_j,\pk_j)\in T$.
% \item \adv and \oracle remove the elements of \inputs from \curnotes.
% \end{itemize}
% 
% 
%  
% \subsection{Non-malleability w.r.t outside adversary}
% \begin{claim}\label{clm:nmal-sapling-outside}
%  Suppose \adv interacts with \oracle as described above.
%  Then it outputs a transaction $(\ledger,\tx,\inp\in\tx)$.
%  The probability that there exists $\tx'\in T,\inp'\in \inputs(\tx')$ such that 
%  \begin{enumerate}
%   \item $\rawof{\tx}\neq \rawof{\tx'},\forall \tx'\in T$.
%   \item $\nf(\inp)=\nf(\inp')$.
%  \end{enumerate}
% is \negl.
% \end{claim}
% \begin{proof}
% Reduce to Claim \ref{clm:nmal-sapling}.
% We
% \end{proof}
\section{Indistinguishability w.r.t outside adversaries}\label{sec:indist}
For a sequence of random variables $X_1,\ldots,X_n$ it will be convenient in this section to denote  
$X_{<i}\defeq (X_1,\ldots,X_{i-1})$.
Let us say that random variables $X,Y$ are $\gamma$-independent if for
any events $A,B$
\[|\pr(X\in A \wedge Y\in B)-\pr(X\in A)\cdot \pr(Y\in B)|\leq \gamma.\]

We recall that the \emph{statistical distance} between $X$ and $Y$ is the maximum over all events $T$ of
\[|\pr(X\in T) - \pr(Y\in T)|.\]

We say $X,Y$ are \emph{$\gamma$-close} if they have statistical distance at most $\gamma$.

A calculation proves
\begin{claim}\label{clm:close_to_ind}
 Suppose $X=(X_1,X_2), Y=(Y_1,Y_2)$ are such that 
 \begin{itemize}
 \item $X_1$ and $Y_1$ are on the same range, are $\gamma_1$-independent and $\gamma_1$-close.
  \item 
 e.w.p $\gamma_2$ over the value $(x_1,y_1)$ of $(X_1,Y_1)$, $(X|X_1=x_1), (Y|Y_1 = y_1)$ are $\gamma_3$-independent.
 \item e.w.p $\gamma_2$ over the value $x_1$ of $X_1$, we have that $(X|X_1=x_1), (Y|Y_1=x_1)$ are $\gamma_3$-close.
 \end{itemize}

 Then $X,Y$ are $\gamma_1+\gamma_2+\gamma_3$-independent and $\gamma_1+\gamma_2+\gamma_3$-close.
 \end{claim}

 Induction then shows that
 \begin{claim}\label{clm:neg_close_to_ind}
  Suppose $t=\poly$. Suppose random variables $X=(X_1,\ldots,X_t),Y=(Y_1,\ldots,Y_t)$ are such that
  for any $i\in [n]$,
  
  \begin{itemize}
   \item 
e.w.p \negl over the value $(x,y)$ of $(X_{<i},Y_{<i})$,

  $(X_i|X_{<i}=x)$ and $(Y_i|Y_{<i}=y)$ are \negl-independent;
  and
  \item e.w.p \negl over the value $x$ of $X_{<i}$,
  $(X_i|X_{<i}=x)$ and $(Y_i|Y_{<i}=x)$
  are \negl-close.
  \end{itemize}
  Then $X,Y$ are \negl-independent and \negl-close.
 \end{claim}

% 
% \begin{claim}\label{clm:pairs_to_all}
%  Suppose $t=\poly$. Suppose \set{X_1,\ldots,X_t,X'_1,\ldots,X'_t} is a set of random variables such that
%  they are all identically distributed; and any pair of variables $X,Y$ from the set is \negl-close to independent.
%  Then, defining $X=(X_1,\ldots,X_t), X'=(X'_1,\ldots,X'_t)$, we have that $X,X'$ are \negl-close to independent and 
%  have statistical distance \negl.
% \end{claim}

Below we use \ROsig to denote the random oracle used by the signature algorithm.
\begin{thm}\label{thm:indist-sapling}
%Fix any $\rt,\vbal$.
Assume that 
\begin{enumerate}
 \item 
$\NF(\nk,\notecom(\note),\pos)= \RO(\nk,\MPH(\note,\pos))$ where \RO is a random oracle and \MPH is a collision-resistant function\footnote{The requirement here may seem a bit odd; it models the fact that $\notecom(\note)$ is a pedersen hash which is combined in \NF with a $\pos$-multiple of an independent group generator, followed by an application of BLAKE-2 on the result prefixed with \nk. In particular, BLAKE-2 takes the place of \RO in the implementation.}

\item
\KDF and \ROsig are also random oracles.
\item \symencrypt{K}{m} produces a uniform output when $K$ is uniform and $m$ is fixed.
\item The SNARK we are using is witness indistinguishable - i.e. the proof distribution depends \emph{only} on the public input and not on the witness.
\end{enumerate}


Then, the probability of an efficient \adv finding $\rt,\vbal,\inputs,\outputs,\inputs',\outputs'$
such that
\begin{itemize}
 \item 
$|\inputs|=|\inputs'| = \ell$, $|\outputs|=|\outputs'| =s $. 
\item The positioned notes in \inputs and $\inputs'$ are all distinct.
\item $(\inputs,\outputs)$ and $(\inputs',\outputs')$ are both consistent with $\rt,\vbal$.
\item The distributions of the random variables $D\defeq \makerandomizedtx(\rt,\vbal,\inputs,\outputs)$ and 

$D'\defeq \makerandomizedtx(\rt,\vbal,\inputs',\outputs')$,
over the randomness of the oracles \RO,\KDF and \ROsig, and the inner randomness of the signer, SNARK prover and the \makerandomizedtx method,
are not \negl-close and \negl-independent
\end{itemize}
is \negl.

\end{thm}
\begin{proof}
Let us denote by $(\inps,\outs,\sigval,\sigs)$ the output of $\makerandomizedtx(\rt,\vbal,\inputs,\outputs)$
and by $(\inps',\outs',\sigval',\sigs')$ the output of $\makerandomizedtx(\rt,\vbal,\inputs',\outputs')$
when using independent inner randomness, but joint randomness for the oracles $\RO,\ROsig,\KDF$.

We will consider $D$ and $D'$ as sequences of random variables $D=(X_1,\ldots,X_m), D'= (Y_1,\ldots,Y_m)$,
and show that for every $i\in [m]$ they satisfy the conditions of Claim \ref{clm:neg_close_to_ind}.

We begin with the inputs. Letting, for $i\in [\ell]$, $X_i = \inp_i, Y_i = \inp'_i$, the following claim shows
those conditions hold for the first $i\in [\ell]$.
% $\inp_1,\ldots,\inp_\ell,\inp'_1,\ldots,\inp'_\ell$
% are results of invocations of \makeinput with independent randomness
% $\rcv,\alpha$ and independent randomness of the SNARK prover.
% 
% We show that corresponding inputs and outputs are independent and identically distributed except w.p \negl.

\begin{claim}\label{clm:inps-areind}
E.w.p \negl over the randomness of \adv, for each $i\in [\ell]$ $\inp_{i},\inp'_{i}$ are identically distributed and independent given any fixing of $\inp_{<i},\inp'_{<i}$. 

\end{claim}																	
\begin{proof}
We show first that e.w.p. \negl over the randomness of \adv, $\inp_i,\inp'_i$ are independent conditioned on any fixing of $\inp_{<i},\inp'_{<i}$.
$\inp_1,\ldots,\inp_\ell,\inp'_1,\ldots,\inp'_\ell$
are results of invocations of \makeinput with independent randomness
$\rcv,\alpha$ and independent randomness of the SNARK prover.
Inspection shows the only opportunity for dependence amongst any two of them, even after conditioning on the value of the others, is having 
the random oracle  \RO queried at the same point during the invocations.
%Denote for convenience $\inp_{\ell+j} = \inp'_j$ for $j\in [\ell]$.
\RO is queried for the computation of \NF; so this only happens if %for some $i\neq j\in [2\ell]$ 
 \[(\nk_i,\MPH(\note_i,\pos_i)) =(\nk'_i,\MPH(\note'_i,\pos'_i)).\]
This implies $\MPH(\note_i,\pos_i) = \MPH(\note'_i,\pos'_i)$,
but \adv will only find such a collision w.p \negl.
When this doesn't happen $\inp_i$ and $\inp'_i$ are independent also given any fixing of the previous inputs.


Now to show they are identically distributed given a fixing of $\inp_{<i},\inp'_{<i}$.

 Suppose $\inp_i=(\nf,\rt,\rk,\cv,\prf)$, and $\inp'_i=(\nf',\rt',\rk',\cv',\prf')$.
 We show each element is identically distributed conditioned on any fixing of the previous ones.
 \begin{itemize}
  \item  $\nf =\RO(q)$ and $\nf'=\RO(q')$ where $q=(\nk,\MPH(\note,\pos)),q'=(\nk',\MPH(\note',\pos'))$. These are both uniform \emph{unless} one of the queries $q,q'$ was already made to \RO in a previous invocation; which would mean $\sett{(\note^*,\pos^*)}{(\note^*,\pos^*)\in \inp_{<i+1}\cup\inp_{<i+1}}$ contains a collision of \MPH which \adv can find only w.p \negl.
  \item $\rt=\rt'$.
  \item $\rk=\ak + \alpha\cdot \g$, $\rk' = \ak' +\alpha'\cdot \g$. Are both uniform in \G because of the uniform choice of $\alpha,\alpha'$ in \makerandomizedtx.
  \item $\cv=\val\cdot \gv + \rcv\cdot \gr$,$\cv'=\val'\cdot \gv' + \rcv'\cdot \gr'$. Are both uniform in \G because of the uniform choices of $\rcv,\rcv'\in \F$ in the executions of \makerandomizedtx.
  \item $\prf,\prf'$ - When  $(\nf,\rt,\rk,\cv)=(\nf',\rt',\rk',\cv')$, it follows from the witness indistinguishability of the SNARK
  that $\prf$ and $\prf'$ are identically distributed. They are independent for any fixing of the previous values, as given this fixing the value
  of $\prf,\prf'$ depends only on the inner randomness of the SNARK prover.
 \end{itemize}
 
\end{proof} 
We proceed with the elements of the the ouputs. It will be convenient now to view each element in $\out_j,\out'_j$ as 
separate random variables $X_i,Y_i$, and show that 
% for any fixing of $X_{<i},X'a_{<i}$
% they are \negl-close and \negl-independent.
% We go over the different possibilities \cv,\epk,\prf,\noteenc of the ``type'' of $X_i$
% \end{claim}
 
 \begin{enumerate}
  \item 
 E.w.p \negl over the fixing of $X_{<i}$, they are identically distributed given this fixing of both $X_{<i}$ and $Y_{<i}$.
 
 \item E.w.p \negl over the fixing of $X_{<i},Y_{<i}$ they are independent given the fixing.
\end{enumerate}
We show this for the different types of elements in $\out_j,\out'_j$:
 \begin{itemize}
  \item $\cv=\val\cdot \gv + \rcv\cdot \gr,\cv'=\val'\cdot \gv + \rcv'\cdot \gr$: are independent and uniform in \G because of the independent uniform choices of $\rcv,\rcv'\in \F$ in \makerandomizedtx.
  \item $\cm = \notecom(\gd,\pk,\val,\rcm)$,$\cm' = \notecom(\gd',\pk',\val',\rcm')$: are uniform and independent in \G because of the independent uniform choices of $\rcm,\rcm'\in \F$ in \makerandomizedoutput.
  \item $\epk=\esk\cdot \gd,\epk'=\esk'\cdot \gd$ are uniform and independent in \G because of the independent and uniform choices of $\esk,\esk'\in \F$ in \makerandomizedoutput.
  \item $\prf,\prf'$ - Assuming the pubic inputs $(\epk,\cm,\cv)=(\epk',\cm',\cv')$, it follows from the witness indistinguishability of the SNARK
  that $\prf$ and $\prf'$ are identically distributed. They are independent for any fixing of the previous values, as given this fixing the value
  of $\prf,\prf'$ depends only on the inner randomness of the SNARK prover.
  \item $\noteenc = \symencrypt{\KDF(k)}{(\gd,\pk,\val)}$,$\noteenc' = \symencrypt{\KDF(k')}{(\gd',\pk',\val')}$
  where $k\defeq (\esk\cdot\pk,\epk)$ and $k'\defeq (\esk'\cdot\pk',\epk')$:
 Assuming $k\neq k'$, and moreover \set{k,k'} are different from all the ``key seeds'' \set{k_j,k'_j} used in previous outputs; we have that the encryption keys $\KDF(k),\KDF(k')$ are uniform and independent of all previous variables.
 And thus by the theorem's assumption that \KDF is a random oracle $\noteenc,\noteenc'$ are uniform and independent in this case.
 Thus there are at most $\ell$ values of the preceding $\esk$ and at most $\ell$ values of the preceding $\esk'$ that 
 can prevent \noteenc and \noteenc' from being uniform and independent;
 which is a \negl-fraction of the possible values of the preceding values.
  \end{itemize}
  
  
  It is now left to deal with the signature elements. $\sigval,\sigval',\set{\sig_i,\sig'_i}$.
  
  The distribution of these elements is determined by the public key $\pk=\rk_i$ (or $\pk =S$ the sum of value commitments in the case of \sigval),
  the message $\msg = \sighash(\rawtx)$ they are signing, the internal randomness of the signing algorithm and the reply of the random oracle 
  \ROsig on the query point $(R,\pk,\msg)$.
  Thus, given a fixing of previous variables, the only case where a dependence between $\sig_i$ or $\sig'_i$ could be created is if there
  as a collision between the signatures in the choice of $R$ which happens w.p. \negl.
\end{proof}



% Now it's easy to see that
% \begin{claim}\label{clm:ind_of_inputs}
% Except with probability \negl, over the randomness of \adv,
%  $\inp_1,\ldots,\inp_\ell,\out_1,\ldots,\out_s,\inp'_1,\ldots,\inp'_\ell,\out'_1,\ldots,\out'_s$ are \negl-close to independent random variables.
% \end{claim}
% \begin{proof}
%   It follows from the above two claims that any pair of inputs, or pair of outputs are \negl-close to independent.
%   Since there are no colliding random oracle queries between inputs and outputs, the claim follows.
% \end{proof}
% 
% 
% Denote $\sig_0\defeq \sigval$.
% 
% 
% \begin{claim}\label{clm:ind_of_sigs}
% For any $i\in [0..\ell]$, and any 
%  Conditioned on any fixing of $\inp_1,\ldots,\inp_\ell,\out_1,\ldots,\out_s,\inp'_1,\ldots,\inp'_\ell,\out'_1,\ldots,\out'_s,\sig_0,\ldots,\sig_{i-1},\sig'_0,\ldots,\sig'_{i-1}$ the values
%  $\set{\sig_i,\sig'_i}$ are \negl-close to independent.
% \end{claim}
% \begin{proof}
%  The distribution of any given $\sig_i$ is of the form $R,u$ where $R\in \G$ is uniformly chosen by the signing algorithm as $a\cdot \gr$,
%  and $u=a+c\cdot \sk$ where $c=\ROsig(R,\pk,\sighash(\rawtx)$.
%  For dependence to be created we would need $R=R`$ which happens with probability $1/|\F|$.
%  More formally, e.w.p $1/|\F|$ over the probability of the values $x,y$ of $\sig_i,\sig'_i$,
%  we have 
% \[\pr(\sig_i=x \wedge \sig'_i =y)=\pr(\sig_i =x)\cdot \pr(\sig'_i =y)\]
%  which means $\sig_i,\sig'_i$ (conditioned on any fixing of all previous variables mentioned in the claim statement) are \negl-close to independent.
%  
% \end{proof}
% 
% 
% 
% 
% \begin{proof} (of Theorem \ref{thm:indist-sapling})
% Note that 
% % $\inp_1,\ldots,\inp_\ell, \out_1,\ldots,\out_s$ are all independent from each other. (Here we use that \set{\pos_j} are all different and thus \set{\nf_j}
% are independent values of the random oracle \NF at distinct inputs).
% $\sig_1,\ldots,\sig_\ell$ are independent from each other, depend on \inps and the inner randomness of the signer.
% 
% 
% $\inp_j$ has the form
% \[\inp_j = (\nf,\rt,\rk,\cv,\prf)\]
% 
%   
% 
% the signature \sigval: can be simulating by a signing oracle except w.p. \negl (get's ruined if \RO was already queried on point)
% the signatures \sigs: same.
% \end{proof}
\subsection{Balance}
The following claim states an adversary should not be able to create ``money out of thin air'';
or more specifically, extract more money from the shielded pool than was put in it.
In Sapling, the value $\vbal=\vbal(\tx)$ in a transaction \tx corresponds to the alleged difference of spend and output values (see Section 4.12 in the spec) and \tx is thought of as having  ;
thus over-extracting from the pool corresponds to a constructing a ledger where the sum of all \vbal values is strictly positive.
\begin{claim}\label{clm:balance-sapling}
 The probability that an efficient \adv generates ledger $\ledger=(\tx_1,\ldots,\tx_n)$ such that
 \[\sum_{\tx\in \ledger} \vbal(\tx) >0 \]
 is \negl.
\end{claim}

 \begin{proof}
 Given \adv that produces a ledger as in the claim statement w.p. $\gamma$, we construct an efficient \adv' that
 w.p $\gamma/2-\negl$ produces a collision of \IVK,\notecom,\treehash or \valcom.
 It follows that $\gamma =\negl$.
\begin{enumerate}
\item \adv' begins by running \adv and aborting if \adv hasn't output a ledger as in the claim.
\item Otherwise, given such a ledger \ledger, \adv' can apply an extractor for each SNARK proof in all inputs and ouputs in all transactions.
 For each transaction input $\inp\in \tx\in \ledger$, $\inp=(\cv,\nf,\rt,\rk,\pi)$, the extractor except w.p. \negl 
 outputs an input witness $\inpwitness = (\input=(\note,\path,\pos),\pak,\rcv,\alpha))$.
 We denote by $\posnote$ the \emph{positioned note} corresponding to \inp, $\posnote \defeq (\note,\pos)$.
 Similarly for every transaction output in some \tx in \ledger, $\out = (\cv,\cm,\epk,\pi,\noteenc)$,
 the extractor outputs $\outwitness= (\note,\esk,\rcv)$. The value \pos for the output note can be deduced from when it was added to \ledger,
 i.e., the location of \cm in the commitment tree.
 So again we can define for each \out, the corresponding positioned note $\posnote = (\note,\pos)$.
For $i\in [n]$ let us denote respectively by $\inpnotes_i,\outnotes_i$ the positioned input and output notes in $\tx_i$ \emph{with non-zero value}\footnote{Sapling enables the creation of dummy notes with zero value, for which the spend statement doesn't check Merkle path validity, cf. Section 4.7.2 in the spec).}.


We also use the extractor from Theorem \ref{thm:extractSchnorr} to find $s$ such that $S=s\cdot \gr$
where
\[S\defeq\sum_{i=1}^\ell \cv_i - \sum_{i=\ell+1}^{\ell+s}\cv_i-\vbal\cdot \gv\]
is the public key in the value binding signature \sigval.

If one of the extractor runs fails \adv' aborts. Note that w.p. at least $\gamma/2 -\negl$ \adv' doesn't abort.

\item  \adv' checks if for some $i\in [n]$ and $\inp\in \tx_i, \posnote(\inp)\notin \outnotes_{<i}$.

If so, let $\tx=\tx_i$. Let \rt be the root of the tree used in the public input of \inp; this is the tree $T_j$ formed from $\set{\tx_1,\ldots,\tx_j}$ for some $j<i$.
Let $\posnote=(\gd,\pk,\val,\rcm,\pos)$ and $\cm=\notecom(\gd,\pk,\val,\rcm)$.
\inpwitness contains a path $\path$ from \cm to \rt.
If \pos is an index of a leaf in $T_j$, there exists an extended note $\posnote'$ that was inserted to this position when constructing the ledger
and from \posnote' we can derive a path \path' from $\cm' = \notecom(\gd',\pk',\val',\rcm')$ in position \pos to \rt.
If $\path\neq\path'$, then going down from \rt to the first difference between \path and \path'
(ask Sean/Daira : is $T$ always a full tree with zeroes on other leaves? No you have filler values for the empty subtrees, need to check this are values that are hard to find route to - their impossible to find rout to - have no preimage)
%Assuming \path' always exists (the zero-padding option)
this difference gives a collision of \treehash that \adv' can output.


Otherwise, we have $\cm=\cm'$.
\note must be different from \note' because $\posnote' = (\note',\pos)\in \outnotes_{<i}$ but $(\note,\pos)\notin \outnotes_{<i}$.

Thus $\note,\note'$ is a collision of \notecom. In this case, \adv' outputs this collision and terminates.


Now suppose \pos is not a position of a leaf in $T_j$. This means there is only a partial path \path' in $T_j$ from \rt to a filler value with no preimage (see spec for details).
So, similarly we follow \path and \path' to their first difference - a difference that must exist becaues of the filler value; and this gives us a collision of \treehash that \adv' outputs.





\item Now \adv' checks if as a multiset $\inpnotes \defeq \inpnotes_1\cup\ldots\cup\inpnotes_n$ contains a repetition.
That is, there exists $\posnote= (\gd,\pk,\val,\rcm,\pos)$ such that for two distinct transaction inputs $\inp = (\cv,\nf,\rt,\rk,\pi), \inp'=(\cv',\nf',\rt',\rk',\pi')$ in \ledger;
if the corresponding extracted witnesses are $\inpwitness = (\input=(\note,\path,\pos),\pak,\rcv,\alpha)$,
$\inpwitness' = (\input'=(\note',\path',\pos'),\pak',\rcv',\alpha')$; then $(\note,\pos) = (\note',\pos') = \posnote$.


We show in this case that \adv' can output a collision of \IVK:


Let $\cm=\notecom(\gd,\pk,\val,\rcm)$.
Since $\nf\neq \nf'$,
and 
$\nf = \NF(\nk,\note,\pos),\nf'= \NF(\nk',\note,\pos)$;

we have  $\nk \neq\nk'$.

Also $\ivk = \IVK(\ak,\nk), \ivk'=\IVK(\ak',\nk')$,
and $\pk=\ivk\cdot \gd = \ivk'\cdot \gd$.
So $\ivk=\ivk'$ \ariel{Check with Sean is ivk canonical - checked}
And thus, \adv' can output $(\ak,\nk),(\ak',\nk')$ as a collision of \IVK.


\item Let us denote by $\bal(\tx)$ the (integer) sum of values in inputs of \tx minus the sum of values in output of \tx (notes meaning those output by the extractors);
and by $\rcv(\tx)$ the sum of values $\rcv$ in input witnesses of \tx minus the sum of values \rcv in output witnesses of \tx.
When reaching this point with no output we know that:

For each $i\in [n], \inpnotes_i \subset \outnotes_1\cup\ldots\cup\outnotes_{i-1}\setminus(\inpnotes_1\cup\ldots\cup\inpnotes_{i-1})$.

This implies 
\[\sum_{\tx\in\ledger} \bal(\tx) \leq 0.\]
 
We claim that we must have for some $\tx\in\ledger$, $\bal(\tx)\neq \vbal(\tx)$:
Otherwise, we would have
\[\sum_{\tx\in \ledger} \vbal(\tx) = \sum_{\tx\in\ledger} \bal(\tx) \leq 0,\]

contradicting the fact that \adv has managed to output \ledger with a positive sum of $\vbal$ values.

Thus, let $\tx=\tx_i$ be such that $\bal(\tx)\neq\vbal(\tx)$. We show in the next step how $\adv'$ uses this to output a collision of \valcom.

\item At this point, we know that $\bal(\tx) \neq \vbal(\tx)$. As both these values are in the open interval \footnote{See 
the spec for details: \vbal and \val in each transaction input/output are at most $2^{64}$ in absolute value, so assuming 
less than, e.g., $2^{r-66}$ transaction inputs and outputs in any transaction, this is true.} $(-r/2,r/2)$, we have also $\bal(\tx)\neq \vbal(\tx)$ $(\mathrm{mod}\;  r)$.
We show how to find a collision of \valcom with probability
$\gamma/\poly$. Since \tx verifies, we know that
$\versig^{\RO}_{\gr}(S,\sighash(\rawtx),\sigval)$ for 
\[S=\sum_{i=1}^\ell \cv_i - \sum_{i=\ell+1}^{\ell+s}\cv_i-\vbal\cdot \gv= \left(\sum_{i=1}^{\ell} \val_i-\sum_{i=\ell+1}^{s} \val_i\right)\cdot \gv + \left(\sum_{i=1}^{\ell} \rcv_i-\sum_{i=\ell+1}^{s} \rcv_i\right)\cdot \gr  - \vbal\cdot \gv.\]
% Using Theorem \ref{thm:extractSchnorr}, \adv' can 
% with probability $\gamma/2$ find $s$ such that $s\cdot \gr = S$.
Let $R\defeq \sum_{i=1}^{\ell} \rcv_i-\sum_{i=\ell+1}^{s} \rcv_i$  and $v\defeq \bal(\tx)-\vbal(\tx) (\mathrm{mod}\;  r)$.
We have $\valcom(v,R) = S$.

Recall that if \adv' has reached this stage without aborting, it has obtained $s$ such that $s\cdot\gr =S$.
Thus, we also have $\valcom(0,s) = S$.
Hence, noticing that $v\neq0$, $\adv'$ can output $(0,s), (v,R)$ as a collision of \valcom.

\end{enumerate}

 \end{proof}
 
\subsection{Spendability}

\paragraph{Valid transaction bases:}
A sequence $\txinput = (\inputs,\outputs,\vbal)$ is
a \emph{valid transaction base} if $\vbal =  \sum \val(\input_i) - \sum \val(\output_j)$.

We review note encryption and decryption from the spec in our notation.

% \paragraph{Encrypting notes:}
% Given $\note=(\gd,\pk,\val,\rcm)$ and outgoing viewing key \ovk.
% \begin{enumerate}
%  \item Choose random $\esk\in \F$ and let $\epk\def \esk\cdot g$.
%  \item Let $\secret \defeq \esk\cdot \pk$.
%  \item Let $\notenc = \symencrypt{\secret}{\note}$
% \end{enumerate}



\paragraph{Decrypting notes:\\}
\noindent
$\underline{\dec(\ivk,\out=(\cv,\cm,\epk,\prf,\noteenc))}$
\begin{enumerate}
\item Let $K\defeq \KDF(\epk\cdot \ivk)$
 \item Let $\np=\symdecrypt{K}{\noteenc}$. If \symdecrypt{}{} fails output \rej.
 \item Suppose $\np=(\d,\val,\rcm,\mathsf{memo})$. If $\rcm\geq r$ output \rej. 
\item Let $\gd\defeq \ghash(\d)$.
 \item Let $\pk\defeq \gd\cdot \ivk$. Let $\note\defeq (\gd,\pk,\val,\rcm)$.
 \item Check that $\cm=\notecom(\note)$. Output \rej if not.
 \item Output \note.
\end{enumerate}
We define 
\[\dec(\ivk,\tx) \defeq \cup_{\out\in\tx} \dec(\ivk,\out),\]
\[\dec(\ivk,\ledger) \defeq \cup_{\tx\in\ledger} \dec(\ivk,\tx)\]
And also
\[\nfof{\tx} \defeq \cup_{\inp\in\inps(\tx)}\nfof{\inp},\nfof{\ledger}\defeq\cup_{\tx\in\ledger}\nfof{\tx}\]
%We consider an adversary \adv that has access to \signallinputs queries of \oracle, identically to the non-malleability section.
% \adv receives a challenge $\pak = (\ak,\nsk)$ where $\nsk\in \F,\ak\in \G$ were chosen uniformly.
% Let $\ivk\defeq \IVK(\pak)$.
In the spendability game \adv tries to create a ledger where a note successfully decrypted with \ivk cannot be spent.
Formally, the game proceeds as follows.
\begin{enumerate}
 \item We choose uniform $\sk = (\ask,\nsk)$; and give $\pak=(\ask\cdot \gsig, \nsk)$ to \adv.
\item \adv outputs a ledger \ledger, a positioned note $(\note,\pos)$, a set of output notes \outputs, and
a set of incoming viewing keys \ivks. 
\item We choose random $\rcvs\in \F^{\ell+s}$ and compute $\tx = \maketx(\inputs,\outputs,\vbal,\ask)$.
\item Let $\ivk \defeq \IVK(\ak,\nk)$. \adv wins iff 
\begin{enumerate}
\item $\note \in \dec(\ivk,\ledger)$.
\item  $((\note),\outputs,\vbal)$ is a valid transaction base.
\item For each $i\in [s]$, $\output_i$ belongs to $\ivk_i$.
 \item $\verifytx{\ledger}{\tx}$.
 \item For some $i\in [s]$, $\dec(\ivk_i,\out_i)$ does not return $\output_i$.
\end{enumerate}
\end{enumerate}

We wish to show that the success of any efficient \adv in this game is \negl.


Let $\nk =\nsk\cdot\gnk$.
Inspection of the protocol shows this exactly corresponds to the nullifier of \note with nullifier key \nk already appearing in the ledger.
Thus, it suffices to prove the following.
\begin{claim}\label{sapling-spendability}
 Fix any efficient \adv.
 Suppose that \adv  is given uniformly chosen \pak, and let $\ivk \defeq \IVK(\pak)$.
The probability that \adv generates a ledger \ledger and positioned note (\note,\pos) such that 
 \begin{enumerate}
  \item $(\note,\pos)\in \dec(\ivk,\ledger)$
  \item $\NF(\nk,\notecom(\note),\pos)\in \nfof{\ledger}$ 
 \end{enumerate}
 is \negl.
\end{claim}
\begin{proof}
Let $\gamma$ be the probability that \adv outputs $\ledger,\note$ satisfying the two properties in the claim.
We construct an efficient \advprime that receives a forgery challenge \ak of \schnorr and w.p. $\gamma-\negl$ does one of the following.
\begin{itemize}
\item Output a collision of either \NF, \notecom or \IVK.
 \item Output a forgery w.r.t to randomization of \schnorr for the challenge \ak.
\end{itemize}


\advprime works as follows.

 \begin{enumerate}
  \item  \advprime receives a challenge \ak; chooses random $\nsk\in \F$ and sends $\pak=(\ak,\nsk)$ to \adv.
\item \advprime receives the output $(\ledger,\note,\pos)$ of \adv.
\item \advprime checks that $\ledger,(\note,\pos)$ satisfy the two properties in the claim; if not it aborts.
\item  Let $\nf \defeq \NF(\nk,\notecom(\note),\pos)$.
Fix the $\out,\tx$ with $\out\in\tx\in \ledger$ such that $\dec(\ivk,\out) = (\note,\pos)$.
\out contains a valid SNARK proof for \spendstatement{\rt,\cv,\nf,\rk} for some $\cv,\rt$.
Apply the relevant extractor \ext relating to the snark proof to
obtain e.w.p \negl a witness $\path,\pos',\gd',\pk',\val',\rcm',\cm',\rcv',\alpha,\ak',\nsk'$ for the statement.
\item Let $\nk' \defeq \nsk'\cdot \gnk$. If $(\nk,\cm,\pos)\neq (\nk',\cm',\pos')$, \advprime outputs $(\nk,\cm,\pos),(\nk',\cm',\pos')$ as a collision of \NF.
\item Otherwise, let $\note' = (\gd',\pk',\val',\rcm')$. We have $\cm=\notecom(\note)=\notecom(\note')$. If $(\gd',\pk',\val')\neq (\gd,\pk,\val)$, \advprime outputs $(\note,\note')$ as a collision of \notecom.
\item Otherwise, we must have $\ivk'=\ivk$ (cause $\gd\cdot \ivk = \gd \cdot \ivk' = \pk$). Then $\ivk = \IVK(\ak',\nk)$ (by this stage we know $\nk=\nk'$).
If $\ak\neq \ak'$, \advprime outputs $(\ak,\nk),  (\ak',\nk)$ as a collision of \IVK.
\item Otherwise $\ak=\ak'$, and $\rk = \ak + \alpha \cdot \g$. Let $\sigma$ be the signature of \rawtx with public key \rk in \inp.
and \advprime outputs $(\alpha, \rawtx, \sig)$ as a forgery of \schnorr with challenge \ak.
 \end{enumerate}

 
 
\end{proof}



\begin{remark}
 Note that in the spendability and non-malleability property \adv can choose what value \nf to work with.
 It seems likely that in a weaker model where the values \nf are generated randomly via honest users' notes, a second preimage resistance property of \NF would suffice (Thanks to Sean Bowe and Zooko Wilcox for mentioning this).
\end{remark}





% 
% ----------SECOND  ATEMPT-------------------
% 
% \adv interacts with \oracle by maketx queries and createaddr queries,
% can also insert txs to ledger.
% Keeps track of inputs not used yet.
% 
% 
% Del Spender in spendability game:
% List of unspent notes.
% Makes $\signallinputs(\tx)$ queries.
% These make $\nf(\tx)$ crossed off - actually what crossed off? Have \inp, not \input.
% Can add to ledger \ledger any valid \tx.
% $\decode_{\sk}(\tx)$ added to \curnotes.
% 
% 
% 
% % \subsection{Uniqueness}
% How to define?
% 
% 1 - Interact with honest player, either inserting tx to ledger, or 
% give them inputs and outputs, with inputs in their create address output.
% % honest decodes at the end of each transaction, 
% 
% output ledger, legal transaction input \txinput where \inputs
% are coins of honest player  that haven't been used.
% Such that \createtx{\ledger}{\txinput}
% fails (with some probability? with noticeable prob?)
% 
% is \negl.


%\subsection{Indistinguishability of diversified addresses}


% El-gammal encryption
% private key \sk
% public key $[\sk]\cdot \g$
% encryption of $x$: [\sk]
\section*{Acknowledgements}
We thank Matthew D. Green for conversations on simulation extractability that in particular 	inspired the definition and use of invertible group samplers.
\bibliography{refs}
\bibliographystyle{plain}
\end{document}