From 1cc1cdf9af5154b7ffb0240595da3da7ae5b6336 Mon Sep 17 00:00:00 2001
From: Guillermo Ramos
Date: Mon, 2 Jun 2014 19:18:26 +0200
Subject: Sugerencias de Pablo, a falta de un par de cosas

---
 memoria.tex | 77 ++++++++++++++++++++++++++++++++-----------------------------
 1 file changed, 40 insertions(+), 37 deletions(-)

(limited to 'memoria.tex')

diff --git a/memoria.tex b/memoria.tex
index 64bd1ce..13ef1e4 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -130,7 +130,7 @@ representados como programas probabilísticos:
 \end{game}
 
 El Juego 1 define la propiedad de seguridad
-IND-CPA\footnote{Indistinguishability under Chosen Plaintext Attack} de los
+IND-CPA (<<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 un par de claves
 $(pk,sk)$, permite que el adversario elija dos textos $(m_0,m_1)$ conociendo
@@ -139,7 +139,7 @@ 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 \textbf{evento} $S$ y una
+En general, a cada juego se le asocia 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
@@ -171,12 +171,12 @@ un motor de resolución de \textbf{lógica de Hoare Relacional Probabilística}
 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.
+Proof General, un modo del editor de texto Emacs, 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.
+código fuente. A continuación veremos cuáles son, con algunos ejemplos.
 
 \subsection{Lenguajes de especificacion}
 \label{sec:leng-de-espec}
@@ -202,6 +202,11 @@ $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$.
 
+Los argumentos de los tipos polimórficos se colocan delante del tipo en
+cuestión (\rawec{int list} significa <<lista de enteros>>), y se usa una comilla
+simple delante de las variables de tipo (\rawec{'a list} significa <<lista de
+cualquier tipo>>).
+
 \begin{easycrypt}[caption=Lenguaje de expresiones]{}{}
 type 'a predicate = 'a -> bool.
 datatype 'a option = None | Some of 'a.
@@ -218,8 +223,8 @@ un tipo (\rawec{'a distr}) que representa sub-distribuciones discretas sobre
 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):
+(\rawec{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=Distribución uniforme sobre bool]{}{}
 op dbool : bool distr.
@@ -270,7 +275,7 @@ Estos lenguajes se usan para definir lemas y demostrarlos.
 
 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
+veracidad, un juicio deberá demostrarse usando el lenguaje de tácticas
 (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:
@@ -310,17 +315,16 @@ Hoare que se usan para razonar sobre la ejecución de programas:
   memoria al ser ejecutado.
 \end{itemize}
 
-\paragraph{Tactics}
+\paragraph{Tácticas}
 \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.
+(\textit{tactics}). Una demostración consiste en una secuencia de tácticas que
+se van ejecutando iterativamente, donde cada táctica 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.
 
-\begin{easycrypt}[caption=Uso de tactics]{}
+\begin{easycrypt}[caption=Uso de tácticas]{}
 lemma hd_tl_cons :
   forall (xs:'a list),
     xs <> [] => (hd xs)::(tl xs) = xs.
@@ -341,20 +345,19 @@ 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 (\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 \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.
+una táctica 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).
+
+Una táctica que vale la pena destacar es \rawec{smt}, que intenta resolver el
+objetivo actual de la demostración invocando \textbf{resolvedores}
+(\textit{solvers}) \textbf{SMT}(<<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}
@@ -363,10 +366,10 @@ 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:
+Cramer-Shoup o el modo de operación CBC para cifradores de bloque, EasyCrypt
+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
@@ -390,9 +393,9 @@ este trabajo se abordarán e intentarán resolver dos problemas de distinta
   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.
+  hora). Además, toda la interacción con EasyCrypt se realiza a través de
+  ProofGeneral y Emacs, 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
-- 
cgit v1.2.3

