From 93cb47db104cd4e2ffcee8b2bfa02281ca1ae1ad Mon Sep 17 00:00:00 2001 From: Guillermo Ramos Date: Mon, 2 Jun 2014 00:31:21 +0200 Subject: Cambios varios --- memoria.tex | 125 ++++++++++++++++++++++++++++++++++-------------------------- 1 file 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 <> y <> (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} -- cgit v1.2.3