simplify code include

paper/preliminaries.tex

@@ -31,9 +31,9 @@ Details of the formalization can be found in Section~\ref{montgomery}.
 \end{definition}
 
 Points over $M_{a,b}(\K)$ can be equipped with a structure of an abelian group
-with the addition operation $\oplus$ and with neutral element the point at infinity $\Oinf$.
+with the addition operation $\boxplus$ and with neutral element the point at infinity $\Oinf$.
 Using this law, we have the scalar multiplication over $M_{a,b}(\K)$ defined by:
-  $$n\cdot P = \underbrace{P \oplus \cdots \oplus P}_{n\text{ times}}$$
+  $$n\cdot P = \underbrace{P \boxplus \cdots \boxplus P}_{n\text{ times}}$$
 
 We now consider x-coordinate-only operations. In order to simplify computations,
 such coordinates are represented as $X/Z$ fractions. We define two operations:
@@ -41,8 +41,22 @@ such coordinates are represented as $X/Z$ fractions. We define two operations:
 \texttt{xADD} &: (X_P, Z_P, X_Q , Z_Q, X_{P-Q}, Z_{P-Q}) \mapsto (X_{P+Q}, Z_{P+Q})\\
 \texttt{xDBL} &: (X_P, Z_P) \mapsto (X_{2P}, Z_{2P})\\
 \end{align*}
-By using this differential addition and doubling operations we define the Montgomery ladder
-computing a x-coordinate-only scalar multiplication (see Algorithm~\ref{montgomery-ladder}).
+To remove secret-dependent if-statements we use a constant-time conditional swap
+(see Algorithm~\ref{c-swap}).
+\begin{algorithm}
+\caption{\texttt{SWAP} : Constant-time conditional swap}
+\label{c-swap}
+\begin{algorithmic}
+\REQUIRE{$b \in \{0, 1\}$ and a pair $(X_0, X_1)$ of objects encoded as $n$-bit strings}
+\ENSURE{$(X_b, X_{1-b})$}
+\STATE $b \leftarrow (b, \ldots, b)_n$
+\STATE $mask \leftarrow b\texttt{ AND } (X_0\texttt{ XOR } X_1)$
+\RETURN $(x_0 \texttt{ XOR } mask, x_1 \texttt{ XOR } mask)$
+\end{algorithmic}
+\end{algorithm}
+
+By using the differential addition and doubling operations we define the Montgomery ladder
+computing a $x$-coordinate-only scalar multiplication (see Algorithm~\ref{montgomery-ladder}).
 \begin{algorithm}
 \caption{Montgomery ladder for scalar mult.}
 \label{montgomery-ladder}
@@ -52,19 +66,14 @@ computing a x-coordinate-only scalar multiplication (see Algorithm~\ref{montgome
 \STATE $Q \leftarrow \Oinf$
 \STATE $R \leftarrow (X_P,Z_P)$
 \FOR{$k$ := $m$ down to $1$}
-  \IF{$k^{\text{th}}$ bit of $n$ is $0$}
-    \STATE $R \leftarrow \texttt{xADD}(Q,R,X_P,Z_P)$
-    \STATE $Q \leftarrow \texttt{xDBL}(Q)$
-  \ELSE
-    \STATE $Q \leftarrow \texttt{xADD}(Q,R,X_P,Z_P)$
-    \STATE $R \leftarrow \texttt{xDBL}(R)$
-  \ENDIF
+  \STATE $(Q,R) \leftarrow \texttt{SWAP}(k^{\text{th}}\text{ bit of }n, (Q,R))$
+  \STATE $Q \leftarrow \texttt{xDBL}(Q)$
+  \STATE $R \leftarrow \texttt{xADD}(Q,R,X_P,Z_P)$
+  \STATE $(Q,R) \leftarrow \texttt{SWAP}(k^{\text{th}}\text{ bit of }n, (Q,R))$
 \ENDFOR
+\RETURN $Q$
 \end{algorithmic}
 \end{algorithm}
-$n$ is a secret input of algorithm~\ref{montgomery-ladder}.
-The if statements are secret-dependent and are replaced with constant-time
-conditional swap between $Q$ and $R$ in the TweetNaCl implementation.
 
 \subsection{The X25519 key exchange}
 \label{preliminaries:A}

paper/setup.sty

@@ -350,7 +350,7 @@ literate=
 
 \lstdefinelanguage{Ctweetnacl}{%
   morekeywords=[1]{FOR,for, return},
-  morekeywords=[2]{sv, int, i64, gf, long, u8},
+  morekeywords=[2]{sv, int, i64, gf, unsigned, char, long, u8},
   morekeywords=[3]{const, typedef},
   morekeywords=[4]{A, Z, M, S, car25519, pack25519, inv25519,
   crypto_scalarmult, unpack25519, sel25519, set25519},

paper/tweetnacl.tex

 \subsection{The complete X25519 code from TweetNaCl}
+\label{verified-C-and-diff}
 
 \subheading{Verified C Code} We provide below the code we verified.
 
-\begin{lstlisting}[language=Ctweetnacl]
-#define FOR(i,n) for (i = 0;i < n;++i)
-#define sv static void
-
-typedef unsigned char u8;
-typedef unsigned long u32;
-typedef unsigned long long u64;
-typedef long long i64 __attribute__((aligned(8)));
-typedef i64 gf[16];
-
-sv set25519(gf r, const gf a)
-{
-  int i;
-  FOR(i,16) r[i]=a[i];
-}
-
-sv car25519(gf o)
-{
-  int i;
-  i64 c;
-  FOR(i,15) {
-    o[(i+1)]+=o[i]>>16;
-    o[i]&=0xffff;
-  }
-  o[0]+=38*(o[15]>>16);
-  o[15]&=0xffff;
-}
-
-sv sel25519(gf p,gf q,i64 b)
-{
-  int i;
-  i64 t,c=~(b-1);
-  FOR(i,16) {
-    t= c&(p[i]^q[i]);
-    p[i]^=t;
-    q[i]^=t;
-  }
-}
-
-sv pack25519(u8 *o,const gf n)
-{
-  int i,j;
-  i64 b;
-  gf t,m={0};
-  set25519(t,n);
-  car25519(t);
-  car25519(t);
-  car25519(t);
-  FOR(j,2) {
-    m[0]=t[0]- 0xffed;
-    for(i=1;i<15;i++) {
-      m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
-      m[i-1]&=0xffff;
-    }
-    m[15]=t[15]-0x7fff-((m[14]>>16)&1);
-    m[14]&=0xffff;
-    b=1-((m[15]>>16)&1);
-    sel25519(t,m,b);
-  }
-  FOR(i,16) {
-    o[2*i]=t[i]&0xff;
-    o[2*i+1]=t[i]>>8;
-  }
-}
-
-sv unpack25519(gf o, const u8 *n)
-{
-  int i;
-  FOR(i,16) o[i]=n[2*i]+((i64)n[2*i+1]<<8);
-  o[15]&=0x7fff;
-}
-
-sv A(gf o,const gf a,const gf b)
-{
-  int i;
-  FOR(i,16) o[i]=a[i]+b[i];
-}
-
-sv Z(gf o,const gf a,const gf b)
-{
-  int i;
-  FOR(i,16) o[i]=a[i]-b[i];
-}
-
-sv M(gf o,const gf a,const gf b)
-{
-  int i,j;
-  i64 t[31], aux;
-  FOR(i,31) t[i]= 0;
-  FOR(i,16) {
-    aux = a[i];
-    FOR(j,16) t[i+j]+=aux*b[j];
-  }
-  FOR(i,15) t[i]+=(i64)38*t[i+16];
-  FOR(i,16) o[i]=t[i];
-  car25519(o);
-  car25519(o);
-}
-
-sv S(gf o,const gf a)
-{
-  M(o,a,a);
-}
-
-sv inv25519(gf o,const gf a)
-{
-  gf c;
-  int i;
-  set25519(c,a);
-  for(i=253;i>=0;i--) {
-    S(c,c);
-    if(i!=2&&i!=4) M(c,c,a);
-  }
-  FOR(i,16) o[i]=c[i];
-}
-
-int crypto_scalarmult(u8 *q,const u8 *n,const u8 *p)
-{
-  u8 z[32];
-  i64 r;
-  int i;
-  gf x,a,b,c,d,e,f;
-  FOR(i,31) z[i]=n[i];
-  z[31]=(n[31]&127)|64;
-  z[0]&=248;
-  unpack25519(x,p);
-  FOR(i,16) {
-    b[i]=x[i];
-    d[i]=a[i]=c[i]=0;
-  }
-  a[0]=d[0]=1;
-  for(i=254;i>=0;--i) {
-    r=(z[i>>3]>>(i&7))&1;
-    sel25519(a,b,r);
-    sel25519(c,d,r);
-    A(e,a,c);
-    Z(a,a,c);
-    A(c,b,d);
-    Z(b,b,d);
-    S(d,e);
-    S(f,a);
-    M(a,c,a);
-    M(c,b,e);
-    A(e,a,c);
-    Z(a,a,c);
-    S(b,a);
-    Z(c,d,f);
-    M(a,c,_121665);
-    A(a,a,d);
-    M(c,c,a);
-    M(a,d,f);
-    M(d,b,x);
-    S(b,e);
-    sel25519(a,b,r);
-    sel25519(c,d,r);
-  }
-  inv25519(c,c);
-  M(a,a,c);
-  pack25519(q,a);
-  return 0;
-}
-\end{lstlisting}
+\lstinputlisting[linerange={2-5,8-9,266-320,336-386,399-444},language=Ctweetnacl]{../proofs/vst/c/tweetnaclVerifiableC.c}
 
 \subheading{Diff from TweetNaCl} We provide below the diff between the original code of TweetNaCl and the code we verified.