\documentclass[a3paper]{article}
\usepackage[margin=.25in]{geometry}
\usepackage[sets,operators,adversary,advantage,probability]{cryptocode}
\usepackage{tikz}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{hyperref}
\newcommand{\pcas}{~\highlightkeyword{as}}
\newtheorem{theorem}{Theorem}
\newtheorem{claim}{Claim}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\newcommand\lit[1]{\ensuremath{\mathtt{#1}}}
\renewcommand\O[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\M}[1]{\ensuremath{\text{\texttt{#1}}}}
\newcommand{\n}[1]{\ensuremath{\mathit{#1}}}
\tikzstyle{package} = [inner sep=1pt,align=center,rounded corners,draw,minimum width=2cm,minimum height=1cm,font=\small]
\tikzstyle{onarrow} = [inner sep=1pt,font=\scriptsize,anchor=west,at start,align=left,fill=white]
\title{Theorem: Simple4WHS}
\begin{document}
\maketitle
\tableofcontents
\clearpage
\section{Games}
\begin{minipage}{.245\textwidth}
\subsection*{\hyperref[section:game:Hybrid0]{Hybrid0 Game}}
\scalebox{0.66}{\input{CompositionGraph_Hybrid0.tex}}
\end{minipage}
\begin{minipage}{.245\textwidth}
\subsection*{\hyperref[section:game:Hybrid1]{Hybrid1 Game}}
\scalebox{0.66}{\input{CompositionGraph_Hybrid1.tex}}
\end{minipage}
\begin{minipage}{.245\textwidth}
\subsection*{\hyperref[section:game:Hybrid2]{Hybrid2 Game}}
\scalebox{0.66}{\input{CompositionGraph_Hybrid2.tex}}
\end{minipage}
\begin{minipage}{.245\textwidth}
\subsection*{\hyperref[section:game:Hybrid3]{Hybrid3 Game}}
\scalebox{0.66}{\input{CompositionGraph_Hybrid2.tex}}
\end{minipage}
\\
\begin{minipage}{.245\textwidth}
\subsection*{\hyperref[section:game:Real_Hybrid3]{Real\_Hybrid3 Game}}
\scalebox{0.66}{\input{CompositionGraph_Hybrid2.tex}}
\end{minipage}
\begin{minipage}{.245\textwidth}
\subsection*{\hyperref[section:game:Ideal_Hybrid3]{Ideal\_Hybrid3 Game}}
\scalebox{0.66}{\input{CompositionGraph_Hybrid2.tex}}
\end{minipage}
\begin{minipage}{.245\textwidth}
\subsection*{\hyperref[section:game:Ideal_PRF]{Ideal\_PRF Game}}
\scalebox{0.66}{\input{CompositionGraph_PRF.tex}}
\end{minipage}
\begin{minipage}{.245\textwidth}
\subsection*{\hyperref[section:game:Real_PRF]{Real\_PRF Game}}
\scalebox{0.66}{\input{CompositionGraph_PRF.tex}}
\end{minipage}
\\
\clearpage
\subsection{Hybrid0 Game}
\label{section:game:Hybrid0}
\begin{center}
\input{CompositionGraph_Hybrid0.tex}
\end{center}
\begin{pchstack}
\input{Package_Prot_in_Hybrid0_lossy.tex}
\pchspace
\input{Package_KX_in_Hybrid0_lossy.tex}
\pchspace
\end{pchstack}
\clearpage
\subsection{Hybrid1 Game}
\label{section:game:Hybrid1}
\begin{center}
\input{CompositionGraph_Hybrid1.tex}
\end{center}
\begin{pchstack}
\input{Package_Prot_in_Hybrid1_lossy.tex}
\pchspace
\input{Package_KX_in_Hybrid1_lossy.tex}
\pchspace
\end{pchstack}
\clearpage
\subsection{Hybrid2 Game}
\label{section:game:Hybrid2}
\begin{center}
\input{CompositionGraph_Hybrid2.tex}
\end{center}
\begin{pchstack}
\input{Package_Prf_in_Hybrid2_lossy.tex}
\pchspace
\input{Package_Prot_in_Hybrid2_lossy.tex}
\pchspace
\input{Package_KX_in_Hybrid2_lossy.tex}
\pchspace
\end{pchstack}
\clearpage
\subsection{Hybrid3 Game}
\label{section:game:Hybrid3}
\begin{center}
\input{CompositionGraph_Hybrid2.tex}
\end{center}
\begin{pchstack}
\input{Package_Prf_in_Hybrid2_lossy.tex}
\pchspace
\input{Package_Prot_in_Hybrid2_lossy.tex}
\pchspace
\input{Package_KX_in_Hybrid2_lossy.tex}
\pchspace
\end{pchstack}
\clearpage
\subsection{Real\_Hybrid3 Game}
\label{section:game:Real_Hybrid3}
\begin{center}
\input{CompositionGraph_Hybrid2.tex}
\end{center}
\begin{pchstack}
\input{Package_Prf_in_Hybrid2_lossy.tex}
\pchspace
\input{Package_Prot_in_Hybrid2_lossy.tex}
\pchspace
\input{Package_KX_in_Hybrid2_lossy.tex}
\pchspace
\end{pchstack}
\clearpage
\subsection{Ideal\_Hybrid3 Game}
\label{section:game:Ideal_Hybrid3}
\begin{center}
\input{CompositionGraph_Hybrid2.tex}
\end{center}
\begin{pchstack}
\input{Package_Prf_in_Hybrid2_lossy.tex}
\pchspace
\input{Package_Prot_in_Hybrid2_lossy.tex}
\pchspace
\input{Package_KX_in_Hybrid2_lossy.tex}
\pchspace
\end{pchstack}
\clearpage
\subsection{Ideal\_PRF Game}
\label{section:game:Ideal_PRF}
\begin{center}
\input{CompositionGraph_PRF.tex}
\end{center}
\begin{pchstack}
\input{Package_PRF_in_PRF_lossy.tex}
\pchspace
\end{pchstack}
\clearpage
\subsection{Real\_PRF Game}
\label{section:game:Real_PRF}
\begin{center}
\input{CompositionGraph_PRF.tex}
\end{center}
\begin{pchstack}
\input{Package_PRF_in_PRF_lossy.tex}
\pchspace
\end{pchstack}
\clearpage
\section{Advantages}
\begin{definition}[prf]
\label{advantage:assumption:prf:Real_PRF:Ideal_PRF}
For all adversaries $\adv$, we define the asp-name advantage as\[\mathsf{Adv}(\adv;Real_PRF,Ideal_PRF):=\abs{\begin{array}{l}\phantom{-}\prob{1 = \adv\rightarrow Real_PRF}\\-\prob{1 = \adv\rightarrow Ideal_PRF}\end{array}},
                      \]where Real\_PRF and Ideal\_PRF are defined in Sec.~\ref{section:game:Real_PRF} and Sec.~\ref{section:game:Ideal_PRF}, respectively.\end{definition}
\begin{figure}
\hfill\begin{tikzpicture}
\node[anchor=south west,align=center,package,minimum height=3cm,fill=red!50] (node0) at (10.5,0.5) {\M{Prf}};\node[anchor=south west,align=center,package,minimum height=1cm,fill=white] (node1) at (7,2.5) {\M{Prot}};\node[anchor=south west,align=center,package,minimum height=2cm,fill=white] (node2) at (3.5,1.5) {\M{KX}};\draw[-latex,rounded corners]
    (9,3) -- node[onarrow] {\O{Eval}} (10.5,3);
\draw[-latex,rounded corners]
    (5.5,2) -- node[onarrow] {\O{Hon}\\\O{Eval}} (10.5,2);
\draw[-latex,rounded corners]
    (5.5,3) -- node[onarrow] {\O{Run1}\\\O{Run2}\\\O{Run3}\\\O{Run4}\\\O{Run5}} (7,3);
\draw[-latex,rounded corners] (2,1) -- node[onarrow] {\O{NewKey}} (10.5,1);
\draw[-latex,rounded corners] (2,2) -- node[onarrow] {\O{NewSession}\\\O{Send1}\\\O{Send2}\\\O{Send3}\\\O{Send4}\\\O{Send5}\\\O{Reveal}\\\O{Test}} (3.5,2);
\end{tikzpicture}
\hfill\begin{tikzpicture}
\node[anchor=south west,align=center,package,minimum height=3cm,fill=red!50] (node0) at (10.5,0.5) {\M{Prf}};\node[anchor=south west,align=center,package,minimum height=1cm,fill=white] (node1) at (7,2.5) {\M{Prot}};\node[anchor=south west,align=center,package,minimum height=2cm,fill=white] (node2) at (3.5,1.5) {\M{KX}};\draw[-latex,rounded corners]
    (9,3) -- node[onarrow] {\O{Eval}} (10.5,3);
\draw[-latex,rounded corners]
    (5.5,2) -- node[onarrow] {\O{Hon}\\\O{Eval}} (10.5,2);
\draw[-latex,rounded corners]
    (5.5,3) -- node[onarrow] {\O{Run1}\\\O{Run2}\\\O{Run3}\\\O{Run4}\\\O{Run5}} (7,3);
\draw[-latex,rounded corners] (2,1) -- node[onarrow] {\O{NewKey}} (10.5,1);
\draw[-latex,rounded corners] (2,2) -- node[onarrow] {\O{NewSession}\\\O{Send1}\\\O{Send2}\\\O{Send3}\\\O{Send4}\\\O{Send5}\\\O{Reveal}\\\O{Test}} (3.5,2);
\end{tikzpicture}
\hfill\caption{Reduction: Hybrid2 $\approx$ Hybrid3 assuming prf. The sub-graphs corresponding to Real\_PRF and Ideal\_PRF, respectively, are highlighted in red. The remaining graph constitutes the reduction.}\label{figure:reduction:prf:Hybrid2:Hybrid3}
\end{figure}
\section{Gamehops}
\subsection{Equivalence between Hybrid0 and Hybrid1}
\subsection{Equivalence between Hybrid1 and Hybrid2}
\subsection{Reduction to prf}
\subsubsection{Game Hybrid2 with Assumption Game Real\_PRF highlighted in red}
\begin{center}
\begin{tikzpicture}
\node[anchor=south west,align=center,package,minimum height=3cm,fill=red!50] (node0) at (10.5,0.5) {\M{Prf}};\node[anchor=south west,align=center,package,minimum height=1cm,fill=white] (node1) at (7,2.5) {\M{Prot}};\node[anchor=south west,align=center,package,minimum height=2cm,fill=white] (node2) at (3.5,1.5) {\M{KX}};\draw[-latex,rounded corners]
    (9,3) -- node[onarrow] {\O{Eval}} (10.5,3);
\draw[-latex,rounded corners]
    (5.5,2) -- node[onarrow] {\O{Hon}\\\O{Eval}} (10.5,2);
\draw[-latex,rounded corners]
    (5.5,3) -- node[onarrow] {\O{Run1}\\\O{Run2}\\\O{Run3}\\\O{Run4}\\\O{Run5}} (7,3);
\draw[-latex,rounded corners] (2,1) -- node[onarrow] {\O{NewKey}} (10.5,1);
\draw[-latex,rounded corners] (2,2) -- node[onarrow] {\O{NewSession}\\\O{Send1}\\\O{Send2}\\\O{Send3}\\\O{Send4}\\\O{Send5}\\\O{Reveal}\\\O{Test}} (3.5,2);
\end{tikzpicture}
\end{center}
\subsubsection{Game Hybrid3 with Assumption Game Ideal\_PRF highlighted  in red}
\begin{center}
\begin{tikzpicture}
\node[anchor=south west,align=center,package,minimum height=3cm,fill=red!50] (node0) at (10.5,0.5) {\M{Prf}};\node[anchor=south west,align=center,package,minimum height=1cm,fill=white] (node1) at (7,2.5) {\M{Prot}};\node[anchor=south west,align=center,package,minimum height=2cm,fill=white] (node2) at (3.5,1.5) {\M{KX}};\draw[-latex,rounded corners]
    (9,3) -- node[onarrow] {\O{Eval}} (10.5,3);
\draw[-latex,rounded corners]
    (5.5,2) -- node[onarrow] {\O{Hon}\\\O{Eval}} (10.5,2);
\draw[-latex,rounded corners]
    (5.5,3) -- node[onarrow] {\O{Run1}\\\O{Run2}\\\O{Run3}\\\O{Run4}\\\O{Run5}} (7,3);
\draw[-latex,rounded corners] (2,1) -- node[onarrow] {\O{NewKey}} (10.5,1);
\draw[-latex,rounded corners] (2,2) -- node[onarrow] {\O{NewSession}\\\O{Send1}\\\O{Send2}\\\O{Send3}\\\O{Send4}\\\O{Send5}\\\O{Reveal}\\\O{Test}} (3.5,2);
\end{tikzpicture}
\end{center}
\subsection{Equivalence between Real\_Hybrid3 and Ideal\_Hybrid3}
\end{document}
