File renaming

1 files changed, 280 insertions, 0 deletions

diff --git a/tfm.tex b/tfm.tex
new file mode 100755
index 0000000..4840bdc
--- /dev/null
+++ b/tfm.tex
@@ -0,0 +1,280 @@
+\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}
+
+
+
+\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}