zenon/formal-methods-fstar
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Finish report

Browse Source
This commit is contained in:
Tobias Eidelpes 2021-06-03 17:28:08 +02:00
parent f042ef4a8d
commit 809a33cafc
1 changed files with 49 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
report/report.tex
View File

@ -23,7 +23,7 @@
\setlength{\textheight}{680pt} \setlength{\textheight}{680pt}
\pagestyle{fancy} \pagestyle{fancy}
\fancyhf{} \fancyhf{}
\fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - ProVerif} \fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - \fstar}
\fancyhead[C]{} \fancyhead[C]{}
\fancyhead[R]{Group \groupnumber} \fancyhead[R]{Group \groupnumber}
\renewcommand{\headrulewidth}{0.4pt} \renewcommand{\headrulewidth}{0.4pt}
@ -116,7 +116,7 @@ It is allowed to reduce \texttt{step\_simp te cs} to \texttt{cs}, because
\texttt{cs} is already final. \texttt{cs} is already final.
Now it is possible to prove the lemma \texttt{progress}: \texttt{cs == Now it is possible to prove the lemma \texttt{progress}: \texttt{cs ==
step\_simp te cs} $\rightarrow$ \texttt{isFinal cs}. Since, \texttt{step\_simp} step\_simp te cs} $\rightarrow$ \texttt{isFinal cs}. Since \texttt{step\_simp}
has the same value as the \texttt{step} function, when the outcome is has the same value as the \texttt{step} function, when the outcome is
\texttt{Next}, the call stack is different from \texttt{cs}. This means that the \texttt{Next}, the call stack is different from \texttt{cs}. This means that the
left side of the lemma does not hold and therefore the right side does not have left side of the lemma does not hold and therefore the right side does not have
@ -135,17 +135,59 @@ equality and therefore propositional equality is needed.
\section{Uniqueness of call stacks} \section{Uniqueness of call stacks}
\paragraph{Paper proofs} \paragraph{Paper proofs}
%TODO
\paragraph{Explanation on lemma \texttt{order\_ineq}} Note: The previously defined measure is written as \texttt{|cs|}, where
\texttt{cs} is a call stack.
To prove \texttt{order\_decreases} it needs to be shown that from \texttt{nsteps
n te cs == cs'} and $n > 0$ follows \texttt{|cs'| << |cs|} for all
$n\in\mathbb{N}$. The proof is by induction on \texttt{n}. For \texttt{n = 1},
\texttt{nsteps 1 te cs} is equal to \texttt{step\_simp te cs}. Similarly to
Exercise 2.2 it follows that the hypothesis holds, because \texttt{cs} is not a
final state. After that, the induction step is \texttt{nsteps (n+1) te cs ==
cs'}, which can be rewritten as \texttt{nsteps n te (step\_simp te cs) == cs'}
(definition of \texttt{nsteps}). With the reasoning from the base case where
\texttt{n = 1}, it follows that \texttt{|step\_simp te cs| << |cs|}. Now there
are two cases: either the call stack \texttt{|step\_simp te cs} is final or not.
For the first case, the lemma \texttt{nsteps\_stop} can be used to derive
\texttt{step\_simp te cs == cs'} from \texttt{nsteps n te (step\_simp te cs) ==
cs'}, where \texttt{|step\_simp te cs| << |cs|} holds. For the second case, we
simply take the induction hypothesis to conclude that the induction holds.
Taking the previous proof, for \texttt{callstacks\_unique} it is evident that
\texttt{|cs'| << |cs|} holds. It follows that \texttt{cs'} $\neq$ \texttt{cs} by
proof of contradiction: Assuming that \texttt{cs' == cs} and \texttt{|cs'| <<
|cs|} is true, it would require that the top constant in both lists
\texttt{LexTop} satisfies \texttt{LexTop << LexTop}. Since this is impossible,
it contradicts the assumption and therefore it follows that \texttt{cs'} $\neq$
\texttt{cs}.
\section{Exception Propagation} \section{Exception Propagation}
\paragraph{Paper proof} \paragraph{Paper proof}
%TODO
\paragraph{Explanation on alternative formulations} Proof by induction:
%TODO
\begin{verbatim}
length ps = 0
nsteps (2 * (length [])) te (Ter ExcState []) == (Ter ExcState [])
nsteps 0 te (Ter ExcState []) == (Ter ExcState [])
(Ter ExcState []) == (Ter ExcState [])
\end{verbatim}
\begin{verbatim}
length ps to (length ps) + 1
nsteps (2 * (length ps)) te (Ter ExcState ps) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 1) te (step simp (Ter ExcState ps)) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 1) te (Exec (apply returneffects ts s)::ps’) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 1) te (Exec s’::ps’) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 2) te (step simp (Exec s’::ps’)) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 2) te (Ter (ExcState ps’)) == (Ter ExcState [])
nsteps (2 * ((length ps) - 1)) te (Ter (ExcState ps’)) == (Ter ExcState [])
nsteps (2 * (length ps’)) te (Ter (ExcState ps’)) == (Ter ExcState [])
\end{verbatim}
\end{document} \end{document}