src/crypto/aead/chacha20poly1305.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead/chacha20poly1305.bend as Chacha20poly1305
4 imports
import Base import ../chacha/chacha20.bend as CH import ../poly1305/poly1305.bend as P import ../subtle.bend as S
Definitions
def poly_key source · line 22 · raw
@key:List<&2, U32> -> @nonce:List<&2, U32> -> List<&2, U32>
poly1305_key_gen: the first 32 bytes of the block with counter 0.
def pad16 source · line 25 · raw
@+xs:List<&2, U32> -> List<&2, U32>
def le8 source · line 29 · raw
@n:Nat -> @+x:Nat -> List<&2, U32>
The eight little-endian bytes of a length.
def mac_data source · line 34 · raw
@+aad:List<&2, U32> -> @+ct:List<&2, U32> -> List<&2, U32>
def tag source · line 38 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ct:List<&2, U32> -> List<&2, U32>
def encrypt_ct source · line 42 · raw
@key:List<&2, U32> -> @nonce:List<&2, U32> -> @+pt:List<&2, U32> -> List<&2, U32>
chacha20_encrypt(key, 1, nonce, plaintext).
def seal source · line 46 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> List<&2, U32>
ciphertext || tag, without length checks.
def open_tag source · line 50 · raw
@ok:Bool -> @+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+ct:List<&2, U32> -> Maybe<&2, List<&2, U32>>
def open_split source · line 55 · 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 58 · 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 66 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> Maybe<&2, List<&2, U32>>
The plaintext of ciphertext || tag, without key/nonce length checks.
def xkey source · line 71 · raw
@key:List<&2, U32> -> @nonce:List<&2, U32> -> List<&2, U32>
XChaCha20-Poly1305: the HChaCha20 subkey of nonce[0..16] and the nonce 0x00000000 || nonce[16..24].
def xnonce source · line 74 · raw
@nonce:List<&2, U32> -> List<&2, U32>
def xseal source · line 77 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> List<&2, U32>
def xopen source · line 80 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> Maybe<&2, List<&2, U32>>
def lengths_ok source · line 85 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @n:Nat -> Bool
def when source · line 88 · raw
@ok:Bool -> @x:List<&2, U32> -> Maybe<&2, List<&2, U32>>
def when_open source · line 93 · raw
@ok:Bool -> @r:Maybe<&2, List<&2, U32>> -> Maybe<&2, List<&2, U32>>
def encrypt source · line 98 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> Maybe<&2, List<&2, U32>>
def decrypt source · line 101 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> Maybe<&2, List<&2, U32>>
def xencrypt source · line 104 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> Maybe<&2, List<&2, U32>>
def xdecrypt source · line 107 · raw
@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+data:List<&2, U32> -> Maybe<&2, List<&2, U32>>