\documentclass[12pt,a4paper,parskip=full]{scrreprt}
\usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry}

\usepackage[spanish]{babel} \usepackage[utf8]{inputenc} \usepackage{url}
\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,urlcolor=black,citecolor=blue]{hyperref}
\usepackage{perpage}

\usepackage{tikz}

\usepackage{float}
\floatstyle{boxed}
\newfloat{ocaml}{thp}{ext}

\usepackage{alltt}
\usepackage{color}
\input{ocaml_colors}

\usetikzlibrary{shapes,arrows}

\input{defs}
\input{portada/defs}

\MakePerPage{footnote}

\def\emptypage{\newpage\thispagestyle{empty}\mbox{}}

\begin{document}
\input{portada/portada}

\pagenumbering{roman}
\emptypage
\chapter*{Resumen}
\chapter*{Abstract}
\emptypage

\tableofcontents

\chapter{INTRODUCCIÓN}
\label{cha:introduccion}
\pagenumbering{arabic}
\setcounter{page}{1}

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 (ver figura \ref{fig:proofs}). 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).

\begin{figure}[h]
    \centering
    \includegraphics[width=0.6\textwidth]{img/proofs.png}
    \caption{Construcción de pruebas}
    \label{fig:proofs}
\end{figure}

\section{Criptografía asimétrica}
\label{sec:cript-asim}

En esta sección se introducirán algunos conceptos fundamentales de criptografía
asimétrica, ya que serán de utilidad a la hora de explicar la siguiente sección
(\ref{sec:secuencias-de-juegos}) y algunos ejemplos posteriores.

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. 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$$

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 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. $\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}

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:

\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\};$
  $c \leftarrow \Enc(pk,m_b);\\$
  $\tilde{b} \leftarrow A_2(c)$
\end{game}

El Juego 1 define la propiedad de seguridad
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
$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 \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
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 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}

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 \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, 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 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.

\paragraph{Lenguaje de expresiones}
El lenguaje principal de especificación de EasyCrypt es el de las expresiones,
que define una serie de \textbf{tipos} (conjuntos de valores) y
\textbf{operadores} sobre ellos. En EasyCrypt, siguiendo la notación del cálculo
lambda tipado \cite{Church40}, la relación de tipado se representa con los dos
puntos. Así, (\rawec{b:bool}) denota la pertenencia del valor \rawec{b} al tipo
\rawec{bool}. EasyCrypt posee un potente sistema de tipos que soporta
polimorfismo y tipos de orden superior. Los tipos de orden superior están
parametrizados por otros tipos que se colocan delante: <<\rawec{int
  list}>> significa <<lista de enteros>>. Los tipos se pueden generalizar
usando una variable de tipo (variable precedida de una comilla simple):
<<\rawec{'a list}>> significa <<lista de cualquier tipo>>.

Los \textbf{operadores} son funciones definidas sobre tipos, y se introducen con
la palabra reservada <<\rawec{op}>>: (\rawec{op par : nat -> bool}). La aplicación
de un operador a un valor se realiza poniendo un espacio entre el operador y su
argumento: (\rawec{par 3}). Aunque los operadores se definen de forma abstracta (sin
proporcionar una implementación), la semántica de los operadores viene de la
definición de lemas y axiomas que describen su comportamiento de forma
observacional, o extensional. EasyCrypt asume que todos los tipos están
habitados, por lo que los operadores son funciones totales. Para soportar
operadores que reciban varios argumentos se usa la técnica de la
\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$.

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, label={lst:exprlang}]{}{}
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}

Las primeras dos líneas defininen los tipos \rawec{predicate} y
\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}).

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
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
(\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,
  label={lst:booldistr}]{}{}
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}.

\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}$
    | while $\mathcal{E}$ do $\mathcal{C}$
    | $\mathcal{V} \leftarrow \mathcal{P}(\mathcal{E}, ..., \mathcal{E})$
  $\mathcal{C} ::=$ skip
    | $\mathcal{I}$; $\mathcal{C}$
\end{bnf}

% % 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}
\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 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:

\begin{itemize}
\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 \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 (\textit{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 (\textit{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
  \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
  memoria al ser ejecutado.
\end{itemize}

\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 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 tácticas, label={lst: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 (\textit{head}) y cola
(\textit{tail}). Lo que aparece a continuación es la demostración del lema, con
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}
\textbf{SMT}(<<Satisfiability Modulo Theories>>) (ver sección
\ref{sec:arqu-de-easycrypt}). 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{Objetivos}
\label{sec: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, 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
  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.

  Trabajar con costes implica, por una parte, \textbf{especificarlos}, y por
  otra \textbf{usarlos para demostrar} lemas. La primera parte del proyecto
  consistirá en la implementación de un mecanismo que permita su
  \textbf{especificación}, ya que implementar un mecanismo para demostrar con
  ellos es una tarea considerablemente difícil y que supera los objetivos del
  Trabajo de Fin de Grado.

\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
  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
  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
\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
Isabelle/HOL\footnote{\url{http://isabelle.in.tum.de/}} son todas las
facilidades que proporciona para trabajar, concretamente, en el ámbito de la
criptografía. Algunos ejemplos son el soporte a demostraciones basadas en
secuencias de juegos, la riqueza de juicios (lógica de Hoare y variantes) o su
exhaustiva biblioteca estándar, que define tipos de datos habituales (cadenas de
bits, distribuciones probabilísticas, etc.), funciones para manipularlos,
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 seguridad en criptografía depende de la
capacidad computacional del adversario. Por tanto, existen muchas propiedades
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
algoritmos en EasyCrypt.

TODO referencias a dónde se explica qué.

\newpage
\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 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).

\subsection{Axioma de coste}
\label{sec:axioma-de-coste}

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}

EasyCrypt está escrito en el lenguaje de programación
OCaml\footnote{\url{http://ocaml.org/}}, que forma parte de la familia ML de
lenguajes especialmente diseñados para el desarrollo de demostraciones. La
unidad de compilación básica de OCaml es el \textbf{módulo}, consistente en un
fichero de implementación con extensión \textbf{.ml} y un fichero de interfaz
con extensión \textbf{.mli} donde se declaran las funciones, tipos, etc. La
compilación es relativamente compleja y se automatiza con ayuda de GNU
Make\footnote{\url{http://www.gnu.org/software/make/}} y
ocamlbuild\footnote{\url{http://caml.inria.fr/pub/docs/manual-ocaml-400/manual032.html}}.

EasyCrypt usa varios programas externos para llevar a cabo ciertas tareas, pero
los más destacables son los dos siguientes:

\begin{itemize}
\item
  \textbf{Resolvedores SMT}. Existen multitud de programas que deciden la
  satisfacibilidad de instancias SMT. Como ya se dijo anteriormente, una
  instancia de fórmula SMT está expresada en lógica de primer orden y tiene
  interpretaciones en teorías como los números reales, vectores, bits,
  etc. Durante una demostración en EasyCrypt se pueden invocar estos
  resolvedores para tratar de encontrar una solución que satisfaga el objetivo
  actual usando la táctica \rawec{smt}. Internamente, EasyCrypt estará
  comunicándose con uno o varios resolvedores y obteniendo la respuesa al
  problema, si es que existe. Para contar con una única interfaz de
  programación ante la diversidad de resolvedores, EasyCrypt usa la plataforma
  \textbf{Why3}\footnote{\url{http://why3.lri.fr/}}.
\item \textbf{Menhir}\footnote{\url{http://gallium.inria.fr/~fpottier/menhir/}}.
  Menhir es una biblioteca para generar analizadores léxicos y sintácticos en
  OCaml. Se verá con mayor profundidad en las secciones
  \ref{sec:modif-al-anal-lex} y \ref{sec:modif-al-anal-sin}, tras explicar las
  fases del análisis del lenguaje.
\end{itemize}

A fin de cuentas, EasyCrypt es un intérprete: lee un fichero fuente y realiza
acciones en función de su contenido. Por ello, el componente fundamental es el
\textbf{analizador del lenguaje}, cuya tarea es transformar el código fuente
(secuencia de caracteres) en un árbol sintáctico abstracto anotado con
información de tipos, o mostrar un error y finalizar en caso de que el programa
esté mal formado.

El análisis del lenguaje consta de varias fases encargadas de abordar niveles
de abstracción distintos. Conceptualmente, las fases de análisis son las
siguientes:

\begin{itemize}
\item \textbf{Análisis léxico}
Esta fase es la primera que se lleva a cabo y la que tiene un menor nivel de
abstracción; su entrada es el propio fichero fuente. Durante el análisis léxico
se transforma la secuencia de caracteres que forma el código fuente en unidades
mínimas de información (\textbf{tokens}): número, cadena de caracteres,
identificador, comentario, inicio de bloque, etc. La salida de esta fase es una
lista conteniendo todos los tokens que describen el programa original, formando
una estructura de datos muy simple pero más sencilla de recorrer y manejar.

\item \textbf{Análisis sintáctico} Durante esta fase se transforma la lista de
  tokens generada durante el análisis léxico en el denominado \textbf{árbol
    sintáctico abstracto} (AST), una estructura de datos que contiene la
  estructura sintáctica del código fuente. Este analizador está especificado por
  la gramática formal del lenguaje (gramáticas libres de contexto, por lo
  general), cuyas reglas determinan el algoritmo a seguir durante la
  construcción del árbol sintáctico.
\item \textbf{Análisis semántico/contextual}
Durante esta fase se recorre el árbol sintáctico generado previamente y se anota
con información de tipos, se construye la tabla de símbolos y se comprueba que
el programa, además de estar bien formado sintácticamente, tiene sentido
semánticamente.
\end{itemize}

EasyCrypt implementa cada una de estas etapas en tres módulos (EcLexer, EcParser
y EcTyping) y define las estructuras de datos intermedias en otros dos
(EcParseTree para el árbol sintáctico abstracto y EcFol para el árbol sintáctico
anotado con información de tipos). Los módulos EcLexer y EcParser hacen uso de
la biblioteca Menhir mencionada anteriormente para generar los
analizadores. Estos módulos contienen las definiciones de tokens y las reglas de
las gramáticas regular y libre de contexto usadas para indicar, respectivamente,
el comportamiento de los analizadores léxico y sintáctico.

El siguiente diagrama resume el proceso de análisis del lenguaje de EasyCrypt:

\tikzstyle{block} = [rectangle, draw, fill=blue!20,
    text width=5em, text centered, rounded corners, minimum height=4em]
\tikzstyle{invisbl} = [text width=5em, text centered, minimum height=4em]
\tikzstyle{line} = [draw, -latex']
\tikzstyle{cloud} = [draw, ellipse,fill=blue!10, node distance=3cm,
    minimum height=2em]

\begin{center}
\begin{tikzpicture}[node distance = 3cm, auto]
    % Nodes
    \node [invisbl] (upper) {};
    \node [block, below of=upper] (lexer) {EcLexer};
    \node [block, below of=lexer] (parser) {EcParser};
    \node [block, below of=parser] (typing) {EcTyping};
    \node [invisbl, below of=typing] (lower) {...};
    \node [cloud, left of=lexer] (menhir1) {Menhir};
    \node [cloud, left of=parser] (menhir2) {Menhir};
    % Edges
    \path [line,dashed] (menhir1) -- (lexer);
    \path [line,dashed] (menhir2) -- (parser);
    \path [line]
    (upper) edge [] node {\textbf{Código fuente}} (lexer)
    (lexer) edge [] node {\textbf{Tokens} (EcParser/EcLexer)} (parser)
    (parser) edge [] node {\textbf{AST} (EcParseTree)} (typing)
    (typing) edge [] node {\textbf{AST tipado} (EcFol)} (lower);
\end{tikzpicture}
\end{center}

Para la implementación del coste es necesario modificar cada uno de los módulos
involucrados en este proceso. A continuación analizaremos las etapas de la
implementación tanto del operador especial de coste como del axioma de coste.

\section{Modificaciones al analizador léxico}
\label{sec:modif-al-anal-lex}

EcLexer es el módulo que define el analizador léxico. Este módulo está contenido
en el fichero <<ecLexer.mll>>, cuya extensión refleja el hecho de que no es un
fichero OCaml válido, sino un fichero de definición de analizadores léxicos que
deberá ser procesado por Menhir para generar el analizador real.

La función principal de este módulo es asociar expresiones regulares con sus
tokens correspondientes. Por ejemplo, la expresión regular \textbf{[0-9]*} emite
el token UINT (Unsigned INTeger) parametrizado por el valor de la cadena
coincidente convertida a número entero.

La única modificación que debemos realizar a este módulo es el reconocimiento de
nuestros dos nuevos tokens: \textbf{cost} y \textbf{caxiom}. Estos tokens son
palabras reservadas: identificadores con significado especial dentro del
lenguaje. En EcLexer, cuando se encuentra un identificador, se busca dentro de
un \textbf{hash map} que relaciona palabras reservadas con sus respectivos
tokens: en caso de existir la clave, se emite el token asociado; en caso
contrario, se emite el token genérico IDENT. Por tanto, basta con añadir dos
entradas a este hash map para que EcLexer emita los tokens COST y CAXIOM cuando
encuentre los identificadores `cost` y `caxiom`, respectivamente:

\begin{ocaml}
\begin{alltt}

\Clet{let} _keywords \Cnonalphakeyword{=} \Cnonalphakeyword{[}
  \Cstring{"admit"} \Cnonalphakeyword{,} \Cconstructor{ADMIT}\Cnonalphakeyword{;}
  \Cstring{"forall"}\Cnonalphakeyword{,} \Cconstructor{FORALL}\Cnonalphakeyword{;}
  \Cstring{"exists"}\Cnonalphakeyword{,} \Cconstructor{EXIST}\Cnonalphakeyword{;}
  \Cstring{"pragma"}\Cnonalphakeyword{,} \Cconstructor{PRAGMA}\Cnonalphakeyword{;}
  \Ccomment{(* ... *)}

  \Cstring{"cost"}  \Cnonalphakeyword{,} \Cconstructor{COST}\Cnonalphakeyword{;}
  \Cstring{"caxiom"}\Cnonalphakeyword{,} \Cconstructor{CAXIOM}
\Cnonalphakeyword{]}

\Clet{let} keywords \Cnonalphakeyword{=} \Cconstructor{Hashtbl}\Cnonalphakeyword{.}create 100
\Clet{let} \Cnonalphakeyword{_} \Cnonalphakeyword{=} \Cconstructor{List}\Cnonalphakeyword{.}iter
    \Cnonalphakeyword{(}\Cfun{fun} \Cnonalphakeyword{(}x\Cnonalphakeyword{,} y\Cnonalphakeyword{)} \Cnonalphakeyword{->} \Cconstructor{Hashtbl}\Cnonalphakeyword{.}add keywords x y\Cnonalphakeyword{)} _keywords
\end{alltt}
\end{ocaml}

\section{Modificaciones al analizador sintáctico}
\label{sec:modif-al-anal-sin}

TODO: Más Menhir, modificaciones en EcParser y EcParseTree

\section{Modificaciones al analizador semántico}
\label{sec:modif-al-anal-sem}

TODO: Modificaciones en EcTyping, EcFol, EcEnv, EcScope, EcTheory, EcPV,
EcCommands... :)

\section{Modificaciones al pretty-printer}
\label{sec:modif-al-anal-sem}

TODO: Modificaciones en EcPrinting

\chapter{DESARROLLO: INTERFAZ WEB}

Como ya mencionamos en la sección \ref{sec:objetivos}, EasyCrypt es un programa
complejo y una de las prioridades para favorecer su adopción es facilitar su uso
en la medida de lo posible.

A lo largo de este capítulo se describirá el proceso de diseño e implementación
de una interfaz web para trabajar con EasyCrypt remotamente desde un
navegador.

\section{Diseño}
\label{sec:diseno-1}

La mayor inspiración que tenemos para el diseño es el del propio Proof General,
que es con lo que se trabaja en EasyCrypt normalmente:

//
\\
\\
// [screenshot de Emacs + ProofGeneral]
\\
\\
//

En nuestro caso, la parte fundamental de la interfaz será el editor de código
fuente. Los resultados de la evaluación del código se mostrarán a la derecha del
mismo, como en Proof General, y añadiremos un navegador de ficheros (ya que el
código se almacena remotamente). Por último, necesitaremos una barra de
navegación en la parte superior para realizar actividades complementarias como
crear proyectos, iniciar/cerrar sesión, etc. En la figura \ref{fig:prototype} se
puede ver el primer prototipo de la página principal de la web\footnote{A pesar
  de que la web debe contar con muchas otras páginas (pantalla de inicio,
  formulario de creación de cuentas de usuario, etc.), en este documento no se
  mencionarán por no ser tan relevantes en su interacción con EasyCrypt.}.

\begin{figure}[h]
    \centering
    \includegraphics[width=0.8\textwidth]{img/web-prototype.png}
    \caption{Diseño de la web}
    \label{fig:prototype}
\end{figure}

En cuanto al diseño del sistema en general, se han utilizado varios marcos y
herramientas web para implementar toda la funcionalidad necesaria en un nivel
superior, evitando en la medida de lo posible el uso directo de las tecnologías
web básicas (HTML, CSS, JavaScript), más tediosas y propensas a error:

\begin{itemize}
\item \textbf{Django}\footnote{\url{https://www.djangoproject.com/}}. La base
  del sistema es Django, un marco web usado para implementar la funcionalidad en
  el lado del servidor. Django está escrito en Python, que es también el
  lenguaje que se usa para implementar el resto de la funcionalidad. Se ha
  utilizado el módulo
  crispy-forms\footnote{\url{https://django-crispy-forms.readthedocs.org/en/latest/}}
  para poder definir los formularios HTML directamente en Python.

\item \textbf{Twitter
    Bootstrap}\footnote{\url{http://getbootstrap.com/}}. Bootstrap es un marco
  orientado al desarrollo de interfaces web. Sus características más
  interesantes son la gestión del esquema de la web usando un sistema de
  rejillas, una gran cantidad de clases CSS predefinidas y funcionalidad
  JavaScript como generación de ventanas <<modales>> (flotantes).

\item \textbf{jQuery}\footnote{\url{http://jquery.com/}}. En el lado del cliente
  hay mucha funcionalidad dinámica que debe ser implementada en JavaScript.
  Buena parte de este trabajo consiste en manipular la estructura HTML del
  documento: el DOM. Para este tipo de tarea se ha usado jQuery, que tiene una
  gran biblioteca de funciones para crear, eliminar, buscar y modificar nodos
  HTML, por ejemplo a la hora de mostrar el navegador de ficheros. Asimismo,
  para poder tener varios ficheros abiertos al mismo tiempo, se ha usado un
  widget de gestión de pestañas proporcionado por la biblioteca jQuery
  UI\footnote{\url{http://jqueryui.com/}}.

\item \textbf{Ace}\footnote{\url{http://ace.c9.io/}}. Ace es un editor de código
  fuente diseñado para integrarse en sitios web. Además, como permite que la
  misma instancia del editor pueda tener varias sesiones distintas (estados),
  podemos asociar una sesión a cada pestaña (fichero abierto) y guardar por
  separado sus estados: posición del cursor, código evaluado, etc.

\item \textbf{WebSockets}\footnote{\url{http://www.websocket.org/}}. Para
  evaluar remotamente el código definido en el editor es necesario disponer de
  una conexión persistente y bidireccional con un servidor que ejecute una
  instancia de EasyCrypt. Precisamente por estas necesidades se ha decidido
  implementar las comunicaciones entre el cliente web y el servidor de EasyCrypt
  usando WebSockets, una tecnología relativamente reciente pero soportada por
  prácticamente todos los navegadores actuales (a la fecha de redacción del
  presente documento, el único navegador que no soporta WebSockets es Opera
  Mini). Para la implementación de WebSockets en el lado del servidor de
  EasyCrypt se ha usado una biblioteca para Python llamada
  \textbf{Tornado}\footnote{\url{http://www.tornadoweb.org//}}.
\end{itemize}

Todas estas partes se integran entre sí tal y como se muestra en el siguiente
esquema:

\tikzstyle{block} = [rectangle, draw, fill=blue!20,
    text width=5em, text centered, rounded corners, minimum height=4em]
\tikzstyle{line} = [draw]
\tikzstyle{cloud} = [draw, ellipse,fill=blue!10, node distance=3cm,
    minimum height=2em]
\tikzstyle{ncloud} = [draw, ellipse,fill=blue!10, node distance=2cm,
    minimum height=2em]

\begin{center}
\begin{tikzpicture}[node distance = 6cm, auto]
    % Nodes
    \node [block] (client) {Cliente};
    \node [block, right of=client] (wserver) {Servidor web};
    \node [block, below of=wserver, node distance=4cm] (ecserver) {Servidor EasyCrypt};

    \node [ncloud, above of=client] (bootstrap) {Twitter Bootstrap};
    \node [cloud, left of=client] (jquery) {jQuery};
    \node [ncloud, below of=client] (ace) {Ace Editor};

    \node [cloud, right of=wserver] (django) {Django};
    \node [ncloud, above of=django] (crispy) {crispy_forms};

    \node [cloud, right of=ecserver, fill=green!20] (easycrypt) {EasyCrypt};
    \node [ncloud, below of=ecserver] (tornado) {Tornado};

    % Edges
    \path [line,dashed] (bootstrap) -- (client);
    \path [line,dashed] (jquery) -- (client);
    \path [line,dashed] (ace) -- (client);

    \path [line,dashed] (django) -- (wserver);
    \path [line,dashed] (django) -- (crispy);

    \path [line,dashed] (easycrypt) -- (ecserver);
    \path [line,dashed] (tornado) -- (ecserver);

    \path [line]
    (client) edge [] node {\textbf{HTTP}} (wserver)
    (client) edge [] node {\textbf{WebSockets}} (ecserver);
\end{tikzpicture}
\end{center}

A continuación veremos cómo se ha implementado cada uno de estos componentes y
formado el sistema completo.

\section{Implementación: cliente}

TODO

\section{Implementación: servidor web}

TODO

\section{Implementación: servidor EasyCrypt}

TODO

\chapter{RESULTADOS Y CONCLUSIONES}

\chapter{CONTRIBUCIONES}

\chapter{ANEXOS}

\pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}

\end{document}