Commit inicial: Introducción

6 files changed, 829 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..1d4c2d3
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,10 @@
+auto
+*.aux
+*.bbl
+*.blg
+*.brf
+*.dvi
+*.log
+*.lol
+*.out
+*.log
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..9c825ab
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,14 @@
+all: bib tex
+
+tex:
+	pdflatex memoria
+	pdflatex memoria
+
+bib:
+	pdflatex memoria
+	bibtex memoria
+
+clean:
+	rm -rf *.aux *.bbl *.blg *.log
+
+.PHONY : tex bib clean
diff --git a/bib.bib b/bib.bib
new file mode 100755
index 0000000..4ae6ee4
--- /dev/null
+++ b/bib.bib
@@ -0,0 +1,75 @@
+@article{Shoup04,
+  author    = {Victor Shoup},
+  title     = {Sequences of games: a tool for taming complexity in security
+               proofs},
+  journal   = {IACR Cryptology ePrint Archive},
+  volume    = 2004,
+  year      = 2004,
+  pages     = 332,
+  ee        = {http://eprint.iacr.org/2004/332},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@inproceedings{BartheGHB11,
+  author    = {Gilles Barthe and
+               Benjamin Gr{\'e}goire and
+               Sylvain Heraud and
+               Santiago Zanella B{\'e}guelin},
+  title     = {Computer-Aided Security Proofs for the Working Cryptographer},
+  booktitle = {CRYPTO},
+  year      = {2011},
+  pages     = {71-90},
+  ee        = {http://dx.doi.org/10.1007/978-3-642-22792-9_5},
+  crossref  = {DBLP:conf/crypto/2011},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@proceedings{DBLP:conf/crypto/2011,
+  editor    = {Phillip Rogaway},
+  title     = {Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology
+               Conference, Santa Barbara, CA, USA, August 14-18, 2011.
+               Proceedings},
+  booktitle = {CRYPTO},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {6841},
+  year      = {2011},
+  isbn      = {978-3-642-22791-2},
+  ee        = {http://dx.doi.org/10.1007/978-3-642-22792-9},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@inproceedings{BartheGB09,
+  author    = {Gilles Barthe and
+               Benjamin Gr{\'e}goire and
+               Santiago Zanella B{\'e}guelin},
+  title     = {Formal certification of code-based cryptographic proofs},
+  booktitle = {POPL},
+  year      = {2009},
+  pages     = {90-101},
+  ee        = {http://doi.acm.org/10.1145/1480881.1480894},
+  crossref  = {DBLP:conf/popl/2009},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@proceedings{DBLP:conf/popl/2009,
+  editor    = {Zhong Shao and
+               Benjamin C. Pierce},
+  title     = {Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on
+               Principles of Programming Languages, POPL 2009, Savannah,
+               GA, USA, January 21-23, 2009},
+  booktitle = {POPL},
+  publisher = {ACM},
+  year      = {2009},
+  isbn      = {978-1-60558-379-2},
+  ee        = {http://dl.acm.org/citation.cfm?id=1480881},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@article{GoldwasserM84,
+  author    = {Shafi Goldwasser and
+               Silvio Micali},
+  title     = {Probabilistic Encryption},
+  journal   = {J. Comput. Syst. Sci.},
+  volume    = {28},
+  number    = {2},
+  year      = {1984},
+  pages     = {270-299},
+  ee        = {http://dx.doi.org/10.1016/0022-0000(84)90070-9},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
diff --git a/defs.tex b/defs.tex
new file mode 100755
index 0000000..7a9c73d
--- /dev/null
+++ b/defs.tex
@@ -0,0 +1,340 @@
+% Source: EasyCrypt manual (https://www.easycrypt.info)
+
+% !TeX root = easycrypt.tex
+%% Names
+% Tools
+ \newcommand{\EasyCrypt}{\textsf{EasyCrypt}\xspace}
+ \newcommand{\CertiCrypt}{\textsf{CertiCrypt}\xspace}
+ \newcommand{\CertiPriv}{\textsf{CertiPriv}\xspace}
+ \newcommand{\SsReflect}{\textsf{SsReflect}\xspace}
+ \newcommand{\Coq}{\textsf{Coq}\xspace}
+ \newcommand{\WhyThree}{\textsf{Why3}\xspace}
+
+% Languages and Logics
+ \newcommand{\pWHILE}{\textsf{p}\textsc{While}\xspace}
+ \newcommand{\pRHL}{\textsf{pRHL}\xspace}
+
+% Version numbers
+ \newcommand{\ECversion}{0.$\beta$\xspace}
+
+%% Misc
+\newcommand{\DONE}{}% {{\color{red}DONE}}
+\newcommand{\Example}{\paragraph*{Example}}
+\newcommand{\Syntax}{\paragraph*{Syntax}}
+\newcommand{\Description}{\paragraph*{Description}}
+\setcounter{secnumdepth}{3}
+\renewcommand{\thesubsubsection}{\arabic{chapter}.\arabic{section}.\arabic{subsection}.\arabic{subsubsection}}
+\newbox\minicodebox
+\newenvironment{minicode}[1]{%
+\minipage[t]{#1\linewidth} %
+\centering %
+\verbatim %
+}{%
+\endverbatim %
+\endminipage% 
+}
+
+
+\newcounter{alarmcounter}
+\setcounter{alarmcounter}{1}
+\newcommand{\alarm}[1]
+            {\begingroup
+              \def\thefootnote{{\normalsize\color{red}(\arabic{footnote})}}
+              \footnote{\textsf{\textbf{{\color{red}\sc \bf ALARM:}
+                  #1}}}\endgroup}
+
+
+\newcommand{\infr}[2]{
+{\renewcommand{\arraystretch}{1.1}
+\begin{array}{c}
+{#1}\\
+\hline
+{#2}
+\end{array}}}
+
+%% Indexing
+\newcommand{\define}[2][]{\emph{#2}\index{easycrypt}{\ifx&#1&#2\else#1\fi}}
+
+%% Cross-referencing
+% \providecommand{\eqref}[1]{\textup{(\ref{#1})}}
+% \providecommand{\eqdef}{\raisebox{-.2ex}[.2ex]{$\stackrel{\textrm{\tiny def}}{~=~}$}}
+
+%% IDK
+\newcommand{\rname}[1]{[\textsc{#1}]}
+\newcommand{\result}{\mathsf{res}}
+
+%% Security properties and schemes
+\newcommand{\INDCPA}{\textsf{IND-CPA}\xspace}
+\newcommand{\INDCCAone}{\textsf{IND-CCA1}\xspace}
+\newcommand{\INDCCA}{\textsf{IND-CCA}\xspace}
+\newcommand{\EFCMA}{\textsf{EF-CMA}\xspace}
+\newcommand{\LCDH}{\ensuremath{\mathsf{LCDH}}\xspace}
+\newcommand{\CDH}{\textsf{CDH}\xspace}
+\newcommand{\DDH}{\textsf{DDH}\xspace}
+\newcommand{\ElGamal}{\textsf{ElGamal}\xspace}
+\newcommand{\HElGamal}{\textsf{HElGamal}\xspace}
+\newcommand{\RSA}{\textsf{RSA}\xspace}
+\newcommand{\OAEP}{\textsf{OAEP}\xspace}
+\newcommand{\FDH}{\textsf{FDH}\xspace}
+\newcommand{\HMAC}{\textsf{HMAC}\xspace}
+\newcommand{\CS}{\textsf{CS}\xspace}
+\newcommand{\Skein}{\textsf{Skein}\xspace}
+\newcommand{\TCR}{\textsf{TCR}\xspace}
+
+\newcommand{\KG}{\mathcal{KG}}
+\newcommand{\Enc}{\mathcal{E}}
+\newcommand{\Dec}{\mathcal{D}}
+
+%% Complexity and termination
+\newcommand{\lossless}{\mathsf{lossless}}
+
+%% Sets
+\newcommand{\zeroone}{[0,1]}
+\newcommand{\bit}{\{0,1\}}
+\newcommand{\bitstring}[1]{\ensuremath{\bit^{#1}}}
+\newcommand{\bool}{\mathbb{B}}
+\newcommand{\nat}{\mathbb{N}}
+\newcommand{\real}{\mathbb{R}}
+\newcommand{\option}[1]{#1_\bot}
+
+%% Mathematics
+\newcommand{\conv}[1][]{\mathrel{\leftrightarrow^*_{#1}}}
+\renewcommand{\Pr}[2]{\mathrm{Pr}\left[#1 : #2\right]}
+\newcommand{\Prm}[3]{\mathrm{Pr}\left[#1,#3 : #2\right]}
+\newcommand{\labs}{\left\lvert}
+\newcommand{\rabs}{\right\rvert}
+\newcommand{\charfun}{\mathds{1}}
+
+%% Distribution monad
+\newcommand{\supp}{\mathsf{support}}
+\newcommand{\range}[2]{\mathsf{range}~{#1}~{#2}}
+
+%% Semantics 
+
+% \newcommand{\sem}[1]{\llbracket #1 \rrbracket}
+\newcommand{\subst}[2]{\left[{}^{#2}/{}_{#1}\right]}
+\newcommand{\fv}{\mathsf{fv}}
+\newcommand{\modifies}{\mathsf{mod}}
+\newcommand{\glob}{\mathsf{glob}}
+\newcommand{\Env}{\mathcal{E}}
+
+%% Well-formed adversaries
+%% Program Judgements 
+\newcommand{\Hoare}[3]{\left[{#1}:{#2}\Longrightarrow{#3}\right]}
+\newcommand{\Equiv}[4]{\left[{#1}\sim{#2}:{#3}\Longrightarrow{#4}\right]}
+\newcommand{\bdHoareS}[5]{{\Hoare{#1}{#2}{#3}}\,{#4}\,{#5}}
+\newcommand{\HoareLe}[4]{\bdHoareS{#1}{#2}{#3}{\leq}{#4}}
+\newcommand{\HoareEq}[4]{\bdHoareS{#1}{#2}{#3}{=}{#4}}
+\newcommand{\HoareGe}[4]{\bdHoareS{#1}{#2}{#3}{\geq}{#4}}
+
+
+% \newcommand{\Equiv}[4]{\models {#1} \sim {#2} : {#3} \Longrightarrow {#4}}
+% \newcommand{\AEquiv}[6]{\models {#2} \sim_{#5,#6} {#3} : {#1} \Longrightarrow {#4}}
+% \newcommand{\JAEquiv}[6]{{#2} \sim_{#5,#6} {#3} : {#1} \Longrightarrow {#4}}
+% \newcommand{\EquivMem}[2]{\models {#1} \equiv {#2}}
+% \newcommand{\EqObs}[4]{\models {#1} \simeq^{#3}_{#4} {#2}}
+% \newcommand{\AEqObs}[5]{\models {#1} \simeq^{#3}_{{#4}} {#2} \preceq {#5}} 
+% \newcommand{\ACEqObs}[7]
+%         {\AEqObs{\left[ #1 \right]_{#6}}{\left[ #2 \right]_{#7}}{#3}{#4}{#5}}
+% \newcommand{\Triple}[3]{\sem{#2} {#3} \preceq {#1}}
+% \newcommand{\DTriple}[3]{\sem{#2} {#3} \succeq {#1}}
+% \newcommand{\dequiv}[3]{{#1} \simeq_{#3} {#2}}
+% \newcommand{\fequiv}[3]{{#1} =_{#3} {#2}}
+% \newcommand{\Pre}{\Psi}
+% \newcommand{\Post}{\Phi}
+% \newcommand{\Inv}{\Phi}
+\newcommand{\side}[1]{\langle #1 \rangle}
+\newcommand{\sidel}{\side{1}}
+\newcommand{\sider}{\side{2}}
+% \newcommand{\eqobsin}{\mathsf{eqobs\_in}}
+% \newcommand{\eqobsout}{\mathsf{eqobs\_out}}
+\newcommand{\pre}{\Psi}
+\newcommand{\post}{\Phi}
+\newcommand{\bound}{\delta}
+\newcommand{\ECinsupp}[2]{\mathec{Distr.in_supp}\,{#1}\,{#2}}
+\newcommand{\insupp}[2]{{#1}\in\mathec{supp}\,{#2}}
+%% Variables
+
+% \newcommand{\LH}{\gl{L}_H}
+% \newcommand{\LD}{\gl{L}_\Dec}
+% \newcommand{\cdef}{\gl{\gamma_\mathsf{def}}}
+\newcommand{\var}[1]{\ensuremath{\mathit{#1}} \xspace}
+
+%% Constants and operators
+% TODO: Update!
+\newcommand{\true}{\mathsf{true}}
+\newcommand{\false}{\mathsf{false}}
+\newcommand{\nil}{\mathsf{nil}}
+\newcommand{\hd}{\mathsf{hd}}
+\newcommand{\tl}{\mathsf{tl}}
+\newcommand{\app}{\mathbin{+\mkern-7mu+}}
+\newcommand{\concat}{\parallel}
+\newcommand{\xor}{\oplus}
+\newcommand{\msb}[2]{[#1]^{#2}}
+\newcommand{\lsb}[2]{[#1]_{#2}}
+\newcommand{\dom}{\mathsf{dom}}
+\newcommand{\ran}{\mathsf{ran}}
+\newcommand{\fst}{\mathsf{fst}}
+\newcommand{\snd}{\mathsf{snd}}
+\newcommand{\some}[1]{#1}
+\newcommand{\none}{\bot}
+
+\newcommand{\Int}{\mathsf{Int}}
+\newcommand{\tint}{\mathsf{int}}
+
+\newcommand{\tbool}{\mathsf{bool}}
+
+%% Language
+% TODO: Update!
+\newcommand{\Skip}{\mathsf{skip}}
+\newcommand{\Seq}[2]{#1;\ #2}
+\newcommand{\Ass}[2]{#1 \leftarrow #2}
+\newcommand{\Rand}[2]{#1 \stackrel{\raisebox{-.25ex}[.25ex]%
+{\tiny $\mathdollar$}}{\raisebox{-.2ex}[.2ex]{$\leftarrow$}} #2}
+\newcommand{\Randi}[2]{\Rand{#1}{[0..#2]}}
+\newcommand{\Randb}[1]{\Rand{#1}{\bit}}
+\newcommand{\Randbs}[2]{\Rand{#1}{\bitstring{#2}}}
+\newcommand{\Cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}
+\newcommand{\Condt}[2]{\mathsf{if}\ #1\ \mathsf{then}\ #2}
+\newcommand{\Else}{\mathsf{else}\ }
+\newcommand{\Elsif}{\mathsf{elsif}\ }
+\newcommand{\nWhile}[3]{\mathsf{while}_{#1}\ #2\ \mathsf{do}\ #3}
+\newcommand{\While}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2}
+\newcommand{\Call}[3]{#1 \leftarrow #2\mathsf{(}#3\mathsf{)}}
+\newcommand{\Return}{\mathsf{return}}
+% \newcommand{\Assert}[1]{\mathsf{assert}~#1}
+
+%% Tactics
+\newcommand{\tacname}{Error tacname}
+\newcommand{\vtacname}{Error tacname}
+\newcommand{\vararg}[1]{\ec{#1}}
+\newcommand{\cstarg}[1]{\ec{#1}}
+\newcommand{\typarg}[1]{\textit{#1}}
+\newcommand{\tacarg}[2]{(\vararg{#1}:\typarg{#2})}
+
+\newcommand{\addTacticIdx}[2]{\index{#1}{#2@\rawec{#2}}}
+
+\newcommand{\addTacticNoIdx}[2]{
+  \renewcommand{\tacname}{\rawec{#1}}
+  \renewcommand{\vtacname}{#1}
+  \subsubsection{#1}
+  \Syntax \ec{#1} #2
+  \Description}
+
+\newcommand{\addTacticPlain}[2]{
+  \renewcommand{\tacname}{\rawec{#1}}
+  \renewcommand{\vtacname}{#1}
+  \subsubsection{#1}
+  \Syntax {#2}
+  \Description}
+
+\newcommand{\addTactic}[3]{
+  \addTacticIdx{#1}{#2}
+  \addTacticNoIdx{#2}{#3}}
+
+%% Language definition
+\lstnewenvironment{easycrypt}[2][]%
+  {\lstset{language=easycrypt,caption={#2},#1}}%
+  {}
+
+\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline[language=easycrypt,#1]{#2}}
+\newcommand{\mathec}[1]{\mbox{\rawec{#1}}}
+\newcommand{\ec}[2][basicstyle=\normalsize\sffamily]{\lstinline[language=easycrypt,style=easycrypt-pretty,#1]{#2}}
+
+\newcommand{\ecimport}[4][]{\lstinputlisting[language=easycrypt,linerange=#4,caption=#2,#1]{#3}}
+
+\lstdefinelanguage{easycrypt}{
+  style=easycrypt-default,
+%  procnamekeys={op,pred,fun},
+%  procnamestyle={\sffamily\itshape},
+  keywordsprefix={'},
+  morekeywords=[1]{unit,bool,int,real,bitstring,array,list,matrix,word},
+  morekeywords=[2]{type,datatype,op,axiom,lemma,module,pred,const,declare},
+  morekeywords=[3]{var,fun},
+  morekeywords=[4]{while,if},
+  morekeywords=[5]{theory,end,clone,import,export,as,with,section},
+  morekeywords=[6]{forall,exists,lambda},
+  morekeywords=[7]{idtac,change,beta,iota,zeta,logic,delta,simplify,congr,generalize,
+                   pose,split,left,right,case,intros,cut,elim,apply,rewrite,elimT,subst,
+                   progress,trivial},
+  morekeywords=[8]{by,assumption,smt,reflexivity},
+  morekeywords=[9]{first,last,do,try},
+%  moredirectives={prover,print}, % Incomplete
+  morecomment=[n][\itshape]{(*}{*)},
+  morecomment=[n][\bfseries]{(**}{*)}
+}
+
+\lstdefinestyle{easycrypt-default}{
+  columns=fullflexible,
+  % captionpos=b,
+  frame=tb,
+  xleftmargin=.1\textwidth,
+  xrightmargin=.1\textwidth,
+  rangebeginprefix={(**\ begin\ },
+  rangeendprefix={(**\ end\ },
+  rangesuffix={\ *)},
+  includerangemarker=false,
+  basicstyle=\small\sffamily,
+  identifierstyle={},
+  keywordstyle=[1]{\itshape\color{OliveGreen}},
+  keywordstyle=[2]{\bfseries\color{Blue}},
+  keywordstyle=[3]{\bfseries},
+  keywordstyle=[4]{\bfseries},
+  keywordstyle=[5]{\bfseries\color{OliveGreen}},
+  keywordstyle=[6]{\itshape\color{Blue}},
+  keywordstyle=[7]{\color{Blue}},
+  keywordstyle=[8]{\color{Red}},
+  keywordstyle=[9]{\color{OliveGreen}},
+  literate={phi}{{$\!\phi\,$}}1
+           {phi1}{{$\!\phi_1$}}1
+           {phi2}{{$\!\phi_2$}}1
+           {phi3}{{$\!\phi_3$}}1
+           {phin}{{$\!\phi_n$}}1
+}
+
+\lstdefinestyle{easycrypt-pretty}{
+    basicstyle=\small\sffamily,
+    literate={:=}{{$\mathrel{\gets}$}}1
+              {<=}{{$\mathrel{\leq}$}}1
+              {>=}{{$\mathrel{\geq}$}}1
+              {<>}{{$\mathrel{\neq}$}}1
+              {=\$}{{$\stackrel{\$}{\gets}$}}1
+              {forall}{{$\forall$}}1
+              {exists}{{$\exists$}}1
+              {->}{{$\rightarrow\;$}}1
+              {<-}{{$\leftarrow\;$}}1
+              {<->}{{$\leftrightarrow\;$}}1
+              {<=>}{{$\Leftrightarrow\;$}}1
+              {=>}{{$\Rightarrow\;$}}1
+              {==>}{{$\Rrightarrow\;$}}1
+              {\/\\}{{$\wedge$}}1
+              {\\\/}{{$\vee$}}1
+              {.\[}{{[}}1
+              {''ora}{{$\mathrel{||}$}}1 %needed for correct display in index
+              {'a}{{\color{OliveGreen}$\alpha\,$}}1
+              {'b}{{\color{OliveGreen}$\beta\,$}}1
+              {'c}{{\color{OliveGreen}$\gamma\,$}}1
+              {'t}{{\color{OliveGreen}$\tau\,$}}1
+              {'x}{{\color{OliveGreen}$\chi\,$}}1
+              {lambda}{{$\lambda\,$}}1
+}
+
+%% Typesetting
+\newcommand{\titledbox}[4]{{\color{#1}\fbox{\begin{minipage}{#2}{\textbf{#3:} \color{black}#4}\end{minipage}}}}
+\newcommand{\warningbox}[1]{\titledbox{red}{.9\textwidth}{Warning}{#1}}
+\newcommand{\futurebox}[1]{\titledbox{blue}{.9\textwidth}{Future}{#1}}
+
+
+
+\newcommand{\NotDocumented}{
+  \begin{center}{\color{blue}\fbox{\begin{minipage}{120pt}{\centering
+            \textbf{Not yet documented}}
+        \end{minipage}}}\end{center}}
+\newcommand{\NotImplemented}{
+  \begin{center}{\color{blue}\fbox{\begin{minipage}{120pt}{\centering
+            \textbf{Not yet implemented}}
+        \end{minipage}}}\end{center}}
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "easycrypt"
+%%% End: 
\ No newline at end of file
diff --git a/memoria.pdf b/memoria.pdf
new file mode 100755
index 0000000..bfccbb7
--- /dev/null
+++ b/memoria.pdf
diff --git a/memoria.tex b/memoria.tex
new file mode 100755
index 0000000..0fab1a6
--- /dev/null
+++ b/memoria.tex
@@ -0,0 +1,390 @@
+% Preguntas:
+% - BNF?
+% - Numeración independiente Juego/Ejemplo/... en lstlisting
+
+\documentclass[12pt,a4paper]{article}
+
+\usepackage[spanish]{babel} \usepackage[utf8]{inputenc} \usepackage{url}
+\usepackage{parskip} \usepackage{graphicx} \usepackage{cite}
+\usepackage{amsmath} \usepackage{mathtools} \usepackage{listings}
+\usepackage{syntax}
+\usepackage[compact,small]{titlesec}\usepackage[usenames,dvipsnames]{xcolor}
+\usepackage[pagebackref,colorlinks=true,linkcolor=black,linktoc=all,citecolor=blue]{hyperref}
+
+\setlength\voffset{-1.2in} \setlength\hoffset{-0.7in} \setlength\topmargin{3cm}
+\setlength\textwidth{16cm} \setlength\headsep{0cm}
+
+\input{defs}
+
+\title{Trabajo de fin de Grado} \author{Guillermo Ramos Gutiérrez - r090050}
+\date{TODO}
+
+\begin{document}
+\maketitle
+\pagebreak
+
+\section{Introducción}
+
+Con el paso del tiempo, la sociedad está aumentando progresivamente su
+dependencia de los sistemas informáticos, tanto a nivel local como global
+(internet). La gente gestiona sus cuentas bancarias por internet, está
+permanentemente en contacto con sus conocidos a través de aplicaciones de
+mensajería instantánea y almacena en \textit{la nube} gran cantidad de material
+personal. Esta dependencia trae consigo la necesidad de tener unas ciertas
+garantías de seguridad (confidencialidad, disponibilidad, integridad) tanto a la
+hora de transmitir la información como de almacenarla. Construir un sistema de
+seguridad no es una tarea fácil, ya que a menudo consta de muchos componentes
+que han de ser examinados individualmente de forma rigurosa para poder afirmar
+que el conjunto es seguro.
+
+Uno de los componentes básicos de prácticamente cualquier sistema de seguridad
+es la criptografía. Su utilidad no se limita a impedir que una persona no
+autorizada con acceso a datos privados pueda entenderlos (cifrado), sino que
+también cubre otras necesidades como la de verificación de identidad
+(autenticación) o la de poder garantizar de que una información no ha sido
+alterada (integridad). Poniendo como ejemplo el caso de una persona accediendo
+via web a la página web de su banco para realizar una transferencia, la
+criptografía juega un papel central a la hora de garantizar la seguridad de la
+operación: un protocolo de transporte seguro empleará un esquema de criptografía
+asimétrica para garantizar al cliente que el servidor es quien dice ser, un
+algoritmo de cifrado para hacer imposible que cualquier intermediario pueda
+interceptar la comunicación, y un código de autenticación de mensaje para
+verificar que los datos no se modifican mientras están viajando.
+
+Por lo general, estas primitivas criptográficas basan su seguridad en la
+dificultad computacional que tiene resolver ciertos problemas. Por ejemplo, uno
+de los protocolos más utilizados para autenticar servidores, RSA, se basa en que
+un atacante que intente suplantar al servidor en cuestión tendrá antes que
+descomponer un número en dos factores primos, problema que se considera
+inabordable para números lo suficientemente grandes (con la capacidad
+computacional actual). Como resultado, normalmente no se habla en términos de
+seguridad absoluta, sino de seguridad \textbf{condicionada a la capacidad
+  computacional del atacante}.
+
+Para estar seguros de que los mecanismos criptográficos realmente cumplen con su
+cometido, es necesario someterlos a un proceso de verificación riguroso. El
+objetivo es poder razonar sobre ellos y demostrar que cumplen ciertas
+propiedades de seguridad que consideramos favorables. En la mayoría de los casos
+se intenta encontrar una \textbf{reducción} \cite{GoldwasserM84} del
+criptosistema a un problema difícil computacionalmente, de forma que un ataque
+exitoso contra el primero implicaría poder resolver de forma eficiente el
+segundo. Continuando el ejemplo anterior, RSA se considera seguro porque la
+existencia de un ataque eficiente contra el criptosistema implicaría también la
+existencia de una forma eficiente de factorizar enteros (que hasta el día de
+hoy, se desconoce).
+
+\subsection{Secuencias de juegos}
+
+Hoy en día, las demostraciones siguen una estructura denominada
+\textbf{secuencia de juegos} \cite{Shoup04}. Básicamente consisten en definir
+\textit{juegos} entre un \textit{desafiador} y un \textit{adversario}, ambos
+representados como programas probabilísticos:
+
+\renewcommand{\lstlistingname}{Juego}
+\begin{lstlisting}[mathescape=true,frame=single,
+                   caption=IND-CPA (fuente: \cite{BartheGB09})]
+  $(pk,sk) \leftarrow \KG();$
+  $(m_0,m_1) \leftarrow A_1(pk);$
+  $b \overset{\$}{\leftarrow} \{0,1\};$
+  $c \leftarrow \Enc(pk,m_b);\\$
+  $\tilde{b} \leftarrow A_2(c)$
+\end{lstlisting}
+
+El Juego 1 define la propiedad de seguridad
+IND-CPA\footnote{Indistinguishability under Chosen Plaintext Attack} de los
+esquemas de cifrado asimétrico. El adversario está representado como la pareja
+de procedimientos $(A_1,A_2)$. El desafiador crea una pareja de claves
+$(pk,sk)$, permite que el adversario elija dos textos $(m_0,m_1)$ conociendo
+$pk$, cifra aleatoriamente uno de los dos y se lo entrega al adversario para que
+adivine cuál de los dos textos originales fue cifrado. Si el adversario no es
+capaz de acertar con una probabilidad mayor que $1/2$ (intento a ciegas), se
+considera que el criptosistema cumple la propiedad IND-CPA.
+
+En general, a cada juego se le asocia un un evento $S$ y una
+\textbf{probabilidad objetivo}, y se dice que cumple su propiedad de seguridad
+cuando para cualquier posible adversario, la posibilidad de que ocurra el evento
+$S$ es arbitrariamente cercana a la probabilidad objetivo. En el Juego 1, el
+evento al finalizar la ejecución del juego sería $b=\tilde{b}$ (el adversario
+logra adivinar cuál de sus dos textos fue cifrado); y la probabilidad objetivo,
+1/2. Una secuencia de juegos es un conjunto de juegos en el que la probabilidad
+de que suceda el evento $S$ en cada juego es muy cercana a la del juego previo.
+
+En \cite{Shoup04} se demuestra que el criptosistema ElGamal efectivamente cumple
+la propiedad IND-CPA realizando una reducción del juego original de IND-CPA
+(para $KG$ y $E$ los algoritmos de generación de claves y de cifrado,
+respectivamente, de ElGamal) a uno en el que se resuelve el problema de decisión
+de Diffie-Hellman, ambos con una probabilidad de $S$ muy cercana. Esta
+demostración es válida porque el problema de decisión de Diffie-Hellman se
+considera inabordable a día de hoy.
+
+\subsection{EasyCrypt}
+
+El proceso de elaborar estas demostraciones es una tarea ardua y propensa a
+error, por lo que últimamente se han empezado a desarrollar herramientas para
+abordar la construcción y verificación de estas demostraciones en forma de
+secuencias de juegos, como CertiCrypt y su versión mejorada EasyCrypt
+\cite{BartheGHB11}.
+
+EasyCrypt es un marco formado por un \textit{lenguaje de programación} junto a
+un motor de resolución de \textit{lógica de Hoare Relacional Probabilística}
+\cite{BartheGB09}. EasyCrypt funciona como un intérprete de un lenguaje de
+propósito general y de forma interactiva: cuando se le proporciona un fichero
+fuente a evaluar, lo recorre de arriba hacia abajo comprobando que todos los
+pasos de las demostraciones son correctos. Usando Proof General es posible ir
+escribiendo un fichero fuente a la vez que el intérprete va evaluando lo que ya
+se ha escrito, ayudando y guiando al usuario a medida que éste va desarrollando
+cada demostración.
+
+EasyCrypt usa varios lenguajes de programación distintos a la hora de evaluar un
+código fuente. A continuación veremos mostrará cuáles son, con algunos ejemplos.
+
+\subsection{Lenguajes de especificacion}
+
+Estos lenguajes se usan para declarar y definir tipos, funciones, axiomas,
+juegos, oráculos, adversarios, entidades involucradas en las pruebas, etc.
+
+\paragraph{Lenguaje de expresiones}
+El lenguaje principal de especificación de EasyCrypt es el de las
+\textbf{expresiones}, que define una serie de tipos y operadores sobre
+ellos. EasyCrypt soporta tipos polimórficos de orden superior. Los operadores
+son funciones totales definidas sobre tipos (conjuntos de valores). Aunque los
+operadores se definen de forma abstracta (sin proporcionar una implementación),
+EasyCrypt asume que todos los tipos están habitados, por lo que cualquier
+aplicación de un operador debe generar un tipo habitado al menos por un
+valor. La semántica de los operadores viene de la definición de lemas y axiomas
+que describen su comportamiento de forma observacional, o extensional. Para
+soportar operadores que reciban varios argumentos se usa la técnica de la
+\textit{currificación}, que convierte una función de múltiples argumentos en una
+que al ser aplicada al primer argumento devuelve una nueva función que recibe el
+segundo argumento, y así sucesivamente. Por ejemplo $f : (A \times B\times C)
+\rightarrow D$ pasaría a ser $f : A \rightarrow (B \rightarrow (C \rightarrow
+D))$, o lo que es lo mismo, $f : A \rightarrow B \rightarrow C \rightarrow D$.
+
+\newpage
+\renewcommand{\lstlistingname}{Ejemplo}
+\begin{easycrypt}[caption=Lenguaje de expresiones]{}
+type 'a predicate = 'a -> bool.
+datatype 'a option = None | Some of 'a.
+op find : 'a predicate -> 'a list -> 'a option.
+axiom find_head :
+  forall (x : bool) (l : bool list),
+    hd l = x => find (lambda e, e = x) l = Some x.
+\end{easycrypt}
+
+\paragraph{Lenguaje de expresiones probabilísticas}
+Para poder razonar sobre distribuciones de probabilidad, EasyCrypt proporciona
+un tipo (\rawec{'a distr}) que representa sub-distribuciones discretas sobre
+\rawec{'a}. La principal herramienta para trabajar sobre sub-distribuciones es
+el operador (\rawec{op mu : 'a distr -> ('a -> bool) -> real}), que devuelve la
+probabilidad de un evento. Por ejemplo, la distribución uniforme sobre booleanos
+está definida en la biblioteca estándar de EasyCrypt de la siguiente manera
+(charfun es la función característica de p evaluado en x, es decir, devuelve 1
+si p x = true y 0 si p x = false):
+
+\begin{easycrypt}[caption=Definición de la distribución uniforme sobre bool]{}
+op dbool : bool distr.
+axiom mu_def : forall (p : bool -> bool),
+  mu dbool p =
+    (1/2) * charfun p true +
+    (1/2) * charfun p false.
+\end{easycrypt}
+
+\paragraph{Lenguaje pWhile}
+Los lenguajes de expresiones a menudo son inadecuados para definir juegos y
+otras estructuras de datos como esquemas de cifrado u oráculos, debido a la
+necesidad de representar algoritmos secuenciales, entidades con estado,
+etc. Para ello, EasyCrypt implementa un lenguaje distinto llamado pWhile
+(probabilistic While) \cite{BartheGB09}.
+
+\renewcommand{\lstlistingname}{Listado}
+\begin{lstlisting}[mathescape=true,frame=single,caption=Gramática de pWhile]
+  $\mathcal{I} ::= \mathcal{V} \leftarrow \mathcal{E}$
+    | $\mathcal{V} \overset{\$}{\leftarrow} \mathcal{DE}$
+    | if $\mathcal{E}$ then $\mathcal{C}$ else $\mathcal{C}$
+    | while $\mathcal{E}$ do $\mathcal{C}$
+    | $\mathcal{V} \leftarrow \mathcal{P}(\mathcal{E}, ..., \mathcal{E})$
+
+  $\mathcal{C} ::=$ skip
+    | $\mathcal{I}$; $\mathcal{C}$
+\end{lstlisting}
+
+% % https://tex.stackexchange.com/questions/24886/which-package-can-be-used-to-write-bnf-grammars
+% \setlength{\grammarparsep}{20pt plus 1pt minus 1pt}
+% \setlength{\grammarindent}{12em}
+% \begin{grammar}
+%
+% <statement> ::= <ident> '=' <expr>
+% \alt `for' <ident> `=' <expr> `to' <expr> `do' <statement>
+% \alt `{' <stat-list> `}'
+% \alt <empty>
+%
+% <stat-list> ::= <statement> `;' <stat-list> | <statement>
+%
+% \end{grammar}
+
+\subsection{Lenguajes de demostración}
+
+Estos lenguajes se usan para definir lemas y demostrarlos.
+
+\paragraph{Juicios}
+Los juicios son proposiciones que se pueden realizar en EasyCrypt, y tienen
+asociado un valor de verdad (pueden ser ciertos o falsos). Para demostrar su
+veracidad, un juicio deberá demostrarse usando el lenguaje de los tactics
+(detallado a continuación). Además de los juicios expresados en lógica de primer
+orden, EasyCrypt cuenta con diversos tipos de juicio derivados de la Lógica de
+Hoare que se usan para razonar sobre la ejecución de programas:
+
+\begin{itemize}
+\item Lógica de Hoare (\textbf{HL}). Tienen la siguiente forma:
+
+  $$c : P \Longrightarrow Q$$
+
+  donde $P$ y $Q$ son aserciones (predicados) y $c$ es un mandato o
+  programa. $P$ es la \textit{precondición} y $Q$ es la
+  \textit{postcondición}. El juicio expresa que si la precondición se cumple al
+  momento de ejecutar el mandato, la postcondición también se cumplirá cuando
+  éste termine (si es que lo hace).
+
+\item Lógica de Hoare probabilística (\textbf{pHL}). A los juicios de Hoare
+  anteriores se les asigna una probabilidad, que puede ser exacta o una cota
+  superior/inferior.
+
+  $$[c : P \Longrightarrow Q] \leq \delta$$
+  $$[c : P \Longrightarrow Q] = \delta$$
+  $$[c : P \Longrightarrow Q] \geq \delta$$
+
+\item Lógica de Hoare relacional probabilística (\textbf{pRHL}). Tienen la
+  siguiente forma:
+
+  $$c_1 \sim c_2 : \Psi \Longrightarrow \Phi$$
+
+  En este caso, el juicio expresa que si la precondición $\Psi$ se cumple antes
+  de la ejecución de $c_1$ y $c_2$, tras su ejecución también se cumplirá la
+  postcondición $\Phi$. En este caso las (pre,post)condiciones son
+  \textit{relaciones} entre las memorias de los dos programas, por lo que este
+  tipo de juicios expresa una \textit{equivalencia} entre dos programas con
+  respecto a ellas. Además, en este caso los programas $c_1$ y $c_2$ son
+  probabilísticos: su evaluación produce como resultado una distribución de
+  probabilidad sobre los posibles estados en los que se podrá encontrar la
+  memoria al ser ejecutado.
+\end{itemize}
+
+\paragraph{Tactics}
+Para demostrar juicios, EasyCrypt cuenta con un lenguaje basado en
+\textit{tactics}. Una demostración consiste en una secuencia de \textit{tactics}
+que se van ejecutando iterativamente, donde cada \textit{tactic} aplica una
+transformación sintáctica al \textit{objetivo} actual (la fórmula que se está
+demostrando) hasta que el último resuelve finalmente el objetivo.
+
+\renewcommand{\lstlistingname}{Ejemplo}
+\begin{easycrypt}[caption=Uso de tactics]{}
+lemma hd_tl_cons :
+  forall (xs:'a list),
+    xs <> [] => (hd xs)::(tl xs) = xs.
+proof.
+  intros xs.
+  elim / list_ind xs.
+  simplify.
+  intros x xs' IH h {h}.
+  rewrite hd_cons.
+  rewrite tl_cons.
+  reflexivity.
+qed.
+\end{easycrypt}
+
+En este ejemplo obtenido de la biblioteca estándar de EasyCrypt (ligeramente
+modificado para mejorar su comprensión) se ilustra cómo se realizan las
+demostraciones. Lo que aparece a continuación del nombre del lema es su
+especificación formal en lógica de primer orden: una propiedad acerca de la
+descomposición de las listas en cabeza y cola. Lo que aparece a continuación es
+la demostración del lema, con un \textit{tactic} por cada línea. La demostración
+se vale de algunos axiomas definidos anteriormente como el de la inducción sobre
+listas (list_ind) o la definición de 'hd' y 'tl' (hd_cons, tl_cons).
+
+Un \textit{tactic} que vale la pena destacar es \rawec{smt}, que intenta
+resolver el objetivo actual de la demostración invocando \textit{resolvedores
+  SMT (Satisfiability Modulo Theories)} externos. Estas herramientas están
+diseñadas para intentar encontrar soluciones a fórmulas expresadas en lógica de
+primer orden, permitiendo ciertas interpretaciones adicionales sobre los
+símbolos. Normalmente soportan ciertas teorías muy útiles en criptografía como
+arrays, listas, aritmética entera, etc., y a menudo son capaces de resolver de
+forma automática partes repetitivas y tediosas de las demostraciones, liberando
+de esa carga de trabajo al criptógrafo.
+
+\pagebreak
+\section{Motivación y objetivos}
+
+Para este trabajo se ha decidido contribuir dentro de lo posible a mejorar el
+sistema EasyCrypt, desarrollado principalmente en el Instituto IMDEA Software en
+Madrid. Aunque es un sistema que ya se ha utilizado para demostrar la seguridad
+de construcciones criptográficas ampliamente usadas como el criptosistema de
+Cramer-Shoup o el modo de operación CBC para cifradores de bloque, sigue en
+constante desarrollo y tiene muchas posibilidades de ampliación. En concreto, en
+este trabajo se abordarán e intentarán resolver dos problemas de distinta
+índole:
+
+\begin{itemize}
+\item \textbf{La posibilidad de trabajar con el coste de algoritmos.} Para poder
+  deducir la capacidad computacional requerida para romper un criptosistema se
+  necesita un método para especificar el coste computacional asociado a computar
+  ciertas operaciones. El objetivo es ser capaz de relacionar la seguridad de un
+  sistema con los recursos del atacante, por ejemplo para afirmar que el sistema
+  es seguro mientras los recursos del atacante no superen cierto límite.
+
+  Para poder trabajar con costes, es necesario hacer dos cosas: especificarlos y
+  trabajar con ellos (es decir, que en el desarrollo de una demostración se
+  pueda tenerlos en cuenta a la hora de derivar conclusiones). La primera parte
+  del proyecto consistirá en la implementación de un mecanismo que permita
+  \textbf{especificar} los costes computacionales (implementar un mecanismo para
+  \textbf{trabajar} con ellos es una tarea considerablemente difícil y que se
+  escapa a los recursos temporales del TFG).
+
+\item \textbf{Mejorar la usabilidad del sistema.} Idealmente, EasyCrypt debería
+  ser utilizado por criptólogos como herramienta de verificación, pero para ello
+  es necesario hacer su uso lo más sencillo posible. Aunque EasyCrypt es
+  bastante más usable que su predecesor CertiCrypt, sigue estando lejos de ser
+  sencillo. La primera barrera de entrada consiste en su propia instalación: es
+  necesario clonar el repositorio donde está alojado el código y compilarlo
+  junto con sus dependencias (proceso que puede llegar a tardar hasta una
+  hora). Además, toda la interacción con EasyCrypt se realiza a través de Emacs
+  (editor de texto), por lo que tiene que estar instalado y el usuario debe de
+  tener cierta experiencia para usarlo cómodamente.
+
+  Una forma relativamente sencilla de eliminar esta barrera de entrada es
+  ofrecer una interfaz web con todo lo necesario para usar EasyCrypt sin tenerlo
+  instalado en el sistema local. Además de ahorrar tiempo en la instalación y en
+  aprender a usar Emacs, haría más sencillo trabajar desde múltiples sitios al
+  tener toda la estructura del proyecto centralizada en el servidor remoto.
+
+  En la segunda parte del proyecto se llevará a cabo el diseño e implementación
+  de este sitio web, con el fin de hacer más sencillo usar EasyCrypt y fomentar
+  su utilización en los círculos de gente que se dedica a la criptografía.
+\end{itemize}
+
+\pagebreak
+\section{Desarrollo: Coste de algoritmos}
+
+TODO TODO TODO
+
+\subsection{Arquitectura de EasyCrypt}
+
+\subsection{Ejemplo de uso (del coste)}
+
+$$\forall (lst : [\alpha]) (p : \alpha -> bool) (x : \alpha). cost[find, p, lst]
+<= cost[p, x] * length(lst)$$
+
+\pagebreak
+\section{Desarrollo: Interfaz web}
+
+\pagebreak
+\section{Resultados y conclusiones}
+
+\pagebreak
+\section{Contribuciones}
+
+\pagebreak
+\section{Anexos}
+
+\pagebreak \bibliography{bib}{} \bibliographystyle{apalike} % plain, alpha, apalike
+
+\end{document}