usenix-f.tex 2.51 KB
 Peter Schwabe committed Oct 01, 2020 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 \newpage \section{Usenix Security 2020 Review \#324F} \begin{tabular}{rl} \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).