~/bend-docscommunity

spec/crypto/chacha20poly1305.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/chacha20poly1305.bend as Chacha20poly1305

4 imports
import Base
import ./chacha.bend as CH
import ./poly1305.bend as PS
import ./subtle.bend as EQ

Definitions

def poly_key source · line 15 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> List<&2, U32>

2.6 poly1305_key_gen: the first 32 bytes of the block with counter 0.

def pad16 source · line 20 · raw

@+xs:List<&2, U32> -> List<&2, U32>

pad16(x): zero bytes up to a multiple of 16, i.e. (16 - len(x) % 16) % 16 of them ("if (len(x) % 16) == 0 then NULL else copies(0, 16 - len % 16)").

def le8 source · line 24 · raw

@n:Nat -> @+x:Nat -> List<&2, U32>

num_to_8_le_bytes

def mac_data source · line 31 · raw

@+aad:List<&2, U32> -> @+ct:List<&2, U32> -> List<&2, U32>

mac_data = aad | pad16(aad) | ciphertext | pad16(ciphertext) | num_to_8_le_bytes(aad.length) | num_to_8_le_bytes(ciphertext.length)

def tag source · line 35 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> List<&2, U32>

def seal source · line 40 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> List<&2, U32>

2.8 chacha20_aead_encrypt: ciphertext = chacha20_encrypt(key, 1, nonce, plaintext), then the tag over aad and ciphertext.

def open_tag source · line 46 · raw

@ok:Bool -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+ct:List<&2, U32> -> Maybe<&2, List<&2, U32>>

Decryption: the tag is recomputed over the received ciphertext and the plaintext released only when it matches.

def open_split source · line 51 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> @+t:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def open_len source · line 54 · raw

@short:Bool -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def open source · line 61 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def xseal source · line 66 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> List<&2, U32>

XChaCha20-Poly1305: ChaCha20-Poly1305 under the HChaCha20 subkey of the first 16 nonce bytes, with the nonce 0x00000000 || nonce[16..24].

def xopen source · line 69 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> Maybe<&2, List<&2, U32>>