Subject: [Cfrg] Implementation / spec of draft-nir-cfrg-chacha20-poly1305 in Cryptol

From: Dylan McNamee <[email-masked]>
Date: Mon, 12 May 2014 15:35:36 -0700

Hello CFRG,

I was pointed to draft-nir-cfrg-chacha20-poly1305 by Kyle Isom, who has
been implementing ChaCha20 in the Go language, and said he found this
draft document a helpful guide to some of the trickier / ambiguous bits
in the ChaCha20 specification.

I totally agree - I spent much of last week turning the document into a
"literate Cryptol" specification of ChaCha20, Poly1305 and the AEAD
construction -- it would have taken me much, much longer to complete
these specifications just starting from the source documents. Both Adam
and Yoav helped me through a couple sticky bits, and they suggested I
bring any lessons I learned to this group.

For those who aren't familiar with it, Cryptol is a domain specific
specification language for cryptographic algorithms. The current
version of Cryptol, 2.0, was released a couple weeks ago as an open
source project. See http://cryptol.net for details.

The interim result of turning the ChaCha20/Poly1305 document into literate 
Cryptol is on my github, here:

https://github.com/dylanmc/cryptol/blob/master/examples/ChaChaPolyCryptolIETF.md

I'm new to this community, so it's not surprising that there were a number of 
places where I got tripped up. I corrected most of them in the version of 
the text on GitHub.

In particular, I found the second bullet point, in section 2.5 "the Poly1305 
algorithm", to be befuddling:

  o Read the block as a little-endian number.  (so far, so good)
  o Add one bit beyond the number of octets.  For a 16-byte block this
      is equivalent to adding 2^128 to the number.  For the shorter
      block it can be 2^120, 2^112, or any power of two that is evenly
      divisible by 8, all the way down to 2^8.

I translated this to:

  o Prepend a 0x01 byte to the sequence of octets.

In Cryptol this is:

	0x01 # (littleendian block)

The sentence that follows in the first version was confusing because
prepending a 0x01 byte (which is what we're supposed to do, I think)
does a complicated thing when interpreted in little-endian mode, which
is the mode we're in according to the previous bullet.

In the Cryptol specification, I was forced to choose exact bit-widths
for each of the intermediate results in Poly1305, which I think adds
some clarity to the math, and should be helpful since the
implementation guide suggests avoiding "bignum" packages.

The other place I got tripped up, which I think is clarified in a
literate program, is in the AEAD construction, I found myself getting
lost in the nested description of intermediate results and arguments to
helper functions, vs. the overall construction. Adam and Yoav were kind
enough to help me through this part, but I think the final spec could
benefit from some kind of pseudocode, literate program, or other
clarification.

I hope this is helpful to folks. Comments & feedback are welcome!

cheers,
dylan mcnamee 
(Galois, Inc)

---

From: Ilari Liusvaara <[email-masked]>
Date: Tue, 13 May 2014 02:11:07 +0300

> is the mode we're in according to the previous bullet.

In octet space, it is append, not prepend (little-endian)
In number space, it is addtion of constant (dependent on length).

-Ilari