diff options
Diffstat (limited to 'tfm.tex')
| -rw-r--r-- | tfm.tex | 33 |
1 files changed, 19 insertions, 14 deletions
@@ -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} |