129 lines
3.5 KiB
TeX
129 lines
3.5 KiB
TeX
\documentclass[12pt,a4paper]{article}
|
|
|
|
\usepackage[cm]{fullpage}
|
|
\usepackage{amsthm}
|
|
\usepackage{amsmath}
|
|
\usepackage{amsfonts}
|
|
\usepackage{amssymb}
|
|
\usepackage{xspace}
|
|
\usepackage[english]{babel}
|
|
\usepackage{fancyhdr}
|
|
\usepackage{titling}
|
|
\renewcommand{\thesection}{Exercise \projnumber.\arabic{section}:}
|
|
|
|
\newcommand{\groupnumber}{5}
|
|
\newcommand{\name}{Tobias Eidelpes}
|
|
\newcommand{\matriculation}{01527193}
|
|
|
|
\newcommand\fstar{F$^\star$\xspace}
|
|
\newcommand{\projnumber}{2}
|
|
\newcommand{\Title}{\fstar}
|
|
\setlength{\headheight}{15.2pt}
|
|
\setlength{\headsep}{20pt}
|
|
\setlength{\textheight}{680pt}
|
|
\pagestyle{fancy}
|
|
\fancyhf{}
|
|
\fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - ProVerif}
|
|
\fancyhead[C]{}
|
|
\fancyhead[R]{Group \groupnumber}
|
|
\renewcommand{\headrulewidth}{0.4pt}
|
|
\fancyfoot[C]{\thepage}
|
|
|
|
|
|
\begin{document}
|
|
\thispagestyle{empty}
|
|
\noindent\framebox[\linewidth]{%
|
|
\begin{minipage}{\linewidth}%
|
|
\hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2021)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\
|
|
|
|
\begin{center}
|
|
{\bf\Large Project \projnumber~-- \Title}
|
|
\end{center}
|
|
|
|
\vspace*{5pt}\hspace*{5pt} \hfill TU Wien \hspace*{5pt}
|
|
\end{minipage}%
|
|
}
|
|
\vspace{0.5cm}
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
|
|
\section*{Group \groupnumber}
|
|
Our group consists of the following members:
|
|
\begin{center}
|
|
\textbf{\name}
|
|
|
|
\matriculation
|
|
\end{center}
|
|
|
|
\section{Small-step semantics}
|
|
|
|
\textit{Notes on semantics. Not mandatory.}
|
|
|
|
\section{Termination}
|
|
|
|
\paragraph{Explanation of the used measure}
|
|
|
|
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}
|
|
|
|
|
|
|
|
\paragraph{Explanation on used equalities}
|
|
%TODO
|
|
|
|
\section{Uniqueness of call stacks}
|
|
|
|
\paragraph{Paper proofs}
|
|
%TODO
|
|
|
|
\paragraph{Explanation on lemma \texttt{order\_ineq}}
|
|
%TODO
|
|
|
|
\section{Exception Propagation}
|
|
|
|
\paragraph{Paper proof}
|
|
%TODO
|
|
|
|
\paragraph{Explanation on alternative formulations}
|
|
%TODO
|
|
|
|
\end{document}
|
|
|