Poly1305 RFC to hacpsec and F*

ChaCha20Poly1305 is specified in RFC 7539. It specifies Poly1305 as follows in Section 2.5.1.

  clamp(r): r &= 0x0ffffffc0ffffffc0ffffffc0fffffff
  poly1305_mac(msg, key):
     r = (le_bytes_to_num(key[0..15])
     clamp(r)
     s = le_num(key[16..31])
     accumulator = 0
     p = (1<<130)-5
     for i=1 upto ceil(msg length in bytes / 16)
        n = le_bytes_to_num(msg[((i-1)*16)..(i*16)] | [0x01])
        a += n
        a = (r * a) % p
        end
     a += s
     return num_to_16_le_bytes(a)
     end

Translating RFC specification to hacpsec

The algorithm can be easily written in hacspec. The following gives the hacspec versions of the corresponding RFC definitions for poly1305 as well as the compiled F*.

setup

The RFC defines the Poly1305 parameters as:

A 256-bit one-time key
The output is a 128-bit tag.
set the constant prime "P" be 2^130-5: 3fffffffffffffffffffffffffffffffb.
divide the message into 16-byte blocks

hacspec

blocksize:int = 16
block_t = bytes_t(16)
key_t = bytes_t(32)
tag_t = bytes_t(16)
subblock_t = refine_t(vlbytes_t, lambda x: bytes.length(x) <= 16)
p130m5 : nat_t = (2 ** 130) - 5

felem_t = natmod_t(p130m5)
def felem(n:nat_t) -> felem_t:
    return natmod(n,p130m5)

F*

let blocksize: int = 16
let block_t: Type0 = array_t uint8_t 16
let key_t: Type0 = array_t uint8_t 32
let tag_t: Type0 = array_t uint8_t 16
let subblock_t: Type0 = (x: vlbytes_t{(bytes_length x) <=. 16})
let p130m5: nat_t = (2 **. 130) -. 5

let felem_t: Type0 = natmod_t p130m5
let felem (n: nat_t) : felem_t = natmod n p130m5

---

bytes to int

le_bytes_to_num(msg[((i-1)*16)..(i*16)] | [0x01])

hacspec

def encode(block: subblock_t) -> felem_t:
    b : block_t = array.create(16, uint8(0))
    b[0:bytes.length(block)] = block
    welem : felem_t = felem(bytes.to_nat_le(b))
    lelem : felem_t = felem(2 ** (8 * array.length(block)))
    return lelem + welem

F*

let encode (block: subblock_t) : felem_t =
  let b = array_create 16 (uint8 0) in
  let b = array_update_slice b 0 (bytes_length block) (block) in
  let welem = felem (bytes_to_nat_le b) in
  let lelem = felem (2 **. (8 *. (array_length block))) in
  lelem +. welem

---

clamp

clamp(r): r &= 0x0ffffffc0ffffffc0ffffffc0fffffff

hacspec

def encode_r(r: block_t) -> felem_t:
    ruint : uint128_t = bytes.to_uint128_le(r)                  # r = (le_bytes_to_num(key[0..15])
    ruint = ruint & uint128(0x0ffffffc0ffffffc0ffffffc0fffffff) # r &= 0x0ffffffc0ffffffc0ffffffc0fffffff
    r_nat : nat_t = uintn.to_nat(ruint)
    return felem(r_nat)

F*

let encode_r (r: block_t) : felem_t =
  let ruint = bytes_to_uint128_le r in
  let ruint = ruint &. (uint128 21267647620597763993911028882763415551) in
  let r_nat = uintn_to_nat ruint in
  felem r_nat

---

poly

a = 0
for i=1 upto ceil(msg length in bytes / 16)
   n = le_bytes_to_num(msg[((i-1)*16)..(i*16)] | [0x01])
   a += n
   a = (r * a) % p
   e

hacspec

def poly(text: vlbytes_t, r: felem_t) -> felem_t:
    blocks : vlarray_t(block_t)
    last : subblock_t
    blocks, last = array.split_blocks(text, blocksize)
    acc : felem_t = felem(0)
    for i in range(array.length(blocks)):              # for i=1 upto ceil(msg length in bytes / 16)
        acc = (acc + encode(blocks[i])) * r            # n = le_bytes_to_num(msg[((i-1)*16)..(i*16)] | [0x01])
                                                       # a += n
                                                       # a = (r * a) % p
    if (array.length(last) > 0):
        acc = (acc + encode(last)) * r
    return acc

F*

let poly (text: vlbytes_t) (r: felem_t) : felem_t =
  let blocks, last = array_split_blocks text blocksize in
  let acc = felem 0 in
  let acc = repeati (array_length blocks)
    (fun i acc -> (acc +. (encode blocks.[ i ])) *. r) acc in
  let acc = if (array_length last) >. 0 then
    (acc +. (encode last)) *. r else acc in
  acc

---

poly mac

poly1305_mac(msg, key):
   r = (le_bytes_to_num(key[0..15])
   clamp(r)
   s = le_num(key[16..31])
   p = (1<<130)-5
   a = poly(msg, r)
   a += s
   return num_to_16_le_bytes(a)
   end

hacspec

def poly1305_mac(text: vlbytes_t, k: key_t) -> tag_t:
    r : block_t = k[0:blocksize]                      # key[0..15]
    s : block_t = k[blocksize:2*blocksize]            # key[16..31]
    relem : felem_t = encode_r(r)
    selem : uint128_t = bytes.to_uint128_le(s)        # s = le_num(key[16..31])
    a : felem_t   = poly(text, relem)
    n : uint128_t = uint128(natmod.to_nat(a)) + selem # a += s
    return bytes.from_uint128_le(n)                   # num_to_16_le_bytes(a)

F*

let poly1305_mac (text: vlbytes_t) (k: key_t) : tag_t =
  let r = array_slice k 0 blocksize in
  let s = array_slice k blocksize (2 *. blocksize) in
  let relem = encode_r r in
  let selem = bytes_to_uint128_le s in
  let a = poly text relem in
  let n = (uint128 ((natmod_to_nat a) % (2 **. 128))) +. selem in
  bytes_from_uint128_le n