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, by passing the same buffer for both plaintext and ciphertext.

Buffers have the following size requirements:

  • tag: 16 bytes
  • pk, sk, ck: 32 bytes
  • n: 24 bytes

Box

One-shot interface

val box : pt:bytes -> n:bytes -> pk:bytes -> sk:bytes -> ct:bytes -> tag:bytes -> bool

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

val box_open : ct:bytes -> tag:bytes -> n:bytes -> pk:bytes -> sk:bytes -> pt:bytes -> bool

box_open ct tag n pk sk pt attempts to verify and decrypt ciphertext ct and message authentication tag tag using public key pk, secret key sk, and nonce n and if successful writes the plaintext in pt and returns true.

Precomputation interface

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

val box_afternm : pt:bytes -> n:bytes -> ck:bytes -> ct:bytes -> tag:bytes -> bool

box_afternm pt n ck ct tag authenticates and encrypts pt using shared key ck and nonce n and writes the ciphertext in ct and the message authentication tag in tag. Returns true if successful.

val box_open_afternm : ct:bytes -> tag:bytes -> n:bytes -> ck:bytes -> pt:bytes -> bool

box_open_afternm ct tag n ck pt attempts to verify and decrypt ciphertext ct and message authentication tag tag using shared key ck and nonce n and if successful writes the plaintext in pt and returns true.

Secretbox

val secretbox : pt:bytes -> n:bytes -> key:bytes -> ct:bytes -> tag:bytes -> bool

secretbox pt n key ct tag authenticates and encrypts plaintext pt using secret key key and nonce n and writes the ciphertext in ct and the message authentication tag in tag. Returns true if successful.

val secretbox_open : ct:bytes -> tag:bytes -> n:bytes -> key:bytes -> pt:bytes -> bool

secretbox_open ct tag n key pt attempts to verify and decrypt ciphertext ct and message authentication tag tag using secret key key and nonce n and if successful writes the plaintext in pt and returns true.