bend-collections

Search uses release 1.0.0.0 · 4,483 definitions

Releases (1)

1.0.0.0 indexed

Definitions (4,483)

proofs/crypto/sha/packed/packed_proof.bend

proofs/crypto/sha/packed/proof.bend

law digest_octets_length

proofs/crypto/sha/padding.bend

law zeros_correctUniversal bridge from implementation modular padding to the FIPS piecewise rule.

spec/crypto/chacha.bend

def getElement i of a list, 0 past its end.
def putThe list with element i replaced (unchanged past its end).
def rotlx <<< n: rotation of a 32-bit word left by n bits (0 < n < 32).
def quarter2.2: QUARTERROUND(a, b, c, d) applied to the state at those positions: a += b; d ^= a; d <<<= 16; c += d; b ^= c; b <<<= 12; a += b; d ^= a; d <<<= 8; c += d; b ^= c; b <<<= 7;
def inner_blockinner_block: four column rounds, then four diagonal rounds.
def inner_blocksn applications of inner_block (ChaCha20: n = 10, twenty rounds).
def wordA little-endian word from the low 8 bits of four bytes.
def wordsThe words of a byte list, four bytes each (a partial tail is dropped).
def octetsThe four little-endian bytes of a word.
def serialize
def constants"expa" "nd 3" "2-by" "te k"
def stateThe initial state: constants, key (eight words), block counter, nonce (three words).
def add_words
def block_bodychacha20_block with n double rounds: working state after n inner blocks, added to the initial state, serialized little-endian (64 bytes).
def block_roundsThe same, entered through a match on the key's first cell.
def block
def prefixThe first n bytes of a list, and the rest.
def suffix
def blocksThe plaintext cut into 64-byte blocks; the last one may be shorter (and there is none for the empty plaintext).
def xor_bytesByte-wise XOR of a block with the keystream (as long as the block).
def encrypt_blocksfor j = 0 ..
def encrypt_roundschacha20_encrypt(key, counter, nonce, plaintext) with n double rounds.
def encrypt
def hstateHChaCha20 (draft-irtf-cfrg-xchacha-03 section 2.2): the state is set up as for ChaCha20 with the 16-byte nonce in words 12..15; after twenty rounds (no feed-forward) words 0..3 and 12..15 are the 32-byte subkey.
def hchacha_body
def hchacha_roundsEntered through a match on the key, as block_rounds.
def hchacha20
def xsubkeySection 2.3: XChaCha20 is ChaCha20 under the HChaCha20 subkey of the first 16 nonce bytes, with the nonce 0x00000000 || nonce[16..24].
def xnonce
def xencrypt

spec/crypto/chacha20poly1305.bend

def poly_key2.6 poly1305_key_gen: the first 32 bytes of the block with counter 0.
def pad16pad16(x): zero bytes up to a multiple of 16, i.e.
def le8num_to_8_le_bytes
def mac_datamac_data = aad | pad16(aad) | ciphertext | pad16(ciphertext) | num_to_8_le_bytes(aad.length) | num_to_8_le_bytes(ciphertext.length)
def tag
def seal2.8 chacha20_aead_encrypt: ciphertext = chacha20_encrypt(key, 1, nonce, plaintext), then the tag over aad and ciphertext.
def open_tagDecryption: the tag is recomputed over the received ciphertext and the plaintext released only when it matches.
def open_split
def open_len
def open
def xsealXChaCha20-Poly1305: ChaCha20-Poly1305 under the HChaCha20 subkey of the first 16 nonce bytes, with the nonce 0x00000000 || nonce[16..24].
def xopen

spec/crypto/hkdf.bend

def hash_len
def max_lengthRFC 5869: L <= 255*HashLen.
def extract2.2 Step 1: Extract.
def t_blocks2.3 Step 2: Expand.
def block_countN = ceil(L/HashLen).
def okmOKM = the first L octets of T = T(1) | T(2) | ...
def expand_ifExpand is defined for L <= 255*HashLen only.
def expand
def hkdf

spec/crypto/hmac.bend

def block_lenB, the block size of SHA-256 in bytes, and L, its output size.
def hash_len
def ipadRFC 2104: ipad = the byte 0x36 repeated B times, opad = 0x5C repeated B times.
def opad
def hash
def shorten_ifFIPS 198-1 steps 1-3: a key of exactly B bytes is K0 itself; a longer key is hashed first (K0 = H(K) || zeros); a shorter one is zero-padded to B.