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 --- defs.tex | 8 +++---- memoria.tex | 77 ++++++++++++++++++++++++++++++++----------------------------- 2 files changed, 44 insertions(+), 41 deletions(-) diff --git a/defs.tex b/defs.tex index a71c390..ac2b955 100755 --- a/defs.tex +++ b/defs.tex @@ -146,13 +146,13 @@ keywordsprefix={'}, morekeywords=[1]{unit,bool,int,real,bitstring,array,list,matrix,word}, morekeywords=[2]{type,datatype,op,axiom,lemma,module,pred,const,declare}, - morekeywords=[3]{var,fun}, + morekeywords=[3]{var,fun,charfun}, morekeywords=[4]{while,if}, morekeywords=[5]{theory,end,clone,import,export,as,with,section}, morekeywords=[6]{forall,exists,lambda}, - morekeywords=[7]{idtac,change,beta,iota,zeta,logic,delta,simplify,congr,generalize, - pose,split,left,right,case,intros,cut,elim,apply,rewrite,elimT,subst, - progress,trivial}, + morekeywords=[7]{idtac,change,beta,iota,zeta,logic,delta,simplify,congr, + generalize,pose,split,left,right,case,intros,cut,elim,apply,rewrite,elimT, + subst,progress,trivial}, morekeywords=[8]{by,assumption,smt,reflexivity}, morekeywords=[9]{first,last,do,try}, morecomment=[n][\itshape]{(*}{*)}, 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 (<>) 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 <>), y se usa una comilla +simple delante de las variables de tipo (\rawec{'a list} significa <>). + \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 <> 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 \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 +<> y <> (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}(<>). 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