diff options
Diffstat (limited to 'memoria.tex')
| -rwxr-xr-x | memoria.tex | 194 |
1 files changed, 153 insertions, 41 deletions
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} |