AEAD interface improvements

[hannesm]

It would be good to enhance the interface with:

val of_secret : Cstruct.t -> key
(** [of_secret k] validates [k] to be of appropriate size etc. *)

val tag_size : int
(** [tag_size] is the size in octets of the authentication tag. *)

To achieve this, CCM needs to take the maclen as functor argument (instead of as argument to of_secret). This is fine since the call site usually defines (by protocol spec) how long the tag should be. Unclear how to avoid defining CCM_4, CCM_6, CCM_8, CCM_10, CCM_12, CCM_14, CCM_16 - maybe allow the user to construct them themselves (i.e. exposing S.Core and CCM_of).

[hannesm]

JOSE transmits the ciphertext and tag separately, thus an interface such as:

val decrypt_raw : key -> nonce -> adata -> ciphertext -> tag -> plaintext option

val encrypt_raw : key -> nonce -> adata -> plaintext -> ciphertext * tag

could be useful (NB: the names _raw should be revised). the encrypt_aead / decrypt_aead can be implemented in terms of the functions above.

[hannesm]

on a separate note, there could be (measurable) speedup of AEAD encryption if the allocated cipher-stream is extended by tag-size (i.e. Cstruct.len msg + tag_size) -- thus a Cstruct.append can be avoided (which is costly since it allocates and memmoves).

[hannesm]

similarly, the Chacha20 implementation -- where djb does 64 bit nonce and 64 bit counter -- while IETF does 96 bit nonce and 32 bit counter -- could be functorised to allow more static checkng (and fewer conditional branches at runtime in the hot loop [incrementing the counter]).

[anmonteiro]

Came here to ask for tag_size in the AEAD interface, and remebered about this issue again.

[hannesm]

@anmonteiro currently, GCM.tag_size, and Poly1305.mac_size are provided. For CCM it is what you passed as ~maclen into CCM.of_secret ~maclen.

[hannesm]

See #171 which integrates "of_secret", "tag_size" and also "authenticate_encrypt_tag" and "authenticate_decrypt_tag". Any feedback on the PR is welcome.