_files.tex 6.86 KB
 Benoit Viguier committed Sep 30, 2019 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 \documentclass[8pt]{extarticle} \usepackage[a4paper,margin=1cm]{geometry} \usepackage{epsfig} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage[switch]{lineno} \usepackage[pdf]{pstricks} \usepackage{amsfonts,amsmath,amscd,amscd,amssymb,array} \usepackage{xspace} \newcommand{\p}{\ensuremath{2^{255}-19}} \newcommand{\Zfield}{\ensuremath{\mathbb{Z}_{\p}}} \newcommand{\Ffield}{\ensuremath{\mathbb{F}_{\p}}} \newcommand{\Z}{\ensuremath{\mathbb{Z}}\xspace} \newcommand{\K}{\ensuremath{\mathbb{K}}\xspace} \newcommand{\F}[1]{\ensuremath{\mathbb{F}_{#1}}\xspace} \pagenumbering{gobble} \begin{document} \begin{table*}[h] \centering \begin{tabular}{ l | l | l } Definition & File & Description \\ \hline \texttt{ZofList} & \texttt{ListsOp/ZofList.v} & \Z $\rightarrow$ List \Z $\rightarrow$ \Z\\ \texttt{ListofZ32} & \texttt{ListsOp/ListofZ.v} & \Z $\rightarrow$ \Z $\rightarrow$ list \Z\\ \hline \multicolumn{3}{c}{Elliptic Curve \& Fields }\\ \hline \texttt{mcuType} & \texttt{High/mc.v} & $M_{a,b}$ \\ % \texttt{oncurve} & \texttt{High/mc.v} & Boolean decision of a point on a curve \\ \texttt{mc} & \texttt{High/mc.v} & $M_{a,b}(\K)$ \\ \texttt{neg} & \texttt{High/mc.v} & Negation \\ \texttt{add} & \texttt{High/mc.v} & Addition \\ \texttt{ec\_of\_mc} & \texttt{High/mcgroup.v} & $M_{a,b}(\K) \mapsto E(\K)$ \\ \texttt{mc\_of\_ec} & \texttt{High/mcgroup.v} & $E(\K) \mapsto M_{a,b}(\K)$ \\ \texttt{point\_x0} & \texttt{High/montgomery.v} & $\chi_0 : M_{a,b}(\K) \to \K$ \\ \texttt{point\_x} & \texttt{High/montgomery.v} & $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$ \\ % \texttt{mcu\_no\_square} & \texttt{High/montgomery.v} & $a^2-4$ is not a square in \K \\ \texttt{cswap} & \texttt{High/opt\_ladder.v} & Conditional swap \\ \texttt{opt\_montgomery} & \texttt{High/opt\_ladder.v} & Montgomery over \K \\ % \texttt{mcu\_no\_square} & \texttt{High/opt\_ladder.v} & $a^2-4$ is not a square in \K \\ \texttt{Zmodp.type} & \texttt{High/Zmodp.v} & $\F{p}$ with $p = \p$ \\ \texttt{Zmodp2.type} & \texttt{High/Zmodp2.v} & $\F{p^2}$ with $p = \p$ \\ \texttt{curve25519\_Fp\_ladder} & \texttt{High/curve25519\_Fp.v} & Montgomery ladder for the curve $M_{486662,1}$ over \F{p} \\ \texttt{curve25519\_Fp\_to\_Fp2} & \texttt{High/curve25519\_Fp\_incl\_Fp2.v} & $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$ \\ \texttt{twist25519\_Fp\_ladder} & \texttt{High/twist25519\_Fp.v} & Montgomery ladder for the quadratic twist $M_{486662,2}$ over \F{p} \\ \texttt{twist25519\_Fp\_to\_Fp2} & \texttt{High/twist25519\_Fp\_incl\_Fp2.v} & $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$ \\ % \texttt{primo} & \texttt{High/prime\_cert.v} & $\p$ is prime \\ \hline \multicolumn{3}{c}{Generic ladder}\\ \hline \texttt{get\_a} & \texttt{Gen/Get\_abcdef.v} & $(a,b,c,d,e,f) \mapsto a$ \\ \texttt{get\_c} & \texttt{Gen/Get\_abcdef.v} & $(a,b,c,d,e,f) \mapsto c$ \\ \texttt{Ops.A} & \texttt{Gen/AMZubSqSel.v} & Addition \\ \texttt{Ops.M} & \texttt{Gen/AMZubSqSel.v} & Multiplication \\ \texttt{Ops.Zub} & \texttt{Gen/AMZubSqSel.v} & Subtraction \\ \texttt{Ops.Sq} & \texttt{Gen/AMZubSqSel.v} & Squaring \\ \texttt{Ops.C\_0} & \texttt{Gen/AMZubSqSel.v} & Constant $0$ \\ \texttt{Ops.C\_1} & \texttt{Gen/AMZubSqSel.v} & Constant $1$ \\ \texttt{Ops.C\_121665} & \texttt{Gen/AMZubSqSel.v} & Constant $121665$ \\ \texttt{Ops.Sel25519} & \texttt{Gen/AMZubSqSel.v} & Conditional swap \\ \texttt{Ops.Getbit} & \texttt{Gen/GetBit.v} & Bit selection \\ \texttt{montgomery\_rec} & \texttt{Gen/montgomery\_rec.v} & Montgomery ladder \\ \hline \multicolumn{3}{c}{Operations over \Z and \Zfield}\\ \hline \texttt{Mid.A} & \texttt{Mid/AMZubSqSel.v} & Addition \\ \texttt{Mid.M} & \texttt{Mid/AMZubSqSel.v} & Multiplication \\ \texttt{Mid.Zub} & \texttt{Mid/AMZubSqSel.v} & Subtraction \\ \texttt{Mid.Sq} & \texttt{Mid/AMZubSqSel.v} & Squaring \\ \texttt{Mid.C\_0} & \texttt{Mid/AMZubSqSel.v} & Constant $0$ \\ \texttt{Mid.C\_1} & \texttt{Mid/AMZubSqSel.v} & Constant $1$ \\ \texttt{Mid.C\_121665} & \texttt{Mid/AMZubSqSel.v} & Constant $121665$ \\ \texttt{Mid.Sel25519} & \texttt{Mid/AMZubSqSel.v} & Conditional swap \\ \texttt{Mid.car25519} & \texttt{Mid/Car25519.v} & Carry propagation \\ \texttt{Mid.getbit} & \texttt{Mid/GetBit.v} & Bit selection \\ \texttt{Inv25519\_Z} & \texttt{Mid/Inv25519.v} & $x^{2^{255}-21}$ \\ \texttt{ZInv25519} & \texttt{Mid/Inv25519.v} & power computed recursively \\ \texttt{modP} & \texttt{Mid/Mod.v} & mod \p\\ \texttt{ZPack25519} & \texttt{Mid/Pack25519.v} & packing mod \p\\ \texttt{Zclamp} & \texttt{Mid/Prep\_n.v} & Clamping \\ \texttt{ZUnpack25519} & \texttt{Mid/Unpack25519.v} & unpacking (mod $2^{255}$)\\ \hline \multicolumn{3}{c}{Operations over list of \Z}\\ \hline \texttt{Low.A} & \texttt{Low/A.v} & Addition \\ \texttt{Low.M} & \texttt{Low/M.v} & Multiplication \\ \texttt{Low.Z} & \texttt{Low/Z.v} & Subtraction \\ \texttt{Low.S} & \texttt{Low/S.v} & Squaring \\ \texttt{Low.C\_0} & \texttt{Low/Constant.v} & Constant $0$ \\ \texttt{Low.C\_1} & \texttt{Low/Constant.v} & Constant $1$\\ \texttt{Low.C\_121665} & \texttt{Low/Constant.v} & Constant $121665$\\ \texttt{Low.C\_25519} & \texttt{Low/Constant.v} & Constant $2^{255}-19$\\ \texttt{Low.Sel25519} & \texttt{Low/Sel25519.v} & Conditional swap \\ \texttt{car25519} & \texttt{Low/Car25519.v} & Carry propagation \\ \texttt{Low.getbit} & \texttt{Low/GetBit.v} & Bit selection \\ \texttt{Inv25519} & \texttt{Low/Inv25519.v} & Recursive power \\ \texttt{Pack25519} & \texttt{Low/Pack25519.v} & packing mod \p\\ \texttt{clamp} & \texttt{Low/Prep\_n.v} & Clamping \\ \texttt{Unpack25519} & \texttt{Low/Unpack25519.v} & unpacking (mod $2^{255}$)\\ \hline  Benoit Viguier committed Jan 17, 2020 103  \multicolumn{3}{c}{Instantiation of \texttt{Ops}}\\  Benoit Viguier committed Sep 30, 2019 104  \hline  Benoit Viguier committed Jan 17, 2020 105 106 107  \texttt{Z25519\_Ops} & \texttt{Mid/Instances.v} & Instantiation over \F{p} with $p = \p$\\ \texttt{Z\_Ops} & \texttt{Mid/Instances.v} & Instantiation over $\Zfield$ \\ \texttt{List\_Z\_Ops} & \texttt{Mid/Instances.v} & Instantiation lists of \Z \\  Benoit Viguier committed Sep 30, 2019 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123  \hline \multicolumn{3}{c}{X25519 over \Z and list of \Z}\\ \hline \texttt{ZCrypto\_Scalarmult} & \texttt{Mid/Crypto\_Scalarmult.v} & integers specification of X25519\\ \texttt{Crypto\_Scalarmult} & \texttt{Low/Crypto\_Scalarmult.v} & list specification of X25519\\ \hline \multicolumn{3}{c}{RFC~7748}\\ \hline \texttt{decodeScalar25519} & \texttt{rfc/rfc.v} & Decode the scalar\\ \texttt{decodeUCoordinate} & \texttt{rfc/rfc.v} & Decode the x-coordinate\\ \texttt{encodeUCoordinate} & \texttt{rfc/rfc.v} & Encode the resulting x-coordinate\\ \texttt{RFC} & \texttt{rfc/rfc.v} & specification of X25519 as in RFC~7748\\ \hline \end{tabular} \end{table*} \end{document}