text:
%%
%% This is file `xkvex2.tex',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% xkeyval.dtx  (with options: `xkvex2')
%%
%% ---------------------------------------
%% Copyright (C) 2004-2014 Hendri Adriaens
%% ---------------------------------------
%%
%% This work may be distributed and/or modified under the
%% conditions of the LaTeX Project Public License, either version 1.3
%% of this license or (at your option) any later version.
%% The latest version of this license is in
%%   http://www.latex-project.org/lppl.txt
%% and version 1.3 or later is part of all distributions of LaTeX
%% version 2003/12/01 or later.
%%
%% This work has the LPPL maintenance status "maintained".
%%
%% This Current Maintainer of this work is Hendri Adriaens.
%%
%% This work consists of the file xkeyval.dtx and derived files
%% keyval.tex, xkvtxhdr.tex, xkeyval.sty, xkeyval.tex, xkvview.sty,
%% xkvltxp.sty, xkvutils.tex, pst-xkey.tex, pst-xkey.sty, xkveca.cls,
%% xkvecb.cls, xkvesa.sty, xkvesb.sty, xkvesc.sty, xkvex1.tex,
%% xkvex2.tex, xkvex3.tex and xkvex4.tex.
%%
%% The following files constitute the xkeyval bundle and must be
%% distributed as a whole: readme, xkeyval.pdf, keyval.tex,
%% pst-xkey.sty, pst-xkey.tex, xkeyval.sty, xkeyval.tex, xkvview.sty,
%% xkvltxp.sty, xkvtxhdr.tex, xkvutils.tex, pst-xkey.dtx and xkeyval.dtx.
%%
\documentclass{article}
\usepackage{xkeyval}
\usepackage{xcolor,calc}

%% Example of setting keyval options using xkeyval
\usepackage{hyperref}
\usepackage{helvet}
\setkeys{Hyp,Hel}{colorlinks,urlcolor=green,scaled=.85}

\title{\textsf{xkeyval} package\\\normalsize\emph{Example 2}}
\author{Hendri Adriaens}
\setlength{\parindent}{0cm}

\makeatletter

\begin{document}
\maketitle

This example demonstrates the use of the new macros for setting
keys of the \textsf{xkeyval} package. Below each piece of verbatim
code, you can find its output.

\section{Simple operations}

Define keys.
\begin{verbatim}
\define@key{fami}{keyi}{key 1: #1\space}
\define@key{famii}{keyii}{key 2: #1\space}
\define@key{famiii}{keyiii}[test 2]{key 3: #1\space}
\define@key{famiv}{keyi}{key 4: #1\space}
\end{verbatim}
\define@key{fami}{keyi}{key 1: #1\space}
\define@key{famii}{keyii}{key 2: #1\space}
\define@key{famiii}{keyiii}[test 2]{key 3: #1\space}
\define@key{famiv}{keyi}{key 4: #1\space}

Set keys from multiple families.
\begin{verbatim}
\setkeys{fami,famii,famiii}{keyi=test 1,keyiii}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\setkeys{fami,famii,famiii}{keyi=test 1,keyiii}
\end{itemize}

Multiplely defined keys will be taken from the first family on the
list that defines the key. When \verb|+| is used, all families
defining the key will set it.
\begin{verbatim}
\setkeys{fami,famiv}{keyi=test 3}
\setkeys{famiv,fami}{keyi=test 4}
\setkeys+{fami,famiv}{keyi=test 5}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\setkeys{fami,famiv}{keyi=test 3}\par
\setkeys{famiv,fami}{keyi=test 4}\par
\setkeys+{fami,famiv}{keyi=test 5}
\end{itemize}

Starred form sets keys that it can find in the families specified.
Keys that cannot be located will be put onto a list for later use
by \verb+\setrmkeys+.
\begin{verbatim}
\setkeys*{famiv}{keyi=test 9,keyii=\url{http://www.test10.com},
  keyiii=this key has been set on page \thepage}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\setkeys*{famiv}{keyi=test 9,keyii=\url{http://www.test10.com},
  keyiii=this key has been set on page \thepage}
\end{itemize}

Try to set the remaining keys from the previous step. The starred
version defines a new list in case there are still keys that
cannot be located in the given families. The command below does
not do anything since the \verb+keyi+ key has already been taken
from family \verb+famiv+ above.
\begin{verbatim}
\setrmkeys*{fami}
\end{verbatim}
\setrmkeys*{fami}\par

The normal version will complain (as \verb+\setkeys+) when it
cannot locate a key which was previously submitted to
\verb+\setkeys+ and hasn't been set yet by previous commands.
\textsf{xkeyval} commands can also be used to set \textsf{keyval}
options as is done to the color of the url created with the
\textsf{hyperref} package and the scaling of the font used for
`\textsf{xkeyval}' with the \textsf{helvet} package. (See the
preamble of the example for the code).
\begin{verbatim}
\setrmkeys{famii,famiii}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\setrmkeys{famii,famiii}
\end{itemize}

Set keys, excluding some keys.
\begin{verbatim}
\setkeys{fami,famii,famiii}[keyi,keyiii]{keyi=test 6,keyii=test 7,keyiii=test 8}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\setkeys{fami,famii,famiii}[keyi,keyiii]{keyi=test 6,keyii=test 7,keyiii=test 8}
\end{itemize}

Test whether a key is defined in a family from the list.
\begin{verbatim}
\key@ifundefined{fami,famii}{keyiii}
{keyiii is not defined in family `fami' or `famii'}
{keyiii is defined in family `fami' or `famii'}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\key@ifundefined{fami,famii}{keyiii}
{keyiii is not defined in family `fami' or `famii'}
{keyiii is defined in family `fami' or `famii'}
\end{itemize}

Define some keys and macros.
\begin{verbatim}
\define@cmdkey[my]{fama}[my@]{keya}[none]{}
\define@choicekey[my]{fama}{keyb}{a,b,c}[b]{correct input: #1}
\define@boolkey[my]{famb}{keyc}[true]{}
\def\testa{\setkeys[my]{fama}}
\def\testb{\setkeys[my]{famb}}
\def\testset{\setkeys[my]{fama,famb}}
\end{verbatim}
\define@cmdkey[my]{fama}[my@]{keya}[none]{}
\define@choicekey[my]{fama}{keyb}{a,b,c}[b]{correct input: #1}
\define@boolkey[my]{famb}{keyc}[true]{}
\def\testa{\setkeys[my]{fama}}
\def\testb{\setkeys[my]{famb}}
\def\testset{\setkeys[my]{fama,famb}}
Now \verb+\testa+ can only set \verb+keya+, \verb+\testb+ can only
set \verb+keyb+ and \verb+\testset+ can set both.
\begin{verbatim}
\testa{keya}
  \my@keya\
\testa{keyb}
\testb{keyc}
  \ifmy@famb@keyc true \else false \fi
\testset{keya=test 11,keyb=c,keyc=false}
  \my@keya\space
  \ifmy@famb@keyc true \else false \fi
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\testa{keya}
  \my@keya\
\testa{keyb}
\testb{keyc}
  \ifmy@famb@keyc true \else false \fi
\testset{keya=test 11,keyb=c,keyc=false}
  \my@keya\space
  \ifmy@famb@keyc true \else false \fi
\end{itemize}

\section{Pointers and values}

First we (re)define some keys.
\begin{verbatim}
\define@key{fam}{keyi}{key 1: #1 }
\define@key{fam}{keyii}{key 2: #1 }
\define@key{fam}{keyiii}[test 2]{key 3: #1 }
\end{verbatim}
\define@key{fam}{keyi}{key 1: #1 }
\define@key{fam}{keyii}{key 2: #1 }
\define@key{fam}{keyiii}[test 2]{key 3: #1 }

Pointers can be used to copy the value of other keys in the same
family. This can be done in two ways. The first example shows `on
the spot' value saving.
\begin{verbatim}
\setkeys{fam}{\savevalue{keyi}=test 12,\savevalue{keyii}=\usevalue{keyi}}
\setkeys{fam}{keyiii=\usevalue{keyii}}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\setkeys{fam}{\savevalue{keyi}=test 12,\savevalue{keyii}=\usevalue{keyi}}
\setkeys{fam}{keyiii=\usevalue{keyii}}
\end{itemize}

However, you can also predefine the keys to be saved for the entire
document with a single command. Note that we force keys to be saved
globally. This is necessary here since the commands in the source of
this document appear in an environment.
\begin{verbatim}
\savekeys{fam}{\global{keyi},\global{keyii}}
\setkeys{fam}{keyi=test 13,keyii=\usevalue{keyi}}
\setkeys{fam}{keyiii=\usevalue{keyii}}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\savekeys{fam}{\global{keyi},\global{keyii}}
\setkeys{fam}{keyi=test 13,keyii=\usevalue{keyi}}
\setkeys{fam}{keyiii=\usevalue{keyii}}
\end{itemize}

Pointers can be used in default values as well. Remember that the
previous example used \verb+\savekeys+ for \verb+keyi+ and \verb+keyii+.
\begin{verbatim}
\define@key{fam}{keyi}{keyi: #1 }
\define@key{fam}{keyii}[\usevalue{keyi}]{keyii: #1 }
\define@key{fam}{keyiii}[\usevalue{keyii}]{keyiii: #1 }
\setkeys{fam}{keyi=test 14}
\setkeys{fam}{keyii}
\setkeys{fam}{keyiii}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\define@key{fam}{keyi}{keyi: #1 }
\define@key{fam}{keyii}[\usevalue{keyi}]{keyii: #1 }
\define@key{fam}{keyiii}[\usevalue{keyii}]{keyiii: #1 }
\setkeys{fam}{keyi=test 14}
\setkeys{fam}{keyii}
\setkeys{fam}{keyiii}
\end{itemize}

\section{Presetting keys}

Simple example of the preset system.
\begin{verbatim}
\define@key{fam}{keyi}{keyi: #1 }
\define@key{fam}{keyii}{keyii: #1 }
\presetkeys{fam}{keyi=blue}{keyii=\usevalue{keyi}}
\setkeys{fam}{}\par
\setkeys{fam}{keyi=red}\par
\setkeys{fam}{keyii=red}
\presetkeys{fam}{keyi=red}{}
\setkeys{fam}{keyii=\usevalue{keyi}}
\end{verbatim}
\begin{itemize}
\item[$\Rightarrow$]
\define@key{fam}{keyi}{keyi: #1 }
\define@key{fam}{keyii}{keyii: #1 }
\presetkeys{fam}{keyi=blue}{keyii=\usevalue{keyi}}
\setkeys{fam}{}\par
\setkeys{fam}{keyi=red}\par
\setkeys{fam}{keyii=red}
\presetkeys{fam}{keyi=red}{}\par
\setkeys{fam}{keyii=\usevalue{keyi}}
\end{itemize}

\section{Application of pointers, values and presets}

\setkeys{Hyp}{urlcolor=black}
More complicated example of the preset
system and pointer system. See for more information about this
example the
\textsf{xkeyval} article on\par
\url{http://www.tug.org/TUGboat/tb25-2/tb81adriaens.pdf}.
\begin{verbatim}
\newdimen\shadowsize
\define@boolkey{Fbox}{frame}[true]{}
\define@boolkey{Fbox}{shadow}[true]{}
\define@key{Fbox}{framecolor}{\def\Fboxframecolor{#1}}
\define@key{Fbox}{shadowcolor}{\def\Fboxshadowcolor{#1}}
\define@key{Fbox}{framesize}{\setlength\fboxrule{#1}}
\define@key{Fbox}{shadowsize}{\setlength\shadowsize{#1}}
\presetkeys{Fbox}{frame,framecolor=red,framesize=0.5pt}%
 {shadow=\usevalue{frame},shadowcolor=\usevalue{framecolor}!40,%
  shadowsize=\usevalue{framesize}*4}
\savekeys{Fbox}{frame,framecolor,framesize}
\newcommand*\Fbox[2][]{%
 \setkeys{Fbox}{#1}%
 {\ifKV@Fbox@frame\else\fboxrule0pt\fi
  \ifKV@Fbox@shadow\else\shadowsize0pt\fi
  \sbox0{\fcolorbox{\Fboxframecolor}{white}{#2}}%
  \hskip\shadowsize
  \color{\Fboxshadowcolor}%
  \rule[-\dp0]{\wd0}{\ht0+\dp0}%
  \llap{\raisebox{\shadowsize}%
   {\box0\hskip\shadowsize}}}%
}
\Fbox{demo1}
\Fbox[framecolor=blue]{demo2}
\Fbox[shadow=false]{demo3}
\Fbox[framesize=1pt]{demo4}
\Fbox[frame=false,shadow]{demo5}
\end{verbatim}
\newdimen\shadowsize
\define@boolkey{Fbox}{frame}[true]{}
\define@boolkey{Fbox}{shadow}[true]{}
\define@key{Fbox}{framecolor}%
 {\def\Fboxframecolor{#1}}
\define@key{Fbox}{shadowcolor}%
 {\def\Fboxshadowcolor{#1}}
\define@key{Fbox}{framesize}%
 {\setlength\fboxrule{#1}}
\define@key{Fbox}{shadowsize}%
 {\setlength\shadowsize{#1}}
\presetkeys{Fbox}%
 {frame,framecolor=red,framesize=0.5pt}%
 {shadow=\usevalue{frame},
  shadowcolor=\usevalue{framecolor}!40,
  shadowsize=\usevalue{framesize}*4}
\savekeys{Fbox}{frame,framecolor,framesize}
\newcommand*\Fbox[2][]{%
 \setkeys{Fbox}{#1}%
 {\ifKV@Fbox@frame\else\fboxrule0pt\fi
  \ifKV@Fbox@shadow\else\shadowsize0pt\fi
  \sbox0{\fcolorbox{\Fboxframecolor}{white}{#2}}%
  \hskip\shadowsize
  \color{\Fboxshadowcolor}%
  \rule[-\dp0]{\wd0}{\ht0+\dp0}%
  \llap{\raisebox{\shadowsize}%
   {\box0\hskip\shadowsize}}}%
}
\Fbox{demo1}
\Fbox[framecolor=blue]{demo2}
\Fbox[shadow=false]{demo3}
\Fbox[framesize=1pt]{demo4}
\Fbox[frame=false,shadow]{demo5}

\end{document}
\endinput
%%
%% End of file `xkvex2.tex'.

max_stars_repo_licenses: MIT Unlicense

max_issues_repo_licenses: MIT Unlicense

max_forks_repo_licenses: MIT Unlicense


text:
% !TEX root = main.tex
% !TEX spellcheck = en-US
\section{Introduction}
Zero-knowledge proof systems that allow a prover to convince a verifier of a statement without revealing anything beyond the truth of the statement have broad application in cryptography and theory of computation~\cite{FOCS:GolMicWig86,STOC:Fortnow87,C:BGGHKMR88}.
When restricted to computationally sound proofs, called \emph{argument systems}, proof length can be shorter than the length of the witness~\cite{brassard1988minimum}.
Zero-knowledge Succinct Non-interactive ARguments of Knowledge (zkSNARKs) are zero-knowledge argument systems that additionally have a succinctness property -- small proof sizes and fast verification.
Since their introduction in~\cite{FOCS:Micali94}, zk-SNARKs have been a powerful and versatile design tool for secure cryptographic protocols. They became particularly relevant for blockchain applications that demand short proofs and fast verification, such as privacy-preserving cryptocurrencies~\cite{SP:BCGGMT14} in Zcash and scalable and private smart contracts in Ethereum\footnote{\url{https://z.cash/} and \url{https://ethereum.org} respectively}.

%The work of~\cite{EC:GGPR13} proposed a preprocessing zk-SNARK for general NP statements phrased in the language of Quadratic Span Programs (QSP) and Quadratic Arithmetic Programs (QAP) for Boolean and arithmetic circuits respectively. This built on previous works of~\cite{IKO07,AC:Groth10a,TCC:Lipmaa12} and led to several works~\cite{TCC:BCIOP13,SP:PHGR13,C:BCGTV13,AC:Lipmaa13,USENIX:BCTV14,EC:Groth16} with very short proof sizes and fast verification.

While research on zkSNARKs has seen rapid progress~\cite{EC:GGPR13,AC:Groth10a,TCC:Lipmaa12,TCC:BCIOP13,SP:PHGR13,C:BCGTV13,AC:Lipmaa13,USENIX:BCTV14,EC:Groth16} with many works proposing significant improvements in efficiency of different parameters like proof size, verifier efficiency, and complexity of the public setup, less attention has been paid to non-malleable zkSNARKs and succinct signatures of knowledge, (SoK) also known as SNARKY signatures~\cite{C:GroMal17,EPRINT:BKSV20}. A signature of knowledge~\cite{C:CamSta97,C:ChaLys06} uses an instance of an NP-language as the public verification key. Instead of signing using a secret key, which typically would be related to the public key via a discrete logarithm or some other hard relation~\cite{AC:DHLW10}, SoK signing requires knowledge of the NP-witness. Chase and Lysyanskaya~\cite{C:ChaLys06} require signatures of knowledge to be simulatable to assure protection against signing key/witness extraction. Given a trapdoor associated with the public setup, signatures can be simulated without the witness. Furthermore, to model strong existential unforgeability of signatures, even when given an oracle for obtaining signatures on different instances, an attacker must not be able to produce new signatures. Chase and Lysyanskaya model this via the notion of simulation-extractability which guarantees extraction of the witness even in the presence of simulated signatures.
Moreover,  Groth and Maller \cite{C:GroMal17} showed how to construct
SoK from zkSNARK schemes that have simulation-extractability.
Therefore, our focus can be moved from SoK to the main building block,  zkSNARK schemes,  for which we have many new efficient constructions in the recent literature.

\paragraph{Relevance of simulation extractability.}

Most zkSNARKs are shown to only satisfy a standard knowledge soundness property. Intuitively, this guarantees that
a prover that creates a valid proof knew a valid witness. However, deployments of zkSNARKs in real-world applications unless they are carefully designed to have application specific malleability protection, e.g.~\cite{SP:BCGGMT14}, require a stronger property -- \textit{simulation-extractability} (SE) that as discussed above corresponds more closely to existential unforgeability of signatures.
In practice, an adversary against the zkSNARK has access to proofs provided by other parties using the same
zkSNARK.  The definition of knowledge soundness ignores the ability of an adversary to see other valid proofs that may occur in real-world applications.  For instance, in applications of
zkSNARKs in privacy-preserving blockchains, proofs are posted on the chain for all
blockchain-participants to see.
%Therefore, it is necessary for a zero-knowledge proof system to be \emph{non-malleable}, that is, resilient against adversaries that additionally get to see proofs generated by different parties before trying to forge.
%Therefore, it is necessary for a zero-knowledge proof system to be \emph{simulation-extractable}, that is, resilient against adversaries that additionally get to see proofs generated by different parties before trying to forge.
%This captures the more general scenario where an adversary against the zkSNARK has access to proofs provided by other parties as it is in applications of zkSNARKs in privacy-preserving blockchains, where proofs are posted on the chain for all
%participants in the network to verify.

\paragraph{Fiat-Shamir based zkSNARKs.}
Most modern zkSNARK constructions follow a modular blueprint that involves the design of an information theoretic interactive protocol, e.g. an Interactive Oracle Proof (IOP), that is then compiled via cryptographic tools to obtain an interactive argument system.  This is then turned into a zkSNARK using the hash-based Fiat-Shamir transform. By additionally hashing the message, the Fiat-Shamir transform is also a popular technique for constructing signatures. While well understood for 3-round sigma protocols and justifiable in the random oracle
model (ROM)~\cite{CCS:BelRog93}, is only a heuristic that should be used with
care since there are counterexamples that it is
unsound~\cite{FOCS:GolKal03}.

%The Fiat--Shamir (FS) transform takes a public-coin interactive protocol and makes it interactive by hashing the current protocol transcript to compute the verifier's public coins.
%
%The FS transform is a popular design tool for constructing
%zkSNARKs. In the updatable universal SRS setting, works like \sonic{}~\cite{CCS:MBKM19}
%\plonk{}~\cite{EPRINT:GabWilCio19}, and \marlin~\cite{EC:CHMMVW20} are designed
%and proven secure as multi-round interactive protocols. Security is then only
%\emph{conjectured} for their non-interactive variants by employing the FS
%transform.

In particular, several schemes such as
$\sonic$~in \cite{CCS:MBKM19}, $\plonk$~\cite{EPRINT:GabWilCio19}, $\textsf{Marlin}$~\cite{EC:CHMMVW20}
follow this approach where the information theoretic object is a multi-round algebraic variant of IOP, and the cryptographic primitive in the compiler is a polynomial commitment scheme (PC) that requires a trusted setup. To date, this blueprint lacks an analysis in the ROM in terms of simulation extractability.

\paragraph{Updatable setup zkSNARKs}
One of the downsides of efficient zkSNARKs like~\cite{AC:Groth10a,TCC:Lipmaa12,EC:GGPR13,SP:PHGR13,AC:Lipmaa13,AC:DFGK14,EC:Groth16} is that they rely on a \textit{trusted setup}, where there is a structured reference string (SRS) that is assumed to be generated by a trusted party. In practice, however, this assumption is not well founded; if the party that generates the SRS is not honest, then they can produce proofs of false statement. That is, if the trusted setup assumption does not hold, knowledge soundness breaks down.
Groth et al~\cite{C:GKMMM18} propose a setting to tackle this challenge which allows parties -- provers and verifiers -- to \emph{update} the SRS, that is, take a current SRS and contribute to it randomness in a verifiable way to obtain a new SRS. The guarantee in this \textit{updatable setting} is that knowledge soundness holds as long as one of the parties who updates the SRS is honest. The SRS is also \emph{universal}, in that it does not depend on the relation to be proved but only on an upper bound in the size of the statements.
Although inefficient, as the SRS length is quadratic in the size of the statement,~\cite{C:GKMMM18} set a new
paradigm of universal updatable setting for designing zkSNARKs.

The first universal zkSNARK with updatable and linear size SRS was
$\sonic$ proposed by Maller et al.~in \cite{CCS:MBKM19}. Subsequently, Gabizon et
al.~designed $\plonk$~\cite{EPRINT:GabWilCio19} which currently is the
most efficient updatable universal zkSNARK. Independently, Chiesa et
al.~\cite{EC:CHMMVW20} proposed $\textsf{Marlin}$ with comparable efficiency to
$\plonk$.

\paragraph{The challenge of SE in the updatable setting.}

The notion of simulation-extractability for zkSNARKs which is well motivated in practice has not been studied in this updatable setting.

Consider the following scenario: We assume a rushing adversary that starts off with a sequence of malicious updates by colluding parties resulting in a subverted reference string $\srs$. By combining their trapdoor contributions and employing the simulation algorithm, these parties can easily compute a proof $(\srs,x,\pi)$ for a statement $x$ without knowing a witness. Now, assume that at a later stage a party produces a proof $(\srs',x,\pi')$ for the same statement with respect to an updated $\srs'$ that has an honest update contribution. We would like the guarantee that this party must known a witness corresponding to $x$. The ability to ``move" the proof $\pi$ from the old SRS to a proof $\pi'$ for the new SRS without knowing a witness would clearly violates security. A natural idea is to require that honestly \emph{updated} reference strings are indistinguishable from honestly \emph{generated} reference strings. However, this is not sufficient as the rushing adversary can also rush toward the end of the SRS generation ceremony to perform the last update.
%That is, an adversary who does not knows the trapdoor for the update from $\srs$ to $\srs'$ should not be able to break SE. % as long as there was at least one honest update to $\srs$.\markulf{30/09/2021}{We currently don't achieve this strong USE notion.}

A definition of SE in the updatable setting should take these additional powers of the adversary, which are not captured by existing definitions of SE, into consideration.
While generic lifting techniques/compilers~\cite{EPRINT:KZMQCP15,CCS:AbdRamSla20} can be applied to updatable SRS SNARKs to obtain SE, not only do they inevitably incur overheads and lead to efficiency loss, we contend that the standard definition of SE does not suffice in the updatable setting.

We investigate the non-malleability properties of a class of zkSNARK protocols obtained by FS-compiling multi-round protocols in the updatable SRS setting and give a modular approach to analyse the simulation-extractability of zkSNARKs.
\subsection{Our Contributions}
\begin{itemize}
\item
\emph{Updatable simulation extractability (USE)}.
We propose a definition of simulation extractability in the updatable SRS setting called USE, that captures the additional power the adversary gets by being able to update the SRS.% and seeing proofs with respect to different SRSs.\michals{28.09}{Now the adversary sees additional proofs wrt to the final SRS.}

  \item \emph{General theorem for USE of FS-compiled interactive protocols.} We
        then show that a class of interactive proofs of knowledge that when
        the Fiat--Shamir transform is applied to them are \changedm{trapdoor-less simulatable}, have a
        unique response property in the updatable setting, and satisfy a
        property we define called forking special soundness \emph{are USE
        out-of-the box} in the random oracle model. Informally, our notion of forking
        special soundness is a variant of special soundness where the
        transcripts provided to the extractor are obtained through interaction
        with an honest verifier, and the extraction guarantee is computational
        instead of unconditional. Our extractor only needs oracle access to the
        adversary, it does not depend on the adversary’s code, nor does it rely on
        knowledge assumptions.

\item
\emph{USE for concrete zkSNARKs.}
We then prove that the most efficient updatable SRS SNARKS -- Plonk/Sonic/Marlin -- satisfy the notions necessary to invoke our general theorem. We thus show that these zkSNARKs are updatable simulation extractable.
Only in this step we rely on the algebraic group model (AGM).

\item
  \emph{SNARKY signatures in the updatable setting.} Our results validate the folklore that the Fiat--Shamir transform is a natural means for constructing signatures of knowledge. This gives rise to the first SoK in the updatable setting and confirms that a much larger class of zkSNARKs, beside \cite{C:GroMal17}, can be lifted to SoK.

%\item
%We make several technical contributions along the way. Our generalized forking lemma is of independent interest.
\end{itemize}

\subsection{Technical Overview}
%unique response, forking special soundness. general theorem without additional assumptions. to apply the theorem to concrete schemes like plonk, we show it satisfies unique response, forking soundness, in AGM.

From a high level, the proof of our general theorem for updatable simulation
extractability is along the lines of the simulation extractability proof for
FS-compiled sigma protocol from~\cite{INDOCRYPT:FKMV12}. However, our theorem
introduces new notions that are more general to allow us to consider proof
systems that are richer than sigma protocols and support an updatable setup. We
discuss some of the technical challenges below.

\plonk{}, \sonic{}, and \marlin{} were originally presented as interactive
proofs of knowledge that are made non-interactive by the Fiat--Shamir transform.
In the following, we denote the underlying interactive protocols by $\plonkprot$
(for $\plonk$), $\sonicprot$ (for $\sonic$), and $\marlinprot$ (for \marlin) and
the resulting non-interactive proof systems by $\plonkprotfs$, $\sonicprotfs$,
$\marlinprotfs$ respectively.

\oursubsub{Forking special soundness in the updatable setting.}
Following~\cite{INDOCRYPT:FKMV12}, one would have to show that for the protocols
we consider, a witness can be extracted from sufficiently many valid transcripts
with a common prefix. The standard definition of special soundness for sigma
protocols requires extraction of a witness from any two transcripts with the
same first message. However, most zkSNARK protocols do not satisfy this notion.
We put forth a notion analogous to special soundness, that is more general and
applicable to a wider class of protocols. Namely, protocols can have more than three
rounds and can rely on an updatable SRS. $\plonkprot$, $\sonicprot$, and
$\marlinprot$ have more than 3 rounds and the number of transcripts required for extraction is more
than two. Concretely, $(3 \noofc + 1)$ -- where $\noofc$ is the number of
constraints in the proven circuit -- for Plonk, $(\multconstr + \linconstr + 1)$
-- where $\multconstr$ and $\linconstr$ are the numbers of multiplicative and
linear constraints -- for Sonic, and $(\multconstr + 3)$ -- where $\multconstr$
is the number of multiplicative constraints -- for Marlin. Hence, we do not have
a pair of transcripts, but a \emph{tree of transcripts}.

In protocols that rely on SRS that come with a trapdoor, an adversary in
possession of the trapdoor can produce multiple valid proof transcripts without
knowing the witness and potentially for false statements. This is true even in
the updatable setting, where there exists a trapdoor for any updated SRS. Recall
that the standard special soundness definition requires witness extraction from
\emph{any} tree of acceptable transcripts that share a common root. This means
that there are no such trees for false statements. We define a different,
forking lemma-related, version of soundness that we call forking special soundness.
Forking special soundness guarantees that it is possible to extract a witness from all
(but negligibly many) trees of accepting transcripts produced by probabilistic
polynomial time (PPT) adversaries, given that the trees are generated as
interactions between a (possibly malicious) prover and an honest verifier. That
is, if extraction from such a tree fails, then we break an underlying
computational assumption. Moreover, this should hold even against adversaries
that contribute in the SRS generation.

\oursubsub{Unique response property in the updatable setting.}  Another property required to
show USE is the unique response property~\cite{C:Fischlin05} which says that for $3$-messages
sigma protocols, all but the first message sent by the prover are deterministic (intuitively,
the prover can only employ fresh randomness in the first message of the protocol). We cannot
use this definition as is since the protocols we consider have other rounds with randomized prover
messages. In Plonk, both the first and the second prover's messages are
randomized. Although Sonic prover is deterministic after it picks its first message, the
protocol has more than $3$ rounds. The same holds for Marlin. We propose a generalisation of
the definition which states that a protocol is $\ur{i}$ if the prover is deterministic starting
from its $(i + 1)$-th message. For our proof it is sufficient that this property is met by
Plonk for $i = 2$. Since Sonic and Marlin provers are deterministic from the second message on,
they are $\ur{1}$.

\oursubsub{Trapdoor-less simulatable protocols.}  In order to invoke our main theorem on
(Fiat--Shamir transformed) Plonk, Sonic and Marlin to conclude USE, we also need to show
that simulators in these protocols produces proofs without relying on the knowledge of
trapdoor. More precisely for our reduction, we need simulators that rely only on reordering the
messages and picking suitable verifier challenges, without knowing the SRS trapdoor.  That is,
any PPT party should be able to produce a simulated proof on its own in a trapdoor-less
way. Note that this property does not necessary break soundness of the protocol as the
simulator is required only to produce a transcript and is not involved in a real conversation
with a real verifier. We show simulators for $\plonkprotfs$, $\sonicprotfs$, and
$\marlinprotfs$ that rely only on the programmability of the RO, where programmability is only
needed from some round $i$ onwards. This property can be understood as a generalization of honest-verifier zero-knowledge for Fiat--Shamir transformed prove systems with an SRS.

\oursubsub{Generalising the general forking lemma.}  Consider an interactive $3$-message
special-sound protocol $\ps$ and its non-interactive version $\ps_\fs$ obtained by the
Fiat--Shamir transform. The general forking lemma provides an instrumental lower bound for the
probability of extracting a witness from an adversary who provides two proofs for the same
statement that share the first message. Since $\plonkprot$, $\sonicprot$, and $\marlinprot$ have more than $3$
messages and are not special-sound, the forking lemma of Bellare and Neven~\cite{CCS:BelNev06},
cannot be used directly. We propose a generalization that covers multi-message protocols where
witness extraction requires more than two transcripts.  Unfortunately, we also observe
that the security gap grows with the number of transcripts and the probability that the
extractor succeeds diminishes; the security loss, albeit big, is polynomial.

Most modern zkSNARKs~\cite{SP:BBBPWM18,CCS:MBKM19} heavily
rely on the Fiat--Shamir transform and thus potentially the forking lemma.
%First, an interactive
%protocol is proposed and its security and forking special soundness analysed.\markulf{30.09}{Unclear here whether forking special soundness is for the interactive of the non-interactive protocol.} Second,
%one uses an argument that the Fiat--Shamir transform can be used to get a
%protocol that is non-interactive and shares the same security properties.
We thus see our generalized forking lemma as contributing to a critical assessment of
this approach. The analysis of the interactive protocol is not enough and one
has to consider the security loss implied by the Fiat-Shamir transform for the target security notion.
%Thus one has to either rely on our generalisation of the forking
%lemma or disclose a transformation that does not suffer this loss.
We note that the security loss of our generalized forking lemma may also apply
when knowledge soundness is proven. This is, e.g., the case for the original
$\sonic$ paper, whose security proof relies on so-called witness-extended
emulation. The authors of $\plonk$ and recent work on
$\sonic$~\cite{cryptoeprint:2020:1351} work around this problem by proving
knowledge soundness directly in the AGM.

\subsection{Related Work}

\ourpar{Simulation extractability.}
There are many results on simulation extractability for
non-interactive zero-knowledge proofs (NIZKs). First, Groth \cite{AC:Groth07}
noticed that a (black-box) SE NIZK is
universally-composable (UC)~\cite{EPRINT:Canetti00}. Then Dodis et al.~\cite{AC:DHLW10} introduced a
notion of (black-box) \emph{true simulation extractability} and showed that no
NIZK can be UC-secure if it does not have this property.

In the context of zkSNARKs, the first
SE zkSNARK was proposed by Groth and Maller~\cite{C:GroMal17} and a SE
zkSNARK for QAP was designed by Lipmaa~\cite{EPRINT:Lipmaa19a}.
Kosba's et
al.~\cite{EPRINT:KZMQCP15} give a general transformation from a NIZK to a
black-box SE NIZK. Although their transformation works for zkSNARKs as well,
succinctness of the proof system is not preserved by the transformation.
Recently, Abdolmaleki et al.~\cite{CCS:AbdRamSla20} showed another transformation that
obtains non-black-box simulation extractability but also preserves
succinctness of the argument.
The zkSNARK of~\cite{EC:Groth16} has been shown to be SE by introducing minor modifications to the construction and making
stronger assumptions \cite{EPRINT:BowGab18,EPRINT:AtaBag19}. Recently,~\cite{EPRINT:BKSV20} showed that the
original Groth's proof system from~\cite{EC:Groth16} is weakly SE and
randomizable. None of these results are for zkSNARKs in the updatable SRS setting or for zkSNARKs obtained via the Fiat--Shamir transformation.

\ourpar{Forking lemma generalizations.}
There are several task specific variants, e.g.,~\cite{INDOCRYPT:HerSae03,CCS:BagCheJar08,AC:BelDaiLi19}, of the general forking lemma~\cite{JC:PoiSte00,CCS:BelNev06} for analyzing the forking behavior of random-oracle based executions.
In~\cite{EC:BCCGP16}, Bootle et al.~proposed a novel inner-product argument whose
security relies on, so-called, witness-extended emulation. To show that
property, the authors proposed a new version of the forking lemma that gives a
lower bound on the probability that a tree finding algorithm is able to produce a
tree of acceptable transcripts by rewinding a conversation between a
(potentially malicious) prover and verifier.

Although the result in that paper is dubbed a ``forking lemma'' it
differs from forking lemmas known from e.g.~\cite{JC:PoiSte00,CCS:BelNev06}.
First of all, the forking lemmas in these papers analyse the probability of building
a tree of acceptable transcripts for Fiat--Shamir based non-interactive proof
systems, while the protocol presented by Bootle et al.~is intended to work for
interactive proof systems.

Importantly, it is not obvious how the result of Bootle et al.~can be used to
show security of non-interactive protocols as it relies on interactive provers
whose proving strategies are more limited than proving strategies of
non-interactive provers. For example, if a challenge given by the verifier does not
suit an interactive prover, it can only try to finish a proof with that challenge or
abort. On the other hand, a non-interactive prover has far wider scope of
possible actions--when the protocol is non-interactive the prover may
adapt its strategy based on the random oracle outputs.
This is reminiscent of \emph{state restoration} security~\cite{TCC:BenChiSpo16,EPRINT:Holmgren19} which is also about the security loss incurred by the Fiat--Shamir transformation albeit when proving knowledge soundness from witness extended emulation.

Here, we directly capture the state restoration capability of the prover in the forking lemma instead of defining an interactive game where the prover can rewind the verifier to an earlier state as is done in~\cite{C:GhoTes21}.
The work of~\cite{C:GhoTes21} further shows that state restoration security gives tight security guarantees for the
non-interactive versions of Bulletproof~\cite{SP:BBBPWM18} and \sonic.
Our work differs from~\cite{C:GhoTes21} in the following ways. First, they
focus on showing security of concrete proof systems, while we show
a general theorem about the security of a wide class of protocols.
Second, they only consider knowledge soundness, while we focus on the stronger notion of simulation extractability. Third, the proof of~\cite{C:GhoTes21} is in the AGM which allows for online extraction, whereas we aim to reduce our reliance on the AGM. In particular, our extractor and main theorem do not rely on the AGM and we thus tackle technical challenges arising from extraction by rewinding.
However, arguably due to the design of Plonk, Sonic, and Marlin, we show that these concrete protocols satisfy the preconditions of our main theorem in the AGM.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

ext: tex

max_stars_repo_name: clearmatics/research-plonkext

max_issues_repo_name: clearmatics/research-plonkext

max_forks_repo_name: clearmatics/research-plonkext


text:
% !TEX TS-program = pdflatexmk

%\documentclass[runningheads, envcountsame, hidelinks, a4paper, draft, x11names]{llncs}
\documentclass[runningheads, envcountsame, hidelinks, a4paper, x11names]{article}
\usepackage{fullpage}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage[scaled=0.8]{helvet}    % Less huge \textsf{functionName}
\usepackage[misc,geometry]{ifsym} % for letter symbol
\usepackage{soul}           % \hl for highlighting text; \st for strike-through
\usepackage{graphicx}
\usepackage[dvipsnames]{xcolor}
\usepackage{tikz}
\usetikzlibrary{trees,snakes,arrows}
\usetikzlibrary{shapes,chains}
\usetikzlibrary{positioning}
\usepackage{hyperref}
\usepackage[nospace]{cite}

\input{macros}

\renewcommand{\baselinestretch}{1.1}

\begin{document}
\title{Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices}

\date{}

\author{Karl Norrman\\
    KTH Royal Institute of Technology, Stockholm, Sweden\\
    Ericsson Research, Security, Stockholm, Sweden,\\
    \emph{karl.norrman@ericsson.com}
\and
    Vaishnavi Sundararajan\\
    Ericsson Research, Int. Auton. Systems, Bangalore, India,\\
    \emph{vaishnavi.sundararajan@ericsson.com}
\and
    Alessandro Bruni\\
    IT University of Copenhagen, Copenhagen, Denmark,\\
    \emph{brun@itu.dk}
}

%
\maketitle
%

\begin{abstract}
%\hl{250 words}
The IETF is standardizing an authenticated key establishment (AKE) protocol
named \mEdhoc{} for constrained IoT devices~\cite{selander-lake-edhoc-01}.
%
In contrast to more powerful devices like web cameras and cars, which receive a
lot of media attention, such devices operate under severe energy consumption
and message size restrictions.
%
\mEdhoc{} was first formally analyzed in 2018 by
Bruni~et~al.~\cite{DBLP:conf/secsr/BruniJPS18}.
%
Since then, the protocol has been significantly extended and now has three new
key establishment methods.
%
In this paper, we formally analyze all methods of \mEdhoc{} in a symbolic
Dolev-Yao model, using the \mTamarin{} verification tool.
%
We show that the different methods provide sensible, but also rather
heterogeneous security properties, and discuss various consequences of this.
%
Our work has also led to improvements in the design and the specification of
\mEdhoc.
%
\end{abstract}
%

%\keywords{Formal verification \and Security \and IETF standardization \and
  %Key establishment protocols \and Tamarin}

%-------------------------------------------------------------------------- sec
%\vspace{-2.5em}
\section{Introduction}
\label{sec:introduction}

%-------------------------------------------------------------------------- sub
\subsection{Background and motivation}
\label{sec:motivation}
IoT security threats involving computationally strong devices such as cars
and web-cameras receive the most attention from media and academia.
%
Securing communication between such devices can readily be done using existing
protocols like \mDandTls.
%
Constrained devices and networks, on the other hand, which operate under severe
bandwidth and energy consumption restrictions, have received much less
attention.
%
These devices may be simple sensors which only relay environment
measurements to a server every hour, but need to function autonomously without
maintenance for long periods of time.
%
To keep energy consumption down, highly specialized radio links with small
and heterogeneous frame sizes are sometimes used.
%
The IETF defined the Constrained Application Protocol (\mCoap{}) protocol for
data transmission in such situations~\cite{rfc7252}.
%
\mCoap{} does not include security protection on its own, and in some cases,
\mDandTls{} messages are too large to fit into the radio frames, or is
unsuitable to handle proxy operations with change of underlying transport
protocol.
%
These are some of the reasons the IETF standardized the Object Security for
Constrained RESTful Environments
(\mOscore{}) protocol to secure communications between constrained
devices~\cite{rfc8613}.
%

The \mOscore{} protocol requires a pre-established security context.
%
For a couple of years, requirements and mechanisms for a key
exchange protocol, named \mEdhoc~\cite{selander-lake-edhoc-01}, for
establishing \mOscore{} security contexts have been discussed in the IETF.
%
Naturally, \mEdhoc{} must work under the same constrained requirements as
\mOscore{} itself.
%
While not all use cases for \mEdhoc{} are firmly set, the overall goal is to
establish an \mOscore{} security context, under message size limitations.
%
The work is now being done in the IETF Lightweight Authenticated Key Exchange
(LAKE) working group.
%

%-------------------------------------------------------------------------- sub
\subsection{Related Work}
\label{sec:relatedWork}
%
The first incarnation of \mEdhoc{} appeared in March 2016.
%
It contained two different key establishment methods, one based on a
pre-shared Diffie-Hellman (DH) cryptographic core and a second based on a
variant of challenge-response signatures, in the style of the \mNoise{}
framework~\cite{perrin2016noise}.
%
By a cryptographic core, or simply core, we mean an academic protocol, without
encodings or application specific details required by an industrial protocol.
%
By a key establishment method we mean a core with such details added.
%

The core based on challenge-response signatures was replaced by \mSigma{}
in May 2018.
%
Now, variants using challenge-response signatures have been added again by
integrating the cryptographic core of \mOptls{}.
%
Additionally, mixed variants where one party uses a challenge-response
signature and the other a regular signature have also been added.
%
Consequently, there are now five methods in total, and formal analysis is
required to verify security guarantees for \mEdhoc.
%
This is especially important, since the \mSpec{} itself lacks a description
of the intended security model and overall security goals.
%

Three cores have been analyzed in the computational model (\mSigma{}~\cite{DBLP:conf/crypto/CanettiK02},
\mOptls{}~\cite{DBLP:conf/eurosp/KrawczykW16}, and
\mNoise{}~\cite{DBLP:conf/eurosp/KobeissiNB19}).
%
However, there are significant departures from these cores in \mEdhoc, and
these proofs do not carry over automatically
(See Section~\ref{sec:relationsToOtherProtocols}).
%
The work closest to ours is Bruni~et~al.~\cite{DBLP:conf/secsr/BruniJPS18},
formally analyzing the May 2018 version of \mEdhoc{} (with two methods) in
\mProverif~\cite{DBLP:conf/csfw/Blanchet01}.
%

%-------------------------------------------------------------------------- sub
\subsection{Contributions}
\label{sec:contributions}
We formally analyze the \mEdhoc{} protocol in the \mTamarin{}
tool~\cite{DBLP:conf/cav/MeierSCB13}.
%
This work is presented in Section~\ref{sec:formalization}.
%
The formal models and proven properties are based on the version as on
2020-03-01~\cite{selander-lake-edhoc-01}.
%
We give an explicit security model for the protocol and verify essential
properties, such as session key and entity authentication and perfect forward
secrecy, for all five methods.
%
We also discuss the relationship between proven properties and the claimed
security properties, and the lack of a precise security model for \mEdhoc{}.
%
In fact, the standard has already been improved based on our analysis,
which we discuss in Section~\ref{sec:discussion}.
%

%-------------------------------------------------------------------------- sec
\section{The \mEdhoc{} Protocol}
\label{sec:edhoc}
\input{edhocProtocol}

%-------------------------------------------------------------------------- sec
\section{Formalization and Results}
\label{sec:formalization}
\input{edhocFormalization}

%-------------------------------------------------------------------------- sec
\section{Discussion}
\label{sec:discussion}
There are a few instances where \mEdhoc{} can be improved,
which we found during this work and communicated to the authors. We discuss them below.
%

%-------------------------------------------------------------------------- sub
\subsection{Security Claim Justification}
\label{sec:securityClaims}
The \mSpec{} makes detailed claims about security properties that \mEdhoc{}
enjoys, which the authors assume hold because they reuse cryptographic cores
from existing academic protocols.
%
Specifically, in Section~8.1 of~\cite{selander-lake-edhoc-01}, the authors
claim that ``EDHOC inherits its security properties from the theoretical
\mbox{SIGMA-I}''.
%
The intention is the same for the other reused cryptographic
cores based on \mOptls{} and \mNoise{}, but since the \mSpec{} is still work in
progress, it is not yet written down~\cite{personalCommunication}.
%

While it is good practice to reuse well-studied academic components in
industrial standards, it is important to justify that changes made to these
components preserve security properties.
%
Some properties have been verified~\cite{DBLP:conf/secsr/BruniJPS18} and this paper verifies more, but until some justification is provided, security
claims may benefit from a note of caution.

%-------------------------------------------------------------------------- sub
\subsection{Unclear Intended Use}
\label{sec:unclearProtocolUse}
Formal verification methodologies often clash with industrial standard
development practices; this is true also in our case.
%
The most important reason for the clash is that formal verification aims to
verify whether well-specified and detailed security goals are met, whereas
industrial standards are developed with a clear abstract goal,
but one that lacks specificity.
%
Instead the goals are there typically made more specific by listing resistance
to attacks as these are discovered throughout the work.
%
Granted, as discussed in Section~\ref{sec:claimedProperties}, the \mSpec{} lists
several specific security goals.
%
However, without knowing how the protocol is to be used,
it is not clear whether these are the most important goals for constrained IoT
devices.
%

The abstract goal of \mEdhoc{} is simple: establish an \mOscore{} security
context using few roundtrips and small messages.
%
From that, the design of \mEdhoc{} is mainly driven by what
can be achieved given the technical restrictions.
%
Focusing too much on what can be achieved within given restrictions, and paying
too little attention to the use cases where the
protocol is to be used and their specific goals, risks resulting in
sub-optimal trade-offs and design decisions.
%

\mEdhoc{} is intended to cover a variety of use cases, many of which are
difficult to predict today.
%
Just because it is difficult to predict these use cases, does not
prevent one from collecting \emph{typical} use cases and user stories
to identify more specific security goals that will be important in most cases.
%

While constructing our model, we came up with simple user stories to identify
security properties of interest.
%
Several of these revealed undefined aspects of \mEdhoc{}.
%
We informed the \mEdhoc{} authors, who then included these aspects the \mSpec{}.
%
We present a couple of examples here.
%

\subsubsection{Non-repudiation}
%\runhead{Non-repudiation}
An access control solution for a nuclear power-plant may need to log who is
passing through a door, whereas it may be undesirable for, say, a coffee
machine to log a list of users along with their coffee preferences.
%
Via this simple thought experiment, we realized that the \mSpec{} did not
consider non-repudiation.
%
In response, the authors of the \mSpec{} added a paragraph about which methods
provided which types of (non)-repudiation~\cite{selander-lake-edhoc-01}.

\subsubsection{Unintended Peer Authentication}
%\runhead{Unintended Peer Authentication}
Section~3.2 of the \mSpec{} states that parties must be configured
with a policy restricting the set of peers they can run \mEdhoc{} with.
%
However, the initiator is not required to verify that the \mIdcredr{} received
in the second message is the same as the one intended at initialization.
%
The following thought experiment shows why such a policy is insufficient.
%

Assume that someone has configured all devices in their home to be in the
allowed set of devices, but that one of the devices ($A$) is compromised.
%
If another device $B$, initiates a connection to a third device $C$, the
compromised device $A$ may interfere by responding in $C$'s place, blocking
the legitimate response from $C$.
%
Since $B$ does not verify that the received identity in the second message
matches the intended identity $C$, and device $A$ is part of the allowed set,
$B$ will complete and accept the \mEdhoc{} run with device $A$ instead of the
intended $C$.
%
The obvious solution is for the initiator to match \mIdcredr{} to the intended
identity provided by the application.
%
We have communicated this situation to the \mEdhoc{} authors and they are considering
how to resolve the issue.
%

%------------------------------------------------------------------------- sub
\subsection{Unclear Security Model}
When designing a security protocol, the attacker's capabilities must be
considered so that it is possible to determine whether the protocol is
sufficiently secure.
%
That is, a security model in which the protocol is deemed
secure needs to be defined at least on a high level.
%
We argue that the \mSpec{} gives too little information about what capabilities
an attacker is assumed to have, and that this leads to unclear design goals and
potentially sub-optimal design.
%
%Let us explore this via an example.
%

It is conceivable that IoT devices deployed in a hostile environments can be
hardened by equipping them with a TEE, but \mEdhoc{} is not %intentionally
designed to take advantage of this.
%
Even though \mEdhoc{} incorporates cryptographic cores from different academic
security protocols, its design does not take into account the attacker models
for which these protocols were designed.
%
For example, \mOptls{} is designed to be secure in the CK
model~\cite{DBLP:conf/crypto/CanettiK02}.
%
The CK security model explicitly separates the secure storage of long-term
credentials from storage of session state and ephemeral keys to model the
use of TEEs.
%

The \mEdhoc{} authors indicated to us that it was
not necessary to consider compromised ephemeral session keys separately from
from compromised long-term keys.
%
The rationale is that \mSigma{} cannot protect against compromised ephemeral
keys~\cite{personalCommunication}.
%
That rationale is presumably based on the fact that the \mSigSig{} method is
closely modeled on \mSigmaI{} and that it would be preferable to obtain a
homogeneous security level among the \mEdhoc{}
methods.
%
That rationale is only true, however, if one restricts attention to session key
confidentiality of an ongoing session.
%
TEEs provide value in other ways, for example, by allowing contractions with
weak PCS guarantees.
%
It would be wasteful to not consider TEEs for long-term key storage as part of
the security, since it could otherwise make use of many good properties of the
re-used cryptographic cores, like \mOptls.
%

%-------------------------------------------------------------------------- sub
\subsection{Session Key Material}
\label{sec:sessionKeyMaterial}
\mEdhoc{} establishes session key material, from which session keys
can be derived using the \mEdhoc{}-Exporter.
%
The session key material is affected by \mGxy{}, and if a party uses the
\mStat{} method, also by that party's secret static long-term DH key.
%
As shown in Section~\ref{sec:formalization}, mutual injective agreement cannot
be achieved for \mGiy{}.
%
If this property is not important for constrained IoT devices which cannot use
any of the other methods, then one can simply accept that the methods have
different authentication strengths.
%
However, if it is important, this is a problem.
%

We identified three alternatives for resolving this.
%
One is to include a fourth message from responder to initiator,
carrying a MAC based on a key derived from session key
material including \mGiy{}.
%
Successful MAC verification guarantees
to the initiator that the responder injectively agrees on \mGiy{}.
%
However, our understanding is that adding an extra message is
undesirable, since~\cite{selander-lake-edhoc-01} requests as few messages as
possible.
%

Another possibility is to include \mGi{}, or its hash, in the first and
second messages.
%
This would, however, prevent initiator identity protection and increase message
sizes, grave concerns for \mEdhoc{}.
%

A third alternative is to not derive the session key material from \mGiy{}.
%
Doing so would destroy the protection \mOptls{} provides against compromise
of the initiator's ephemeral DH key.
%

Regardless of how this problem is handled, we have verified that all methods
share a common, but weaker, security property: mutual implicit authentication
on all of \mGxy{}, \mGiy{} and \mGrx{}.
%

%-------------------------------------------------------------------------- sub
\subsection{Cipher Suite Negotiation}
\label{sec:ciphersuiteNegotiation}
As described in Section~\ref{sec:ciphersuite}, cipher suite negotiation in \mEdhoc{} spans one or more executions of the
protocol.
%
As part of the first message, the initiator proposes an ordered list of cipher suites they support (see Section~\ref{sec:edhoc}, Figure~\ref{fig:edhocFramework}). The responder either accepts the highest entry in this list (if they also support that suite) or makes a counter-proposal, namely the highest entry which they do support. If there is no such entry the responder rejects the suite entirely, and the protocol does not continue.
%
If a run terminates due to the proposed cipher suites being rejected by the
responder, the initiator maintains state and initiates a new run, proposing
an updated set of cipher suites.
%
This implicitly creates a long-lived
meta-session covering multiple \mEdhoc{} sessions.
%

However, the time for which the initiator should
remember a rejected cipher suite for a given responder is not specified.
%
From a security perspective, remembering the rejected cipher suite for the
next \mEdhoc{} run in the same meta-session would be sufficient.
%
If the responder is updated with a new cipher suite before the next such
session, this could be taken into account. On the other hand, caching the
rejected cipher suite between meta-sessions would reduce the number of
round-trips for subsequent runs, should the responder not have been updated.
%
This needs to be clearly specified, and we have conveyed this to the authors
of the \mSpec.
%

%-------------------------------------------------------------------------- sec
\section{Conclusions and future work}
\label{sec:conclusions}
We formally modeled all five
methods of the \mEdhoc{} key establishment protocol using the \mTamarin{} tool, and
formulated and verified several important security properties in this model --
PFS; session key material independence; mutual injective agreement on roles, identities and session key material
(except for when the initiator uses the \mStat{} method); implicit
authentication on on the same parameters for all methods; consitency, aliveness
and peer awareness (the last two when mutual injective agreement holds);
entity authentication (also when mutual injective agreement holds).
%
Most importantly, we found that injective agreement on \mGiy{} does not hold for
initiators when they use the \mStat{} method.
%
We verified each method in isolation, and leave as future work to verify whether
the methods are secure under composition.
%

Further, we identified a situation where initiators may establish an \mOscore{}
security context with a different party than the application using \mEdhoc{}
intended, and proposed a simple mitigation.
%
We discussed how the IETF may extract and better define security properties to
enable easier verification.
%
There is some work that was done as part of this effort which has not been mentioned in this paper. These lines of enquiry form the basis for future work.

We considered two more properties, namely key-compromise impersonation (KCI) resistance and weak post-compromise security (PCS). A protocol is said to have KCI resistance if a party $I$ can establish a secure session with party $R$, even if $I$'s keys are compromised at any time, and $R$'s key material is not leaked until the end of the session. The authors of \mSpec{} claim that \mEdhoc{} has KCI resistance. Weak PCS~\cite{cohn2016post} is said to hold if a session key established in a run $\rho$ between parties $I$ and $R$ continues to be secret between them, even if $\rho$ was such that the attacker could perform cryptographic operations using $I$ and $R$'s long term keys (without having access to the keys themselves). We verified that KCI resistance and weak PCS guarantees hold for the \mSigSig{} and \mPskPsk{} methods.
However, the tool does not terminate for these properties on the other methods, and therefore, we do not know whether the \mStat-based methods enjoy these properties or not. We relegate the verification of these properties for the \mStat-based methods to future work.
%

We also tried to incorporate the parameters \mCi, \mCr, and \mAD{} into our model. This too resulted in non-termination for some of the methods, and further study is required to obtain conclusive results along these lines.

Another potential extension is to incorporate the cipher suite negotiation process into the formal modeling.\\
%

%-------------------------------------------------------------------------- ack
\paragraph{Acknowledgments.} This work was partially supported by
the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by
the Knut and Alice Wallenberg Foundation.
%
We are grateful to G\"oran Selander, John Mattsson and Francesca Palombini for
clarifications regarding the specification.
%

%-------------------------------------------------------------------------- bib
\bibliographystyle{spmpsci}
\bibliography{refv}
\end{document}

max_stars_repo_name: hoheinzollern/EDHOC-Verification

max_issues_repo_name: hoheinzollern/EDHOC-Verification

max_forks_repo_name: hoheinzollern/EDHOC-Verification


text:
\hypertarget{classnumpp_1_1differentiation_1_1symbolic_1_1exponential}{}\section{numpp\+:\+:differentiation\+:\+:symbolic\+:\+:exponential$<$ T $>$ Class Template Reference}
\label{classnumpp_1_1differentiation_1_1symbolic_1_1exponential}\index{numpp\+::differentiation\+::symbolic\+::exponential$<$ T $>$@{numpp\+::differentiation\+::symbolic\+::exponential$<$ T $>$}}
\subsection*{Public Types}
\begin{DoxyCompactItemize}
\item
\mbox{\Hypertarget{classnumpp_1_1differentiation_1_1symbolic_1_1exponential_a3627b60b251a1a80cc009ac8d1a68674}\label{classnumpp_1_1differentiation_1_1symbolic_1_1exponential_a3627b60b251a1a80cc009ac8d1a68674}}
{\footnotesize template$<$std\+::size\+\_\+t Active$>$ }\\using {\bfseries derivative} = simplify\+\_\+multiplication$<$ \hyperlink{classnumpp_1_1differentiation_1_1symbolic_1_1exponential}{exponential}$<$ T $>$, typename T\+::template derivative$<$ Active $>$ $>$
\end{DoxyCompactItemize}
\subsection*{Static Public Member Functions}
\begin{DoxyCompactItemize}
\item
\mbox{\Hypertarget{classnumpp_1_1differentiation_1_1symbolic_1_1exponential_a6366faad35aeb046cfccb85208347a61}\label{classnumpp_1_1differentiation_1_1symbolic_1_1exponential_a6366faad35aeb046cfccb85208347a61}}
static C\+O\+N\+S\+T\+E\+X\+PR auto {\bfseries calculate} (auto \&\&values)
\end{DoxyCompactItemize}

The documentation for this class was generated from the following file\+:\begin{DoxyCompactItemize}
\item
differentiation/symbolic/exponential.\+hpp\end{DoxyCompactItemize}

max_stars_repo_name: szymonmaszke/numpp

max_issues_repo_name: vyzyv/numpp

max_forks_repo_name: szymonmaszke/numpp


text:
% =========================================
% COMMAND: _SSL_LEGACY
% =========================================

\newpage
\section{\_SSL\_LEGACY}
\label{cmd:_SSL_LEGACY}

\paragraph{Syntax:}
\subparagraph{}
\texttt{\_SSL\_LEGACY on|off}

\paragraph{Purpose:}
\subparagraph{}
Turns SSL legacy behaviour on or off for renegotiation (for
OpenSSL libraries 0.9.81 and above).

% TODO: Wieso? Beispiel? Von htt-Version abhaengig?


text:
\documentclass{article}
\usepackage{lmodern}%
\usepackage{enumitem}
\usepackage[authoryear]{natbib}

\newtheorem{exercise}{Exercise}[section]
% \newenvironment{exercise}{\begin{@exercise}\rm}{\end{@exercise}}
\newenvironment{ADDITIONAL}[1]{#1}{}
\newenvironment{SOLUTION}[1]{\paragraph*{Solution}\begin{it}#1}{\end{it}}

%\oddsidemargin 0pt
%\evensidemargin \oddsidemargin
%\marginparwidth 0.5in

% \setlength{\topmargin}{15mm}
\setlength{\topmargin}{5mm}

%\setlength{\textwidth}{155mm}
\setlength{\textwidth}{155mm}
%\setlength{\textwidth}{165mm}
\setlength{\textheight}{200mm}
%\setlength{\textheight}{195mm}

\setlength{\evensidemargin}{5mm}
\setlength{\oddsidemargin}{5mm}

\newcommand{\hs}[1]{\hspace{#1}}

% \usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{latexsym}
\usepackage{amsfonts}
\usepackage{listings}
\usepackage{srcltx}
\usepackage{charter}
\usepackage{euler}

\usepackage{latexsym}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{comment}

\ifdefined\studentversion
  \excludecomment{exercise}
  \excludecomment{solution}
  \excludecomment{additional}
\else
% \excludecomment{additional}
\includecomment{exercise}
\includecomment{solution}
\includecomment{additional}
\fi

\newtheorem{@problem}{Exercise}[section]
\newenvironment{problem}{\begin{@problem}\rm}{\end{@problem}}

\newtheorem{@sol}{Solution}[section]
\newenvironment{sol}{\begin{@sol}\rm}{\end{@sol}}

\newcommand{\ext}[1]{\geq_{#1}}

\usepackage{proof}
\usepackage{cdsty}

\newcommand{\nl}{\overline{n}}

\newtheorem{@axiom}{Axiom}
\newenvironment{axiom}{\begin{@axiom}\rm}{\end{@axiom}}
% \newtheorem{@theorem}{Theorem}[section]
% \newenvironment{theorem}{\begin{@theorem}\rm}{\end{@theorem}}

 \newtheorem*{@lemma-nonum}{Lemma}
 \newenvironment{lemma*}{\begin{@lemma-nonum}\rm}{\end{@lemma-nonum}}

 \newtheorem*{@thm-nonum}{Theorem}
 \newenvironment{theorem*}{\begin{@thm-nonum}\rm}{\end{@thm-nonum}}

\input prelude

\usepackage{graphics}
\usepackage{graphicx}

\usepackage{lstextract}

% \includeonly{intro,assign,unif,memo,index,memo-implement,proving}
% \includeonly{index}

\newcommand{\B}{\mathcal{B}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\G}{\mathcal{G}}
\renewcommand{\H}{\mathcal{H}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\Q}{\mathcal{Q}}

\newcommand{\nf}[2]{#1 : #2 ~\mathsf{nf}}
\newcommand{\neu}[2]{#1 : #2 ~\mathsf{ne}}
\newcommand{\hole}{\mathsf{\_}}
\newcommand{\holetype}{\mathsf{~|~}}

 \newcommand{\one}{1}
\newcommand{\SN}{\mathsf{SN}}
\newcommand{\SNe}{\mathsf{SNe}}
\newcommand{\csn}{\mathsf{sn}}
\newcommand{\CR}{\textsf{CR}}
\newcommand{\denot}[1]{\mathcal{R}_{#1}}
\newcommand{\inden}[3]{#1 \vdash #2 \in \denot{#3}}
\newcommand{\mred}{\longrightarrow^*}
\newcommand{\red}{\longrightarrow}
\newcommand{\redsn}{\longrightarrow_\csn}
\newcommand{\redSN}{\longrightarrow_\SN}
\newcommand{\clos}[1]{\overline{#1}}
\newcommand{\imply}{\Longrightarrow}
\renewcommand{\vec}[1]{\overrightarrow #1}

\newcommand{\id}{\textsf{wk}}
\newcommand{\wk}{\textsf{wk}}

\def\lv{\mathopen{{[\kern-0.14em[}}}    % opening [[ value delimiter
\def\rv{\mathclose{{]\kern-0.14em]}}}   % closing ]] value delimiter
\newcommand{\A}{\mathcal{A}}
% \newcommand{\G}{\mathcal{G}}
\newcommand{\den}[1]{\lv #1 \rv}
\newcommand{\Den}[3][]{\den{#2}^{#1}_{#3}}
\newcommand{\dent}[2]{\llparenthesis#1\rrparenthesis_{#2}}

\long\def\ednote#1{\footnote{[{\it #1\/}]}\message{ednote!}}
% \long\def\note#1{\begin{quote}[{\it #1\/}]\end{quote}\message{note!}}

\begin{document}
\title{POPLMark Reloaded Benchmark: An Introduction \\
-- Work in Progress --}
\author{%
Brigitte Pientka \\ McGill University%
  \and Aliya Hameer \\ McGill University%
  \and Alberto Momigliano \\ University of Milan%
  \and Andreas Abel \\ Chalmers %
%
  }
\date{}
\maketitle

\input{intro.tex}

\input{inductive-defn.tex}

\input{reducibility.tex}

\newpage

\input{extensions.tex}

%\section{Reducibility candidates}
%\section{Forward and backward closed}
%\section{Fundamental lemma}

\bibliographystyle{plainnat}
% \bibliography{../../bibliography/bibi,../../bibliography/bp}
\bibliography{bibi-extract}

\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "sn-proof"
%%% End:

%  LocalWords:  Girard Tait llcl lcl redex subterms iff reducts IH
%  LocalWords:  subst subterm todo Girard's instantiation inl inr
%  LocalWords:  subcases Subcase

max_stars_repo_name: andreasabel/strong-normalization

max_issues_repo_name: andreasabel/strong-normalization

max_forks_repo_name: andreasabel/strong-normalization


text:
%-------------------------
% Resume in Latex
% Author : Jake Gutierrez
% Based off of: https://github.com/sb2nov/resume
% License : MIT
%------------------------

\documentclass[letterpaper,11pt]{article}

\usepackage{latexsym}
\usepackage[empty]{fullpage}
\usepackage{titlesec}
\usepackage{marvosym}
\usepackage[usenames,dvipsnames]{color}
\usepackage{verbatim}
\usepackage{enumitem}
\usepackage[hidelinks]{hyperref}
\usepackage{fancyhdr}
\usepackage[english]{babel}
\usepackage{tabularx}
\input{glyphtounicode}

%----------FONT OPTIONS----------
% sans-serif
% \usepackage[sfdefault]{FiraSans}
% \usepackage[sfdefault]{roboto}
% \usepackage[sfdefault]{noto-sans}
% \usepackage[default]{sourcesanspro}

% serif
% \usepackage{CormorantGaramond}
% \usepackage{charter}

\pagestyle{fancy}
\fancyhf{} % clear all header and footer fields
\fancyfoot{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}

% Adjust margins
\addtolength{\oddsidemargin}{-0.5in}
\addtolength{\evensidemargin}{-0.5in}
\addtolength{\textwidth}{1in}
\addtolength{\topmargin}{-.5in}
\addtolength{\textheight}{1.0in}

\urlstyle{same}

\raggedbottom
\raggedright
\setlength{\tabcolsep}{0in}

% Sections formatting
\titleformat{\section}{
  \vspace{-4pt}\scshape\raggedright\large
}{}{0em}{}[\color{black}\titlerule \vspace{-5pt}]

% Ensure that generate pdf is machine readable/ATS parsable
\pdfgentounicode=1

%-------------------------
% Custom commands
\newcommand{\resumeItem}[1]{
  \item\small{
    {#1 \vspace{-2pt}}
  }
}

\newcommand{\resumeSubheading}[4]{
  \vspace{-2pt}\item
    \begin{tabular*}{0.97\textwidth}[t]{l@{\extracolsep{\fill}}r}
      \textbf{#1} & #2 \\
      \textit{\small#3} & \textit{\small #4} \\
    \end{tabular*}\vspace{-8pt}
}

\newcommand{\resumeSubSubheading}[2]{
    \item
    \begin{tabular*}{0.97\textwidth}{l@{\extracolsep{\fill}}r}
      \textit{\small#1} & \textit{\small #2} \\
    \end{tabular*}\vspace{-8pt}
}

\newcommand{\resumeProjectHeading}[2]{
    \item
    \begin{tabular*}{0.97\textwidth}{l@{\extracolsep{\fill}}r}
      \small#1 & #2 \\
    \end{tabular*}\vspace{-8pt}
}

\newcommand{\resumeSubItem}[1]{\resumeItem{#1}\vspace{-5pt}}

\renewcommand\labelitemii{$\vcenter{\hbox{\tiny$\bullet$}}$}

\newcommand{\resumeSubHeadingListStart}{\begin{itemize}[leftmargin=0.15in, label={}]}
\newcommand{\resumeSubHeadingListEnd}{\end{itemize}}
\newcommand{\resumeItemListStart}{\begin{itemize}}
\newcommand{\resumeItemListEnd}{\end{itemize}\vspace{-5pt}}

%-------------------------------------------
%%%%%%  RESUME STARTS HERE  %%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

%----------HEADING----------

\begin{center}
    \textbf{\Huge \scshape Neeraj Kumar Singh} \\ \vspace{1pt}
    \small 1234567890 $|$ \href{mailto:neerajsingh.iitd@gmail.com}{\underline{neerajsingh.iitd@gmail.com}} $|$
    \href{https://linkedin.com/in/neeraj-kumar-singh-3b490a1b2/}{\underline{linkedin.com/in/neeraj}} $|$
    \href{https://github.com/neerajsingh869}{\underline{github.com/neeraj}}
\end{center}

%-----------EDUCATION-----------
\section{Education}
  \resumeSubHeadingListStart
    \resumeSubheading
      {Indian Institute of Technology}{Delhi, India}
      {Bachelor of Technology in Mechanical Engineering~~~~~~~~~CGPA 7.93}{Aug, 2018 -- Jul, 2022}
    \resumeSubheading
      {Central Hindu Boys School}{Varanasi, India}
      {Higher Secondary Education~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~Marks 90.6\%}{Jul, 2015 -- May, 2017}
    \resumeSubheading
      {Raj English School}{Varanasi, India}
       {Secondary Education~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~CGPA 9}{Jun, 2014 -- Jul, 2015}
  \resumeSubHeadingListEnd

%-----------Scholastic Achievements-----------
\section{Scholastic Achievements}
  \resumeItemListStart
      \resumeItem {Secured \textbf{All India Rank 419 (OBC)} among \textbf{1.5 million} candidates in JEE Advanced Exam in 2018}
      \vspace{-5pt}
      \resumeItem {Secured \textbf{All India Rank 29} in FIITJEE Talent Reward Examination (FTRE) conducted by FIITJEE in 2017}
      \vspace{-5pt}
      \resumeItem {Conferred scholarship on qualifying \textbf{UP Science Talent Search Examination} in 2017}
      \vspace{-5pt}
      \resumeItem {Won \textbf{Governor Award} in Scouts and Guides on excellent performance in \textbf{5 days camp} in 2012}
      \vspace{-5pt}
  \resumeItemListEnd
%-----------PROJECTS-----------
\section{Projects}
    \resumeSubHeadingListStart
      \resumeProjectHeading
          {\textbf{WhatsApp Chat Analyzer with Heroku deployment} $|$ \emph{Side Project}}{Jun, 2021 - Aug, 2021}
          \resumeItemListStart
            \resumeItem{Built WhatsApp Chat Analyzer to \textbf{analyze} chats with the help of useful \textbf{statistics} and engaging \textbf{charts}}
            \resumeItem{Converted WhatsApp chat data into dataframe using \textbf{pandas} and \textbf{regular expression} libraries}
            \resumeItem{Used \textbf{urlextract}, \textbf{wordcloud}, \textbf{collections}, and \textbf{emoji} libraries to answer some questions on the dataset}
            \resumeItem{Constructed Stopwords for \textbf{hinglish} language and used it to remove irrelevant/unnecessary words from the data}
            \resumeItem{Used \textbf{Streamlit} library to create website, and \textbf{Heroku} platform to deploy the project}
          \resumeItemListEnd

      \resumeProjectHeading
          {\textbf{Laptop Price Predictor with AWS EC2 deployment} $|$ \emph{Side Project }}{Jun, 2021 - Jul, 2021}
          \resumeItemListStart
            \resumeItem{Built a \textbf{end to end} laptop price predictor that predicts the laptop's price on the basis of given configurations}
            \resumeItem{Did EDA using \textbf{numpy}, \textbf{pandas}, \textbf{matplotlib} and \textbf{seaborn} libraries after cleaning the dataset}
            \resumeItem{Used \textbf{log transformation} to reduce the skewness in the target feature for better results}
            \resumeItem{Got R2 score of \textbf{87\%} and MAE of \textbf{0.17} on the test dataset using \textbf{Random Forest} model in \textbf{Sklearn} library}
            \resumeItem{Used \textbf{Streamlit} library to create website, and \textbf{AWS EC2} instance to deploy the project}
          \resumeItemListEnd
      \resumeProjectHeading
        {\textbf{ Content Based Movie Recommender System with Heroku deployment} $|$ \emph{Side Project }}{Apr, 2021 - Jun, 2021}
        \resumeItemListStart
            \resumeItem{Built \textbf{end to end} movie recommender system that recommends 5 most similar movies}
            \resumeItem{Used \textbf{Stemming}, \textbf{Stopwords} and \textbf{TFIDF} utilities from \textbf{NLTK} and \textbf{Sklearn} libraries}
            \resumeItem{Used \textbf{cosine distance} to find the similarity score between all pairs of movies}
            \resumeItem{Used \textbf{Streamlit} library to create website, \textbf{TMDB} API to fetch movie posters and \textbf{Heroku} to deploy project}
        \resumeItemListEnd
      \resumeProjectHeading
        {\textbf{ Diagnosing Parkinson Disease using MLP and SVM} $|$ \emph{Prof. Souvik Chakraborty}}{Mar, 2021 - Apr, 2021}
        \resumeItemListStart
            \resumeItem{Developed a \textbf{Decision Support System} to aid the Specialist in diagnosing of Parkinson Disease}
            \resumeItem{ Balanced the dataset using \textbf{SMOTE} technique and reduced dimensionality using \textbf{PCA} technique}
            \resumeItem{Used \textbf{Sklearn} library for deploying \textbf{MLP} and \textbf{SVM} classifers on the Parkinson dataset}
            \resumeItem{Got \textbf{98\%} accuracy and \textbf{0.95} F1 score after Hyperparameter tuning and model selection}
        \resumeItemListEnd

    \resumeSubHeadingListEnd

%
%-----------PROGRAMMING SKILLS-----------
\section{Technical Skills}
 \begin{itemize}[leftmargin=0.15in, label={}]
    \small{\item{
     \textbf{Programming Languages}{: C++, Python, Java, SQL (MySQL)}  \textbf{~~~~~~~~~~~~~~~~~~~~~~Cloud}{: Heroku, AWS (EC2 instance)}\\
     \textbf{Data Science}{: Python libraries, Machine Learning (Sklearn), Deep Learning (TensorFlow and Keras)}\\
     \textbf{Software \& Tools}{: HTML, CSS, Git, LaTex, Anaconda, Jupyter, Streamlit, PyCharm, Google Colab, Visual Studio} \\
    }}
 \end{itemize}

%-----------POSITION OF RESPONSIBILITY-----------
\section{Position Of Responsibility}
    \resumeSubHeadingListStart
      \resumeProjectHeading
          {\textbf{Nucleus Coordinator, Ofce of Career Services} $|$ \emph{IIT Delhi}}{Jun, 2020 - Apr, 2021}
          \resumeItemListStart
            \resumeItem{Appointed after a \textbf{3 Stage} selection process with \textbf{300+} applicants}
            \resumeItem{Responsible to pitch and bring department wise companies in the campus for training and placement session}
            \resumeItem{Working in tandem with \textbf{500+ recruiters} for campus recruitment of \textbf{1000+ students} in a \textbf{40 membered team}}
          \resumeItemListEnd
    \resumeSubHeadingListEnd

%-------------------------------------------
\end{document}


text:
%\begin{center}
%\end{center}
\begin{flushleft}

\chapter{Set up Process on Visual Studio}

\section{\textbf{Introduction}}
\medskip

Visual Studio Express products provide a free development environment to develop applications for the latest platforms. Visual Studio Express can be downloaded from

\medskip

\url{http://www.visualstudio.com/en-us/products/visual-studio-express-vs.aspx}.

\medskip
The experiments on kinect discussed in this manual are designed using C\# and Windows Presentation Foundation (WPF). Before commencing the discussion of experiments and their code, it is essential to understand how to set up the environment to design the same. This includes adding references, the procedure for which is discussed in this chapter.
This is a prerequisite to the experimenting stage to follow.

\medskip
\textbf{Note : }
At the time of making of this manual, the latest version was Visual Studio Express 2013. The same was used for experimenting with kinect.

\medskip
\subsection{\textbf{ System Requirements}}
\medskip
\textbf{Supported Operating System}

Windows 7 SP1 (x86 and x64), Windows 8 (x86 and x64), Windows 8.1 (x86 and x64), Windows Server 2008 R2 SP1 (x64), Windows Server 2012 (x64) and Windows Server 2012 R2 (x64).

\medskip
\begin{itemize}
\item Hardware Requirements
\medskip
\begin{itemize}
\item 1.6 GHz or faster processor
\item 1 GB of RAM (1.5 GB if running on a virtual machine)
\item 5 GB of available hard disk space
\item 5400 RPM hard drive
\item DirectX 9-capable video card running at 1024 x 768 or higher display resolution
\end{itemize}
\medskip

\medskip
\end{itemize}
\subsection{\textbf{ Set up Procedure}}
\addcontentsline{lof}{figure}{\textbf{Set up procedure on Visual Studio 2013}}

\textbf{Step 1 :}
\medskip

Double click the \textbf{VS Express 2013 for desktop} icon to start the application.
Alternately, one can start the application from start menu as well.
Shown in Figure \ref{fig:e1}.
\medskip

\textbf{Step 2 :}

\medskip
Click on \textbf{New Project} to create a new project.
Shown in Figure \ref{fig:e2}.

\medskip

\textbf{Step 3 :}

\medskip
Select
\textbf{Visual C\# $\rightarrow$ WPF Application}
Give a project name and save it in the appropriate directory of your choice. In this example the project name is \textbf{my\_expt} saved in the \textbf{experiment} folder.
Shown in Figure \ref{fig:e3}.

\medskip

\textbf{Step 4 :}

\medskip

The project window will open. On the right hand side you will find the \textbf{Solution Explorer}.
Right click on \textbf{my\_expt $\rightarrow$ Add $\rightarrow$ Reference}
Shown in Figure \ref{fig:e4}.

\medskip

\textbf{Step 5 :}

\medskip

The Reference Manager will open. Go to \textbf{Assemblies $\rightarrow$ Extensions} and select \textbf{Microsoft.Kinect}. Click 'OK' to add.
Shown in Figure \ref{fig:e5}.

\medskip

\textbf{Step 6 :}

\medskip

In the solution explorer right click on \textbf{Solution 'my\_expt'(1 project) $\rightarrow$ Add $\rightarrow$ Existing Project}
Shown in Figure \ref{fig:e6}.

\medskip

\textbf{Step 7 :}

\medskip

Navigate to \textbf{KinectWpfViewers} folder (provided with this manual) and select \textbf{Microsoft.Samples.Kinect.WpfViewers.csproj}. Click 'Open' to add this project.
Shown in Figure \ref{fig:e7}.

\medskip

\textbf{Step 8 :}

\medskip
Now we need to reference this project.
Right click on \textbf{my\_expt $\rightarrow$ Add $\rightarrow$ Reference}.
Go to \textbf{Solution $\rightarrow$ Projects} and select \textbf{Microsoft.Samples.kinect.WpfViewers}
Shown in Figure \ref{fig:e8}.

\medskip

\textbf{Step 9 :}

\medskip
Now add the final 2 references.
Right click on \textbf{my\_expt $\rightarrow$ Add $\rightarrow$ Reference}.
Go to Browse and navigate to
\textbf{KinectWpfViewers} folder (provided with this manual) \textbf{$\rightarrow$ bin $\rightarrow$ Debug}
and select the 2 files :
\textbf{Microsoft.Kinect.Toolkit.dll} and
\textbf{Microsoft.Samples.Kinect.WpfViewers.dll}
Click 'OK' to add the same.

Shown in Figure \ref{fig:e9}.
\medskip

\textbf{Step 10 :}

\medskip
This completes the set up process. The Project window after completion of setup is shown in Figure \ref{fig:e10}.
You can now start programming on C\# and WPF for kinect applications

\medskip

\begin{figure}
\begin{center}
\includegraphics[scale=0.6]{s1}
\end{center}
\caption{Step 1 - Open VS Express 2013 for windows desktop}
\label{fig:e1}
\end{figure}

\medskip
\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s2}
\end{center}
\caption{Step 2 - Click on New Project}
\label{fig:e2}
\end{figure}
\medskip

\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s3}
\end{center}
\caption{Step 3 - Create a new C\# project}
\label{fig:e3}
\end{figure}

\medskip
\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s4}
\end{center}
\caption{Step 4 - Adding Reference}
\label{fig:e4}
\end{figure}

\medskip
\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s5}
\end{center}
\caption{Step 5 - Add reference to Microsoft.Kinect}
\label{fig:e5}
\end{figure}

\medskip
\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s6}
\end{center}
\caption{Step 6 - Adding existing project}
\label{fig:e6}
\end{figure}
\medskip
\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s7}
\end{center}
\caption{Step 7 - Select the project in KinectWpfViewers}
\label{fig:e7}
\end{figure}

\medskip
\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s8}
\end{center}
\caption{Step 8 - Reference the added project}
\label{fig:e8}
\end{figure}

\medskip
\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s9}
\end{center}
\caption{Step 9 - Adding final 2 references}
\label{fig:e9}
\end{figure}
\medskip
\begin{figure}
\begin{center}
\includegraphics[scale=0.5]{s10}
\end{center}
\caption{Step 10 - Project window post setup}
\label{fig:e10}
\end{figure}
\medskip
\Large{\textbf{Congratulations ! You have successfuly completed the set up on Visual Studio to design codes for working on the Kinect sensor.}}

\end{flushleft}

max_stars_repo_path: Kinect Based Module Development/Reference Material/Latex Files/Ch3-Setup.tex