From 71811a0d4bb5820f313433bc4c3d7eb611b9a061 Mon Sep 17 00:00:00 2001
From: Guillermo Ramos
Date: Sun, 22 Jun 2014 18:09:45 +0200
Subject: Sección: Diseño

---
 memoria.tex | 194 +++++++++++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 153 insertions(+), 41 deletions(-)

(limited to 'memoria.tex')

diff --git a/memoria.tex b/memoria.tex
index b6cbe53..68322d9 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -89,11 +89,12 @@ asimétrica, ya que serán de utilidad a la hora de explicar la siguiente secci
 La criptografía \textbf{asimétrica} o \textbf{de clave pública} engloba todos
 aquellos algoritmos criptográficos que usan dos funciones, $\Enc$ y $\Dec$, para
 cifrar y descifrar la información respectivamente. Intuitivamente, cifrar una
-información consiste en modificarla hasta hacerla ininteligible. Cada una de
-estas funciones usa una \textbf{clave} distinta para llevar a cabo su tarea, por
-lo que es necesario un procedimiento de generación de claves $\KG$ para
-conseguir un par de claves pública-privada $(pk,sk)$. Las funciones de cifrado y
-descifrado tienen la siguiente forma:
+información consiste en modificarla hasta hacerla ininteligible. El
+comportamiento de cada una de estas funciones está parametrizado por una
+\textbf{clave} distinta (para que el resultado no sea siempre el mismo para cada
+entrada), por lo que también es necesario un procedimiento de generación de
+claves $\KG$ para conseguir un par de claves pública-privada $(pk,sk)$. Las
+funciones de cifrado y descifrado tienen la siguiente forma:
 
 $$\Enc(pk,T) = C$$
 $$\Dec(sk,C) = T$$
@@ -101,14 +102,14 @@ $$\Dec(sk,C) = T$$
 Donde $T$ significa \textbf{texto en claro} o \textbf{mensaje}, y $C$,
 \textbf{texto cifrado} o \textbf{cifra}. Para que un esquema de criptografía
 asimétrica sea útil, siempre que el par $(pk,sk)$ se haya generado en una sola
-llamada a $\KG$ se debe cumplir la siguiente ecuación:
+llamada a $\KG$ se debe cumplir la siguiente igualdad:
 
 $$\forall t \in T. \Dec(sk, \Enc(pk, t)) = t$$
 
 Dicho de otra forma, la función de descifrado \textbf{invierte} la función de
-cifrado. El objetivo es que cualquier persona pueda mandar un mensaje cifrado al
-propietario de un par de claves sabiendo que sólo dicho propietario podrá
-descifrar el mensaje.
+cifrado. $\Enc(pk)$ es lo que se denomina \textbf{función trampa} ya que su
+inversa, $\Dec(sk)$, es muy sencilla de computar si se conoce $sk$ pero
+extremadamente difícil en caso contrario.
 
 \section{Secuencias de juegos}
 \label{sec:secuencias-de-juegos}
@@ -116,10 +117,10 @@ descifrar el mensaje.
 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
+(\textit{challenger}) y un \textbf{adversario} (\textit{adversary}), ambos
 representados como programas probabilísticos:
 
-\begin{game}[caption=IND-CPA (\cite{BartheGB09})]{}{}
+\begin{game}[caption=IND-CPA (\cite{BartheGB09}), label={lst:indcpa}]{}{}
   $(pk,sk) \leftarrow \KG();$
   $(m_0,m_1) \leftarrow A_1(pk);$
   $b \overset{\$}{\leftarrow} \{0,1\};$
@@ -146,13 +147,13 @@ 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 $\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.
+En \cite{Shoup04} se demuestra que el criptosistema de clave pública ElGamal
+efectivamente cumple la propiedad IND-CPA realizando una reducción del juego
+original de IND-CPA (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}
@@ -214,7 +215,7 @@ $f : (A \times B\times C) \rightarrow D$ pasaría a ser $f : A \rightarrow (B
 En este ejemplo se ilustra la metodología general de definición de tipos y
 operadores en el lenguaje de expresiones de EasyCrypt:
 
-\begin{easycrypt}[caption=Lenguaje de expresiones]{}{}
+\begin{easycrypt}[caption=Lenguaje de expresiones, label={lst:exprlang}]{}{}
 type 'a predicate = 'a -> bool.
 datatype 'a option = None | Some of 'a.
 op find : 'a predicate -> 'a list -> 'a option.
@@ -224,13 +225,23 @@ axiom find_head :
 \end{easycrypt}
 
 Las primeras dos líneas defininen los tipos \rawec{predicate} y
-\rawec{option}. A continuación se define el operador \rawec{find}, que dado un
+\rawec{option}. El primero representa funciones que devuelven \rawec{bool}, y el
+segundo, datos que pueden tomar los valores \rawec{None} o \rawec{Some x} (se
+usan para representar a nivel de tipos un dato que podría no existir).
+
+A continuación se define el operador \rawec{find}, que dado un
 predicado y una lista de elementos, devuelve el elemento de la lista que
-satisface el predicado (o \rawec{None} si ninguno lo satisface). Por último, se
-define un axioma llamado \rawec{find_head}: si dado un elemento \rawec{x} y una
-lista, siendo \rawec{x} el primer elemento de la lista, se llama a \rawec{find}
-con el predicado <<igual a \rawec{x}>>, el resultado deberá ser (\rawec{Some
-  x}).
+satisface el predicado (o \rawec{None} si ninguno lo satisface).
+
+Por último, se define un axioma llamado \rawec{find_head}: si dado un elemento
+\rawec{x} y una lista, siendo \rawec{x} el primer elemento de la lista, se llama
+a \rawec{find} con el predicado <<igual a \rawec{x}>>, el resultado deberá ser
+(\rawec{Some x}).
+
+En EasyCrypt hay dos formas de definir hechos: usando
+\textbf{axiomas} o \textbf{lemas}. La diferencia es que un axioma es válido por
+sí mismo, mientras que un lema se debe acompañar de una demostración, como se
+verá en el apartado \ref{sec:tactics}.
 
 \paragraph{Lenguaje de expresiones probabilísticas}
 Para poder razonar sobre distribuciones de probabilidad, EasyCrypt proporciona
@@ -242,7 +253,8 @@ está definida en la biblioteca estándar de EasyCrypt de la siguiente manera
 (\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]{}{}
+\begin{easycrypt}[caption=Distribución uniforme sobre bool,
+  label={lst:booldistr}]{}{}
 op dbool : bool distr.
 axiom mu_def : forall (p : bool -> bool),
   mu dbool p =
@@ -257,7 +269,7 @@ necesidad de representar algoritmos secuenciales, entidades con estado,
 etc. Para ello, EasyCrypt implementa un lenguaje distinto llamado pWhile
 (probabilistic While) \cite{BartheGB09}.
 
-\begin{bnf}[caption=Lenguaje pWhile]{}{}
+\begin{bnf}[caption=Lenguaje pWhile, label={lst:pwhile}]{}{}
   $\mathcal{I ::= V \leftarrow E}$
     | $\mathcal{V \overset{\$}{\leftarrow} DE}$
     | if $\mathcal{E}$ then $\mathcal{C}$ else $\mathcal{C}$
@@ -340,7 +352,7 @@ 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 tácticas]{}
+\begin{easycrypt}[caption=Uso de tácticas, label={lst:tactics}]{}
 lemma hd_tl_cons :
   forall (xs:'a list),
     xs <> [] => (hd xs)::(tl xs) = xs.
@@ -441,10 +453,10 @@ axiomas y lemas de uso común, etc.
 Un concepto muy significativo en criptografía es el del \textbf{coste}. El coste
 de un algoritmo es una medida de los recursos (tiempo, espacio, ...) que
 requiere su ejecución. Como hemos visto en la introducción, salvo en casos muy
-concretos (OTP \cite{Shannon49}), la criptografía basa su seguridad en la
+concretos (OTP \cite{Shannon49}), la seguridad en criptografía depende de la
 capacidad computacional del adversario. Por tanto, existen muchas propiedades
-que se pueden expresar acerca de la seguridad de un criptosistema que de una u
-otra forma dependen del coste de llevar a cabo un ataque contra él.
+acerca de la seguridad de un criptosistema que de una u otra forma dependen del
+coste de llevar a cabo un ataque contra él.
 
 A lo largo de este capítulo se detallará el proceso que se ha seguido para
 implementar la funcionalidad que permita a la especificación del coste de
@@ -453,20 +465,124 @@ algoritmos en EasyCrypt.
 TODO referencias a dónde se explica qué.
 
 \newpage
-\section{Ejemplo de uso}
-\label{sec:ejemplo-de-uso}
+\section{Motivación}
+\label{sec:motivacion}
 
 Supongamos que el usuario está construyendo una demostración de que un
 criptosistema de clave pública es seguro siempre que los recursos del adversario
 no sean superiores a cierto límite. En este caso, por <<seguro>> nos referimos a
 que el adversario no es capaz de descifrar un texto cifrado sin poseer la clave
 privada correspondiente. Como hemos visto en la sección \ref{sec:cript-asim},
-esto es equivalente a decir que no es capaz de \textbf{invertir} la función de
-cifrado.
+esto es equivalente a decir que el adversario no es capaz de \textbf{invertir}
+la función de cifrado.
+
+La primera parte de la prueba consistiría en demostrar que $\Enc(pk)$ y
+$\Dec(sk)$ realmente constituyen una función trampa. En este caso, la seguridad
+dependería única y exclusivamente de la dificultad de adivinar $sk$. Suponiendo
+que el sistema no tenga fallos que permitan extraer información de alguna otra
+forma, el adversario no tendrá más remedio que usar la \textbf{fuerza bruta}:
+probar todas las claves posibles hasta encontrar la correcta. Por este mismo
+motivo, la complejidad de la clave (longitud, aleatoriedad) es crucial: adivinar
+una clave aleatoria de 32 bits requerirá como mucho $2^{32} = 4294967296$
+intentos, mientras que una clave aleatoria de 256 bits requerirá una cantidad de
+intentos del orden de la cantidad de átomos en el universo.
+
+En este punto, el criptosistema será seguro siempre que se pueda probar que el
+adversario no es capaz de adivinar la clave correcta en un tiempo razonable. Por
+ello, si queremos proporcionar una cota exacta de la cantidad de trabajo
+necesario que requiere romper el criptosistema (coste) necesitamos una forma de
+especificar los costes de cada operación, combinarlos para obtener el coste del
+algoritmo completo, y tenerlos en cuenta a la hora de realizar las
+demostraciones. A lo largo de este capítulo veremos cómo se ha implementado esta
+funcionalidad.
+
+\section{Diseño}
+\label{sec:diseno}
+
+\subsection{Operador especial de coste}
+\label{sec:operador-de-coste}
+
+Para empezar, necesitamos una forma de hacer referencia al coste asociado a un
+operador. Una primera aproximación podría ser usar una \textbf{función} que dado
+un operador de cualquier tipo (constant o función) devuelva su coste en
+forma de número entero positivo:
+
+\begin{easycrypt}[caption=Definición 1 del coste, label={lst:cost1}]{}
+op cost : 'a -> int.
+\end{easycrypt}
+
+Sin embargo, hay un problema con esta solución. En EasyCrypt la igualdad se
+define de forma extensional, por lo que dos funciones se consideran la misma
+cuando su resultado es el mismo para las mismas entradas. Dicho de un modo más
+formal:
+
+$$\forall f, g. (\forall x. f(x) = g(x)) \Rightarrow f = g$$
+
+Esta aproximación nos permitiría deducir que dos funciones extensionalmente
+iguales tienen siempre el mismo coste, ya que $f = g$ implica $cost(f) =
+cost(g)$. El problema es que dos funciones extensionalmente iguales no tienen
+por qué tener el mismo coste, ni siquiera la misma clase de complejidad (por
+ejemplo, cualquier algoritmo que se ejecute en tiempo lineal se puede reducir a
+otro algoritmo que se ejecute en tiempo cuadrático).
+
+Una segunda aproximación es la de usar un \textbf{operador especial} definido
+dentro del propio compilador (en lugar de en una biblioteca del lenguaje, como
+hubiera sido el caso anterior) para evitar que se le apliquen las mismas
+suposiciones que al resto de funciones y así evitar inconsistencias en la
+lógica:
+
+\begin{easycrypt}[caption=Definición 2 del coste, label={lst:cost2}]{}
+cost[myop, arg1, arg2, ...] : int
+\end{easycrypt}
+
+El operador especial \rawec{cost} devolvería el coste en forma de entero
+positivo, como en el caso anterior, pero esta vez sería necesario especificar la
+totalidad de los argumentos del operador cuyo coste estemos definiendo. El
+operador debe de estar declarado anteriormente, y los argumentos pueden ser
+valores literales, otros operadores o variables cuantificadas universalmente
+(como queremos diferenciar entre la cuantificación universal introducida por la
+construcción \rawec{forall} y ésta, tendremos que indroducir un ámbito especial
+con el axioma de coste, explicado a continuación).
 
-\section{Objetivos}
+\subsection{Axioma de coste}
+\label{sec:axioma-de-coste}
 
-Operador, axioma.
+Además de poder hacer referencia a los costes con el operador especial de coste,
+necesitamos una forma de poder definirlos. Para esto necesitamos otra
+construcción nueva del lenguaje: el \textbf{axioma de coste}:
+
+\begin{easycrypt}[caption=Axioma de coste, label={lst:costaxiom}]{}
+caxiom name param1 param2 ... : spec.
+\end{easycrypt}
+
+Como se puede apreciar, es muy similar a la definición de un axioma normal en
+EasyCrypt (ver listado \ref{lst:exprlang}). La diferencia son los parámetros que
+van a continuación del nombre del axioma. Estas variables se ligan
+implícitamente con un cuantificador universal para ser referenciadas dentro del
+operador especial de coste, que puede aparecer dentro de la
+especificación.
+
+En este ejemplo se axiomatiza el hecho de que ejecutar la función \rawec{sum}
+tiene coste cero cuando uno de sus argumentos es cero:
+
+\begin{easycrypt}[caption=Coste (parcial) de \rawec{sum}, label={lst:costuse}]{}
+caxiom sum_zero x :
+  cost[sum, 0, x] = 0 &&
+  cost[sum, x, 0] = 0.
+\end{easycrypt}
+
+En este otro ejemplo se define el coste de ejecutar la función \rawec{find}
+(listado \ref{lst:exprlang}), que busca en una lista el elemento que satisface
+un predicado:
+
+\begin{easycrypt}[caption=Coste de \rawec{find}, label={lst:listcost}]{}
+caxiom find_cost (l : 'a list) (p : 'a predicate) (x : 'a) :
+  cost[find, p, l] <= cost[p, x] * length l.
+\end{easycrypt}
+
+Una vez definida la funcionalidad que se quiere conseguir (\textbf{operador
+  especial de coste} y \textbf{axioma de coste}), pasamos a analizar el proceso
+de su implementación.
 
 \section{Arquitectura de EasyCrypt}
 \label{sec:arqu-de-easycrypt}
@@ -486,10 +602,6 @@ qué partes lo integran y cómo está organizado a nivel de código.
 % Why3
 % Solvers
 
-% \section{Ejemplo de uso (del coste)}
-
-% $$\forall (lst : [\alpha]) (p : \alpha -> bool) (x : \alpha). cost[find, p, lst]
-% <= cost[p, x] * length(lst)$$
 
 \chapter{DESARROLLO: INTERFAZ WEB}
 
-- 
cgit v1.2.3

