From a4b68d6ce6cafd530d3d2cf9d61125a42da731c2 Mon Sep 17 00:00:00 2001
From: Tobias Eidelpes <tobias@eidelpes.info>
Date: Thu, 3 Jun 2021 14:13:49 +0200
Subject: [PATCH] Add explanation for 2.2

---
 report/report.tex | 63 +++++++++++++++++++++++++++++++++--------------
 1 file changed, 45 insertions(+), 18 deletions(-)

diff --git a/report/report.tex b/report/report.tex
index f0bfa23..b2211da 100644
--- a/report/report.tex
+++ b/report/report.tex
@@ -11,19 +11,10 @@
 \usepackage{titling}
 \renewcommand{\thesection}{Exercise \projnumber.\arabic{section}:}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% This part needs customization from you %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\groupnumber}{5}
+\newcommand{\name}{Tobias Eidelpes}
+\newcommand{\matriculation}{01527193}
 
-% please enter your group number your names and matriculation numbers here
-%TODO
-\newcommand{\groupnumber}{Our group number}
-\newcommand{\name}{Our names}
-\newcommand{\matriculation}{Our matriculations, same order as the names}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%           End of customization         %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \newcommand\fstar{F$^\star$\xspace}
 \newcommand{\projnumber}{2}
 \newcommand{\Title}{\fstar}
@@ -31,7 +22,7 @@
 \setlength{\headsep}{20pt}
 \setlength{\textheight}{680pt}
 \pagestyle{fancy}
-\fancyhf{} 
+\fancyhf{}
 \fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - ProVerif}
 \fancyhead[C]{}
 \fancyhead[R]{Group \groupnumber}
@@ -43,7 +34,7 @@
 \thispagestyle{empty}
 \noindent\framebox[\linewidth]{%
  \begin{minipage}{\linewidth}%
- \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2018)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\
+ \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2021)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\
 
  \begin{center}
   {\bf\Large Project \projnumber~-- \Title}
@@ -59,9 +50,9 @@
 \section*{Group \groupnumber}
 Our group consists of the following members:
 \begin{center}
-\textbf{\name} %please fill the information above
+\textbf{\name}
 
-\matriculation %please fill the information above
+\matriculation
 \end{center}
 
 \section{Small-step semantics}
@@ -71,12 +62,48 @@ Our group consists of the following members:
 \section{Termination}
 
 \paragraph{Explanation of the used measure}
-%TODO
+
+The measure consists of a list of size three. The entries are:
+
+\begin{enumerate}
+    \item The amount of gas in the execution state.
+    \item The size of the call stack.
+    \item If the call stack is constructed with \texttt{Exec}, the third element
+        is the natural number 1 and if the call stack is constructed with
+        \texttt{Ter}, the third element is the natural number 0.
+\end{enumerate}
+
+For the amount of gas, there are three different possibilities:
+
+\begin{enumerate}
+    \item The call stack is a plain call stack.
+    \item If the call stack is in a halting state, gas specifies the amount of
+        remaining gas.
+    \item If there is an exception state, the amount of gas is set to 0.
+\end{enumerate}
+
+Additionally, there are three match clauses in the \texttt{step} function. The
+first case matches a termination state with an empty call stack. If the state
+before that was an exception, the first elements are equal but the size of the
+call stack before the application of the \texttt{step} function was greater.
+This means that the measure decreases. If there was no exception but of type
+\texttt{Exec} with a positive amount of gas, the measure also decreases.
+
+In the second match clause, a termination state with a non-empty call stack is
+handled. The amount of gas decreases if there is a termination state of
+\texttt{ExcState}, because it is set to 0. If the termination state is
+\texttt{HaltState}, the amount of gas also decreases.
+
+The third match clause handles execution of a plain call stack. If a
+\texttt{HaltState} is reached, the amount of gas reduces by 1. Again, if there
+occurs an exception, looking at the third element of the list gives a value
+change from 1 to 0.
 
 \section{Final states}
 
 \paragraph{Paper proofs}
-%TODO
+
+
 
 \paragraph{Explanation on used equalities}
 %TODO