path: root/memoria.tex

\documentclass[12pt,a4paper,parskip=full]{scrreprt}
\usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry}

% \usepackage[spanish]{babel}
\usepackage[utf8]{inputenc} \usepackage{url}
\usepackage{graphicx} \usepackage{cite} \usepackage{amsmath}
\usepackage{mathtools} \usepackage{listings} \usepackage{syntax}
% \usepackage[compact,small]{titlesec}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage[backref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref}
\usepackage{perpage} \usepackage{subcaption}

\usepackage{tikz}
% \usepackage{minted}

\usepackage{float}
\floatstyle{boxed}
\newfloat{code}{th}{los}[chapter]
\floatname{code}{Code listing}

\usetikzlibrary{shapes,arrows}

\hypersetup{pageanchor=false}


\input{defs}
\input{portada/defs}

\MakePerPage{footnote}

\def\emptypage{\newpage\thispagestyle{empty}\mbox{}}

\begin{document}
\input{portada/portada}

\pagenumbering{roman}


\emptypage
\chapter*{Resumen}

La sociedad depende hoy más que nunca de la tecnología, pero la inversión en
seguridad es escasa y los sistemas informáticos siguen estando muy lejos de ser
seguros. La criptografía es una de las piedras angulares de la seguridad en este
ámbito, por lo que recientemente se ha dedicado una cantidad considerable de
recursos al desarrollo de herramientas que ayuden en la evaluación y mejora de
los algoritmos criptográficos. EasyCrypt es uno de estos sistemas, desarrollado
recientemente en el Instituto IMDEA Software en respuesta a la creciente
necesidad de disponer de herramientas fiables de verificación formal de
criptografía.

(TODO: En este documento se explicará cripto y reescritura de términos para bla
bla)

\chapter*{Abstract}

Today, society depends more than ever on technology, but the investment in
security is still scarce and using computer systems are still far from safe to
use. Cryptography is one of the cornerstones of security, so there has been a
considerable amount of effort devoted recently to the development of tools
oriented to the evaluation and improvement of cryptographic algorithms. One of
these tools is EasyCrypt, developed recently at IMDEA Software Institute in
response to the increasing need of reliable formal verification tools for
cryptography.

(TODO: In this document we will see crypto and term rewriting theory in order to
understand EasyCrypt and implement bla bla bla)

\emptypage
\tableofcontents

%% Content begins here
%
%% Level    | Spaces before | '%'s after
%  ---------+---------------+-----------
%  part     | 5             | until EOL
%  chapter  | 4             | 10
%  section  | 3             | 2
%  subs.    | 2             |
%  subsubs. | 1             |




\emptypage
\chapter{INTRODUCTION} %%%%%%%%%%

\pagenumbering{arabic}
\setcounter{page}{1}



\section{Problem} %%



\section{Contributions} %%

\begin{itemize}
\item Reference implementations of various rewriting engines
\item Improvement of EasyCrypt's one
\end{itemize}





\part{STATE OF THE ART} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\chapter{CRYPTOGRAPHY} %%%%%%%%%%

(TODO: Intro to crypto)



\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
cryptography, as they will be useful to understand the next sections on
sequences of games (TODO: ref).

\textbf{Asymmetric cryptography} (also called \textbf{Public Key cryptography}),
refers to cryptographic algorithms that make use of two different keys, $pk$
(public key) and $sk$ (secret key). There must be some mathematical relationship
that allows a specific pair of keys to perform dual operations, e.g., $pk$ to
encrypt and $sk$ to decrypt, $pk$ to verify a signature and $sk$ to create it,
and so on. A pair of (public, secret) keys can be generated using a procedure
called \textbf{key generation} ($\KG$).

The encryption ($\Enc$) and decryption ($\Dec$) functions work in the
following way:

$$\Enc(pk,M) = C$$
$$\Dec(sk,C) = M$$

That is, a message ($M$) can be encrypted using a public key to obtain a
ciphertext ($C$).

\section{Sequences of games} %%



\section{Verification: EasyCrypt} %%


\subsection{Specification languages}

\subsubsection{Expressions}

\subsubsection{Probabilistic expressions}

\subsubsection{pWhile language}


\subsection{Proof languages}

\subsubsection{Judgments}

\subsubsection{Tactics}




\chapter{TERM REWRITING} %%%%%%%%%%



\section{Term Rewriting Systems/Theory} %%



\section{Lambda Calculus} %%


\subsection{Extensions}

\subsubsection{Case expressions}

\subsubsection{Fixpoints}


\subsection{Reduction rules}

http://adam.chlipala.net/cpdt/html/Equality.html

\begin{itemize}
\item Alpha reduction
\item Beta reduction
\item ...
\end{itemize}



\section{Evaluation Strategies} %%



\section{Abstract Machines} %%


\subsection{Krivine Machine}

\cite{Krivine07}


\subsection{ZAM}

\cite{GregoireLeroy02}



\part{IMPLEMENTATION} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\chapter{KRIVINE MACHINE} %%%%%%%%%%

- Outside EasyCrypt: weak symbolic with fixpts and cases
- Inside EasyCrypt: bla bla






\chapter{ZAM} %%%%%%%%%%




\chapter{REDUCTION IN EASYCRYPT} %%%%%%%%%%



\section{Architecture overview} %%





\part{EPILOGUE} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\chapter{CONCLUSIONS} %%%%%%%%%%




\chapter{FUTURE WORK} %%%%%%%%%%




\chapter{ANNEX} %%%%%%%%%%



\section{Krivine Machine source code} %%



\section{ZAM source code} %%


\pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}

\end{document}