From 619ce91ac41d3065ee6027693b692db313202820 Mon Sep 17 00:00:00 2001 From: Guillermo Ramos Date: Sat, 24 May 2014 17:24:42 +0200 Subject: Commit inicial: Introducción --- .gitignore | 10 ++ Makefile | 14 +++ bib.bib | 75 ++++++++++++ defs.tex | 340 ++++++++++++++++++++++++++++++++++++++++++++++++++++ memoria.pdf | Bin 0 -> 203305 bytes memoria.tex | 390 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 829 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100755 bib.bib create mode 100755 defs.tex create mode 100755 memoria.pdf create mode 100755 memoria.tex diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..1d4c2d3 --- /dev/null +++ b/.gitignore @@ -0,0 +1,10 @@ +auto +*.aux +*.bbl +*.blg +*.brf +*.dvi +*.log +*.lol +*.out +*.log diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..9c825ab --- /dev/null +++ b/Makefile @@ -0,0 +1,14 @@ +all: bib tex + +tex: + pdflatex memoria + pdflatex memoria + +bib: + pdflatex memoria + bibtex memoria + +clean: + rm -rf *.aux *.bbl *.blg *.log + +.PHONY : tex bib clean diff --git a/bib.bib b/bib.bib new file mode 100755 index 0000000..4ae6ee4 --- /dev/null +++ b/bib.bib @@ -0,0 +1,75 @@ +@article{Shoup04, + author = {Victor Shoup}, + title = {Sequences of games: a tool for taming complexity in security + proofs}, + journal = {IACR Cryptology ePrint Archive}, + volume = 2004, + year = 2004, + pages = 332, + ee = {http://eprint.iacr.org/2004/332}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@inproceedings{BartheGHB11, + author = {Gilles Barthe and + Benjamin Gr{\'e}goire and + Sylvain Heraud and + Santiago Zanella B{\'e}guelin}, + title = {Computer-Aided Security Proofs for the Working Cryptographer}, + booktitle = {CRYPTO}, + year = {2011}, + pages = {71-90}, + ee = {http://dx.doi.org/10.1007/978-3-642-22792-9_5}, + crossref = {DBLP:conf/crypto/2011}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/crypto/2011, + editor = {Phillip Rogaway}, + title = {Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology + Conference, Santa Barbara, CA, USA, August 14-18, 2011. + Proceedings}, + booktitle = {CRYPTO}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {6841}, + year = {2011}, + isbn = {978-3-642-22791-2}, + ee = {http://dx.doi.org/10.1007/978-3-642-22792-9}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@inproceedings{BartheGB09, + author = {Gilles Barthe and + Benjamin Gr{\'e}goire and + Santiago Zanella B{\'e}guelin}, + title = {Formal certification of code-based cryptographic proofs}, + booktitle = {POPL}, + year = {2009}, + pages = {90-101}, + ee = {http://doi.acm.org/10.1145/1480881.1480894}, + crossref = {DBLP:conf/popl/2009}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/popl/2009, + editor = {Zhong Shao and + Benjamin C. Pierce}, + title = {Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on + Principles of Programming Languages, POPL 2009, Savannah, + GA, USA, January 21-23, 2009}, + booktitle = {POPL}, + publisher = {ACM}, + year = {2009}, + isbn = {978-1-60558-379-2}, + ee = {http://dl.acm.org/citation.cfm?id=1480881}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@article{GoldwasserM84, + author = {Shafi Goldwasser and + Silvio Micali}, + title = {Probabilistic Encryption}, + journal = {J. Comput. Syst. Sci.}, + volume = {28}, + number = {2}, + year = {1984}, + pages = {270-299}, + ee = {http://dx.doi.org/10.1016/0022-0000(84)90070-9}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} diff --git a/defs.tex b/defs.tex new file mode 100755 index 0000000..7a9c73d --- /dev/null +++ b/defs.tex @@ -0,0 +1,340 @@ +% Source: EasyCrypt manual (https://www.easycrypt.info) + +% !TeX root = easycrypt.tex +%% Names +% Tools + \newcommand{\EasyCrypt}{\textsf{EasyCrypt}\xspace} + \newcommand{\CertiCrypt}{\textsf{CertiCrypt}\xspace} + \newcommand{\CertiPriv}{\textsf{CertiPriv}\xspace} + \newcommand{\SsReflect}{\textsf{SsReflect}\xspace} + \newcommand{\Coq}{\textsf{Coq}\xspace} + \newcommand{\WhyThree}{\textsf{Why3}\xspace} + +% Languages and Logics + \newcommand{\pWHILE}{\textsf{p}\textsc{While}\xspace} + \newcommand{\pRHL}{\textsf{pRHL}\xspace} + +% Version numbers + \newcommand{\ECversion}{0.$\beta$\xspace} + +%% Misc +\newcommand{\DONE}{}% {{\color{red}DONE}} +\newcommand{\Example}{\paragraph*{Example}} +\newcommand{\Syntax}{\paragraph*{Syntax}} +\newcommand{\Description}{\paragraph*{Description}} +\setcounter{secnumdepth}{3} +\renewcommand{\thesubsubsection}{\arabic{chapter}.\arabic{section}.\arabic{subsection}.\arabic{subsubsection}} +\newbox\minicodebox +\newenvironment{minicode}[1]{% +\minipage[t]{#1\linewidth} % +\centering % +\verbatim % +}{% +\endverbatim % +\endminipage% +} + + +\newcounter{alarmcounter} +\setcounter{alarmcounter}{1} +\newcommand{\alarm}[1] + {\begingroup + \def\thefootnote{{\normalsize\color{red}(\arabic{footnote})}} + \footnote{\textsf{\textbf{{\color{red}\sc \bf ALARM:} + #1}}}\endgroup} + + +\newcommand{\infr}[2]{ +{\renewcommand{\arraystretch}{1.1} +\begin{array}{c} +{#1}\\ +\hline +{#2} +\end{array}}} + +%% Indexing +\newcommand{\define}[2][]{\emph{#2}\index{easycrypt}{\ifx\else#1\fi}} + +%% Cross-referencing +% \providecommand{\eqref}[1]{\textup{(\ref{#1})}} +% \providecommand{\eqdef}{\raisebox{-.2ex}[.2ex]{$\stackrel{\textrm{\tiny def}}{~=~}$}} + +%% IDK +\newcommand{\rname}[1]{[\textsc{#1}]} +\newcommand{\result}{\mathsf{res}} + +%% Security properties and schemes +\newcommand{\INDCPA}{\textsf{IND-CPA}\xspace} +\newcommand{\INDCCAone}{\textsf{IND-CCA1}\xspace} +\newcommand{\INDCCA}{\textsf{IND-CCA}\xspace} +\newcommand{\EFCMA}{\textsf{EF-CMA}\xspace} +\newcommand{\LCDH}{\ensuremath{\mathsf{LCDH}}\xspace} +\newcommand{\CDH}{\textsf{CDH}\xspace} +\newcommand{\DDH}{\textsf{DDH}\xspace} +\newcommand{\ElGamal}{\textsf{ElGamal}\xspace} +\newcommand{\HElGamal}{\textsf{HElGamal}\xspace} +\newcommand{\RSA}{\textsf{RSA}\xspace} +\newcommand{\OAEP}{\textsf{OAEP}\xspace} +\newcommand{\FDH}{\textsf{FDH}\xspace} +\newcommand{\HMAC}{\textsf{HMAC}\xspace} +\newcommand{\CS}{\textsf{CS}\xspace} +\newcommand{\Skein}{\textsf{Skein}\xspace} +\newcommand{\TCR}{\textsf{TCR}\xspace} + +\newcommand{\KG}{\mathcal{KG}} +\newcommand{\Enc}{\mathcal{E}} +\newcommand{\Dec}{\mathcal{D}} + +%% Complexity and termination +\newcommand{\lossless}{\mathsf{lossless}} + +%% Sets +\newcommand{\zeroone}{[0,1]} +\newcommand{\bit}{\{0,1\}} +\newcommand{\bitstring}[1]{\ensuremath{\bit^{#1}}} +\newcommand{\bool}{\mathbb{B}} +\newcommand{\nat}{\mathbb{N}} +\newcommand{\real}{\mathbb{R}} +\newcommand{\option}[1]{#1_\bot} + +%% Mathematics +\newcommand{\conv}[1][]{\mathrel{\leftrightarrow^*_{#1}}} +\renewcommand{\Pr}[2]{\mathrm{Pr}\left[#1 : #2\right]} +\newcommand{\Prm}[3]{\mathrm{Pr}\left[#1,#3 : #2\right]} +\newcommand{\labs}{\left\lvert} +\newcommand{\rabs}{\right\rvert} +\newcommand{\charfun}{\mathds{1}} + +%% Distribution monad +\newcommand{\supp}{\mathsf{support}} +\newcommand{\range}[2]{\mathsf{range}~{#1}~{#2}} + +%% Semantics + +% \newcommand{\sem}[1]{\llbracket #1 \rrbracket} +\newcommand{\subst}[2]{\left[{}^{#2}/{}_{#1}\right]} +\newcommand{\fv}{\mathsf{fv}} +\newcommand{\modifies}{\mathsf{mod}} +\newcommand{\glob}{\mathsf{glob}} +\newcommand{\Env}{\mathcal{E}} + +%% Well-formed adversaries +%% Program Judgements +\newcommand{\Hoare}[3]{\left[{#1}:{#2}\Longrightarrow{#3}\right]} +\newcommand{\Equiv}[4]{\left[{#1}\sim{#2}:{#3}\Longrightarrow{#4}\right]} +\newcommand{\bdHoareS}[5]{{\Hoare{#1}{#2}{#3}}\,{#4}\,{#5}} +\newcommand{\HoareLe}[4]{\bdHoareS{#1}{#2}{#3}{\leq}{#4}} +\newcommand{\HoareEq}[4]{\bdHoareS{#1}{#2}{#3}{=}{#4}} +\newcommand{\HoareGe}[4]{\bdHoareS{#1}{#2}{#3}{\geq}{#4}} + + +% \newcommand{\Equiv}[4]{\models {#1} \sim {#2} : {#3} \Longrightarrow {#4}} +% \newcommand{\AEquiv}[6]{\models {#2} \sim_{#5,#6} {#3} : {#1} \Longrightarrow {#4}} +% \newcommand{\JAEquiv}[6]{{#2} \sim_{#5,#6} {#3} : {#1} \Longrightarrow {#4}} +% \newcommand{\EquivMem}[2]{\models {#1} \equiv {#2}} +% \newcommand{\EqObs}[4]{\models {#1} \simeq^{#3}_{#4} {#2}} +% \newcommand{\AEqObs}[5]{\models {#1} \simeq^{#3}_{{#4}} {#2} \preceq {#5}} +% \newcommand{\ACEqObs}[7] +% {\AEqObs{\left[ #1 \right]_{#6}}{\left[ #2 \right]_{#7}}{#3}{#4}{#5}} +% \newcommand{\Triple}[3]{\sem{#2} {#3} \preceq {#1}} +% \newcommand{\DTriple}[3]{\sem{#2} {#3} \succeq {#1}} +% \newcommand{\dequiv}[3]{{#1} \simeq_{#3} {#2}} +% \newcommand{\fequiv}[3]{{#1} =_{#3} {#2}} +% \newcommand{\Pre}{\Psi} +% \newcommand{\Post}{\Phi} +% \newcommand{\Inv}{\Phi} +\newcommand{\side}[1]{\langle #1 \rangle} +\newcommand{\sidel}{\side{1}} +\newcommand{\sider}{\side{2}} +% \newcommand{\eqobsin}{\mathsf{eqobs\_in}} +% \newcommand{\eqobsout}{\mathsf{eqobs\_out}} +\newcommand{\pre}{\Psi} +\newcommand{\post}{\Phi} +\newcommand{\bound}{\delta} +\newcommand{\ECinsupp}[2]{\mathec{Distr.in_supp}\,{#1}\,{#2}} +\newcommand{\insupp}[2]{{#1}\in\mathec{supp}\,{#2}} +%% Variables + +% \newcommand{\LH}{\gl{L}_H} +% \newcommand{\LD}{\gl{L}_\Dec} +% \newcommand{\cdef}{\gl{\gamma_\mathsf{def}}} +\newcommand{\var}[1]{\ensuremath{\mathit{#1}} \xspace} + +%% Constants and operators +% TODO: Update! +\newcommand{\true}{\mathsf{true}} +\newcommand{\false}{\mathsf{false}} +\newcommand{\nil}{\mathsf{nil}} +\newcommand{\hd}{\mathsf{hd}} +\newcommand{\tl}{\mathsf{tl}} +\newcommand{\app}{\mathbin{+\mkern-7mu+}} +\newcommand{\concat}{\parallel} +\newcommand{\xor}{\oplus} +\newcommand{\msb}[2]{[#1]^{#2}} +\newcommand{\lsb}[2]{[#1]_{#2}} +\newcommand{\dom}{\mathsf{dom}} +\newcommand{\ran}{\mathsf{ran}} +\newcommand{\fst}{\mathsf{fst}} +\newcommand{\snd}{\mathsf{snd}} +\newcommand{\some}[1]{#1} +\newcommand{\none}{\bot} + +\newcommand{\Int}{\mathsf{Int}} +\newcommand{\tint}{\mathsf{int}} + +\newcommand{\tbool}{\mathsf{bool}} + +%% Language +% TODO: Update! +\newcommand{\Skip}{\mathsf{skip}} +\newcommand{\Seq}[2]{#1;\ #2} +\newcommand{\Ass}[2]{#1 \leftarrow #2} +\newcommand{\Rand}[2]{#1 \stackrel{\raisebox{-.25ex}[.25ex]% +{\tiny $\mathdollar$}}{\raisebox{-.2ex}[.2ex]{$\leftarrow$}} #2} +\newcommand{\Randi}[2]{\Rand{#1}{[0..#2]}} +\newcommand{\Randb}[1]{\Rand{#1}{\bit}} +\newcommand{\Randbs}[2]{\Rand{#1}{\bitstring{#2}}} +\newcommand{\Cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} +\newcommand{\Condt}[2]{\mathsf{if}\ #1\ \mathsf{then}\ #2} +\newcommand{\Else}{\mathsf{else}\ } +\newcommand{\Elsif}{\mathsf{elsif}\ } +\newcommand{\nWhile}[3]{\mathsf{while}_{#1}\ #2\ \mathsf{do}\ #3} +\newcommand{\While}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2} +\newcommand{\Call}[3]{#1 \leftarrow #2\mathsf{(}#3\mathsf{)}} +\newcommand{\Return}{\mathsf{return}} +% \newcommand{\Assert}[1]{\mathsf{assert}~#1} + +%% Tactics +\newcommand{\tacname}{Error tacname} +\newcommand{\vtacname}{Error tacname} +\newcommand{\vararg}[1]{\ec{#1}} +\newcommand{\cstarg}[1]{\ec{#1}} +\newcommand{\typarg}[1]{\textit{#1}} +\newcommand{\tacarg}[2]{(\vararg{#1}:\typarg{#2})} + +\newcommand{\addTacticIdx}[2]{\index{#1}{#2@\rawec{#2}}} + +\newcommand{\addTacticNoIdx}[2]{ + \renewcommand{\tacname}{\rawec{#1}} + \renewcommand{\vtacname}{#1} + \subsubsection{#1} + \Syntax \ec{#1} #2 + \Description} + +\newcommand{\addTacticPlain}[2]{ + \renewcommand{\tacname}{\rawec{#1}} + \renewcommand{\vtacname}{#1} + \subsubsection{#1} + \Syntax {#2} + \Description} + +\newcommand{\addTactic}[3]{ + \addTacticIdx{#1}{#2} + \addTacticNoIdx{#2}{#3}} + +%% Language definition +\lstnewenvironment{easycrypt}[2][]% + {\lstset{language=easycrypt,caption={#2},#1}}% + {} + +\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline[language=easycrypt,#1]{#2}} +\newcommand{\mathec}[1]{\mbox{\rawec{#1}}} +\newcommand{\ec}[2][basicstyle=\normalsize\sffamily]{\lstinline[language=easycrypt,style=easycrypt-pretty,#1]{#2}} + +\newcommand{\ecimport}[4][]{\lstinputlisting[language=easycrypt,linerange=#4,caption=#2,#1]{#3}} + +\lstdefinelanguage{easycrypt}{ + style=easycrypt-default, +% procnamekeys={op,pred,fun}, +% procnamestyle={\sffamily\itshape}, + 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=[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=[8]{by,assumption,smt,reflexivity}, + morekeywords=[9]{first,last,do,try}, +% moredirectives={prover,print}, % Incomplete + morecomment=[n][\itshape]{(*}{*)}, + morecomment=[n][\bfseries]{(**}{*)} +} + +\lstdefinestyle{easycrypt-default}{ + columns=fullflexible, + % captionpos=b, + frame=tb, + xleftmargin=.1\textwidth, + xrightmargin=.1\textwidth, + rangebeginprefix={(**\ begin\ }, + rangeendprefix={(**\ end\ }, + rangesuffix={\ *)}, + includerangemarker=false, + basicstyle=\small\sffamily, + identifierstyle={}, + keywordstyle=[1]{\itshape\color{OliveGreen}}, + keywordstyle=[2]{\bfseries\color{Blue}}, + keywordstyle=[3]{\bfseries}, + keywordstyle=[4]{\bfseries}, + keywordstyle=[5]{\bfseries\color{OliveGreen}}, + keywordstyle=[6]{\itshape\color{Blue}}, + keywordstyle=[7]{\color{Blue}}, + keywordstyle=[8]{\color{Red}}, + keywordstyle=[9]{\color{OliveGreen}}, + literate={phi}{{$\!\phi\,$}}1 + {phi1}{{$\!\phi_1$}}1 + {phi2}{{$\!\phi_2$}}1 + {phi3}{{$\!\phi_3$}}1 + {phin}{{$\!\phi_n$}}1 +} + +\lstdefinestyle{easycrypt-pretty}{ + basicstyle=\small\sffamily, + literate={:=}{{$\mathrel{\gets}$}}1 + {<=}{{$\mathrel{\leq}$}}1 + {>=}{{$\mathrel{\geq}$}}1 + {<>}{{$\mathrel{\neq}$}}1 + {=\$}{{$\stackrel{\$}{\gets}$}}1 + {forall}{{$\forall$}}1 + {exists}{{$\exists$}}1 + {->}{{$\rightarrow\;$}}1 + {<-}{{$\leftarrow\;$}}1 + {<->}{{$\leftrightarrow\;$}}1 + {<=>}{{$\Leftrightarrow\;$}}1 + {=>}{{$\Rightarrow\;$}}1 + {==>}{{$\Rrightarrow\;$}}1 + {\/\\}{{$\wedge$}}1 + {\\\/}{{$\vee$}}1 + {.\[}{{[}}1 + {''ora}{{$\mathrel{||}$}}1 %needed for correct display in index + {'a}{{\color{OliveGreen}$\alpha\,$}}1 + {'b}{{\color{OliveGreen}$\beta\,$}}1 + {'c}{{\color{OliveGreen}$\gamma\,$}}1 + {'t}{{\color{OliveGreen}$\tau\,$}}1 + {'x}{{\color{OliveGreen}$\chi\,$}}1 + {lambda}{{$\lambda\,$}}1 +} + +%% Typesetting +\newcommand{\titledbox}[4]{{\color{#1}\fbox{\begin{minipage}{#2}{\textbf{#3:} \color{black}#4}\end{minipage}}}} +\newcommand{\warningbox}[1]{\titledbox{red}{.9\textwidth}{Warning}{#1}} +\newcommand{\futurebox}[1]{\titledbox{blue}{.9\textwidth}{Future}{#1}} + + + +\newcommand{\NotDocumented}{ + \begin{center}{\color{blue}\fbox{\begin{minipage}{120pt}{\centering + \textbf{Not yet documented}} + \end{minipage}}}\end{center}} +\newcommand{\NotImplemented}{ + \begin{center}{\color{blue}\fbox{\begin{minipage}{120pt}{\centering + \textbf{Not yet implemented}} + \end{minipage}}}\end{center}} +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "easycrypt" +%%% End: \ No newline at end of file diff --git a/memoria.pdf b/memoria.pdf new file mode 100755 index 0000000..bfccbb7 Binary files /dev/null and b/memoria.pdf differ diff --git a/memoria.tex b/memoria.tex new file mode 100755 index 0000000..0fab1a6 --- /dev/null +++ b/memoria.tex @@ -0,0 +1,390 @@ +% Preguntas: +% - BNF? +% - Numeración independiente Juego/Ejemplo/... en lstlisting + +\documentclass[12pt,a4paper]{article} + +\usepackage[spanish]{babel} \usepackage[utf8]{inputenc} \usepackage{url} +\usepackage{parskip} \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,linktoc=all,citecolor=blue]{hyperref} + +\setlength\voffset{-1.2in} \setlength\hoffset{-0.7in} \setlength\topmargin{3cm} +\setlength\textwidth{16cm} \setlength\headsep{0cm} + +\input{defs} + +\title{Trabajo de fin de Grado} \author{Guillermo Ramos Gutiérrez - r090050} +\date{TODO} + +\begin{document} +\maketitle +\pagebreak + +\section{Introducción} + +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. 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). + +\subsection{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 +representados como programas probabilísticos: + +\renewcommand{\lstlistingname}{Juego} +\begin{lstlisting}[mathescape=true,frame=single, + caption=IND-CPA (fuente: \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} + +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 +$(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 +\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 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, +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. + +\subsection{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 \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 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} + +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 +\textbf{expresiones}, que define una serie de tipos y operadores sobre +ellos. EasyCrypt soporta tipos polimórficos de orden superior. Los operadores +son funciones totales definidas sobre tipos (conjuntos de valores). Aunque los +operadores se definen de forma abstracta (sin proporcionar una implementación), +EasyCrypt asume que todos los tipos están habitados, por lo que cualquier +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$. + +\newpage +\renewcommand{\lstlistingname}{Ejemplo} +\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. +axiom find_head : + forall (x : bool) (l : bool list), + hd l = x => find (lambda e, e = x) l = Some x. +\end{easycrypt} + +\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 +(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]{} +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}. + +\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}$ + | 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{lstlisting} + +% % 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} +% +% ::= '=' +% \alt `for' `=' `to' `do' +% \alt `{' `}' +% \alt +% +% ::= `;' | +% +% \end{grammar} + +\subsection{Lenguajes de demostración} + +Estos lenguajes se usan para definir lemas y demostrarlos. + +\paragraph{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 +(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 (\textbf{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 + 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 + 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 (\textbf{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 + \textit{relaciones} entre las memorias de los dos programas, por lo que este + tipo de juicios expresa una \textit{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{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. + +\renewcommand{\lstlistingname}{Ejemplo} +\begin{easycrypt}[caption=Uso de 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 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). + +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. + +\pagebreak +\section{Motivación y 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, 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. + + Para poder trabajar con costes, es necesario hacer dos cosas: especificarlos y + trabajar con ellos (es decir, que en el desarrollo de una demostración se + pueda tenerlos en cuenta a la hora de derivar conclusiones). La primera parte + del proyecto consistirá en la implementación de un mecanismo que permita + \textbf{especificar} los costes computacionales (implementar un mecanismo para + \textbf{trabajar} con ellos es una tarea considerablemente difícil y que se + escapa a los recursos temporales del TFG). + +\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 Emacs + (editor de texto), 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 +\section{Desarrollo: Coste de algoritmos} + +TODO TODO TODO + +\subsection{Arquitectura de EasyCrypt} + +\subsection{Ejemplo de uso (del coste)} + +$$\forall (lst : [\alpha]) (p : \alpha -> bool) (x : \alpha). cost[find, p, lst] +<= cost[p, x] * length(lst)$$ + +\pagebreak +\section{Desarrollo: Interfaz web} + +\pagebreak +\section{Resultados y conclusiones} + +\pagebreak +\section{Contribuciones} + +\pagebreak +\section{Anexos} + +\pagebreak \bibliography{bib}{} \bibliographystyle{apalike} % plain, alpha, apalike + +\end{document} -- cgit v1.2.3