path: root/tfm.tex

\documentclass[12pt,a4paper,parskip=full]{scrreprt}
\usepackage{scrhack} % http://tex.stackexchange.com/questions/51867/koma-warning-about-toc

\usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry}

% \usepackage[spanish]{babel}
\usepackage{fontspec} \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{ec-defs}
\input{front/front-init}

\MakePerPage{footnote}

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

\begin{document}
\input{front/front-body}

\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}

In the last years, society is becoming ever more dependent on computer
systems. People manage their bank accounts via web, are constantly in touch with
their contacts thanks to instant messaging applications, and have huge amounts
of personal data stored in the \textit{cloud}. All this personal information
flowing through computer networks need to be protected by correctly implementing
adequate security measures regarding both information transmission and
storage. Building strong security systems is not an easy task, because there are
lots of parts that must be studied in order to assure the system as a whole
behaves as intended.

One of the most fundamental tools used to build security computer systems is
\textbf{cryptography}. Due to its heavy mathematical roots, cryptography today
is a mature science that, when correctly implemented, can provide strong
security guarantees to the systems using it. In fact, it is usually the case
that cryptography is one of the \textit{most secure} parts of the system, and a
lot of other concerns should be taken care of, such as underlying operating
systems, security policies, or the human factor.

At this point, one could be tempted of just ``using strong, NIST-approved
cryptography'' and focusing on the security of other parts of the system.  The
reality is that correctly implementing cryptography is a pretty difficult task
on its own, mainly because there is not a one-size-fits-all construction that
covers all security requirements. Every cryptographic primitive has its own
security assumptions and guarantees, so one must be exceptionally cautious when
combining them in order to build larger systems. For example, a given
cryptographic construction could be well suited for a concrete scenario and
totally useless in some others. In turn, this situation can produce a false
sense of security, potentially worse that not having any security at all.

In order to have the best guarantee that some cryptographic construction meets
its security requirements, we can use use formal methods to prove that the
requirements follow from the assumptions (scenario).

(TODO: maybe a sub-section on sequences of games, Hoare logic, etc.)



\section{Problem} %%

(TODO: Need of Computer-assisted proofs)


\subsection{EasyCrypt}

(TODO: What is EasyCrypt (Coq-like, screens, etc))



\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} %%

While mathematical proofs greatly enhance the confidence we have in that a given
cryptosystem behaves as expected, with the recent increase in complexity it has
become more and more difficult to write and verify the proofs by hand, to the
point of being practically non-viable. In 2004 \cite{Shoup04}, Victor Shoup
introduced the concept of \textbf{sequences of games} as a method of taming the
complexity of cryptography related proofs. A game is like a program written in a
well-defined, probabilistic programming language, and a sequence of games is the
result of applying transformations over the initial one.



\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}