Ready to write

1 files changed, 211 insertions, 24 deletions

diff --git a/memoria.tex b/memoria.tex
index 3d194e2..98c2b69 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -7,7 +7,7 @@
 \usepackage{mathtools} \usepackage{listings} \usepackage{syntax}
 % \usepackage[compact,small]{titlesec}
 \usepackage[usenames,dvipsnames]{xcolor}
-\usepackage[pagebackref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref}
+\usepackage[backref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref}
 \usepackage{perpage} \usepackage{subcaption}
 
 \usepackage{tikz}
@@ -23,7 +23,7 @@
 \hypersetup{pageanchor=false}
 
 
-% \input{defs}
+\input{defs}
 \input{portada/defs}
 
 \MakePerPage{footnote}
@@ -39,51 +39,238 @@
 \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}
-\label{cha:introduction}
+\chapter{INTRODUCTION} %%%%%%%%%%
+
 \pagenumbering{arabic}
 \setcounter{page}{1}
 
-EasyCrypt\footnote{\url{https://www.easycrypt.info/}} is a crypto framework...
 
 
+\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} %%
+
 
-- EasyCrypt
-- Term rewriting
- - Some theory (books?)
- - Extensions of lambda calculus
 
-\chapter{STATE OF THE ART}
+\section{Lambda Calculus} %%
 
-- Reduction things
-- Abstract machines
- - Krivine
- - ZAM\cite{Gregoire-Leroy-02}
 
-\chapter{IMPLEMENTATION}
+\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} %%%%%%%%%%
+
 
-\chapter{CONTRIBUTIONS}
-\label{cha:contribuciones}
 
-- EasyCrypt rules
+\section{Krivine Machine source code} %%
 
-\chapter{CONCLUSIONS}
-\label{cha:result-y-concl}
 
-- Writing real things.
-- Hey arst
 
-\chapter{ANNEX}
-\label{cha:anexos}
+\section{ZAM source code} %%
 
 
 \pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}