package hacl-star

  1. Overview
  2. Docs
package hacl-star
Legend:
Library
Module
Module type
Parameter
Class
Class type

The detached interface uses 2 separate buffers for the ciphertext and the message authentication tag. This allows users to encrypt and decrypt data in-place, in buffer buf.

By default, these functions use the whole buf, but users can choose to only pass a portion of buf, by passing one or both of these optional arguments:

  • offset: start at position offset in buf (0 by default)
  • len: take only the first len bytes in buf, starting at offset (Note: As opposed to not passing len at all, passing len=0 will result in using an empty buffer.)

Buffers have the following size requirements:

  • tag: 16 bytes
  • pk, sk, ck: 32 bytes
  • n: 24 bytes
  • offset: positive, <= size of buf
  • len: positive, <= size of buf - offset

Box

One-shot interface

val box : buf:bytes -> tag:bytes -> ?offset:int -> ?len:int -> n:bytes -> pk:bytes -> sk:bytes -> unit -> bool

box buf tag n pk sk authenticates and encrypts in-place the plaintext in buf using public key pk, secret key sk, and nonce n and writes the message authentication tag in tag. Returns true if successful.

val box_open : buf:bytes -> tag:bytes -> ?offset:int -> ?len:int -> n:bytes -> pk:bytes -> sk:bytes -> unit -> bool

box_open buf tag n pk sk attempts to verify and decrypt in-place the ciphertext in ct and message authentication tag tag using public key pk, secret key sk, and nonce n. Returns true if successful.

Precomputation interface

The shared key ck is obtained using NaCl.box_beforenm or NaCl.Noalloc.box_beforenm.

val box_afternm : buf:bytes -> tag:bytes -> ?offset:int -> ?len:int -> n:bytes -> ck:bytes -> unit -> bool

box buf tag n pk sk authenticates and encrypts in-place the plaintext in buf using shared key ck and nonce n and writes the message authentication tag in tag. Returns true if successful.

val box_open_afternm : buf:bytes -> tag:bytes -> ?offset:int -> ?len:int -> n:bytes -> ck:bytes -> unit -> bool

box_open buf tag n pk sk attempts to verify and decrypt in-place the ciphertext in ct and message authentication tag tag using shared key ck and nonce n. Returns true if successful.

Secretbox

val secretbox : buf:bytes -> tag:bytes -> ?offset:int -> ?len:int -> n:bytes -> key:bytes -> unit -> bool

secretbox buf tag n key authenticates and encrypts in-place the plaintext in buf using secret key key and nonce n and writes the message authentication tag in tag. Returns true if successful.

val secretbox_open : buf:bytes -> tag:bytes -> ?offset:int -> ?len:int -> n:bytes -> key:bytes -> unit -> bool

secretbox_open buf tag n key attempts to verify and decrypt in-place the ciphertext in buf and message authentication tag tag using secret key key and nonce n. Returns true if successful.