From 60f9d9d8f951bdee1c5df0398c0f90ad94825508 Mon Sep 17 00:00:00 2001
From: Guillermo Ramos
Date: Thu, 23 Jul 2015 02:48:46 +0200
Subject: 22/07/15

---
 tfm.tex | 33 +++++++++++++++++++--------------
 1 file changed, 19 insertions(+), 14 deletions(-)

(limited to 'tfm.tex')

diff --git a/tfm.tex b/tfm.tex
index 0a0ce0a..49a769e 100644
--- a/tfm.tex
+++ b/tfm.tex
@@ -65,6 +65,10 @@ recientemente en el Instituto IMDEA Software en respuesta a la creciente
 necesidad de disponer de herramientas fiables de verificación formal de
 criptografía.
 
+En este trabajo se abordará la implementación de una mejora en el procesador de
+lenguaje de EasyCrypt, sustituyéndolo por una máquina abstracta derivada de la
+ZAM (lenguaje OCaml). 
+
 (TODO: crypto, reescritura de términos, máquinas abstractas, mejoras a EasyCrypt)
 
 \chapter*{Abstract}
@@ -246,12 +250,6 @@ what can be improved)
 
 
 
-\section{Symmetric Cryptography} %%
-
-(TODO: not sure if this section is really needed)
-
-
-
 \section{Asymmetric Cryptography} %%
 
 Here we will introduce some of the most fundamental concepts in asymmetric
@@ -570,7 +568,7 @@ that can be applied over terms in order to perform the computation:
 
 \subsection{Reduction rules}
 
-Arguably the most important rule in Lambda Calculus is the \textbf{beta
+The most prominent reduction rule in Lambda Calculus is the \textbf{beta
   reduction}, or $\beta$-reduction. This rule represents function evaluation,
 and can be outlined in the following way:
 
@@ -856,7 +854,7 @@ is evaluating ($C$), an auxiliar \textbf{stack} ($S$) and the current
 \textbf{environment} ($E$). The code is just a Lambda expression, the stack is
 where the machine will store \textbf{closures} consisting of non-evaluated code
 together with its environment at the time the closure was created, and an
-environment associates variables (de Bruijn indices) to closures. 
+environment associates variables (de Bruijn indices) to closures.
 
 The typical description of the Krivine Machine \cite{Douence07} is given by the
 following set of rules:
@@ -934,12 +932,12 @@ example $\lambda$-terms:
 
 \begin{code}
   \begin{minted}[fontsize=\scriptsize]{ocaml}
-let m1 =      (* (λx.((λy.y) x)) *)
+let ex_m1 =      (* (λx.((λy.y) x)) *)
   let x = symbol "x" in
   let y = symbol "y" in
   Abs (x, App (Abs (y, Var y), Var x))
 
-let m2 =      (* (((λx.(λy.(y x))) (λz.z)) (λy.y)) *)
+let ex_m2 =      (* (((λx.(λy.(y x))) (λz.z)) (λy.y)) *)
   let x = symbol "x" in
   let y = symbol "y" in
   let z = symbol "z" in
@@ -966,7 +964,7 @@ The results:
 
 \begin{code}
 \begin{verbatim}
-ocaml> List.iter dbi_and_red [m1; m2];;
+ocaml> List.iter dbi_and_red [ex_m1; ex_m2];;
 
 # Lambda term:
     (λx.((λy.y) x))
@@ -989,7 +987,7 @@ variables:
 
 \begin{code}
 \begin{verbatim}
-ocaml> List.iter dbi_and_red [m1; m2];;
+ocaml> List.iter dbi_and_red [ex_m1; ex_m2];;
 
 # Lambda term:
     (λ.((λ.0) 0))
@@ -1150,7 +1148,7 @@ let peano_of_int ?(base=Constr (z, [])) n = peano_add n base
 The second extension we are going to implement in our Krivine Machine is the
 ability to support fixpoints, that is, limited recursion. To prevent infinite
 reductions, every fixpoint must be defined over a constructor, in a way that
-TODO.
+(TODO: this is ZAM!).
 
 Again, we extend the data structures of the Lambda Calculus. As the extension to
 DBILambda follows trivially, we will omit it here:
@@ -1278,6 +1276,11 @@ its argument, so the whole term is a ``by 3'' multiplier.
 
 \chapter{CONCLUSIONS} %%%%%%%%%%
 
+In this work we began by exposing the need to verify cryptographic protocols and
+what is the role that the EasyCrypt framework plays in the field. After
+some background in cryptography and analysing the inner working of
+EasyCrypt.
+
 \begin{itemize}
 \item Brief wrapping of importance of verified crypto today
 \item Survey of available reduction machineries, differences between them
@@ -1307,11 +1310,13 @@ its argument, so the whole term is a ``by 3'' multiplier.
 \section{Krivine Machine source code} %%
 \label{sec:kriv-mach-source}
 
-\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml}
+% TODO: UNCOMMENT
+%\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml}
 
 %\newpage
 \section{ZAM source code} %%
 
+% TODO: UNCOMMENT
 %\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/zam.ml}
 
 \pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}
-- 
cgit v1.2.3

