Cambios varios

1 files changed, 71 insertions, 54 deletions

diff --git a/memoria.tex b/memoria.tex
index 793f7c5..25167db 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -10,9 +10,12 @@
 \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{perpage}
 
 \input{defs}
 
+\MakePerPage{footnote}
+
 \def\emptypage{\newpage\thispagestyle{empty}\mbox{}}
 
 \title{Trabajo de fin de Grado} \author{Guillermo Ramos Gutiérrez - r090050}
@@ -30,6 +33,7 @@
 \tableofcontents
 
 \chapter{INTRODUCCIÓN}
+\label{cha:introduccion}
 \pagenumbering{arabic}
 \setcounter{page}{1}
 
@@ -114,14 +118,16 @@ propietario de un par de claves sabiendo que sólo dicho propietario podrá
 descifrar el mensaje.
 
 \section{Secuencias de juegos}
+\label{sec: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
+Hoy en día, las demostraciones relacionadas con criptografía siguen una
+estructura denominada \textbf{secuencia de juegos} \cite{Shoup04}. Básicamente
+consisten en definir \textbf{juegos} entre un \textbf{desafiador}
+(\textit{challenger}) y un \textbf{adversario} (\textit{adversary}) , ambos
 representados como programas probabilísticos:
 
 \renewcommand{\lstlistingname}{Juego}
-\begin{lstlisting}[mathescape=true,frame=single,
+\begin{lstlisting}[mathescape=true,frame=tb,
                    caption=IND-CPA (fuente: \cite{BartheGB09})]
   $(pk,sk) \leftarrow \KG();$
   $(m_0,m_1) \leftarrow A_1(pk);$
@@ -133,14 +139,14 @@ representados como programas probabilísticos:
 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
+de procedimientos $(A_1,A_2)$. El desafiador crea un par 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
+En general, a cada juego se le asocia un un \textbf{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
@@ -151,13 +157,14 @@ 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,
+(para $\KG$ y $\Enc$ 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.
 
 \section{EasyCrypt}
+\label{sec: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
@@ -165,20 +172,21 @@ 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 es un marco formado por un \textbf{lenguaje de programación} junto a
+un motor de resolución de \textbf{lógica de Hoare Relacional Probabilística}
+(ver sección \ref{sec:juicios}) \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 editar un fichero fuente mientras el intérprete lo va
+evaluando sobre la marcha, ayudando y guiando al usuario a medida que éste
+desarrolla 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}
+\label{sec:leng-de-espec}
 
 Estos lenguajes se usan para declarar y definir tipos, funciones, axiomas,
 juegos, oráculos, adversarios, entidades involucradas en las pruebas, etc.
@@ -194,11 +202,12 @@ 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$.
+\textbf{currificación} (\textit{currying}), 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$.
 
 \renewcommand{\lstlistingname}{Ejemplo}
 \begin{easycrypt}[caption=Lenguaje de expresiones]{}
@@ -220,7 +229,7 @@ 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]{}
+\begin{easycrypt}[caption=Distribución uniforme sobre bool]{}{}
 op dbool : bool distr.
 axiom mu_def : forall (p : bool -> bool),
   mu dbool p =
@@ -235,17 +244,15 @@ 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}$
+\begin{bnf}[caption=Lenguaje pWhile]{}{}
+  $\mathcal{I ::= V \leftarrow E}$
+    | $\mathcal{V \overset{\$}{\leftarrow} 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{C} ::=$ skip
     | $\mathcal{I}$; $\mathcal{C}$
-\end{lstlisting}
+\end{bnf}
 
 % % https://tex.stackexchange.com/questions/24886/which-package-can-be-used-to-write-bnf-grammars
 % \setlength{\grammarparsep}{20pt plus 1pt minus 1pt}
@@ -262,10 +269,13 @@ etc. Para ello, EasyCrypt implementa un lenguaje distinto llamado pWhile
 % \end{grammar}
 
 \subsection{Lenguajes de demostración}
+\label{sec:leng-de-demostr}
 
 Estos lenguajes se usan para definir lemas y demostrarlos.
 
 \paragraph{Juicios}
+\label{sec: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
@@ -274,17 +284,17 @@ 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:
+\item Lógica de Hoare (\textit{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
+  programa. $P$ es la \textbf{precondición} y $Q$ es la
+  \textbf{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
+\item Lógica de Hoare probabilística (\textit{pHL}). A los juicios de Hoare
   anteriores se les asigna una probabilidad, que puede ser exacta o una cota
   superior/inferior.
 
@@ -292,7 +302,7 @@ Hoare que se usan para razonar sobre la ejecución de programas:
   $$[c : P \Longrightarrow Q] = \delta$$
   $$[c : P \Longrightarrow Q] \geq \delta$$
 
-\item Lógica de Hoare relacional probabilística (\textbf{pRHL}). Tienen la
+\item Lógica de Hoare relacional probabilística (\textit{pRHL}). Tienen la
   siguiente forma:
 
   $$c_1 \sim c_2 : \Psi \Longrightarrow \Phi$$
@@ -300,8 +310,8 @@ Hoare que se usan para razonar sobre la ejecución de programas:
   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
+  \textbf{relaciones} entre las memorias de los dos programas, por lo que este
+  tipo de juicios expresa una \textbf{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
@@ -309,11 +319,14 @@ Hoare que se usan para razonar sobre la ejecución de programas:
 \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.
+\label{sec:tactics}
+
+Para demostrar juicios, EasyCrypt cuenta con un lenguaje basado en tácticas
+(\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 \textbf{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]{}
@@ -335,22 +348,25 @@ 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).
+descomposición de las listas en cabeza (\textit{head}) y cola
+(\textit{tail}). 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.
+resolver el objetivo actual de la demostración invocando \textbf{resolvedores}
+(\textit{solvers}) \textbf{SMT}\footnote{Satisfiability Modulo
+  Theories}. 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.
 
 \section{Motivación y objetivos}
+\label{sec:motiv-y-objet}
 
 Para este trabajo se ha decidido contribuir dentro de lo posible a mejorar el
 sistema EasyCrypt, desarrollado principalmente en el Instituto IMDEA Software en
@@ -400,6 +416,7 @@ este trabajo se abordarán e intentarán resolver dos problemas de distinta
 
 \pagebreak
 \chapter{DESARROLLO: COSTE}
+\label{cha:desarrollo:-coste}
 
 La principal aportación de EasyCrypt con respecto a otros demostradores de
 teoremas como Coq\footnote{\url{http://coq.inria.fr/}} o
@@ -439,6 +456,6 @@ $$\forall (lst : [\alpha]) (p : \alpha -> bool) (x : \alpha). cost[find, p, lst]
 
 \chapter{ANEXOS}
 
-\pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr} % plain, alpha, apalike
+\pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}
 
 \end{document}