\newpage
\section*{Usenix Security 2020 Review \#324F}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
Review recommendation & 2. & Reject and resubmit \\
Writing quality & 2. & Needs improvement \\
Reviewer interest & 2. & I might go to a talk about this \\
Reviewer expertise & 3. & Knowledgeable \\
\bottomrule
\end{tabular}
\begin{center}
\subheading{===== Paper summary =====}
\end{center}
The authors formally prove that the TweetNaCl implementation of the X25519
function correctly implements the spec given in RFC 7748. Furthermore, they
prove that the pseudocode spec in RFC 7748 matches the mathematical definitions
of the curve operations originally presented by Bernstein.
\begin{center}
\subheading{===== Strengths =====}
\end{center}
\begin{itemize}
\item Proof that the TweetNaCl source (with very minor modifications) can be trusted.
\end{itemize}
\begin{center}
\subheading{===== Weaknesses =====}
\end{center}
\begin{itemize}
\item The majority of the paper is simply working through proofs.
\item Not written for a USENIX Security audience.
\item No clear value beyond the proof itself; no interesting challenges or solutions.
\end{itemize}
\begin{center}
\subheading{===== Detailed comments for authors =====}
\end{center}
As written, I'm not sure this paper is a good fit for USENIX Security. There
is no clear contribution beyond the mechanized proof that the TweetNaCl
implementation of X25519 is correct. This is useful (proof) engineering, but
it's not clear if any research challenges were addressed. I would say such an
effort is worth accepting if the proof is for something widely used, but
TweetNaCl is not really used seriously last I checked.
Buried in the introduction and conclusion is some text describing how this work
might be made more widely useful. I suggest the authors reframe their paper
with the main focus being any useful challenges and problems that arose during
this work. For example, did extending Bartzia and Strub lead to any new
insights? Proving TweetNaCl's X25519 could be an application/case study a
larger effort (e.g., the authors also mention that it would be easy to port
their curve definitions to other curves).
I found large large sections of the text to be largely ill suited to a USENIX
Security audience (e.g., walking step-by-step through proofs, with no text
explaining why this is important or interesting). I also find bits of the text
somewhat rushed (e.g., paragraph from RFC with no context).
%\begin{answer}
% \todo{Should add some reply here somewhere}
%\end{answer}