Sealed messages
ChaCha20-Poly1305 (RFC 8439 §2.8) is the cipher sysn's Noise IK sends its messages under: aead-seal enciphers a message and writes a tag after it, and aead-open checks the tag and only then deciphers. A caller holds an Aead, a key and its nonce counter, and passes neither nonce nor Poly1305 key: those are the two values whose reuse breaks the cipher, so no caller has a place to reuse them.
What is sealed
Each message has its own nonce, and from the key and the nonce ChaCha20 makes everything else. Block 0's first 32 bytes are the message's Poly1305 key (§2.6), used for that message and zeroed after it. Blocks 1 and on are the keystream, exclusive-ored with the message (§2.4). The tag is Poly1305 over the additional data, which is authenticated but not enciphered (in Noise, the handshake's hash), then the ciphertext, each padded with zeros to 16 bytes, then the two lengths as eight bytes each. The sealed message is the ciphertext with the tag after it, as Noise frames it. Move the lengths to see what Poly1305 takes.
Noise's nonce, kept
The nonce is Noise's (§5.1, §12.3): a counter of 64 bits, given to ChaCha20 as four zero bytes and then the counter's eight, little-endian. It starts at 0 when aead-new or aead-key sets a key, and each call that succeeds advances it by one; at 2^64 − 1, the value Noise reserves, both calls refuse. A message that does not open leaves it where it was, and writes nothing: aead-open asks poly-check before a byte is deciphered, and its contract says so, proven: when it answers false, every byte of the output is as it was. Seal a few messages, and open them, in turn or not, or after one is changed in transit.
One buffer
Nothing in crypto/aead.sysp allocates. aead-new takes a buffer of 54 words the caller lends: Poly1305's state in the first 22, ChaCha20's input and block in the 32 after them; how many bytes Poly1305's block holds is a count aead-mac keeps in a local, public, not a word of the secret buffer (sysc 019). The one-time key goes from the block to poly-start where it lies, with no copy, and aead-forget zeroes the block after every call; aead-buf gives the buffer back zeroed. chacha-xor, new in crypto/chacha.sysp, applies one block's keystream and is proven to write only its range, so a sealed message lands in the caller's buffer and nothing beside it changes.
aead-encrypt and aead-decrypt are the same construction with the key and nonce already in the buffer: the RFC's and Wycheproof's vectors choose their nonces, and only these can take them. They are public only because sysp's privacy is a file's; code outside sysc holds an Aead and never calls them (constitution VI), as it never calls chacha-block.
Tested against
| What | Vectors | And |
|---|---|---|
| sealing and opening | RFC 8439's §2.8.2 sealed and opened, A.5 opened; every one of Wycheproof's 316 with a 96-bit nonce: sealed when valid, opened always, refused when invalid (a tag or ciphertext changed, edge cases of the counter and of Poly1305) | tools/aead.rkt, the RFC's pseudocode on the Racket ChaCha20 and Poly1305: 150 random keys, nonces, data and messages to 2,000 bytes; each with one bit changed in the sealed message, and one in the data, refused |
the Aead | none published: the counter is Noise's | 20 keys: two seals give the nonces 0 and 1; opened in turn both open; out of turn, or changed, the first does not, and the right one opens after it |
Wycheproof's nine vectors with nonces of other lengths cannot be given here, a nonce being 12 bytes, and the test counts them so a new one shows. The vectors are kept as published, in tests/vectors/rfc8439-aead.txt and tests/vectors/wycheproof-chacha20-poly1305.json. With the padding after the data left out, 611 of the test's 1,258 checks fail.