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