diff options
Diffstat (limited to 'memoria.tex')
| -rwxr-xr-x | memoria.tex | 80 |
1 files changed, 52 insertions, 28 deletions
diff --git a/memoria.tex b/memoria.tex index 25167db..64bd1ce 100755 --- a/memoria.tex +++ b/memoria.tex @@ -1,7 +1,3 @@ -% Preguntas: -% - BNF? -% - Numeración independiente Juego/Ejemplo/... en lstlisting - \documentclass[12pt,a4paper,parskip=full]{scrreprt} \usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry} @@ -94,23 +90,22 @@ 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. Cada una de estas funciones -usa una 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 se definen de la siguiente forma: +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: -$$\Enc(pk,t) = c$$ -$$\Dec(sk,c) = t$$ +$$\Enc(pk,T) = C$$ +$$\Dec(sk,C) = T$$ -Donde $t$ es el \textbf{texto} (o \textbf{mensaje}) y $c$ su -\textbf{cifra}. Intuitivamente, $t$ es cualquier información y $c$ es el -resultado de modificarla hasta hacerla ininteligible. 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: +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: -$$\forall t. \Dec(sk, \Enc(pk, t)) = t$$ +$$\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 @@ -126,15 +121,13 @@ 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=tb, - caption=IND-CPA (fuente: \cite{BartheGB09})] +\begin{game}[caption=IND-CPA (\cite{BartheGB09})]{}{} $(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{lstlisting} +\end{game} El Juego 1 define la propiedad de seguridad IND-CPA\footnote{Indistinguishability under Chosen Plaintext Attack} de los @@ -209,8 +202,7 @@ $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]{} +\begin{easycrypt}[caption=Lenguaje de expresiones]{}{} type 'a predicate = 'a -> bool. datatype 'a option = None | Some of 'a. op find : 'a predicate -> 'a list -> 'a option. @@ -328,7 +320,6 @@ Para demostrar juicios, EasyCrypt cuenta con un lenguaje basado en tácticas (la fórmula que se está demostrando) hasta que el último resuelve finalmente el objetivo. -\renewcommand{\lstlistingname}{Ejemplo} \begin{easycrypt}[caption=Uso de tactics]{} lemma hd_tl_cons : forall (xs:'a list), @@ -440,13 +431,46 @@ 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{Ejemplo de uso} +\label{sec:ejemplo-de-uso} + +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. + +\section{Objetivos} + +Operador, axioma. + \section{Arquitectura de EasyCrypt} +\label{sec:arqu-de-easycrypt} + +EasyCrypt es un programa complejo, y antes de poder modificarlo hay que entender +qué partes lo integran y cómo está organizado a nivel de código. + +\begin{enumerate} +\item Lexer +\item Parser +\item AST +\item ... +\end{enumerate} + +% ProofGeneral +% EasyCrypt +% Why3 +% Solvers -\section{Ejemplo de uso (del coste)} +% \section{Ejemplo de uso (del coste)} -$$\forall (lst : [\alpha]) (p : \alpha -> bool) (x : \alpha). cost[find, p, lst] -<= cost[p, x] * length(lst)$$ +% $$\forall (lst : [\alpha]) (p : \alpha -> bool) (x : \alpha). cost[find, p, lst] +% <= cost[p, x] * length(lst)$$ \chapter{DESARROLLO: INTERFAZ WEB} |