From 946a1dcdce00d4a350fee92ae4931300e6170719 Mon Sep 17 00:00:00 2001 From: Guillermo Ramos Date: Thu, 16 Jul 2015 03:17:46 +0200 Subject: File renaming --- Makefile | 6 +- defs.tex | 236 ------------------------------------------ ec-defs.tex | 236 ++++++++++++++++++++++++++++++++++++++++++ front/bg.png | Bin 0 -> 22317 bytes front/fic.png | Bin 0 -> 241098 bytes front/front-body.tex | 53 ++++++++++ front/front-init.tex | 25 +++++ front/upmc.png | Bin 0 -> 15449 bytes img/browser-post.png | Bin 32568 -> 0 bytes img/browser-pre.png | Bin 27742 -> 0 bytes img/editor.png | Bin 68100 -> 0 bytes img/index.png | Bin 84982 -> 0 bytes img/login.png | Bin 80835 -> 0 bytes img/register.png | Bin 84886 -> 0 bytes img/results.png | Bin 44197 -> 0 bytes img/web-finished.png | Bin 180461 -> 0 bytes img/web-prototype.png | Bin 23456 -> 0 bytes memoria.pdf | Bin 305752 -> 0 bytes memoria.tex | 280 -------------------------------------------------- portada/defs.tex | 25 ----- portada/fic.png | Bin 241098 -> 0 bytes portada/portada.png | Bin 22317 -> 0 bytes portada/portada.tex | 53 ---------- portada/upmc.png | Bin 15449 -> 0 bytes tfm.pdf | Bin 0 -> 305752 bytes tfm.tex | 280 ++++++++++++++++++++++++++++++++++++++++++++++++++ 26 files changed, 597 insertions(+), 597 deletions(-) delete mode 100755 defs.tex create mode 100755 ec-defs.tex create mode 100644 front/bg.png create mode 100644 front/fic.png create mode 100644 front/front-body.tex create mode 100644 front/front-init.tex create mode 100644 front/upmc.png delete mode 100644 img/browser-post.png delete mode 100644 img/browser-pre.png delete mode 100644 img/editor.png delete mode 100644 img/index.png delete mode 100644 img/login.png delete mode 100644 img/register.png delete mode 100644 img/results.png delete mode 100644 img/web-finished.png delete mode 100644 img/web-prototype.png delete mode 100644 memoria.pdf delete mode 100755 memoria.tex delete mode 100644 portada/defs.tex delete mode 100644 portada/fic.png delete mode 100644 portada/portada.png delete mode 100644 portada/portada.tex delete mode 100644 portada/upmc.png create mode 100644 tfm.pdf create mode 100755 tfm.tex diff --git a/Makefile b/Makefile index b17eeaf..7faec7d 100644 --- a/Makefile +++ b/Makefile @@ -1,11 +1,11 @@ all: - latexmk -pvc -lualatex memoria.tex + latexmk -pvc -lualatex tfm.tex once: - lualatex memoria.tex + lualatex tfm.tex force: - latexmk -pvc -lualatex -interaction=nonstopmode memoria.tex + latexmk -pvc -lualatex -interaction=nonstopmode tfm.tex re: clean all diff --git a/defs.tex b/defs.tex deleted file mode 100755 index 3cc5e4c..0000000 --- a/defs.tex +++ /dev/null @@ -1,236 +0,0 @@ -% Source: EasyCrypt manual (https://www.easycrypt.info) - -%% 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} - -%% 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{\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{\side}[1]{\langle #1 \rangle} -\newcommand{\sidel}{\side{1}} -\newcommand{\sider}{\side{2}} -\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{\var}[1]{\ensuremath{\mathit{#1}} \xspace} - -%% Constants and operators -\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 -\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}} - -%% Language definition - - -\newcounter{easycrypt} -\lstnewenvironment{easycrypt}[2][]{ - \renewcommand\lstlistingname{Listado de código} - \setcounter{lstlisting}{\value{easycrypt}} - \lstset{language=easycrypt,caption={#2},#1} -} -{\stepcounter{easycrypt}} - -\lstdefinelanguage{easycrypt}{ - style=easycrypt-default, - keywordsprefix={'}, - morekeywords=[1]{unit,bool,int,real,bitstring,array,list,matrix,word}, - morekeywords=[2]{type,datatype,op,caxiom,axiom,lemma,module,pred,const,declare}, - morekeywords=[3]{var,fun,charfun,cost}, - 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}, - 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 -} - -\newcounter{bnf} -\lstnewenvironment{bnf}[2][]{ - \renewcommand\lstlistingname{Gramática} - \setcounter{lstlisting}{\value{bnf}} - \lstset{language=bnf,caption={#2},#1} -} -{\stepcounter{bnf}} - -\lstdefinestyle{bnf-style}{ - frame=tb, - keywordstyle=[1]{\bfseries}, - mathescape=true, -} - -\lstdefinelanguage{bnf}{ - style=bnf-style, - morekeywords=[1]{while,do,if,then,else,skip} -} - -\newcounter{game} -\lstnewenvironment{game}[2][]{ - \renewcommand\lstlistingname{Juego} - \setcounter{lstlisting}{\value{game}} - \lstset{language=game,caption={#2},#1} -} -{\stepcounter{game}} - -\lstdefinestyle{game-style}{ - frame=tb, - keywordstyle=[1]{\bfseries}, - mathescape=true, -} - -\lstdefinelanguage{game}{ - style=game-style, -} - -\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline -[language=easycrypt,#1]{#2}} - -%% 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}} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "memoria" -%%% End: \ No newline at end of file diff --git a/ec-defs.tex b/ec-defs.tex new file mode 100755 index 0000000..7878eb9 --- /dev/null +++ b/ec-defs.tex @@ -0,0 +1,236 @@ +% Source: EasyCrypt manual (https://www.easycrypt.info) + +%% 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} + +%% 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{\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{\side}[1]{\langle #1 \rangle} +\newcommand{\sidel}{\side{1}} +\newcommand{\sider}{\side{2}} +\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{\var}[1]{\ensuremath{\mathit{#1}} \xspace} + +%% Constants and operators +\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 +\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}} + +%% Language definition + + +\newcounter{easycrypt} +\lstnewenvironment{easycrypt}[2][]{ + \renewcommand\lstlistingname{Listado de código} + \setcounter{lstlisting}{\value{easycrypt}} + \lstset{language=easycrypt,caption={#2},#1} +} +{\stepcounter{easycrypt}} + +\lstdefinelanguage{easycrypt}{ + style=easycrypt-default, + keywordsprefix={'}, + morekeywords=[1]{unit,bool,int,real,bitstring,array,list,matrix,word}, + morekeywords=[2]{type,datatype,op,caxiom,axiom,lemma,module,pred,const,declare}, + morekeywords=[3]{var,fun,charfun,cost}, + 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}, + 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 +} + +\newcounter{bnf} +\lstnewenvironment{bnf}[2][]{ + \renewcommand\lstlistingname{Gramática} + \setcounter{lstlisting}{\value{bnf}} + \lstset{language=bnf,caption={#2},#1} +} +{\stepcounter{bnf}} + +\lstdefinestyle{bnf-style}{ + frame=tb, + keywordstyle=[1]{\bfseries}, + mathescape=true, +} + +\lstdefinelanguage{bnf}{ + style=bnf-style, + morekeywords=[1]{while,do,if,then,else,skip} +} + +\newcounter{game} +\lstnewenvironment{game}[2][]{ + \renewcommand\lstlistingname{Juego} + \setcounter{lstlisting}{\value{game}} + \lstset{language=game,caption={#2},#1} +} +{\stepcounter{game}} + +\lstdefinestyle{game-style}{ + frame=tb, + keywordstyle=[1]{\bfseries}, + mathescape=true, +} + +\lstdefinelanguage{game}{ + style=game-style, +} + +\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline +[language=easycrypt,#1]{#2}} + +%% 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}} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "tfm" +%%% End: \ No newline at end of file diff --git a/front/bg.png b/front/bg.png new file mode 100644 index 0000000..c558fa4 Binary files /dev/null and b/front/bg.png differ diff --git a/front/fic.png b/front/fic.png new file mode 100644 index 0000000..2a36204 Binary files /dev/null and b/front/fic.png differ diff --git a/front/front-body.tex b/front/front-body.tex new file mode 100644 index 0000000..d9c7d43 --- /dev/null +++ b/front/front-body.tex @@ -0,0 +1,53 @@ +\title{\Title} +\author{\textbf{Autor}: \Author \\ + \textbf{Director}: \Director} + +% \AddToShipoutPicture*{\BackgroundPic} +\newgeometry{inner=1cm,outer=1cm,top=0.5cm,bottom=1cm,left=1.5cm,right=1.5cm} +\begin{titlepage} + \begin{figure} + \begin{minipage}{.5\linewidth} + \begin{flushleft} + \includegraphics[scale=0.8]{front/upmc.png} + \end{flushleft} + \end{minipage} + \begin{minipage}{.49\linewidth} + \begin{flushright} + \includegraphics[scale=0.21]{front/fic.png} + \end{flushright} + \end{minipage} + \end{figure} + + \begin{center} + % \color{PortadaBlue} + \large{\textbf{UNIVERSIDAD POLITÉCNICA DE MADRID}} \\[1.8cm] + \large{E.T.S.I. INFORMÁTICOS} \\[1.8cm] + \large{MASTER UNIVERSITARIO EN SOFTWARE Y SISTEMAS} \\[1.8cm] + \large{TRABAJO DE FIN DE MASTER} \\[3cm] + + \begin{adjustwidth}{2cm}{1cm} + \begin{center} + \LARGE{\textbf{Implementing a term rewriting}} \\[0.4cm] + \LARGE{\textbf{engine for the EasyCrypt framework}} \\[3cm] + \end{center} + \end{adjustwidth} + + \begin{adjustwidth}{5.5cm}{1cm} + \Large{\textbf{Autor:} \Author} \\[0.2cm] + \Large{\textbf{Director:} \Director} \\[0.2cm] + \Large{\textbf{Co-director:} \Codirector} \\[2.4cm] + \end{adjustwidth} + \end{center} + \begin{flushright} + % \color{PortadaBlue} + \large{MADRID, 28 de julio de 2015} \\ + \end{flushright} +\end{titlepage} + +% \ClearShipoutPicture +\restoregeometry + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../tfm" +%%% End: \ No newline at end of file diff --git a/front/front-init.tex b/front/front-init.tex new file mode 100644 index 0000000..e2f4f66 --- /dev/null +++ b/front/front-init.tex @@ -0,0 +1,25 @@ +\usepackage{xcolor} + +\usepackage{changepage} +\usepackage{eso-pic} + +\newcommand{\BackgroundPic}{ + \put(-4,0){ + \parbox[b][\paperheight]{\paperwidth}{ + \vfill + \centering + \includegraphics[width=\paperwidth,height=\paperheight]{front/bg.png} + \vfill + } + } +} +\definecolor{PortadaBlue}{HTML}{31489F} + +\newcommand{\Author}{Guillermo Ramos Gutiérrez} +\newcommand{\Director}{Manuel Carro Liñares} +\newcommand{\Codirector}{Pierre-Yves Strub} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../tfm" +%%% End: \ No newline at end of file diff --git a/front/upmc.png b/front/upmc.png new file mode 100644 index 0000000..93ea544 Binary files /dev/null and b/front/upmc.png differ diff --git a/img/browser-post.png b/img/browser-post.png deleted file mode 100644 index b45eab5..0000000 Binary files a/img/browser-post.png and /dev/null differ diff --git a/img/browser-pre.png b/img/browser-pre.png deleted file mode 100644 index f5849a6..0000000 Binary files a/img/browser-pre.png and /dev/null differ diff --git a/img/editor.png b/img/editor.png deleted file mode 100644 index 7bdfa46..0000000 Binary files a/img/editor.png and /dev/null differ diff --git a/img/index.png b/img/index.png deleted file mode 100644 index e47be96..0000000 Binary files a/img/index.png and /dev/null differ diff --git a/img/login.png b/img/login.png deleted file mode 100644 index 586d84f..0000000 Binary files a/img/login.png and /dev/null differ diff --git a/img/register.png b/img/register.png deleted file mode 100644 index 60a41ea..0000000 Binary files a/img/register.png and /dev/null differ diff --git a/img/results.png b/img/results.png deleted file mode 100644 index c28f0d0..0000000 Binary files a/img/results.png and /dev/null differ diff --git a/img/web-finished.png b/img/web-finished.png deleted file mode 100644 index 3eb0e5e..0000000 Binary files a/img/web-finished.png and /dev/null differ diff --git a/img/web-prototype.png b/img/web-prototype.png deleted file mode 100644 index f6a5538..0000000 Binary files a/img/web-prototype.png and /dev/null differ diff --git a/memoria.pdf b/memoria.pdf deleted file mode 100644 index 62ab0b3..0000000 Binary files a/memoria.pdf and /dev/null differ diff --git a/memoria.tex b/memoria.tex deleted file mode 100755 index 10c2b19..0000000 --- a/memoria.tex +++ /dev/null @@ -1,280 +0,0 @@ -\documentclass[12pt,a4paper,parskip=full]{scrreprt} -\usepackage{scrhack} % http://tex.stackexchange.com/questions/51867/koma-warning-about-toc - -\usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry} - -% \usepackage[spanish]{babel} -\usepackage{fontspec} \usepackage{url} -\usepackage{graphicx} \usepackage{cite} \usepackage{amsmath} -\usepackage{mathtools} \usepackage{listings} \usepackage{syntax} -% \usepackage[compact,small]{titlesec} -\usepackage[usenames,dvipsnames]{xcolor} -\usepackage[backref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref} -\usepackage{perpage} \usepackage{subcaption} - -\usepackage{tikz} -% \usepackage{minted} - -\usepackage{float} -\floatstyle{boxed} -\newfloat{code}{th}{los}[chapter] -\floatname{code}{Code listing} - -\usetikzlibrary{shapes,arrows} - -\hypersetup{pageanchor=false} - - -\input{defs} -\input{portada/defs} - -\MakePerPage{footnote} - -\def\emptypage{\newpage\thispagestyle{empty}\mbox{}} - -\begin{document} -\input{portada/portada} - -\pagenumbering{roman} - - -\emptypage -\chapter*{Resumen} - -La sociedad depende hoy más que nunca de la tecnología, pero la inversión en -seguridad es escasa y los sistemas informáticos siguen estando muy lejos de ser -seguros. La criptografía es una de las piedras angulares de la seguridad en este -ámbito, por lo que recientemente se ha dedicado una cantidad considerable de -recursos al desarrollo de herramientas que ayuden en la evaluación y mejora de -los algoritmos criptográficos. EasyCrypt es uno de estos sistemas, desarrollado -recientemente en el Instituto IMDEA Software en respuesta a la creciente -necesidad de disponer de herramientas fiables de verificación formal de -criptografía. - -(TODO: En este documento se explicará cripto y reescritura de términos para bla -bla) - -\chapter*{Abstract} - -Today, society depends more than ever on technology, but the investment in -security is still scarce and using computer systems are still far from safe to -use. Cryptography is one of the cornerstones of security, so there has been a -considerable amount of effort devoted recently to the development of tools -oriented to the evaluation and improvement of cryptographic algorithms. One of -these tools is EasyCrypt, developed recently at IMDEA Software Institute in -response to the increasing need of reliable formal verification tools for -cryptography. - -(TODO: In this document we will see crypto and term rewriting theory in order to -understand EasyCrypt and implement bla bla bla) - -\emptypage -\tableofcontents - -%% Content begins here -% -%% Level | Spaces before | '%'s after -% ---------+---------------+----------- -% part | 5 | until EOL -% chapter | 4 | 10 -% section | 3 | 2 -% subs. | 2 | -% subsubs. | 1 | - - - - -\emptypage -\chapter{INTRODUCTION} %%%%%%%%%% - -\pagenumbering{arabic} -\setcounter{page}{1} - - - -\section{Problem} %% - - - -\section{Contributions} %% - -\begin{itemize} -\item Reference implementations of various rewriting engines -\item Improvement of EasyCrypt's one -\end{itemize} - - - - - -\part{STATE OF THE ART} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - - -\chapter{CRYPTOGRAPHY} %%%%%%%%%% - -(TODO: Intro to crypto) - - - -\section{Symmetric Cryptography} %% - -(TODO: not sure if this section is really needed) - - - -\section{Asymmetric Cryptography} %% - -Here we will introduce some of the most fundamental concepts in asymmetric -cryptography, as they will be useful to understand the next sections on -sequences of games (TODO: ref). - -\textbf{Asymmetric cryptography} (also called \textbf{Public Key cryptography}), -refers to cryptographic algorithms that make use of two different keys, $pk$ -(public key) and $sk$ (secret key). There must be some mathematical relationship -that allows a specific pair of keys to perform dual operations, e.g., $pk$ to -encrypt and $sk$ to decrypt, $pk$ to verify a signature and $sk$ to create it, -and so on. A pair of (public, secret) keys can be generated using a procedure -called \textbf{key generation} ($\KG$). - -The encryption ($\Enc$) and decryption ($\Dec$) functions work in the -following way: - -$$\Enc(pk,M) = C$$ -$$\Dec(sk,C) = M$$ - -That is, a message ($M$) can be encrypted using a public key to obtain a -ciphertext ($C$). - -\section{Sequences of games} %% - - - -\section{Verification: EasyCrypt} %% - - -\subsection{Specification languages} - -\subsubsection{Expressions} - -\subsubsection{Probabilistic expressions} - -\subsubsection{pWhile language} - - -\subsection{Proof languages} - -\subsubsection{Judgments} - -\subsubsection{Tactics} - - - - -\chapter{TERM REWRITING} %%%%%%%%%% - - - -\section{Term Rewriting Systems/Theory} %% - - - -\section{Lambda Calculus} %% - - -\subsection{Extensions} - -\subsubsection{Case expressions} - -\subsubsection{Fixpoints} - - -\subsection{Reduction rules} - -http://adam.chlipala.net/cpdt/html/Equality.html - -\begin{itemize} -\item Alpha reduction -\item Beta reduction -\item ... -\end{itemize} - - - -\section{Evaluation Strategies} %% - - - -\section{Abstract Machines} %% - - -\subsection{Krivine Machine} - -\cite{Krivine07} - - -\subsection{ZAM} - -\cite{GregoireLeroy02} - - - -\part{IMPLEMENTATION} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -\chapter{KRIVINE MACHINE} %%%%%%%%%% - -- Outside EasyCrypt: weak symbolic with fixpts and cases -- Inside EasyCrypt: bla bla - - - - - - -\chapter{ZAM} %%%%%%%%%% - - - - -\chapter{REDUCTION IN EASYCRYPT} %%%%%%%%%% - - - -\section{Architecture overview} %% - - - - - -\part{EPILOGUE} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - - -\chapter{CONCLUSIONS} %%%%%%%%%% - - - - -\chapter{FUTURE WORK} %%%%%%%%%% - - - - -\chapter{ANNEX} %%%%%%%%%% - - - -\section{Krivine Machine source code} %% - - - -\section{ZAM source code} %% - - -\pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr} - -\end{document} diff --git a/portada/defs.tex b/portada/defs.tex deleted file mode 100644 index 228d9a7..0000000 --- a/portada/defs.tex +++ /dev/null @@ -1,25 +0,0 @@ -\usepackage{xcolor} - -\usepackage{changepage} -\usepackage{eso-pic} - -\newcommand{\BackgroundPic}{ - \put(-4,0){ - \parbox[b][\paperheight]{\paperwidth}{ - \vfill - \centering - \includegraphics[width=\paperwidth,height=\paperheight]{portada/portada.png} - \vfill - } - } -} -\definecolor{PortadaBlue}{HTML}{31489F} - -\newcommand{\Author}{Guillermo Ramos Gutiérrez} -\newcommand{\Director}{Manuel Carro Liñares} -\newcommand{\Codirector}{Pierre-Yves Strub} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "../memoria" -%%% End: \ No newline at end of file diff --git a/portada/fic.png b/portada/fic.png deleted file mode 100644 index 2a36204..0000000 Binary files a/portada/fic.png and /dev/null differ diff --git a/portada/portada.png b/portada/portada.png deleted file mode 100644 index c558fa4..0000000 Binary files a/portada/portada.png and /dev/null differ diff --git a/portada/portada.tex b/portada/portada.tex deleted file mode 100644 index aede6ba..0000000 --- a/portada/portada.tex +++ /dev/null @@ -1,53 +0,0 @@ -\title{\Title} -\author{\textbf{Autor}: \Author \\ - \textbf{Director}: \Director} - -% \AddToShipoutPicture*{\BackgroundPic} -\newgeometry{inner=1cm,outer=1cm,top=0.5cm,bottom=1cm,left=1.5cm,right=1.5cm} -\begin{titlepage} - \begin{figure} - \begin{minipage}{.5\linewidth} - \begin{flushleft} - \includegraphics[scale=0.8]{portada/upmc.png} - \end{flushleft} - \end{minipage} - \begin{minipage}{.49\linewidth} - \begin{flushright} - \includegraphics[scale=0.21]{portada/fic.png} - \end{flushright} - \end{minipage} - \end{figure} - - \begin{center} - % \color{PortadaBlue} - \large{\textbf{UNIVERSIDAD POLITÉCNICA DE MADRID}} \\[1.8cm] - \large{E.T.S.I. INFORMÁTICOS} \\[1.8cm] - \large{MASTER UNIVERSITARIO EN SOFTWARE Y SISTEMAS} \\[1.8cm] - \large{TRABAJO DE FIN DE MASTER} \\[3cm] - - \begin{adjustwidth}{2cm}{1cm} - \begin{center} - \LARGE{\textbf{Implementing a term rewriting}} \\[0.4cm] - \LARGE{\textbf{engine for the EasyCrypt framework}} \\[3cm] - \end{center} - \end{adjustwidth} - - \begin{adjustwidth}{5.5cm}{1cm} - \Large{\textbf{Autor:} \Author} \\[0.2cm] - \Large{\textbf{Director:} \Director} \\[0.2cm] - \Large{\textbf{Co-director:} \Codirector} \\[2.4cm] - \end{adjustwidth} - \end{center} - \begin{flushright} - % \color{PortadaBlue} - \large{MADRID, 28 de julio de 2015} \\ - \end{flushright} -\end{titlepage} - -% \ClearShipoutPicture -\restoregeometry - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "../memoria" -%%% End: \ No newline at end of file diff --git a/portada/upmc.png b/portada/upmc.png deleted file mode 100644 index 93ea544..0000000 Binary files a/portada/upmc.png and /dev/null differ diff --git a/tfm.pdf b/tfm.pdf new file mode 100644 index 0000000..62ab0b3 Binary files /dev/null and b/tfm.pdf differ diff --git a/tfm.tex b/tfm.tex new file mode 100755 index 0000000..4840bdc --- /dev/null +++ b/tfm.tex @@ -0,0 +1,280 @@ +\documentclass[12pt,a4paper,parskip=full]{scrreprt} +\usepackage{scrhack} % http://tex.stackexchange.com/questions/51867/koma-warning-about-toc + +\usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry} + +% \usepackage[spanish]{babel} +\usepackage{fontspec} \usepackage{url} +\usepackage{graphicx} \usepackage{cite} \usepackage{amsmath} +\usepackage{mathtools} \usepackage{listings} \usepackage{syntax} +% \usepackage[compact,small]{titlesec} +\usepackage[usenames,dvipsnames]{xcolor} +\usepackage[backref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref} +\usepackage{perpage} \usepackage{subcaption} + +\usepackage{tikz} +% \usepackage{minted} + +\usepackage{float} +\floatstyle{boxed} +\newfloat{code}{th}{los}[chapter] +\floatname{code}{Code listing} + +\usetikzlibrary{shapes,arrows} + +\hypersetup{pageanchor=false} + + +\input{ec-defs} +\input{front/front-init} + +\MakePerPage{footnote} + +\def\emptypage{\newpage\thispagestyle{empty}\mbox{}} + +\begin{document} +\input{front/front-body} + +\pagenumbering{roman} + + +\emptypage +\chapter*{Resumen} + +La sociedad depende hoy más que nunca de la tecnología, pero la inversión en +seguridad es escasa y los sistemas informáticos siguen estando muy lejos de ser +seguros. La criptografía es una de las piedras angulares de la seguridad en este +ámbito, por lo que recientemente se ha dedicado una cantidad considerable de +recursos al desarrollo de herramientas que ayuden en la evaluación y mejora de +los algoritmos criptográficos. EasyCrypt es uno de estos sistemas, desarrollado +recientemente en el Instituto IMDEA Software en respuesta a la creciente +necesidad de disponer de herramientas fiables de verificación formal de +criptografía. + +(TODO: En este documento se explicará cripto y reescritura de términos para bla +bla) + +\chapter*{Abstract} + +Today, society depends more than ever on technology, but the investment in +security is still scarce and using computer systems are still far from safe to +use. Cryptography is one of the cornerstones of security, so there has been a +considerable amount of effort devoted recently to the development of tools +oriented to the evaluation and improvement of cryptographic algorithms. One of +these tools is EasyCrypt, developed recently at IMDEA Software Institute in +response to the increasing need of reliable formal verification tools for +cryptography. + +(TODO: In this document we will see crypto and term rewriting theory in order to +understand EasyCrypt and implement bla bla bla) + +\emptypage +\tableofcontents + +%% Content begins here +% +%% Level | Spaces before | '%'s after +% ---------+---------------+----------- +% part | 5 | until EOL +% chapter | 4 | 10 +% section | 3 | 2 +% subs. | 2 | +% subsubs. | 1 | + + + + +\emptypage +\chapter{INTRODUCTION} %%%%%%%%%% + +\pagenumbering{arabic} +\setcounter{page}{1} + + + +\section{Problem} %% + + + +\section{Contributions} %% + +\begin{itemize} +\item Reference implementations of various rewriting engines +\item Improvement of EasyCrypt's one +\end{itemize} + + + + + +\part{STATE OF THE ART} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + + +\chapter{CRYPTOGRAPHY} %%%%%%%%%% + +(TODO: Intro to crypto) + + + +\section{Symmetric Cryptography} %% + +(TODO: not sure if this section is really needed) + + + +\section{Asymmetric Cryptography} %% + +Here we will introduce some of the most fundamental concepts in asymmetric +cryptography, as they will be useful to understand the next sections on +sequences of games (TODO: ref). + +\textbf{Asymmetric cryptography} (also called \textbf{Public Key cryptography}), +refers to cryptographic algorithms that make use of two different keys, $pk$ +(public key) and $sk$ (secret key). There must be some mathematical relationship +that allows a specific pair of keys to perform dual operations, e.g., $pk$ to +encrypt and $sk$ to decrypt, $pk$ to verify a signature and $sk$ to create it, +and so on. A pair of (public, secret) keys can be generated using a procedure +called \textbf{key generation} ($\KG$). + +The encryption ($\Enc$) and decryption ($\Dec$) functions work in the +following way: + +$$\Enc(pk,M) = C$$ +$$\Dec(sk,C) = M$$ + +That is, a message ($M$) can be encrypted using a public key to obtain a +ciphertext ($C$). + +\section{Sequences of games} %% + + + +\section{Verification: EasyCrypt} %% + + +\subsection{Specification languages} + +\subsubsection{Expressions} + +\subsubsection{Probabilistic expressions} + +\subsubsection{pWhile language} + + +\subsection{Proof languages} + +\subsubsection{Judgments} + +\subsubsection{Tactics} + + + + +\chapter{TERM REWRITING} %%%%%%%%%% + + + +\section{Term Rewriting Systems/Theory} %% + + + +\section{Lambda Calculus} %% + + +\subsection{Extensions} + +\subsubsection{Case expressions} + +\subsubsection{Fixpoints} + + +\subsection{Reduction rules} + +http://adam.chlipala.net/cpdt/html/Equality.html + +\begin{itemize} +\item Alpha reduction +\item Beta reduction +\item ... +\end{itemize} + + + +\section{Evaluation Strategies} %% + + + +\section{Abstract Machines} %% + + +\subsection{Krivine Machine} + +\cite{Krivine07} + + +\subsection{ZAM} + +\cite{GregoireLeroy02} + + + +\part{IMPLEMENTATION} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +\chapter{KRIVINE MACHINE} %%%%%%%%%% + +- Outside EasyCrypt: weak symbolic with fixpts and cases +- Inside EasyCrypt: bla bla + + + + + + +\chapter{ZAM} %%%%%%%%%% + + + + +\chapter{REDUCTION IN EASYCRYPT} %%%%%%%%%% + + + +\section{Architecture overview} %% + + + + + +\part{EPILOGUE} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + + +\chapter{CONCLUSIONS} %%%%%%%%%% + + + + +\chapter{FUTURE WORK} %%%%%%%%%% + + + + +\chapter{ANNEX} %%%%%%%%%% + + + +\section{Krivine Machine source code} %% + + + +\section{ZAM source code} %% + + +\pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr} + +\end{document} -- cgit v1.2.3