diff options
Diffstat (limited to 'defs.tex')
| -rwxr-xr-x | defs.tex | 236 |
1 files changed, 0 insertions, 236 deletions
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 |